Metamath Proof Explorer

Theorem pgpfac1

Description: Factorization of a finite abelian p-group. There is a direct product decomposition of any abelian group of prime-power order where one of the factors is cyclic and generated by an element of maximal order. (Contributed by Mario Carneiro, 27-Apr-2016)

Ref Expression
Hypotheses pgpfac1.k ⊢ 𝐾 = ( mrCls ‘ ( SubGrp ‘ 𝐺 ) )
pgpfac1.s ⊢ 𝑆 = ( 𝐾 ‘ { 𝐴 } )
pgpfac1.b ⊢ 𝐵 = ( Base ‘ 𝐺 )
pgpfac1.o ⊢ 𝑂 = ( od ‘ 𝐺 )
pgpfac1.e ⊢ 𝐸 = ( gEx ‘ 𝐺 )
pgpfac1.z ⊢ 0 = ( 0g ‘ 𝐺 )
pgpfac1.l ⊢ ⊕ = ( LSSum ‘ 𝐺 )
pgpfac1.p ⊢ ( 𝜑 → 𝑃 pGrp 𝐺 )
pgpfac1.g ⊢ ( 𝜑 → 𝐺 ∈ Abel )
pgpfac1.n ⊢ ( 𝜑 → 𝐵 ∈ Fin )
pgpfac1.oe ⊢ ( 𝜑 → ( 𝑂 ‘ 𝐴 ) = 𝐸 )
pgpfac1.ab ⊢ ( 𝜑 → 𝐴 ∈ 𝐵 )
Assertion pgpfac1 ( 𝜑 → ∃ 𝑡 ∈ ( SubGrp ‘ 𝐺 ) ( ( 𝑆 ∩ 𝑡 ) = { 0 } ∧ ( 𝑆 ⊕ 𝑡 ) = 𝐵 ) )

Proof

