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 } ∧ ( 𝑆 𝑡 ) = 𝐵 ) )