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