Step Hyp Ref Expression
1 pgpfac1.k ⊢ 𝐾 = ( mrCls ‘ ( SubGrp ‘ 𝐺 ) )
2 pgpfac1.s ⊢ 𝑆 = ( 𝐾 ‘ { 𝐴 } )
3 pgpfac1.b ⊢ 𝐵 = ( Base ‘ 𝐺 )
4 pgpfac1.o ⊢ 𝑂 = ( od ‘ 𝐺 )
5 pgpfac1.e ⊢ 𝐸 = ( gEx ‘ 𝐺 )
6 pgpfac1.z ⊢ 0 = ( 0g ‘ 𝐺 )
7 pgpfac1.l ⊢ ⊕ = ( LSSum ‘ 𝐺 )
8 pgpfac1.p ⊢ ( 𝜑 → 𝑃 pGrp 𝐺 )
9 pgpfac1.g ⊢ ( 𝜑 → 𝐺 ∈ Abel )
10 pgpfac1.n ⊢ ( 𝜑 → 𝐵 ∈ Fin )
11 pgpfac1.oe ⊢ ( 𝜑 → ( 𝑂 ‘ 𝐴 ) = 𝐸 )
12 pgpfac1.ab ⊢ ( 𝜑 → 𝐴 ∈ 𝐵 )
13 ablgrp ⊢ ( 𝐺 ∈ Abel → 𝐺 ∈ Grp )
14 3 subgid ⊢ ( 𝐺 ∈ Grp → 𝐵 ∈ ( SubGrp ‘ 𝐺 ) )
15 9 13 14 3syl ⊢ ( 𝜑 → 𝐵 ∈ ( SubGrp ‘ 𝐺 ) )
16 eleq1 ⊢ ( 𝑠 = 𝑢 → ( 𝑠 ∈ ( SubGrp ‘ 𝐺 ) ↔ 𝑢 ∈ ( SubGrp ‘ 𝐺 ) ) )
17 eleq2 ⊢ ( 𝑠 = 𝑢 → ( 𝐴 ∈ 𝑠 ↔ 𝐴 ∈ 𝑢 ) )
18 16 17 anbi12d ⊢ ( 𝑠 = 𝑢 → ( ( 𝑠 ∈ ( SubGrp ‘ 𝐺 ) ∧ 𝐴 ∈ 𝑠 ) ↔ ( 𝑢 ∈ ( SubGrp ‘ 𝐺 ) ∧ 𝐴 ∈ 𝑢 ) ) )
19 eqeq2 ⊢ ( 𝑠 = 𝑢 → ( ( 𝑆 ⊕ 𝑡 ) = 𝑠 ↔ ( 𝑆 ⊕ 𝑡 ) = 𝑢 ) )
20 19 anbi2d ⊢ ( 𝑠 = 𝑢 → ( ( ( 𝑆 ∩ 𝑡 ) = { 0 } ∧ ( 𝑆 ⊕ 𝑡 ) = 𝑠 ) ↔ ( ( 𝑆 ∩ 𝑡 ) = { 0 } ∧ ( 𝑆 ⊕ 𝑡 ) = 𝑢 ) ) )
21 20 rexbidv ⊢ ( 𝑠 = 𝑢 → ( ∃ 𝑡 ∈ ( SubGrp ‘ 𝐺 ) ( ( 𝑆 ∩ 𝑡 ) = { 0 } ∧ ( 𝑆 ⊕ 𝑡 ) = 𝑠 ) ↔ ∃ 𝑡 ∈ ( SubGrp ‘ 𝐺 ) ( ( 𝑆 ∩ 𝑡 ) = { 0 } ∧ ( 𝑆 ⊕ 𝑡 ) = 𝑢 ) ) )
22 18 21 imbi12d ⊢ ( 𝑠 = 𝑢 → ( ( ( 𝑠 ∈ ( SubGrp ‘ 𝐺 ) ∧ 𝐴 ∈ 𝑠 ) → ∃ 𝑡 ∈ ( SubGrp ‘ 𝐺 ) ( ( 𝑆 ∩ 𝑡 ) = { 0 } ∧ ( 𝑆 ⊕ 𝑡 ) = 𝑠 ) ) ↔ ( ( 𝑢 ∈ ( SubGrp ‘ 𝐺 ) ∧ 𝐴 ∈ 𝑢 ) → ∃ 𝑡 ∈ ( SubGrp ‘ 𝐺 ) ( ( 𝑆 ∩ 𝑡 ) = { 0 } ∧ ( 𝑆 ⊕ 𝑡 ) = 𝑢 ) ) ) )
23 22 imbi2d ⊢ ( 𝑠 = 𝑢 → ( ( 𝜑 → ( ( 𝑠 ∈ ( SubGrp ‘ 𝐺 ) ∧ 𝐴 ∈ 𝑠 ) → ∃ 𝑡 ∈ ( SubGrp ‘ 𝐺 ) ( ( 𝑆 ∩ 𝑡 ) = { 0 } ∧ ( 𝑆 ⊕ 𝑡 ) = 𝑠 ) ) ) ↔ ( 𝜑 → ( ( 𝑢 ∈ ( SubGrp ‘ 𝐺 ) ∧ 𝐴 ∈ 𝑢 ) → ∃ 𝑡 ∈ ( SubGrp ‘ 𝐺 ) ( ( 𝑆 ∩ 𝑡 ) = { 0 } ∧ ( 𝑆 ⊕ 𝑡 ) = 𝑢 ) ) ) ) )
24 eleq1 ⊢ ( 𝑠 = 𝐵 → ( 𝑠 ∈ ( SubGrp ‘ 𝐺 ) ↔ 𝐵 ∈ ( SubGrp ‘ 𝐺 ) ) )
25 eleq2 ⊢ ( 𝑠 = 𝐵 → ( 𝐴 ∈ 𝑠 ↔ 𝐴 ∈ 𝐵 ) )
26 24 25 anbi12d ⊢ ( 𝑠 = 𝐵 → ( ( 𝑠 ∈ ( SubGrp ‘ 𝐺 ) ∧ 𝐴 ∈ 𝑠 ) ↔ ( 𝐵 ∈ ( SubGrp ‘ 𝐺 ) ∧ 𝐴 ∈ 𝐵 ) ) )
27 eqeq2 ⊢ ( 𝑠 = 𝐵 → ( ( 𝑆 ⊕ 𝑡 ) = 𝑠 ↔ ( 𝑆 ⊕ 𝑡 ) = 𝐵 ) )
28 27 anbi2d ⊢ ( 𝑠 = 𝐵 → ( ( ( 𝑆 ∩ 𝑡 ) = { 0 } ∧ ( 𝑆 ⊕ 𝑡 ) = 𝑠 ) ↔ ( ( 𝑆 ∩ 𝑡 ) = { 0 } ∧ ( 𝑆 ⊕ 𝑡 ) = 𝐵 ) ) )
29 28 rexbidv ⊢ ( 𝑠 = 𝐵 → ( ∃ 𝑡 ∈ ( SubGrp ‘ 𝐺 ) ( ( 𝑆 ∩ 𝑡 ) = { 0 } ∧ ( 𝑆 ⊕ 𝑡 ) = 𝑠 ) ↔ ∃ 𝑡 ∈ ( SubGrp ‘ 𝐺 ) ( ( 𝑆 ∩ 𝑡 ) = { 0 } ∧ ( 𝑆 ⊕ 𝑡 ) = 𝐵 ) ) )
30 26 29 imbi12d ⊢ ( 𝑠 = 𝐵 → ( ( ( 𝑠 ∈ ( SubGrp ‘ 𝐺 ) ∧ 𝐴 ∈ 𝑠 ) → ∃ 𝑡 ∈ ( SubGrp ‘ 𝐺 ) ( ( 𝑆 ∩ 𝑡 ) = { 0 } ∧ ( 𝑆 ⊕ 𝑡 ) = 𝑠 ) ) ↔ ( ( 𝐵 ∈ ( SubGrp ‘ 𝐺 ) ∧ 𝐴 ∈ 𝐵 ) → ∃ 𝑡 ∈ ( SubGrp ‘ 𝐺 ) ( ( 𝑆 ∩ 𝑡 ) = { 0 } ∧ ( 𝑆 ⊕ 𝑡 ) = 𝐵 ) ) ) )
31 30 imbi2d ⊢ ( 𝑠 = 𝐵 → ( ( 𝜑 → ( ( 𝑠 ∈ ( SubGrp ‘ 𝐺 ) ∧ 𝐴 ∈ 𝑠 ) → ∃ 𝑡 ∈ ( SubGrp ‘ 𝐺 ) ( ( 𝑆 ∩ 𝑡 ) = { 0 } ∧ ( 𝑆 ⊕ 𝑡 ) = 𝑠 ) ) ) ↔ ( 𝜑 → ( ( 𝐵 ∈ ( SubGrp ‘ 𝐺 ) ∧ 𝐴 ∈ 𝐵 ) → ∃ 𝑡 ∈ ( SubGrp ‘ 𝐺 ) ( ( 𝑆 ∩ 𝑡 ) = { 0 } ∧ ( 𝑆 ⊕ 𝑡 ) = 𝐵 ) ) ) ) )
32 bi2.04 ⊢ ( ( 𝑠 ⊊ 𝑢 → ( 𝑠 ∈ ( SubGrp ‘ 𝐺 ) → ( 𝐴 ∈ 𝑠 → ∃ 𝑡 ∈ ( SubGrp ‘ 𝐺 ) ( ( 𝑆 ∩ 𝑡 ) = { 0 } ∧ ( 𝑆 ⊕ 𝑡 ) = 𝑠 ) ) ) ) ↔ ( 𝑠 ∈ ( SubGrp ‘ 𝐺 ) → ( 𝑠 ⊊ 𝑢 → ( 𝐴 ∈ 𝑠 → ∃ 𝑡 ∈ ( SubGrp ‘ 𝐺 ) ( ( 𝑆 ∩ 𝑡 ) = { 0 } ∧ ( 𝑆 ⊕ 𝑡 ) = 𝑠 ) ) ) ) )
33 impexp ⊢ ( ( ( 𝑠 ∈ ( SubGrp ‘ 𝐺 ) ∧ 𝐴 ∈ 𝑠 ) → ∃ 𝑡 ∈ ( SubGrp ‘ 𝐺 ) ( ( 𝑆 ∩ 𝑡 ) = { 0 } ∧ ( 𝑆 ⊕ 𝑡 ) = 𝑠 ) ) ↔ ( 𝑠 ∈ ( SubGrp ‘ 𝐺 ) → ( 𝐴 ∈ 𝑠 → ∃ 𝑡 ∈ ( SubGrp ‘ 𝐺 ) ( ( 𝑆 ∩ 𝑡 ) = { 0 } ∧ ( 𝑆 ⊕ 𝑡 ) = 𝑠 ) ) ) )
34 33 imbi2i ⊢ ( ( 𝑠 ⊊ 𝑢 → ( ( 𝑠 ∈ ( SubGrp ‘ 𝐺 ) ∧ 𝐴 ∈ 𝑠 ) → ∃ 𝑡 ∈ ( SubGrp ‘ 𝐺 ) ( ( 𝑆 ∩ 𝑡 ) = { 0 } ∧ ( 𝑆 ⊕ 𝑡 ) = 𝑠 ) ) ) ↔ ( 𝑠 ⊊ 𝑢 → ( 𝑠 ∈ ( SubGrp ‘ 𝐺 ) → ( 𝐴 ∈ 𝑠 → ∃ 𝑡 ∈ ( SubGrp ‘ 𝐺 ) ( ( 𝑆 ∩ 𝑡 ) = { 0 } ∧ ( 𝑆 ⊕ 𝑡 ) = 𝑠 ) ) ) ) )
35 impexp ⊢ ( ( ( 𝑠 ⊊ 𝑢 ∧ 𝐴 ∈ 𝑠 ) → ∃ 𝑡 ∈ ( SubGrp ‘ 𝐺 ) ( ( 𝑆 ∩ 𝑡 ) = { 0 } ∧ ( 𝑆 ⊕ 𝑡 ) = 𝑠 ) ) ↔ ( 𝑠 ⊊ 𝑢 → ( 𝐴 ∈ 𝑠 → ∃ 𝑡 ∈ ( SubGrp ‘ 𝐺 ) ( ( 𝑆 ∩ 𝑡 ) = { 0 } ∧ ( 𝑆 ⊕ 𝑡 ) = 𝑠 ) ) ) )
36 35 imbi2i ⊢ ( ( 𝑠 ∈ ( SubGrp ‘ 𝐺 ) → ( ( 𝑠 ⊊ 𝑢 ∧ 𝐴 ∈ 𝑠 ) → ∃ 𝑡 ∈ ( SubGrp ‘ 𝐺 ) ( ( 𝑆 ∩ 𝑡 ) = { 0 } ∧ ( 𝑆 ⊕ 𝑡 ) = 𝑠 ) ) ) ↔ ( 𝑠 ∈ ( SubGrp ‘ 𝐺 ) → ( 𝑠 ⊊ 𝑢 → ( 𝐴 ∈ 𝑠 → ∃ 𝑡 ∈ ( SubGrp ‘ 𝐺 ) ( ( 𝑆 ∩ 𝑡 ) = { 0 } ∧ ( 𝑆 ⊕ 𝑡 ) = 𝑠 ) ) ) ) )
37 32 34 36 3bitr4i ⊢ ( ( 𝑠 ⊊ 𝑢 → ( ( 𝑠 ∈ ( SubGrp ‘ 𝐺 ) ∧ 𝐴 ∈ 𝑠 ) → ∃ 𝑡 ∈ ( SubGrp ‘ 𝐺 ) ( ( 𝑆 ∩ 𝑡 ) = { 0 } ∧ ( 𝑆 ⊕ 𝑡 ) = 𝑠 ) ) ) ↔ ( 𝑠 ∈ ( SubGrp ‘ 𝐺 ) → ( ( 𝑠 ⊊ 𝑢 ∧ 𝐴 ∈ 𝑠 ) → ∃ 𝑡 ∈ ( SubGrp ‘ 𝐺 ) ( ( 𝑆 ∩ 𝑡 ) = { 0 } ∧ ( 𝑆 ⊕ 𝑡 ) = 𝑠 ) ) ) )
38 37 imbi2i ⊢ ( ( 𝜑 → ( 𝑠 ⊊ 𝑢 → ( ( 𝑠 ∈ ( SubGrp ‘ 𝐺 ) ∧ 𝐴 ∈ 𝑠 ) → ∃ 𝑡 ∈ ( SubGrp ‘ 𝐺 ) ( ( 𝑆 ∩ 𝑡 ) = { 0 } ∧ ( 𝑆 ⊕ 𝑡 ) = 𝑠 ) ) ) ) ↔ ( 𝜑 → ( 𝑠 ∈ ( SubGrp ‘ 𝐺 ) → ( ( 𝑠 ⊊ 𝑢 ∧ 𝐴 ∈ 𝑠 ) → ∃ 𝑡 ∈ ( SubGrp ‘ 𝐺 ) ( ( 𝑆 ∩ 𝑡 ) = { 0 } ∧ ( 𝑆 ⊕ 𝑡 ) = 𝑠 ) ) ) ) )
39 bi2.04 ⊢ ( ( 𝑠 ⊊ 𝑢 → ( 𝜑 → ( ( 𝑠 ∈ ( SubGrp ‘ 𝐺 ) ∧ 𝐴 ∈ 𝑠 ) → ∃ 𝑡 ∈ ( SubGrp ‘ 𝐺 ) ( ( 𝑆 ∩ 𝑡 ) = { 0 } ∧ ( 𝑆 ⊕ 𝑡 ) = 𝑠 ) ) ) ) ↔ ( 𝜑 → ( 𝑠 ⊊ 𝑢 → ( ( 𝑠 ∈ ( SubGrp ‘ 𝐺 ) ∧ 𝐴 ∈ 𝑠 ) → ∃ 𝑡 ∈ ( SubGrp ‘ 𝐺 ) ( ( 𝑆 ∩ 𝑡 ) = { 0 } ∧ ( 𝑆 ⊕ 𝑡 ) = 𝑠 ) ) ) ) )
40 bi2.04 ⊢ ( ( 𝑠 ∈ ( SubGrp ‘ 𝐺 ) → ( 𝜑 → ( ( 𝑠 ⊊ 𝑢 ∧ 𝐴 ∈ 𝑠 ) → ∃ 𝑡 ∈ ( SubGrp ‘ 𝐺 ) ( ( 𝑆 ∩ 𝑡 ) = { 0 } ∧ ( 𝑆 ⊕ 𝑡 ) = 𝑠 ) ) ) ) ↔ ( 𝜑 → ( 𝑠 ∈ ( SubGrp ‘ 𝐺 ) → ( ( 𝑠 ⊊ 𝑢 ∧ 𝐴 ∈ 𝑠 ) → ∃ 𝑡 ∈ ( SubGrp ‘ 𝐺 ) ( ( 𝑆 ∩ 𝑡 ) = { 0 } ∧ ( 𝑆 ⊕ 𝑡 ) = 𝑠 ) ) ) ) )
41 38 39 40 3bitr4i ⊢ ( ( 𝑠 ⊊ 𝑢 → ( 𝜑 → ( ( 𝑠 ∈ ( SubGrp ‘ 𝐺 ) ∧ 𝐴 ∈ 𝑠 ) → ∃ 𝑡 ∈ ( SubGrp ‘ 𝐺 ) ( ( 𝑆 ∩ 𝑡 ) = { 0 } ∧ ( 𝑆 ⊕ 𝑡 ) = 𝑠 ) ) ) ) ↔ ( 𝑠 ∈ ( SubGrp ‘ 𝐺 ) → ( 𝜑 → ( ( 𝑠 ⊊ 𝑢 ∧ 𝐴 ∈ 𝑠 ) → ∃ 𝑡 ∈ ( SubGrp ‘ 𝐺 ) ( ( 𝑆 ∩ 𝑡 ) = { 0 } ∧ ( 𝑆 ⊕ 𝑡 ) = 𝑠 ) ) ) ) )
42 41 albii ⊢ ( ∀ 𝑠 ( 𝑠 ⊊ 𝑢 → ( 𝜑 → ( ( 𝑠 ∈ ( SubGrp ‘ 𝐺 ) ∧ 𝐴 ∈ 𝑠 ) → ∃ 𝑡 ∈ ( SubGrp ‘ 𝐺 ) ( ( 𝑆 ∩ 𝑡 ) = { 0 } ∧ ( 𝑆 ⊕ 𝑡 ) = 𝑠 ) ) ) ) ↔ ∀ 𝑠 ( 𝑠 ∈ ( SubGrp ‘ 𝐺 ) → ( 𝜑 → ( ( 𝑠 ⊊ 𝑢 ∧ 𝐴 ∈ 𝑠 ) → ∃ 𝑡 ∈ ( SubGrp ‘ 𝐺 ) ( ( 𝑆 ∩ 𝑡 ) = { 0 } ∧ ( 𝑆 ⊕ 𝑡 ) = 𝑠 ) ) ) ) )
43 df-ral ⊢ ( ∀ 𝑠 ∈ ( SubGrp ‘ 𝐺 ) ( 𝜑 → ( ( 𝑠 ⊊ 𝑢 ∧ 𝐴 ∈ 𝑠 ) → ∃ 𝑡 ∈ ( SubGrp ‘ 𝐺 ) ( ( 𝑆 ∩ 𝑡 ) = { 0 } ∧ ( 𝑆 ⊕ 𝑡 ) = 𝑠 ) ) ) ↔ ∀ 𝑠 ( 𝑠 ∈ ( SubGrp ‘ 𝐺 ) → ( 𝜑 → ( ( 𝑠 ⊊ 𝑢 ∧ 𝐴 ∈ 𝑠 ) → ∃ 𝑡 ∈ ( SubGrp ‘ 𝐺 ) ( ( 𝑆 ∩ 𝑡 ) = { 0 } ∧ ( 𝑆 ⊕ 𝑡 ) = 𝑠 ) ) ) ) )
44 r19.21v ⊢ ( ∀ 𝑠 ∈ ( SubGrp ‘ 𝐺 ) ( 𝜑 → ( ( 𝑠 ⊊ 𝑢 ∧ 𝐴 ∈ 𝑠 ) → ∃ 𝑡 ∈ ( SubGrp ‘ 𝐺 ) ( ( 𝑆 ∩ 𝑡 ) = { 0 } ∧ ( 𝑆 ⊕ 𝑡 ) = 𝑠 ) ) ) ↔ ( 𝜑 → ∀ 𝑠 ∈ ( SubGrp ‘ 𝐺 ) ( ( 𝑠 ⊊ 𝑢 ∧ 𝐴 ∈ 𝑠 ) → ∃ 𝑡 ∈ ( SubGrp ‘ 𝐺 ) ( ( 𝑆 ∩ 𝑡 ) = { 0 } ∧ ( 𝑆 ⊕ 𝑡 ) = 𝑠 ) ) ) )
45 42 43 44 3bitr2i ⊢ ( ∀ 𝑠 ( 𝑠 ⊊ 𝑢 → ( 𝜑 → ( ( 𝑠 ∈ ( SubGrp ‘ 𝐺 ) ∧ 𝐴 ∈ 𝑠 ) → ∃ 𝑡 ∈ ( SubGrp ‘ 𝐺 ) ( ( 𝑆 ∩ 𝑡 ) = { 0 } ∧ ( 𝑆 ⊕ 𝑡 ) = 𝑠 ) ) ) ) ↔ ( 𝜑 → ∀ 𝑠 ∈ ( SubGrp ‘ 𝐺 ) ( ( 𝑠 ⊊ 𝑢 ∧ 𝐴 ∈ 𝑠 ) → ∃ 𝑡 ∈ ( SubGrp ‘ 𝐺 ) ( ( 𝑆 ∩ 𝑡 ) = { 0 } ∧ ( 𝑆 ⊕ 𝑡 ) = 𝑠 ) ) ) )
46 psseq1 ⊢ ( 𝑥 = 𝑠 → ( 𝑥 ⊊ 𝑢 ↔ 𝑠 ⊊ 𝑢 ) )
47 eleq2 ⊢ ( 𝑥 = 𝑠 → ( 𝐴 ∈ 𝑥 ↔ 𝐴 ∈ 𝑠 ) )
48 46 47 anbi12d ⊢ ( 𝑥 = 𝑠 → ( ( 𝑥 ⊊ 𝑢 ∧ 𝐴 ∈ 𝑥 ) ↔ ( 𝑠 ⊊ 𝑢 ∧ 𝐴 ∈ 𝑠 ) ) )
49 ineq2 ⊢ ( 𝑦 = 𝑡 → ( 𝑆 ∩ 𝑦 ) = ( 𝑆 ∩ 𝑡 ) )
50 49 eqeq1d ⊢ ( 𝑦 = 𝑡 → ( ( 𝑆 ∩ 𝑦 ) = { 0 } ↔ ( 𝑆 ∩ 𝑡 ) = { 0 } ) )
51 oveq2 ⊢ ( 𝑦 = 𝑡 → ( 𝑆 ⊕ 𝑦 ) = ( 𝑆 ⊕ 𝑡 ) )
52 51 eqeq1d ⊢ ( 𝑦 = 𝑡 → ( ( 𝑆 ⊕ 𝑦 ) = 𝑥 ↔ ( 𝑆 ⊕ 𝑡 ) = 𝑥 ) )
53 50 52 anbi12d ⊢ ( 𝑦 = 𝑡 → ( ( ( 𝑆 ∩ 𝑦 ) = { 0 } ∧ ( 𝑆 ⊕ 𝑦 ) = 𝑥 ) ↔ ( ( 𝑆 ∩ 𝑡 ) = { 0 } ∧ ( 𝑆 ⊕ 𝑡 ) = 𝑥 ) ) )
54 53 cbvrexvw ⊢ ( ∃ 𝑦 ∈ ( SubGrp ‘ 𝐺 ) ( ( 𝑆 ∩ 𝑦 ) = { 0 } ∧ ( 𝑆 ⊕ 𝑦 ) = 𝑥 ) ↔ ∃ 𝑡 ∈ ( SubGrp ‘ 𝐺 ) ( ( 𝑆 ∩ 𝑡 ) = { 0 } ∧ ( 𝑆 ⊕ 𝑡 ) = 𝑥 ) )
55 eqeq2 ⊢ ( 𝑥 = 𝑠 → ( ( 𝑆 ⊕ 𝑡 ) = 𝑥 ↔ ( 𝑆 ⊕ 𝑡 ) = 𝑠 ) )
56 55 anbi2d ⊢ ( 𝑥 = 𝑠 → ( ( ( 𝑆 ∩ 𝑡 ) = { 0 } ∧ ( 𝑆 ⊕ 𝑡 ) = 𝑥 ) ↔ ( ( 𝑆 ∩ 𝑡 ) = { 0 } ∧ ( 𝑆 ⊕ 𝑡 ) = 𝑠 ) ) )
57 56 rexbidv ⊢ ( 𝑥 = 𝑠 → ( ∃ 𝑡 ∈ ( SubGrp ‘ 𝐺 ) ( ( 𝑆 ∩ 𝑡 ) = { 0 } ∧ ( 𝑆 ⊕ 𝑡 ) = 𝑥 ) ↔ ∃ 𝑡 ∈ ( SubGrp ‘ 𝐺 ) ( ( 𝑆 ∩ 𝑡 ) = { 0 } ∧ ( 𝑆 ⊕ 𝑡 ) = 𝑠 ) ) )
58 54 57 syl5bb ⊢ ( 𝑥 = 𝑠 → ( ∃ 𝑦 ∈ ( SubGrp ‘ 𝐺 ) ( ( 𝑆 ∩ 𝑦 ) = { 0 } ∧ ( 𝑆 ⊕ 𝑦 ) = 𝑥 ) ↔ ∃ 𝑡 ∈ ( SubGrp ‘ 𝐺 ) ( ( 𝑆 ∩ 𝑡 ) = { 0 } ∧ ( 𝑆 ⊕ 𝑡 ) = 𝑠 ) ) )
59 48 58 imbi12d ⊢ ( 𝑥 = 𝑠 → ( ( ( 𝑥 ⊊ 𝑢 ∧ 𝐴 ∈ 𝑥 ) → ∃ 𝑦 ∈ ( SubGrp ‘ 𝐺 ) ( ( 𝑆 ∩ 𝑦 ) = { 0 } ∧ ( 𝑆 ⊕ 𝑦 ) = 𝑥 ) ) ↔ ( ( 𝑠 ⊊ 𝑢 ∧ 𝐴 ∈ 𝑠 ) → ∃ 𝑡 ∈ ( SubGrp ‘ 𝐺 ) ( ( 𝑆 ∩ 𝑡 ) = { 0 } ∧ ( 𝑆 ⊕ 𝑡 ) = 𝑠 ) ) ) )
60 59 cbvralvw ⊢ ( ∀ 𝑥 ∈ ( SubGrp ‘ 𝐺 ) ( ( 𝑥 ⊊ 𝑢 ∧ 𝐴 ∈ 𝑥 ) → ∃ 𝑦 ∈ ( SubGrp ‘ 𝐺 ) ( ( 𝑆 ∩ 𝑦 ) = { 0 } ∧ ( 𝑆 ⊕ 𝑦 ) = 𝑥 ) ) ↔ ∀ 𝑠 ∈ ( SubGrp ‘ 𝐺 ) ( ( 𝑠 ⊊ 𝑢 ∧ 𝐴 ∈ 𝑠 ) → ∃ 𝑡 ∈ ( SubGrp ‘ 𝐺 ) ( ( 𝑆 ∩ 𝑡 ) = { 0 } ∧ ( 𝑆 ⊕ 𝑡 ) = 𝑠 ) ) )
61 8 adantr ⊢ ( ( 𝜑 ∧ ( ∀ 𝑥 ∈ ( SubGrp ‘ 𝐺 ) ( ( 𝑥 ⊊ 𝑢 ∧ 𝐴 ∈ 𝑥 ) → ∃ 𝑦 ∈ ( SubGrp ‘ 𝐺 ) ( ( 𝑆 ∩ 𝑦 ) = { 0 } ∧ ( 𝑆 ⊕ 𝑦 ) = 𝑥 ) ) ∧ ( 𝑢 ∈ ( SubGrp ‘ 𝐺 ) ∧ 𝐴 ∈ 𝑢 ) ) ) → 𝑃 pGrp 𝐺 )
62 9 adantr ⊢ ( ( 𝜑 ∧ ( ∀ 𝑥 ∈ ( SubGrp ‘ 𝐺 ) ( ( 𝑥 ⊊ 𝑢 ∧ 𝐴 ∈ 𝑥 ) → ∃ 𝑦 ∈ ( SubGrp ‘ 𝐺 ) ( ( 𝑆 ∩ 𝑦 ) = { 0 } ∧ ( 𝑆 ⊕ 𝑦 ) = 𝑥 ) ) ∧ ( 𝑢 ∈ ( SubGrp ‘ 𝐺 ) ∧ 𝐴 ∈ 𝑢 ) ) ) → 𝐺 ∈ Abel )
63 10 adantr ⊢ ( ( 𝜑 ∧ ( ∀ 𝑥 ∈ ( SubGrp ‘ 𝐺 ) ( ( 𝑥 ⊊ 𝑢 ∧ 𝐴 ∈ 𝑥 ) → ∃ 𝑦 ∈ ( SubGrp ‘ 𝐺 ) ( ( 𝑆 ∩ 𝑦 ) = { 0 } ∧ ( 𝑆 ⊕ 𝑦 ) = 𝑥 ) ) ∧ ( 𝑢 ∈ ( SubGrp ‘ 𝐺 ) ∧ 𝐴 ∈ 𝑢 ) ) ) → 𝐵 ∈ Fin )
64 11 adantr ⊢ ( ( 𝜑 ∧ ( ∀ 𝑥 ∈ ( SubGrp ‘ 𝐺 ) ( ( 𝑥 ⊊ 𝑢 ∧ 𝐴 ∈ 𝑥 ) → ∃ 𝑦 ∈ ( SubGrp ‘ 𝐺 ) ( ( 𝑆 ∩ 𝑦 ) = { 0 } ∧ ( 𝑆 ⊕ 𝑦 ) = 𝑥 ) ) ∧ ( 𝑢 ∈ ( SubGrp ‘ 𝐺 ) ∧ 𝐴 ∈ 𝑢 ) ) ) → ( 𝑂 ‘ 𝐴 ) = 𝐸 )
65 simprrl ⊢ ( ( 𝜑 ∧ ( ∀ 𝑥 ∈ ( SubGrp ‘ 𝐺 ) ( ( 𝑥 ⊊ 𝑢 ∧ 𝐴 ∈ 𝑥 ) → ∃ 𝑦 ∈ ( SubGrp ‘ 𝐺 ) ( ( 𝑆 ∩ 𝑦 ) = { 0 } ∧ ( 𝑆 ⊕ 𝑦 ) = 𝑥 ) ) ∧ ( 𝑢 ∈ ( SubGrp ‘ 𝐺 ) ∧ 𝐴 ∈ 𝑢 ) ) ) → 𝑢 ∈ ( SubGrp ‘ 𝐺 ) )
66 simprrr ⊢ ( ( 𝜑 ∧ ( ∀ 𝑥 ∈ ( SubGrp ‘ 𝐺 ) ( ( 𝑥 ⊊ 𝑢 ∧ 𝐴 ∈ 𝑥 ) → ∃ 𝑦 ∈ ( SubGrp ‘ 𝐺 ) ( ( 𝑆 ∩ 𝑦 ) = { 0 } ∧ ( 𝑆 ⊕ 𝑦 ) = 𝑥 ) ) ∧ ( 𝑢 ∈ ( SubGrp ‘ 𝐺 ) ∧ 𝐴 ∈ 𝑢 ) ) ) → 𝐴 ∈ 𝑢 )
67 simprl ⊢ ( ( 𝜑 ∧ ( ∀ 𝑥 ∈ ( SubGrp ‘ 𝐺 ) ( ( 𝑥 ⊊ 𝑢 ∧ 𝐴 ∈ 𝑥 ) → ∃ 𝑦 ∈ ( SubGrp ‘ 𝐺 ) ( ( 𝑆 ∩ 𝑦 ) = { 0 } ∧ ( 𝑆 ⊕ 𝑦 ) = 𝑥 ) ) ∧ ( 𝑢 ∈ ( SubGrp ‘ 𝐺 ) ∧ 𝐴 ∈ 𝑢 ) ) ) → ∀ 𝑥 ∈ ( SubGrp ‘ 𝐺 ) ( ( 𝑥 ⊊ 𝑢 ∧ 𝐴 ∈ 𝑥 ) → ∃ 𝑦 ∈ ( SubGrp ‘ 𝐺 ) ( ( 𝑆 ∩ 𝑦 ) = { 0 } ∧ ( 𝑆 ⊕ 𝑦 ) = 𝑥 ) ) )
68 67 60 sylib ⊢ ( ( 𝜑 ∧ ( ∀ 𝑥 ∈ ( SubGrp ‘ 𝐺 ) ( ( 𝑥 ⊊ 𝑢 ∧ 𝐴 ∈ 𝑥 ) → ∃ 𝑦 ∈ ( SubGrp ‘ 𝐺 ) ( ( 𝑆 ∩ 𝑦 ) = { 0 } ∧ ( 𝑆 ⊕ 𝑦 ) = 𝑥 ) ) ∧ ( 𝑢 ∈ ( SubGrp ‘ 𝐺 ) ∧ 𝐴 ∈ 𝑢 ) ) ) → ∀ 𝑠 ∈ ( SubGrp ‘ 𝐺 ) ( ( 𝑠 ⊊ 𝑢 ∧ 𝐴 ∈ 𝑠 ) → ∃ 𝑡 ∈ ( SubGrp ‘ 𝐺 ) ( ( 𝑆 ∩ 𝑡 ) = { 0 } ∧ ( 𝑆 ⊕ 𝑡 ) = 𝑠 ) ) )
69 1 2 3 4 5 6 7 61 62 63 64 65 66 68 pgpfac1lem5 ⊢ ( ( 𝜑 ∧ ( ∀ 𝑥 ∈ ( SubGrp ‘ 𝐺 ) ( ( 𝑥 ⊊ 𝑢 ∧ 𝐴 ∈ 𝑥 ) → ∃ 𝑦 ∈ ( SubGrp ‘ 𝐺 ) ( ( 𝑆 ∩ 𝑦 ) = { 0 } ∧ ( 𝑆 ⊕ 𝑦 ) = 𝑥 ) ) ∧ ( 𝑢 ∈ ( SubGrp ‘ 𝐺 ) ∧ 𝐴 ∈ 𝑢 ) ) ) → ∃ 𝑡 ∈ ( SubGrp ‘ 𝐺 ) ( ( 𝑆 ∩ 𝑡 ) = { 0 } ∧ ( 𝑆 ⊕ 𝑡 ) = 𝑢 ) )
70 69 exp32 ⊢ ( 𝜑 → ( ∀ 𝑥 ∈ ( SubGrp ‘ 𝐺 ) ( ( 𝑥 ⊊ 𝑢 ∧ 𝐴 ∈ 𝑥 ) → ∃ 𝑦 ∈ ( SubGrp ‘ 𝐺 ) ( ( 𝑆 ∩ 𝑦 ) = { 0 } ∧ ( 𝑆 ⊕ 𝑦 ) = 𝑥 ) ) → ( ( 𝑢 ∈ ( SubGrp ‘ 𝐺 ) ∧ 𝐴 ∈ 𝑢 ) → ∃ 𝑡 ∈ ( SubGrp ‘ 𝐺 ) ( ( 𝑆 ∩ 𝑡 ) = { 0 } ∧ ( 𝑆 ⊕ 𝑡 ) = 𝑢 ) ) ) )
71 60 70 syl5bir ⊢ ( 𝜑 → ( ∀ 𝑠 ∈ ( SubGrp ‘ 𝐺 ) ( ( 𝑠 ⊊ 𝑢 ∧ 𝐴 ∈ 𝑠 ) → ∃ 𝑡 ∈ ( SubGrp ‘ 𝐺 ) ( ( 𝑆 ∩ 𝑡 ) = { 0 } ∧ ( 𝑆 ⊕ 𝑡 ) = 𝑠 ) ) → ( ( 𝑢 ∈ ( SubGrp ‘ 𝐺 ) ∧ 𝐴 ∈ 𝑢 ) → ∃ 𝑡 ∈ ( SubGrp ‘ 𝐺 ) ( ( 𝑆 ∩ 𝑡 ) = { 0 } ∧ ( 𝑆 ⊕ 𝑡 ) = 𝑢 ) ) ) )
72 71 a2i ⊢ ( ( 𝜑 → ∀ 𝑠 ∈ ( SubGrp ‘ 𝐺 ) ( ( 𝑠 ⊊ 𝑢 ∧ 𝐴 ∈ 𝑠 ) → ∃ 𝑡 ∈ ( SubGrp ‘ 𝐺 ) ( ( 𝑆 ∩ 𝑡 ) = { 0 } ∧ ( 𝑆 ⊕ 𝑡 ) = 𝑠 ) ) ) → ( 𝜑 → ( ( 𝑢 ∈ ( SubGrp ‘ 𝐺 ) ∧ 𝐴 ∈ 𝑢 ) → ∃ 𝑡 ∈ ( SubGrp ‘ 𝐺 ) ( ( 𝑆 ∩ 𝑡 ) = { 0 } ∧ ( 𝑆 ⊕ 𝑡 ) = 𝑢 ) ) ) )
73 45 72 sylbi ⊢ ( ∀ 𝑠 ( 𝑠 ⊊ 𝑢 → ( 𝜑 → ( ( 𝑠 ∈ ( SubGrp ‘ 𝐺 ) ∧ 𝐴 ∈ 𝑠 ) → ∃ 𝑡 ∈ ( SubGrp ‘ 𝐺 ) ( ( 𝑆 ∩ 𝑡 ) = { 0 } ∧ ( 𝑆 ⊕ 𝑡 ) = 𝑠 ) ) ) ) → ( 𝜑 → ( ( 𝑢 ∈ ( SubGrp ‘ 𝐺 ) ∧ 𝐴 ∈ 𝑢 ) → ∃ 𝑡 ∈ ( SubGrp ‘ 𝐺 ) ( ( 𝑆 ∩ 𝑡 ) = { 0 } ∧ ( 𝑆 ⊕ 𝑡 ) = 𝑢 ) ) ) )
74 73 a1i ⊢ ( 𝑢 ∈ Fin → ( ∀ 𝑠 ( 𝑠 ⊊ 𝑢 → ( 𝜑 → ( ( 𝑠 ∈ ( SubGrp ‘ 𝐺 ) ∧ 𝐴 ∈ 𝑠 ) → ∃ 𝑡 ∈ ( SubGrp ‘ 𝐺 ) ( ( 𝑆 ∩ 𝑡 ) = { 0 } ∧ ( 𝑆 ⊕ 𝑡 ) = 𝑠 ) ) ) ) → ( 𝜑 → ( ( 𝑢 ∈ ( SubGrp ‘ 𝐺 ) ∧ 𝐴 ∈ 𝑢 ) → ∃ 𝑡 ∈ ( SubGrp ‘ 𝐺 ) ( ( 𝑆 ∩ 𝑡 ) = { 0 } ∧ ( 𝑆 ⊕ 𝑡 ) = 𝑢 ) ) ) ) )
75 23 31 74 findcard3 ⊢ ( 𝐵 ∈ Fin → ( 𝜑 → ( ( 𝐵 ∈ ( SubGrp ‘ 𝐺 ) ∧ 𝐴 ∈ 𝐵 ) → ∃ 𝑡 ∈ ( SubGrp ‘ 𝐺 ) ( ( 𝑆 ∩ 𝑡 ) = { 0 } ∧ ( 𝑆 ⊕ 𝑡 ) = 𝐵 ) ) ) )
76 10 75 mpcom ⊢ ( 𝜑 → ( ( 𝐵 ∈ ( SubGrp ‘ 𝐺 ) ∧ 𝐴 ∈ 𝐵 ) → ∃ 𝑡 ∈ ( SubGrp ‘ 𝐺 ) ( ( 𝑆 ∩ 𝑡 ) = { 0 } ∧ ( 𝑆 ⊕ 𝑡 ) = 𝐵 ) ) )
77 15 12 76 mp2and ⊢ ( 𝜑 → ∃ 𝑡 ∈ ( SubGrp ‘ 𝐺 ) ( ( 𝑆 ∩ 𝑡 ) = { 0 } ∧ ( 𝑆 ⊕ 𝑡 ) = 𝐵 ) )