book集

section 主定理
txt 群 \(G\)（演算 \(f\)、単位元 \(e\)）の部分群 \(H\) について、\(G\) が \(n\) 個・\(H\) が \(k\) 個の元をもつなら \(k\) は \(n\) を割る。
txt \(G\) の部分集合 \(S\) で右から \(H\) を掛けて閉じているものについて、\(S\) の個数についての強い帰納法で示します。\(S\) の元 \(a\) をとると、剰余類 \(aH\) は \(S\) に含まれ \(H\) と同じ個数で、\(S \setminus aH\) もまた閉じています。
thm `\\{ And [ ∀ x ∈ G . [ ∀ y ∈ G . ??f (x , y) ∈ G ] ] \\ [ ∀ x ∈ G . [ ∀ y ∈ G . [ ∀ z ∈ G . ??f (??f (x , y) , z) = ??f (x , ??f (y , z)) ] ] ] \\ e ∈ G and [ ∀ x ∈ G . ??f (e , x) = x and ??f (x , e) = x ] \\ [ ∀ x ∈ G . [ ∃ y ∈ G . ??f (y , x) = e and ??f (x , y) = e ] ] \\ H ⊂ G and e ∈ H and [ ∀ x ∈ H . [ ∀ y ∈ H . ??f (x , y) ∈ H ] ] \\ [ ∀ x ∈ H . [ ∃ y ∈ H . ??f (y , x) = e and ??f (x , y) = e ] ] \\ [ n ; k col ∈ 𝕄 ] and G =# n and H =# k \\} ⟹ [ ∃ m ∈ 𝕄 . n = m ⋅ k ]` ◀ W. , ax_s , +𝕄 , *𝕄
prf hy1 <- `[ ∀ x ∈ |G . [ ∀ y ∈ |G . ??f (x , y) ∈ |G ] ]` ;
    hy2 <- `[ ∀ x ∈ |G . [ ∀ y ∈ |G . [ ∀ z ∈ |G . ??f (??f (x , y) , z) = ??f (x , ??f (y , z)) ] ] ]` ;
    hy3 <- `|e ∈ |G and [ ∀ x ∈ |G . ??f (|e , x) = x and ??f (x , |e) = x ]` ;
    hy4 <- `[ ∀ x ∈ |G . [ ∃ y ∈ |G . ??f (y , x) = |e and ??f (x , y) = |e ] ]` ;
    hy5 <- `|H ⊂ |G and |e ∈ |H and [ ∀ x ∈ |H . [ ∀ y ∈ |H . ??f (x , y) ∈ |H ] ]` ;
    hy6 <- `[ ∀ x ∈ |H . [ ∃ y ∈ |H . ??f (y , x) = |e and ??f (x , y) = |e ] ]` ;
    hy7 <- `[ |n ; |k col ∈ 𝕄 ] and |G =# |n and |H =# |k` ;
    A1 <- `[ ∀ x ∈ S . [ ∀ h ∈ |H . ??f (x , h) ∈ S ] ] and a ∈ S and [ ∀ y (y ∈ C ⟺ [ ∃ h ∈ |H . y = ??f (a , h) ]) ] ⟹ C ⊂ S` / ⊂. -| O p;
    Lback <- `[ x ; a col ∈ |G ] and h ∈ |H and h' ∈ |H and ??f (x , h) = ??f (a , h') ⟹ [ ∃ g ∈ |H . x = ??f (a , g) ]` -| hy2 , hy3 , hy5 / ⊂. , hy6 v;
    A2 <- `S ⊂ |G and [ ∀ x ∈ S . [ ∀ h ∈ |H . ??f (x , h) ∈ S ] ] and a ∈ S and [ ∀ y (y ∈ C ⟺ [ ∃ h ∈ |H . y = ??f (a , h) ]) ] ⟹ [ ∀ x ∈ S ∖ C . [ ∀ h ∈ |H . ??f (x , h) ∈ S ∖ C ] ]` / ∖. / ⊂. -| Lback , hy5 / ⊂. v;
    Lcan <- `a ∈ |G and [ x ; y col ∈ |G ] and ??f (a , x) = ??f (a , y) ⟹ x = y` -| hy2 , hy3 , hy4 v;
    Lφs <- `a ∈ |G ⟹ \{ cls p | [ ∃ h ∈ |H . p = \< pr h ; ??f (a , h) \> ] \} ⊂_ |H ^^pr |G` / ^^pr. -| hy1 , hy5 / ⊂. p;
    B3 <- `a ∈ |G ⟹ [ ∃ φ \, [ ∀ p (p ∈ φ ⟺ [ ∃ h ∈ |H . p = \< pr h ; ??f (a , h) \> ]) ] ]` -| ax_s[C_:=`\{ cls p | [ ∃ h ∈ |H . p = \< pr h ; ??f (a , h) \> ] \}`] , Lφs p;
    B1 <- `a ∈ |G and [ ∀ y (y ∈ C ⟺ [ ∃ h ∈ |H . y = ??f (a , h) ]) ] and [ ∀ p (p ∈ φ ⟺ [ ∃ h ∈ |H . p = \< pr h ; ??f (a , h) \> ]) ] ⟹ φ ∈ |H → C` / →.' / ⊂. / ^^pr. -| pr:0 v;
    B2 <- `a ∈ |G and [ ∀ y (y ∈ C ⟺ [ ∃ h ∈ |H . y = ??f (a , h) ]) ] and [ ∀ p (p ∈ φ ⟺ [ ∃ h ∈ |H . p = \< pr h ; ??f (a , h) \> ]) ] ⟹ [ ∀ y ∈ C . [ ∃！ x \< pr x ; y \> ∈ φ ] ]` -| Lcan , hy5 / ⊂. , pr:0 v;
    A3 <- `a ∈ |G and [ ∀ y (y ∈ C ⟺ [ ∃ h ∈ |H . y = ??f (a , h) ]) ] ⟹ |H =# C` / =#.' / →IS.' -| B1 , B2 , B3 v;
    LCs <- `a ∈ |G ⟹ \{ cls y | [ ∃ h ∈ |H . y = ??f (a , h) ] \} ⊂_ |G` -| hy1 , hy5 / ⊂. p;
    A4 <- `a ∈ |G ⟹ [ ∃ C \, [ ∀ y (y ∈ C ⟺ [ ∃ h ∈ |H . y = ??f (a , h) ]) ] ]` -| ax_s[C_:=`\{ cls y | [ ∃ h ∈ |H . y = ??f (a , h) ] \}`] , LCs v;
    Lk <- `|k {/}= 0` -| hy5 , hy7 , =#0 , L0e , ∅.' p;
    Lkj <- `[ ∃ j ∈ 𝕄 . |k = j suc ]` -| INDC[D_:=`\{ cls k | k = 0 or [ ∃ j ∈ 𝕄 . k = j suc ] \}`] , 𝕄1 , hy7 , Lk p;
    Lin <- `[ x ; j col ∈ 𝕄 ] ⟹ x ∈ x + j suc` -| INDC[D_:=`\{ cls j | x ∈ x + j suc \}`] , +𝕄 , Lsucin , Lsucsub / ⊂. , 𝕄1 , `0 ∈ 𝕄` , +∈𝕄 v;
    Llt <- `d' ∈ 𝕄 ⟹ d' ∈ d' + |k` -| Lin , Lkj p;
    Lsplit <- `C ⊂ S ⟹ (S ∖ C) ∩ C = ∅ and (S ∖ C) ∪ C = S` / =. /// W.'!=. -| O p;
    Ldf <- `S ∖ C ⊂ S` / ⊂. / ∖. -| O p;
    Lss <- `S ⊂ |G and a ∈ S ⟹ a ∈ |G and S ∖ C ⊂ |G` / ⊂. / ∖. -| O p;
    A5 <- `C ⊂ S and S =# d and d ∈ 𝕄 and |H =# C ⟹ [ ∃ d' ∈ 𝕄 . S ∖ C =# d' and d = d' + |k ]` -| Lfin , L∪ , LB2 , =#:RTX , hy7 , +∈𝕄 , Lsplit , Ldf v;
    Lz <- `d = 0 ⟹ [ ∃ m ∈ 𝕄 . d = m ⋅ |k ]` -| 0⋅ , hy7 , `0 ∈ 𝕄` p;
    Lne <- `S =# d and d {/}= 0 ⟹ [ ∃ a \, a ∈ S ]` -| =#0 , L0e , ∅.' , =#:RTX p;
    Lg <- `d = d' + |k and d' = m ⋅ |k and m ∈ 𝕄 ⟹ [ ∃ m' ∈ 𝕄 . d = m' ⋅ |k ]` -| suc⋅ , 𝕄1 , hy7 p;
    Lf <- `[ ∀ z ∈ d . [ ∀ S' (S' ⊂ |G and [ ∀ x ∈ S' . [ ∀ h ∈ |H . ??f (x , h) ∈ S' ] ] and S' =# z ⟹ [ ∃ m ∈ 𝕄 . z = m ⋅ |k ]) ] ] and d ∈ 𝕄 and S ⊂ |G and [ ∀ x ∈ S . [ ∀ h ∈ |H . ??f (x , h) ∈ S ] ] and S =# d ⟹ [ ∃ m ∈ 𝕄 . d = m ⋅ |k ]` -| Lz , Lne , Lss , Ldf , A1 , A2 , A3 , A4 , A5 , Llt , Lg v;
    LG <- `n ∈ 𝕄 ⟹ [ ∀ S (S ⊂ |G and [ ∀ x ∈ S . [ ∀ h ∈ |H . ??f (x , h) ∈ S ] ] and S =# n ⟹ [ ∃ m ∈ 𝕄 . n = m ⋅ |k ]) ]` -| SINDC[D_:=`\{ cls d | [ ∀ S (S ⊂ |G and [ ∀ x ∈ S . [ ∀ h ∈ |H . ??f (x , h) ∈ S ] ] and S =# d ⟹ [ ∃ m ∈ 𝕄 . d = m ⋅ |k ]) ] \}`] , Lf v;
    LGG <- `|G ⊂ |G and [ ∀ x ∈ |G . [ ∀ h ∈ |H . ??f (x , h) ∈ |G ] ]` / ⊂. -| hy1 , hy5 / ⊂. p;
    Lend <- `[ ∃ m ∈ 𝕄 . |n = m ⋅ |k ]` -| LG , LGG , hy7 p;
    goal -| W. , ax_s , +𝕄 , *𝕄 h[fix];

articles4/zz71.book

`articles4/zz71.book`