| Step | Hyp | Ref | Expression | 
|---|
| 1 |  | pgpfac1.k | . . . . . . . 8
⊢ 𝐾 =
(mrCls‘(SubGrp‘𝐺)) | 
| 2 |  | pgpfac1.s | . . . . . . . 8
⊢ 𝑆 = (𝐾‘{𝐴}) | 
| 3 |  | pgpfac1.b | . . . . . . . 8
⊢ 𝐵 = (Base‘𝐺) | 
| 4 |  | pgpfac1.o | . . . . . . . 8
⊢ 𝑂 = (od‘𝐺) | 
| 5 |  | pgpfac1.e | . . . . . . . 8
⊢ 𝐸 = (gEx‘𝐺) | 
| 6 |  | pgpfac1.z | . . . . . . . 8
⊢  0 =
(0g‘𝐺) | 
| 7 |  | pgpfac1.l | . . . . . . . 8
⊢  ⊕ =
(LSSum‘𝐺) | 
| 8 |  | pgpfac1.p | . . . . . . . 8
⊢ (𝜑 → 𝑃 pGrp 𝐺) | 
| 9 |  | pgpfac1.g | . . . . . . . 8
⊢ (𝜑 → 𝐺 ∈ Abel) | 
| 10 |  | pgpfac1.n | . . . . . . . 8
⊢ (𝜑 → 𝐵 ∈ Fin) | 
| 11 |  | pgpfac1.oe | . . . . . . . 8
⊢ (𝜑 → (𝑂‘𝐴) = 𝐸) | 
| 12 |  | pgpfac1.u | . . . . . . . 8
⊢ (𝜑 → 𝑈 ∈ (SubGrp‘𝐺)) | 
| 13 |  | pgpfac1.au | . . . . . . . 8
⊢ (𝜑 → 𝐴 ∈ 𝑈) | 
| 14 |  | pgpfac1.w | . . . . . . . 8
⊢ (𝜑 → 𝑊 ∈ (SubGrp‘𝐺)) | 
| 15 |  | pgpfac1.i | . . . . . . . 8
⊢ (𝜑 → (𝑆 ∩ 𝑊) = { 0 }) | 
| 16 |  | pgpfac1.ss | . . . . . . . 8
⊢ (𝜑 → (𝑆 ⊕ 𝑊) ⊆ 𝑈) | 
| 17 |  | pgpfac1.2 | . . . . . . . 8
⊢ (𝜑 → ∀𝑤 ∈ (SubGrp‘𝐺)((𝑤 ⊊ 𝑈 ∧ 𝐴 ∈ 𝑤) → ¬ (𝑆 ⊕ 𝑊) ⊊ 𝑤)) | 
| 18 |  | pgpfac1.c | . . . . . . . 8
⊢ (𝜑 → 𝐶 ∈ (𝑈 ∖ (𝑆 ⊕ 𝑊))) | 
| 19 |  | pgpfac1.mg | . . . . . . . 8
⊢  · =
(.g‘𝐺) | 
| 20 | 1, 2, 3, 4, 5, 6, 7, 8, 9, 10,
11, 12, 13, 14, 15, 16, 17, 18, 19 | pgpfac1lem2 20096 | . . . . . . 7
⊢ (𝜑 → (𝑃 · 𝐶) ∈ (𝑆 ⊕ 𝑊)) | 
| 21 |  | ablgrp 19804 | . . . . . . . . . . . 12
⊢ (𝐺 ∈ Abel → 𝐺 ∈ Grp) | 
| 22 | 9, 21 | syl 17 | . . . . . . . . . . 11
⊢ (𝜑 → 𝐺 ∈ Grp) | 
| 23 | 3 | subgacs 19180 | . . . . . . . . . . 11
⊢ (𝐺 ∈ Grp →
(SubGrp‘𝐺) ∈
(ACS‘𝐵)) | 
| 24 |  | acsmre 17696 | . . . . . . . . . . 11
⊢
((SubGrp‘𝐺)
∈ (ACS‘𝐵) →
(SubGrp‘𝐺) ∈
(Moore‘𝐵)) | 
| 25 | 22, 23, 24 | 3syl 18 | . . . . . . . . . 10
⊢ (𝜑 → (SubGrp‘𝐺) ∈ (Moore‘𝐵)) | 
| 26 | 3 | subgss 19146 | . . . . . . . . . . . 12
⊢ (𝑈 ∈ (SubGrp‘𝐺) → 𝑈 ⊆ 𝐵) | 
| 27 | 12, 26 | syl 17 | . . . . . . . . . . 11
⊢ (𝜑 → 𝑈 ⊆ 𝐵) | 
| 28 | 27, 13 | sseldd 3983 | . . . . . . . . . 10
⊢ (𝜑 → 𝐴 ∈ 𝐵) | 
| 29 | 1 | mrcsncl 17656 | . . . . . . . . . 10
⊢
(((SubGrp‘𝐺)
∈ (Moore‘𝐵)
∧ 𝐴 ∈ 𝐵) → (𝐾‘{𝐴}) ∈ (SubGrp‘𝐺)) | 
| 30 | 25, 28, 29 | syl2anc 584 | . . . . . . . . 9
⊢ (𝜑 → (𝐾‘{𝐴}) ∈ (SubGrp‘𝐺)) | 
| 31 | 2, 30 | eqeltrid 2844 | . . . . . . . 8
⊢ (𝜑 → 𝑆 ∈ (SubGrp‘𝐺)) | 
| 32 | 7 | lsmcom 19877 | . . . . . . . 8
⊢ ((𝐺 ∈ Abel ∧ 𝑆 ∈ (SubGrp‘𝐺) ∧ 𝑊 ∈ (SubGrp‘𝐺)) → (𝑆 ⊕ 𝑊) = (𝑊 ⊕ 𝑆)) | 
| 33 | 9, 31, 14, 32 | syl3anc 1372 | . . . . . . 7
⊢ (𝜑 → (𝑆 ⊕ 𝑊) = (𝑊 ⊕ 𝑆)) | 
| 34 | 20, 33 | eleqtrd 2842 | . . . . . 6
⊢ (𝜑 → (𝑃 · 𝐶) ∈ (𝑊 ⊕ 𝑆)) | 
| 35 |  | eqid 2736 | . . . . . . 7
⊢
(-g‘𝐺) = (-g‘𝐺) | 
| 36 | 35, 7, 14, 31 | lsmelvalm 19670 | . . . . . 6
⊢ (𝜑 → ((𝑃 · 𝐶) ∈ (𝑊 ⊕ 𝑆) ↔ ∃𝑤 ∈ 𝑊 ∃𝑠 ∈ 𝑆 (𝑃 · 𝐶) = (𝑤(-g‘𝐺)𝑠))) | 
| 37 | 34, 36 | mpbid 232 | . . . . 5
⊢ (𝜑 → ∃𝑤 ∈ 𝑊 ∃𝑠 ∈ 𝑆 (𝑃 · 𝐶) = (𝑤(-g‘𝐺)𝑠)) | 
| 38 |  | eqid 2736 | . . . . . . . . . . 11
⊢ (𝑘 ∈ ℤ ↦ (𝑘 · 𝐴)) = (𝑘 ∈ ℤ ↦ (𝑘 · 𝐴)) | 
| 39 | 3, 19, 38, 1 | cycsubg2 19229 | . . . . . . . . . 10
⊢ ((𝐺 ∈ Grp ∧ 𝐴 ∈ 𝐵) → (𝐾‘{𝐴}) = ran (𝑘 ∈ ℤ ↦ (𝑘 · 𝐴))) | 
| 40 | 22, 28, 39 | syl2anc 584 | . . . . . . . . 9
⊢ (𝜑 → (𝐾‘{𝐴}) = ran (𝑘 ∈ ℤ ↦ (𝑘 · 𝐴))) | 
| 41 | 2, 40 | eqtrid 2788 | . . . . . . . 8
⊢ (𝜑 → 𝑆 = ran (𝑘 ∈ ℤ ↦ (𝑘 · 𝐴))) | 
| 42 | 41 | rexeqdv 3326 | . . . . . . 7
⊢ (𝜑 → (∃𝑠 ∈ 𝑆 (𝑃 · 𝐶) = (𝑤(-g‘𝐺)𝑠) ↔ ∃𝑠 ∈ ran (𝑘 ∈ ℤ ↦ (𝑘 · 𝐴))(𝑃 · 𝐶) = (𝑤(-g‘𝐺)𝑠))) | 
| 43 |  | ovex 7465 | . . . . . . . . 9
⊢ (𝑘 · 𝐴) ∈ V | 
| 44 | 43 | rgenw 3064 | . . . . . . . 8
⊢
∀𝑘 ∈
ℤ (𝑘 · 𝐴) ∈ V | 
| 45 |  | oveq2 7440 | . . . . . . . . . 10
⊢ (𝑠 = (𝑘 · 𝐴) → (𝑤(-g‘𝐺)𝑠) = (𝑤(-g‘𝐺)(𝑘 · 𝐴))) | 
| 46 | 45 | eqeq2d 2747 | . . . . . . . . 9
⊢ (𝑠 = (𝑘 · 𝐴) → ((𝑃 · 𝐶) = (𝑤(-g‘𝐺)𝑠) ↔ (𝑃 · 𝐶) = (𝑤(-g‘𝐺)(𝑘 · 𝐴)))) | 
| 47 | 38, 46 | rexrnmptw 7114 | . . . . . . . 8
⊢
(∀𝑘 ∈
ℤ (𝑘 · 𝐴) ∈ V → (∃𝑠 ∈ ran (𝑘 ∈ ℤ ↦ (𝑘 · 𝐴))(𝑃 · 𝐶) = (𝑤(-g‘𝐺)𝑠) ↔ ∃𝑘 ∈ ℤ (𝑃 · 𝐶) = (𝑤(-g‘𝐺)(𝑘 · 𝐴)))) | 
| 48 | 44, 47 | ax-mp 5 | . . . . . . 7
⊢
(∃𝑠 ∈ ran
(𝑘 ∈ ℤ ↦
(𝑘 · 𝐴))(𝑃 · 𝐶) = (𝑤(-g‘𝐺)𝑠) ↔ ∃𝑘 ∈ ℤ (𝑃 · 𝐶) = (𝑤(-g‘𝐺)(𝑘 · 𝐴))) | 
| 49 | 42, 48 | bitrdi 287 | . . . . . 6
⊢ (𝜑 → (∃𝑠 ∈ 𝑆 (𝑃 · 𝐶) = (𝑤(-g‘𝐺)𝑠) ↔ ∃𝑘 ∈ ℤ (𝑃 · 𝐶) = (𝑤(-g‘𝐺)(𝑘 · 𝐴)))) | 
| 50 | 49 | rexbidv 3178 | . . . . 5
⊢ (𝜑 → (∃𝑤 ∈ 𝑊 ∃𝑠 ∈ 𝑆 (𝑃 · 𝐶) = (𝑤(-g‘𝐺)𝑠) ↔ ∃𝑤 ∈ 𝑊 ∃𝑘 ∈ ℤ (𝑃 · 𝐶) = (𝑤(-g‘𝐺)(𝑘 · 𝐴)))) | 
| 51 | 37, 50 | mpbid 232 | . . . 4
⊢ (𝜑 → ∃𝑤 ∈ 𝑊 ∃𝑘 ∈ ℤ (𝑃 · 𝐶) = (𝑤(-g‘𝐺)(𝑘 · 𝐴))) | 
| 52 |  | rexcom 3289 | . . . 4
⊢
(∃𝑤 ∈
𝑊 ∃𝑘 ∈ ℤ (𝑃 · 𝐶) = (𝑤(-g‘𝐺)(𝑘 · 𝐴)) ↔ ∃𝑘 ∈ ℤ ∃𝑤 ∈ 𝑊 (𝑃 · 𝐶) = (𝑤(-g‘𝐺)(𝑘 · 𝐴))) | 
| 53 | 51, 52 | sylib 218 | . . 3
⊢ (𝜑 → ∃𝑘 ∈ ℤ ∃𝑤 ∈ 𝑊 (𝑃 · 𝐶) = (𝑤(-g‘𝐺)(𝑘 · 𝐴))) | 
| 54 | 22 | ad2antrr 726 | . . . . . . . 8
⊢ (((𝜑 ∧ 𝑘 ∈ ℤ) ∧ 𝑤 ∈ 𝑊) → 𝐺 ∈ Grp) | 
| 55 | 3 | subgss 19146 | . . . . . . . . . . 11
⊢ (𝑊 ∈ (SubGrp‘𝐺) → 𝑊 ⊆ 𝐵) | 
| 56 | 14, 55 | syl 17 | . . . . . . . . . 10
⊢ (𝜑 → 𝑊 ⊆ 𝐵) | 
| 57 | 56 | adantr 480 | . . . . . . . . 9
⊢ ((𝜑 ∧ 𝑘 ∈ ℤ) → 𝑊 ⊆ 𝐵) | 
| 58 | 57 | sselda 3982 | . . . . . . . 8
⊢ (((𝜑 ∧ 𝑘 ∈ ℤ) ∧ 𝑤 ∈ 𝑊) → 𝑤 ∈ 𝐵) | 
| 59 |  | simplr 768 | . . . . . . . . 9
⊢ (((𝜑 ∧ 𝑘 ∈ ℤ) ∧ 𝑤 ∈ 𝑊) → 𝑘 ∈ ℤ) | 
| 60 | 28 | ad2antrr 726 | . . . . . . . . 9
⊢ (((𝜑 ∧ 𝑘 ∈ ℤ) ∧ 𝑤 ∈ 𝑊) → 𝐴 ∈ 𝐵) | 
| 61 | 3, 19 | mulgcl 19110 | . . . . . . . . 9
⊢ ((𝐺 ∈ Grp ∧ 𝑘 ∈ ℤ ∧ 𝐴 ∈ 𝐵) → (𝑘 · 𝐴) ∈ 𝐵) | 
| 62 | 54, 59, 60, 61 | syl3anc 1372 | . . . . . . . 8
⊢ (((𝜑 ∧ 𝑘 ∈ ℤ) ∧ 𝑤 ∈ 𝑊) → (𝑘 · 𝐴) ∈ 𝐵) | 
| 63 |  | pgpprm 19612 | . . . . . . . . . . 11
⊢ (𝑃 pGrp 𝐺 → 𝑃 ∈ ℙ) | 
| 64 |  | prmz 16713 | . . . . . . . . . . 11
⊢ (𝑃 ∈ ℙ → 𝑃 ∈
ℤ) | 
| 65 | 8, 63, 64 | 3syl 18 | . . . . . . . . . 10
⊢ (𝜑 → 𝑃 ∈ ℤ) | 
| 66 | 18 | eldifad 3962 | . . . . . . . . . . 11
⊢ (𝜑 → 𝐶 ∈ 𝑈) | 
| 67 | 27, 66 | sseldd 3983 | . . . . . . . . . 10
⊢ (𝜑 → 𝐶 ∈ 𝐵) | 
| 68 | 3, 19 | mulgcl 19110 | . . . . . . . . . 10
⊢ ((𝐺 ∈ Grp ∧ 𝑃 ∈ ℤ ∧ 𝐶 ∈ 𝐵) → (𝑃 · 𝐶) ∈ 𝐵) | 
| 69 | 22, 65, 67, 68 | syl3anc 1372 | . . . . . . . . 9
⊢ (𝜑 → (𝑃 · 𝐶) ∈ 𝐵) | 
| 70 | 69 | ad2antrr 726 | . . . . . . . 8
⊢ (((𝜑 ∧ 𝑘 ∈ ℤ) ∧ 𝑤 ∈ 𝑊) → (𝑃 · 𝐶) ∈ 𝐵) | 
| 71 |  | eqid 2736 | . . . . . . . . 9
⊢
(+g‘𝐺) = (+g‘𝐺) | 
| 72 | 3, 71, 35 | grpsubadd 19047 | . . . . . . . 8
⊢ ((𝐺 ∈ Grp ∧ (𝑤 ∈ 𝐵 ∧ (𝑘 · 𝐴) ∈ 𝐵 ∧ (𝑃 · 𝐶) ∈ 𝐵)) → ((𝑤(-g‘𝐺)(𝑘 · 𝐴)) = (𝑃 · 𝐶) ↔ ((𝑃 · 𝐶)(+g‘𝐺)(𝑘 · 𝐴)) = 𝑤)) | 
| 73 | 54, 58, 62, 70, 72 | syl13anc 1373 | . . . . . . 7
⊢ (((𝜑 ∧ 𝑘 ∈ ℤ) ∧ 𝑤 ∈ 𝑊) → ((𝑤(-g‘𝐺)(𝑘 · 𝐴)) = (𝑃 · 𝐶) ↔ ((𝑃 · 𝐶)(+g‘𝐺)(𝑘 · 𝐴)) = 𝑤)) | 
| 74 |  | eqcom 2743 | . . . . . . 7
⊢ ((𝑃 · 𝐶) = (𝑤(-g‘𝐺)(𝑘 · 𝐴)) ↔ (𝑤(-g‘𝐺)(𝑘 · 𝐴)) = (𝑃 · 𝐶)) | 
| 75 |  | eqcom 2743 | . . . . . . 7
⊢ (𝑤 = ((𝑃 · 𝐶)(+g‘𝐺)(𝑘 · 𝐴)) ↔ ((𝑃 · 𝐶)(+g‘𝐺)(𝑘 · 𝐴)) = 𝑤) | 
| 76 | 73, 74, 75 | 3bitr4g 314 | . . . . . 6
⊢ (((𝜑 ∧ 𝑘 ∈ ℤ) ∧ 𝑤 ∈ 𝑊) → ((𝑃 · 𝐶) = (𝑤(-g‘𝐺)(𝑘 · 𝐴)) ↔ 𝑤 = ((𝑃 · 𝐶)(+g‘𝐺)(𝑘 · 𝐴)))) | 
| 77 | 76 | rexbidva 3176 | . . . . 5
⊢ ((𝜑 ∧ 𝑘 ∈ ℤ) → (∃𝑤 ∈ 𝑊 (𝑃 · 𝐶) = (𝑤(-g‘𝐺)(𝑘 · 𝐴)) ↔ ∃𝑤 ∈ 𝑊 𝑤 = ((𝑃 · 𝐶)(+g‘𝐺)(𝑘 · 𝐴)))) | 
| 78 |  | risset 3232 | . . . . 5
⊢ (((𝑃 · 𝐶)(+g‘𝐺)(𝑘 · 𝐴)) ∈ 𝑊 ↔ ∃𝑤 ∈ 𝑊 𝑤 = ((𝑃 · 𝐶)(+g‘𝐺)(𝑘 · 𝐴))) | 
| 79 | 77, 78 | bitr4di 289 | . . . 4
⊢ ((𝜑 ∧ 𝑘 ∈ ℤ) → (∃𝑤 ∈ 𝑊 (𝑃 · 𝐶) = (𝑤(-g‘𝐺)(𝑘 · 𝐴)) ↔ ((𝑃 · 𝐶)(+g‘𝐺)(𝑘 · 𝐴)) ∈ 𝑊)) | 
| 80 | 79 | rexbidva 3176 | . . 3
⊢ (𝜑 → (∃𝑘 ∈ ℤ ∃𝑤 ∈ 𝑊 (𝑃 · 𝐶) = (𝑤(-g‘𝐺)(𝑘 · 𝐴)) ↔ ∃𝑘 ∈ ℤ ((𝑃 · 𝐶)(+g‘𝐺)(𝑘 · 𝐴)) ∈ 𝑊)) | 
| 81 | 53, 80 | mpbid 232 | . 2
⊢ (𝜑 → ∃𝑘 ∈ ℤ ((𝑃 · 𝐶)(+g‘𝐺)(𝑘 · 𝐴)) ∈ 𝑊) | 
| 82 | 8 | adantr 480 | . . 3
⊢ ((𝜑 ∧ (𝑘 ∈ ℤ ∧ ((𝑃 · 𝐶)(+g‘𝐺)(𝑘 · 𝐴)) ∈ 𝑊)) → 𝑃 pGrp 𝐺) | 
| 83 | 9 | adantr 480 | . . 3
⊢ ((𝜑 ∧ (𝑘 ∈ ℤ ∧ ((𝑃 · 𝐶)(+g‘𝐺)(𝑘 · 𝐴)) ∈ 𝑊)) → 𝐺 ∈ Abel) | 
| 84 | 10 | adantr 480 | . . 3
⊢ ((𝜑 ∧ (𝑘 ∈ ℤ ∧ ((𝑃 · 𝐶)(+g‘𝐺)(𝑘 · 𝐴)) ∈ 𝑊)) → 𝐵 ∈ Fin) | 
| 85 | 11 | adantr 480 | . . 3
⊢ ((𝜑 ∧ (𝑘 ∈ ℤ ∧ ((𝑃 · 𝐶)(+g‘𝐺)(𝑘 · 𝐴)) ∈ 𝑊)) → (𝑂‘𝐴) = 𝐸) | 
| 86 | 12 | adantr 480 | . . 3
⊢ ((𝜑 ∧ (𝑘 ∈ ℤ ∧ ((𝑃 · 𝐶)(+g‘𝐺)(𝑘 · 𝐴)) ∈ 𝑊)) → 𝑈 ∈ (SubGrp‘𝐺)) | 
| 87 | 13 | adantr 480 | . . 3
⊢ ((𝜑 ∧ (𝑘 ∈ ℤ ∧ ((𝑃 · 𝐶)(+g‘𝐺)(𝑘 · 𝐴)) ∈ 𝑊)) → 𝐴 ∈ 𝑈) | 
| 88 | 14 | adantr 480 | . . 3
⊢ ((𝜑 ∧ (𝑘 ∈ ℤ ∧ ((𝑃 · 𝐶)(+g‘𝐺)(𝑘 · 𝐴)) ∈ 𝑊)) → 𝑊 ∈ (SubGrp‘𝐺)) | 
| 89 | 15 | adantr 480 | . . 3
⊢ ((𝜑 ∧ (𝑘 ∈ ℤ ∧ ((𝑃 · 𝐶)(+g‘𝐺)(𝑘 · 𝐴)) ∈ 𝑊)) → (𝑆 ∩ 𝑊) = { 0 }) | 
| 90 | 16 | adantr 480 | . . 3
⊢ ((𝜑 ∧ (𝑘 ∈ ℤ ∧ ((𝑃 · 𝐶)(+g‘𝐺)(𝑘 · 𝐴)) ∈ 𝑊)) → (𝑆 ⊕ 𝑊) ⊆ 𝑈) | 
| 91 | 17 | adantr 480 | . . 3
⊢ ((𝜑 ∧ (𝑘 ∈ ℤ ∧ ((𝑃 · 𝐶)(+g‘𝐺)(𝑘 · 𝐴)) ∈ 𝑊)) → ∀𝑤 ∈ (SubGrp‘𝐺)((𝑤 ⊊ 𝑈 ∧ 𝐴 ∈ 𝑤) → ¬ (𝑆 ⊕ 𝑊) ⊊ 𝑤)) | 
| 92 | 18 | adantr 480 | . . 3
⊢ ((𝜑 ∧ (𝑘 ∈ ℤ ∧ ((𝑃 · 𝐶)(+g‘𝐺)(𝑘 · 𝐴)) ∈ 𝑊)) → 𝐶 ∈ (𝑈 ∖ (𝑆 ⊕ 𝑊))) | 
| 93 |  | simprl 770 | . . 3
⊢ ((𝜑 ∧ (𝑘 ∈ ℤ ∧ ((𝑃 · 𝐶)(+g‘𝐺)(𝑘 · 𝐴)) ∈ 𝑊)) → 𝑘 ∈ ℤ) | 
| 94 |  | simprr 772 | . . 3
⊢ ((𝜑 ∧ (𝑘 ∈ ℤ ∧ ((𝑃 · 𝐶)(+g‘𝐺)(𝑘 · 𝐴)) ∈ 𝑊)) → ((𝑃 · 𝐶)(+g‘𝐺)(𝑘 · 𝐴)) ∈ 𝑊) | 
| 95 |  | eqid 2736 | . . 3
⊢ (𝐶(+g‘𝐺)((𝑘 / 𝑃) · 𝐴)) = (𝐶(+g‘𝐺)((𝑘 / 𝑃) · 𝐴)) | 
| 96 | 1, 2, 3, 4, 5, 6, 7, 82, 83, 84, 85, 86, 87, 88, 89, 90, 91, 92, 19, 93, 94, 95 | pgpfac1lem3 20098 | . 2
⊢ ((𝜑 ∧ (𝑘 ∈ ℤ ∧ ((𝑃 · 𝐶)(+g‘𝐺)(𝑘 · 𝐴)) ∈ 𝑊)) → ∃𝑡 ∈ (SubGrp‘𝐺)((𝑆 ∩ 𝑡) = { 0 } ∧ (𝑆 ⊕ 𝑡) = 𝑈)) | 
| 97 | 81, 96 | rexlimddv 3160 | 1
⊢ (𝜑 → ∃𝑡 ∈ (SubGrp‘𝐺)((𝑆 ∩ 𝑡) = { 0 } ∧ (𝑆 ⊕ 𝑡) = 𝑈)) |