Metamath Proof Explorer

Theorem pgpfac1lem3

Description: Lemma for pgpfac1 . (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.u ⊢ ( 𝜑 → 𝑈 ∈ ( SubGrp ‘ 𝐺 ) )
pgpfac1.au ⊢ ( 𝜑 → 𝐴 ∈ 𝑈 )
pgpfac1.w ⊢ ( 𝜑 → 𝑊 ∈ ( SubGrp ‘ 𝐺 ) )
pgpfac1.i ⊢ ( 𝜑 → ( 𝑆 ∩ 𝑊 ) = { 0 } )
pgpfac1.ss ⊢ ( 𝜑 → ( 𝑆 ⊕ 𝑊 ) ⊆ 𝑈 )
pgpfac1.2 ⊢ ( 𝜑 → ∀ 𝑤 ∈ ( SubGrp ‘ 𝐺 ) ( ( 𝑤 ⊊ 𝑈 ∧ 𝐴 ∈ 𝑤 ) → ¬ ( 𝑆 ⊕ 𝑊 ) ⊊ 𝑤 ) )
pgpfac1.c ⊢ ( 𝜑 → 𝐶 ∈ ( 𝑈 ∖ ( 𝑆 ⊕ 𝑊 ) ) )
pgpfac1.mg ⊢ · = ( .g ‘ 𝐺 )
pgpfac1.m ⊢ ( 𝜑 → 𝑀 ∈ ℤ )
pgpfac1.mw ⊢ ( 𝜑 → ( ( 𝑃 · 𝐶 ) ( +g ‘ 𝐺 ) ( 𝑀 · 𝐴 ) ) ∈ 𝑊 )
pgpfac1.d ⊢ 𝐷 = ( 𝐶 ( +g ‘ 𝐺 ) ( ( 𝑀 / 𝑃 ) · 𝐴 ) )
Assertion pgpfac1lem3 ( 𝜑 → ∃ 𝑡 ∈ ( 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.u ⊢ ( 𝜑 → 𝑈 ∈ ( SubGrp ‘ 𝐺 ) )
13 pgpfac1.au ⊢ ( 𝜑 → 𝐴 ∈ 𝑈 )
14 pgpfac1.w ⊢ ( 𝜑 → 𝑊 ∈ ( SubGrp ‘ 𝐺 ) )
15 pgpfac1.i ⊢ ( 𝜑 → ( 𝑆 ∩ 𝑊 ) = { 0 } )
16 pgpfac1.ss ⊢ ( 𝜑 → ( 𝑆 ⊕ 𝑊 ) ⊆ 𝑈 )
17 pgpfac1.2 ⊢ ( 𝜑 → ∀ 𝑤 ∈ ( SubGrp ‘ 𝐺 ) ( ( 𝑤 ⊊ 𝑈 ∧ 𝐴 ∈ 𝑤 ) → ¬ ( 𝑆 ⊕ 𝑊 ) ⊊ 𝑤 ) )
18 pgpfac1.c ⊢ ( 𝜑 → 𝐶 ∈ ( 𝑈 ∖ ( 𝑆 ⊕ 𝑊 ) ) )
19 pgpfac1.mg ⊢ · = ( .g ‘ 𝐺 )
20 pgpfac1.m ⊢ ( 𝜑 → 𝑀 ∈ ℤ )
21 pgpfac1.mw ⊢ ( 𝜑 → ( ( 𝑃 · 𝐶 ) ( +g ‘ 𝐺 ) ( 𝑀 · 𝐴 ) ) ∈ 𝑊 )
22 pgpfac1.d ⊢ 𝐷 = ( 𝐶 ( +g ‘ 𝐺 ) ( ( 𝑀 / 𝑃 ) · 𝐴 ) )
23 ablgrp ⊢ ( 𝐺 ∈ Abel → 𝐺 ∈ Grp )
24 9 23 syl ⊢ ( 𝜑 → 𝐺 ∈ Grp )
25 3 subgacs ⊢ ( 𝐺 ∈ Grp → ( SubGrp ‘ 𝐺 ) ∈ ( ACS ‘ 𝐵 ) )
26 acsmre ⊢ ( ( SubGrp ‘ 𝐺 ) ∈ ( ACS ‘ 𝐵 ) → ( SubGrp ‘ 𝐺 ) ∈ ( Moore ‘ 𝐵 ) )
27 24 25 26 3syl ⊢ ( 𝜑 → ( SubGrp ‘ 𝐺 ) ∈ ( Moore ‘ 𝐵 ) )
28 3 subgss ⊢ ( 𝑈 ∈ ( SubGrp ‘ 𝐺 ) → 𝑈 ⊆ 𝐵 )
29 12 28 syl ⊢ ( 𝜑 → 𝑈 ⊆ 𝐵 )
30 18 eldifad ⊢ ( 𝜑 → 𝐶 ∈ 𝑈 )
31 29 13 sseldd ⊢ ( 𝜑 → 𝐴 ∈ 𝐵 )
32 1 mrcsncl ⊢ ( ( ( SubGrp ‘ 𝐺 ) ∈ ( Moore ‘ 𝐵 ) ∧ 𝐴 ∈ 𝐵 ) → ( 𝐾 ‘ { 𝐴 } ) ∈ ( SubGrp ‘ 𝐺 ) )
33 27 31 32 syl2anc ⊢ ( 𝜑 → ( 𝐾 ‘ { 𝐴 } ) ∈ ( SubGrp ‘ 𝐺 ) )
34 2 33 eqeltrid ⊢ ( 𝜑 → 𝑆 ∈ ( SubGrp ‘ 𝐺 ) )
35 7 lsmub1 ⊢ ( ( 𝑆 ∈ ( SubGrp ‘ 𝐺 ) ∧ 𝑊 ∈ ( SubGrp ‘ 𝐺 ) ) → 𝑆 ⊆ ( 𝑆 ⊕ 𝑊 ) )
36 34 14 35 syl2anc ⊢ ( 𝜑 → 𝑆 ⊆ ( 𝑆 ⊕ 𝑊 ) )
37 36 16 sstrd ⊢ ( 𝜑 → 𝑆 ⊆ 𝑈 )
38 1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 19 20 21 pgpfac1lem3a ⊢ ( 𝜑 → ( 𝑃 ∥ 𝐸 ∧ 𝑃 ∥ 𝑀 ) )
39 38 simprd ⊢ ( 𝜑 → 𝑃 ∥ 𝑀 )
40 pgpprm ⊢ ( 𝑃 pGrp 𝐺 → 𝑃 ∈ ℙ )
41 8 40 syl ⊢ ( 𝜑 → 𝑃 ∈ ℙ )
42 prmz ⊢ ( 𝑃 ∈ ℙ → 𝑃 ∈ ℤ )
43 41 42 syl ⊢ ( 𝜑 → 𝑃 ∈ ℤ )
44 prmnn ⊢ ( 𝑃 ∈ ℙ → 𝑃 ∈ ℕ )
45 41 44 syl ⊢ ( 𝜑 → 𝑃 ∈ ℕ )
46 45 nnne0d ⊢ ( 𝜑 → 𝑃 ≠ 0 )
47 dvdsval2 ⊢ ( ( 𝑃 ∈ ℤ ∧ 𝑃 ≠ 0 ∧ 𝑀 ∈ ℤ ) → ( 𝑃 ∥ 𝑀 ↔ ( 𝑀 / 𝑃 ) ∈ ℤ ) )
48 43 46 20 47 syl3anc ⊢ ( 𝜑 → ( 𝑃 ∥ 𝑀 ↔ ( 𝑀 / 𝑃 ) ∈ ℤ ) )
49 39 48 mpbid ⊢ ( 𝜑 → ( 𝑀 / 𝑃 ) ∈ ℤ )
50 31 snssd ⊢ ( 𝜑 → { 𝐴 } ⊆ 𝐵 )
51 27 1 50 mrcssidd ⊢ ( 𝜑 → { 𝐴 } ⊆ ( 𝐾 ‘ { 𝐴 } ) )
52 51 2 sseqtrrdi ⊢ ( 𝜑 → { 𝐴 } ⊆ 𝑆 )
53 snssg ⊢ ( 𝐴 ∈ 𝑈 → ( 𝐴 ∈ 𝑆 ↔ { 𝐴 } ⊆ 𝑆 ) )
54 13 53 syl ⊢ ( 𝜑 → ( 𝐴 ∈ 𝑆 ↔ { 𝐴 } ⊆ 𝑆 ) )
55 52 54 mpbird ⊢ ( 𝜑 → 𝐴 ∈ 𝑆 )
56 19 subgmulgcl ⊢ ( ( 𝑆 ∈ ( SubGrp ‘ 𝐺 ) ∧ ( 𝑀 / 𝑃 ) ∈ ℤ ∧ 𝐴 ∈ 𝑆 ) → ( ( 𝑀 / 𝑃 ) · 𝐴 ) ∈ 𝑆 )
57 34 49 55 56 syl3anc ⊢ ( 𝜑 → ( ( 𝑀 / 𝑃 ) · 𝐴 ) ∈ 𝑆 )
58 37 57 sseldd ⊢ ( 𝜑 → ( ( 𝑀 / 𝑃 ) · 𝐴 ) ∈ 𝑈 )
59 eqid ⊢ ( +g ‘ 𝐺 ) = ( +g ‘ 𝐺 )
60 59 subgcl ⊢ ( ( 𝑈 ∈ ( SubGrp ‘ 𝐺 ) ∧ 𝐶 ∈ 𝑈 ∧ ( ( 𝑀 / 𝑃 ) · 𝐴 ) ∈ 𝑈 ) → ( 𝐶 ( +g ‘ 𝐺 ) ( ( 𝑀 / 𝑃 ) · 𝐴 ) ) ∈ 𝑈 )
61 12 30 58 60 syl3anc ⊢ ( 𝜑 → ( 𝐶 ( +g ‘ 𝐺 ) ( ( 𝑀 / 𝑃 ) · 𝐴 ) ) ∈ 𝑈 )
62 22 61 eqeltrid ⊢ ( 𝜑 → 𝐷 ∈ 𝑈 )
63 29 62 sseldd ⊢ ( 𝜑 → 𝐷 ∈ 𝐵 )
64 1 mrcsncl ⊢ ( ( ( SubGrp ‘ 𝐺 ) ∈ ( Moore ‘ 𝐵 ) ∧ 𝐷 ∈ 𝐵 ) → ( 𝐾 ‘ { 𝐷 } ) ∈ ( SubGrp ‘ 𝐺 ) )
65 27 63 64 syl2anc ⊢ ( 𝜑 → ( 𝐾 ‘ { 𝐷 } ) ∈ ( SubGrp ‘ 𝐺 ) )
66 7 lsmsubg2 ⊢ ( ( 𝐺 ∈ Abel ∧ 𝑊 ∈ ( SubGrp ‘ 𝐺 ) ∧ ( 𝐾 ‘ { 𝐷 } ) ∈ ( SubGrp ‘ 𝐺 ) ) → ( 𝑊 ⊕ ( 𝐾 ‘ { 𝐷 } ) ) ∈ ( SubGrp ‘ 𝐺 ) )
67 9 14 65 66 syl3anc ⊢ ( 𝜑 → ( 𝑊 ⊕ ( 𝐾 ‘ { 𝐷 } ) ) ∈ ( SubGrp ‘ 𝐺 ) )
68 eqid ⊢ ( -g ‘ 𝐺 ) = ( -g ‘ 𝐺 )
69 68 7 14 65 lsmelvalm ⊢ ( 𝜑 → ( 𝑥 ∈ ( 𝑊 ⊕ ( 𝐾 ‘ { 𝐷 } ) ) ↔ ∃ 𝑤 ∈ 𝑊 ∃ 𝑦 ∈ ( 𝐾 ‘ { 𝐷 } ) 𝑥 = ( 𝑤 ( -g ‘ 𝐺 ) 𝑦 ) ) )
70 eqid ⊢ ( 𝑛 ∈ ℤ ↦ ( 𝑛 · 𝐷 ) ) = ( 𝑛 ∈ ℤ ↦ ( 𝑛 · 𝐷 ) )
71 3 19 70 1 cycsubg2 ⊢ ( ( 𝐺 ∈ Grp ∧ 𝐷 ∈ 𝐵 ) → ( 𝐾 ‘ { 𝐷 } ) = ran ( 𝑛 ∈ ℤ ↦ ( 𝑛 · 𝐷 ) ) )
72 24 63 71 syl2anc ⊢ ( 𝜑 → ( 𝐾 ‘ { 𝐷 } ) = ran ( 𝑛 ∈ ℤ ↦ ( 𝑛 · 𝐷 ) ) )
73 72 rexeqdv ⊢ ( 𝜑 → ( ∃ 𝑦 ∈ ( 𝐾 ‘ { 𝐷 } ) 𝑥 = ( 𝑤 ( -g ‘ 𝐺 ) 𝑦 ) ↔ ∃ 𝑦 ∈ ran ( 𝑛 ∈ ℤ ↦ ( 𝑛 · 𝐷 ) ) 𝑥 = ( 𝑤 ( -g ‘ 𝐺 ) 𝑦 ) ) )
74 ovex ⊢ ( 𝑛 · 𝐷 ) ∈ V
75 74 rgenw ⊢ ∀ 𝑛 ∈ ℤ ( 𝑛 · 𝐷 ) ∈ V
76 oveq2 ⊢ ( 𝑦 = ( 𝑛 · 𝐷 ) → ( 𝑤 ( -g ‘ 𝐺 ) 𝑦 ) = ( 𝑤 ( -g ‘ 𝐺 ) ( 𝑛 · 𝐷 ) ) )
77 76 eqeq2d ⊢ ( 𝑦 = ( 𝑛 · 𝐷 ) → ( 𝑥 = ( 𝑤 ( -g ‘ 𝐺 ) 𝑦 ) ↔ 𝑥 = ( 𝑤 ( -g ‘ 𝐺 ) ( 𝑛 · 𝐷 ) ) ) )
78 70 77 rexrnmptw ⊢ ( ∀ 𝑛 ∈ ℤ ( 𝑛 · 𝐷 ) ∈ V → ( ∃ 𝑦 ∈ ran ( 𝑛 ∈ ℤ ↦ ( 𝑛 · 𝐷 ) ) 𝑥 = ( 𝑤 ( -g ‘ 𝐺 ) 𝑦 ) ↔ ∃ 𝑛 ∈ ℤ 𝑥 = ( 𝑤 ( -g ‘ 𝐺 ) ( 𝑛 · 𝐷 ) ) ) )
79 75 78 ax-mp ⊢ ( ∃ 𝑦 ∈ ran ( 𝑛 ∈ ℤ ↦ ( 𝑛 · 𝐷 ) ) 𝑥 = ( 𝑤 ( -g ‘ 𝐺 ) 𝑦 ) ↔ ∃ 𝑛 ∈ ℤ 𝑥 = ( 𝑤 ( -g ‘ 𝐺 ) ( 𝑛 · 𝐷 ) ) )
80 73 79 bitrdi ⊢ ( 𝜑 → ( ∃ 𝑦 ∈ ( 𝐾 ‘ { 𝐷 } ) 𝑥 = ( 𝑤 ( -g ‘ 𝐺 ) 𝑦 ) ↔ ∃ 𝑛 ∈ ℤ 𝑥 = ( 𝑤 ( -g ‘ 𝐺 ) ( 𝑛 · 𝐷 ) ) ) )
81 80 rexbidv ⊢ ( 𝜑 → ( ∃ 𝑤 ∈ 𝑊 ∃ 𝑦 ∈ ( 𝐾 ‘ { 𝐷 } ) 𝑥 = ( 𝑤 ( -g ‘ 𝐺 ) 𝑦 ) ↔ ∃ 𝑤 ∈ 𝑊 ∃ 𝑛 ∈ ℤ 𝑥 = ( 𝑤 ( -g ‘ 𝐺 ) ( 𝑛 · 𝐷 ) ) ) )
82 69 81 bitrd ⊢ ( 𝜑 → ( 𝑥 ∈ ( 𝑊 ⊕ ( 𝐾 ‘ { 𝐷 } ) ) ↔ ∃ 𝑤 ∈ 𝑊 ∃ 𝑛 ∈ ℤ 𝑥 = ( 𝑤 ( -g ‘ 𝐺 ) ( 𝑛 · 𝐷 ) ) ) )
83 82 adantr ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑆 ) → ( 𝑥 ∈ ( 𝑊 ⊕ ( 𝐾 ‘ { 𝐷 } ) ) ↔ ∃ 𝑤 ∈ 𝑊 ∃ 𝑛 ∈ ℤ 𝑥 = ( 𝑤 ( -g ‘ 𝐺 ) ( 𝑛 · 𝐷 ) ) ) )
84 simpr ⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝑆 ) ∧ ( 𝑤 ∈ 𝑊 ∧ 𝑛 ∈ ℤ ) ) ∧ 𝑥 = ( 𝑤 ( -g ‘ 𝐺 ) ( 𝑛 · 𝐷 ) ) ) → 𝑥 = ( 𝑤 ( -g ‘ 𝐺 ) ( 𝑛 · 𝐷 ) ) )
85 14 ad3antrrr ⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝑆 ) ∧ ( 𝑤 ∈ 𝑊 ∧ 𝑛 ∈ ℤ ) ) ∧ 𝑥 = ( 𝑤 ( -g ‘ 𝐺 ) ( 𝑛 · 𝐷 ) ) ) → 𝑊 ∈ ( SubGrp ‘ 𝐺 ) )
86 simplrl ⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝑆 ) ∧ ( 𝑤 ∈ 𝑊 ∧ 𝑛 ∈ ℤ ) ) ∧ 𝑥 = ( 𝑤 ( -g ‘ 𝐺 ) ( 𝑛 · 𝐷 ) ) ) → 𝑤 ∈ 𝑊 )
87 simplrr ⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝑆 ) ∧ ( 𝑤 ∈ 𝑊 ∧ 𝑛 ∈ ℤ ) ) ∧ 𝑥 = ( 𝑤 ( -g ‘ 𝐺 ) ( 𝑛 · 𝐷 ) ) ) → 𝑛 ∈ ℤ )
88 87 zcnd ⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝑆 ) ∧ ( 𝑤 ∈ 𝑊 ∧ 𝑛 ∈ ℤ ) ) ∧ 𝑥 = ( 𝑤 ( -g ‘ 𝐺 ) ( 𝑛 · 𝐷 ) ) ) → 𝑛 ∈ ℂ )
89 45 nncnd ⊢ ( 𝜑 → 𝑃 ∈ ℂ )
90 89 ad3antrrr ⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝑆 ) ∧ ( 𝑤 ∈ 𝑊 ∧ 𝑛 ∈ ℤ ) ) ∧ 𝑥 = ( 𝑤 ( -g ‘ 𝐺 ) ( 𝑛 · 𝐷 ) ) ) → 𝑃 ∈ ℂ )
91 46 ad3antrrr ⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝑆 ) ∧ ( 𝑤 ∈ 𝑊 ∧ 𝑛 ∈ ℤ ) ) ∧ 𝑥 = ( 𝑤 ( -g ‘ 𝐺 ) ( 𝑛 · 𝐷 ) ) ) → 𝑃 ≠ 0 )
92 88 90 91 divcan1d ⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝑆 ) ∧ ( 𝑤 ∈ 𝑊 ∧ 𝑛 ∈ ℤ ) ) ∧ 𝑥 = ( 𝑤 ( -g ‘ 𝐺 ) ( 𝑛 · 𝐷 ) ) ) → ( ( 𝑛 / 𝑃 ) · 𝑃 ) = 𝑛 )
93 92 oveq1d ⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝑆 ) ∧ ( 𝑤 ∈ 𝑊 ∧ 𝑛 ∈ ℤ ) ) ∧ 𝑥 = ( 𝑤 ( -g ‘ 𝐺 ) ( 𝑛 · 𝐷 ) ) ) → ( ( ( 𝑛 / 𝑃 ) · 𝑃 ) · 𝐷 ) = ( 𝑛 · 𝐷 ) )
94 24 ad3antrrr ⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝑆 ) ∧ ( 𝑤 ∈ 𝑊 ∧ 𝑛 ∈ ℤ ) ) ∧ 𝑥 = ( 𝑤 ( -g ‘ 𝐺 ) ( 𝑛 · 𝐷 ) ) ) → 𝐺 ∈ Grp )
95 18 eldifbd ⊢ ( 𝜑 → ¬ 𝐶 ∈ ( 𝑆 ⊕ 𝑊 ) )
96 7 lsmsubg2 ⊢ ( ( 𝐺 ∈ Abel ∧ 𝑆 ∈ ( SubGrp ‘ 𝐺 ) ∧ 𝑊 ∈ ( SubGrp ‘ 𝐺 ) ) → ( 𝑆 ⊕ 𝑊 ) ∈ ( SubGrp ‘ 𝐺 ) )
97 9 34 14 96 syl3anc ⊢ ( 𝜑 → ( 𝑆 ⊕ 𝑊 ) ∈ ( SubGrp ‘ 𝐺 ) )
98 36 57 sseldd ⊢ ( 𝜑 → ( ( 𝑀 / 𝑃 ) · 𝐴 ) ∈ ( 𝑆 ⊕ 𝑊 ) )
99 68 subgsubcl ⊢ ( ( ( 𝑆 ⊕ 𝑊 ) ∈ ( SubGrp ‘ 𝐺 ) ∧ 𝐷 ∈ ( 𝑆 ⊕ 𝑊 ) ∧ ( ( 𝑀 / 𝑃 ) · 𝐴 ) ∈ ( 𝑆 ⊕ 𝑊 ) ) → ( 𝐷 ( -g ‘ 𝐺 ) ( ( 𝑀 / 𝑃 ) · 𝐴 ) ) ∈ ( 𝑆 ⊕ 𝑊 ) )
100 99 3expia ⊢ ( ( ( 𝑆 ⊕ 𝑊 ) ∈ ( SubGrp ‘ 𝐺 ) ∧ 𝐷 ∈ ( 𝑆 ⊕ 𝑊 ) ) → ( ( ( 𝑀 / 𝑃 ) · 𝐴 ) ∈ ( 𝑆 ⊕ 𝑊 ) → ( 𝐷 ( -g ‘ 𝐺 ) ( ( 𝑀 / 𝑃 ) · 𝐴 ) ) ∈ ( 𝑆 ⊕ 𝑊 ) ) )
101 100 impancom ⊢ ( ( ( 𝑆 ⊕ 𝑊 ) ∈ ( SubGrp ‘ 𝐺 ) ∧ ( ( 𝑀 / 𝑃 ) · 𝐴 ) ∈ ( 𝑆 ⊕ 𝑊 ) ) → ( 𝐷 ∈ ( 𝑆 ⊕ 𝑊 ) → ( 𝐷 ( -g ‘ 𝐺 ) ( ( 𝑀 / 𝑃 ) · 𝐴 ) ) ∈ ( 𝑆 ⊕ 𝑊 ) ) )
102 97 98 101 syl2anc ⊢ ( 𝜑 → ( 𝐷 ∈ ( 𝑆 ⊕ 𝑊 ) → ( 𝐷 ( -g ‘ 𝐺 ) ( ( 𝑀 / 𝑃 ) · 𝐴 ) ) ∈ ( 𝑆 ⊕ 𝑊 ) ) )
103 22 oveq1i ⊢ ( 𝐷 ( -g ‘ 𝐺 ) ( ( 𝑀 / 𝑃 ) · 𝐴 ) ) = ( ( 𝐶 ( +g ‘ 𝐺 ) ( ( 𝑀 / 𝑃 ) · 𝐴 ) ) ( -g ‘ 𝐺 ) ( ( 𝑀 / 𝑃 ) · 𝐴 ) )
104 29 30 sseldd ⊢ ( 𝜑 → 𝐶 ∈ 𝐵 )
105 3 subgss ⊢ ( 𝑆 ∈ ( SubGrp ‘ 𝐺 ) → 𝑆 ⊆ 𝐵 )
106 34 105 syl ⊢ ( 𝜑 → 𝑆 ⊆ 𝐵 )
107 106 57 sseldd ⊢ ( 𝜑 → ( ( 𝑀 / 𝑃 ) · 𝐴 ) ∈ 𝐵 )
108 3 59 68 grppncan ⊢ ( ( 𝐺 ∈ Grp ∧ 𝐶 ∈ 𝐵 ∧ ( ( 𝑀 / 𝑃 ) · 𝐴 ) ∈ 𝐵 ) → ( ( 𝐶 ( +g ‘ 𝐺 ) ( ( 𝑀 / 𝑃 ) · 𝐴 ) ) ( -g ‘ 𝐺 ) ( ( 𝑀 / 𝑃 ) · 𝐴 ) ) = 𝐶 )
109 24 104 107 108 syl3anc ⊢ ( 𝜑 → ( ( 𝐶 ( +g ‘ 𝐺 ) ( ( 𝑀 / 𝑃 ) · 𝐴 ) ) ( -g ‘ 𝐺 ) ( ( 𝑀 / 𝑃 ) · 𝐴 ) ) = 𝐶 )
110 103 109 eqtrid ⊢ ( 𝜑 → ( 𝐷 ( -g ‘ 𝐺 ) ( ( 𝑀 / 𝑃 ) · 𝐴 ) ) = 𝐶 )
111 110 eleq1d ⊢ ( 𝜑 → ( ( 𝐷 ( -g ‘ 𝐺 ) ( ( 𝑀 / 𝑃 ) · 𝐴 ) ) ∈ ( 𝑆 ⊕ 𝑊 ) ↔ 𝐶 ∈ ( 𝑆 ⊕ 𝑊 ) ) )
112 102 111 sylibd ⊢ ( 𝜑 → ( 𝐷 ∈ ( 𝑆 ⊕ 𝑊 ) → 𝐶 ∈ ( 𝑆 ⊕ 𝑊 ) ) )
113 95 112 mtod ⊢ ( 𝜑 → ¬ 𝐷 ∈ ( 𝑆 ⊕ 𝑊 ) )
114 113 ad3antrrr ⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝑆 ) ∧ ( 𝑤 ∈ 𝑊 ∧ 𝑛 ∈ ℤ ) ) ∧ 𝑥 = ( 𝑤 ( -g ‘ 𝐺 ) ( 𝑛 · 𝐷 ) ) ) → ¬ 𝐷 ∈ ( 𝑆 ⊕ 𝑊 ) )
115 41 ad3antrrr ⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝑆 ) ∧ ( 𝑤 ∈ 𝑊 ∧ 𝑛 ∈ ℤ ) ) ∧ 𝑥 = ( 𝑤 ( -g ‘ 𝐺 ) ( 𝑛 · 𝐷 ) ) ) → 𝑃 ∈ ℙ )
116 coprm ⊢ ( ( 𝑃 ∈ ℙ ∧ 𝑛 ∈ ℤ ) → ( ¬ 𝑃 ∥ 𝑛 ↔ ( 𝑃 gcd 𝑛 ) = 1 ) )
117 115 87 116 syl2anc ⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝑆 ) ∧ ( 𝑤 ∈ 𝑊 ∧ 𝑛 ∈ ℤ ) ) ∧ 𝑥 = ( 𝑤 ( -g ‘ 𝐺 ) ( 𝑛 · 𝐷 ) ) ) → ( ¬ 𝑃 ∥ 𝑛 ↔ ( 𝑃 gcd 𝑛 ) = 1 ) )
118 43 ad3antrrr ⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝑆 ) ∧ ( 𝑤 ∈ 𝑊 ∧ 𝑛 ∈ ℤ ) ) ∧ 𝑥 = ( 𝑤 ( -g ‘ 𝐺 ) ( 𝑛 · 𝐷 ) ) ) → 𝑃 ∈ ℤ )
119 bezout ⊢ ( ( 𝑃 ∈ ℤ ∧ 𝑛 ∈ ℤ ) → ∃ 𝑎 ∈ ℤ ∃ 𝑏 ∈ ℤ ( 𝑃 gcd 𝑛 ) = ( ( 𝑃 · 𝑎 ) + ( 𝑛 · 𝑏 ) ) )
120 118 87 119 syl2anc ⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝑆 ) ∧ ( 𝑤 ∈ 𝑊 ∧ 𝑛 ∈ ℤ ) ) ∧ 𝑥 = ( 𝑤 ( -g ‘ 𝐺 ) ( 𝑛 · 𝐷 ) ) ) → ∃ 𝑎 ∈ ℤ ∃ 𝑏 ∈ ℤ ( 𝑃 gcd 𝑛 ) = ( ( 𝑃 · 𝑎 ) + ( 𝑛 · 𝑏 ) ) )
121 eqeq1 ⊢ ( ( 𝑃 gcd 𝑛 ) = 1 → ( ( 𝑃 gcd 𝑛 ) = ( ( 𝑃 · 𝑎 ) + ( 𝑛 · 𝑏 ) ) ↔ 1 = ( ( 𝑃 · 𝑎 ) + ( 𝑛 · 𝑏 ) ) ) )
122 121 2rexbidv ⊢ ( ( 𝑃 gcd 𝑛 ) = 1 → ( ∃ 𝑎 ∈ ℤ ∃ 𝑏 ∈ ℤ ( 𝑃 gcd 𝑛 ) = ( ( 𝑃 · 𝑎 ) + ( 𝑛 · 𝑏 ) ) ↔ ∃ 𝑎 ∈ ℤ ∃ 𝑏 ∈ ℤ 1 = ( ( 𝑃 · 𝑎 ) + ( 𝑛 · 𝑏 ) ) ) )
123 120 122 syl5ibcom ⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝑆 ) ∧ ( 𝑤 ∈ 𝑊 ∧ 𝑛 ∈ ℤ ) ) ∧ 𝑥 = ( 𝑤 ( -g ‘ 𝐺 ) ( 𝑛 · 𝐷 ) ) ) → ( ( 𝑃 gcd 𝑛 ) = 1 → ∃ 𝑎 ∈ ℤ ∃ 𝑏 ∈ ℤ 1 = ( ( 𝑃 · 𝑎 ) + ( 𝑛 · 𝑏 ) ) ) )
124 94 adantr ⊢ ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝑆 ) ∧ ( 𝑤 ∈ 𝑊 ∧ 𝑛 ∈ ℤ ) ) ∧ 𝑥 = ( 𝑤 ( -g ‘ 𝐺 ) ( 𝑛 · 𝐷 ) ) ) ∧ ( 𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ ) ) → 𝐺 ∈ Grp )
125 118 adantr ⊢ ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝑆 ) ∧ ( 𝑤 ∈ 𝑊 ∧ 𝑛 ∈ ℤ ) ) ∧ 𝑥 = ( 𝑤 ( -g ‘ 𝐺 ) ( 𝑛 · 𝐷 ) ) ) ∧ ( 𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ ) ) → 𝑃 ∈ ℤ )
126 simprl ⊢ ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝑆 ) ∧ ( 𝑤 ∈ 𝑊 ∧ 𝑛 ∈ ℤ ) ) ∧ 𝑥 = ( 𝑤 ( -g ‘ 𝐺 ) ( 𝑛 · 𝐷 ) ) ) ∧ ( 𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ ) ) → 𝑎 ∈ ℤ )
127 125 126 zmulcld ⊢ ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝑆 ) ∧ ( 𝑤 ∈ 𝑊 ∧ 𝑛 ∈ ℤ ) ) ∧ 𝑥 = ( 𝑤 ( -g ‘ 𝐺 ) ( 𝑛 · 𝐷 ) ) ) ∧ ( 𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ ) ) → ( 𝑃 · 𝑎 ) ∈ ℤ )
128 87 adantr ⊢ ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝑆 ) ∧ ( 𝑤 ∈ 𝑊 ∧ 𝑛 ∈ ℤ ) ) ∧ 𝑥 = ( 𝑤 ( -g ‘ 𝐺 ) ( 𝑛 · 𝐷 ) ) ) ∧ ( 𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ ) ) → 𝑛 ∈ ℤ )
129 simprr ⊢ ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝑆 ) ∧ ( 𝑤 ∈ 𝑊 ∧ 𝑛 ∈ ℤ ) ) ∧ 𝑥 = ( 𝑤 ( -g ‘ 𝐺 ) ( 𝑛 · 𝐷 ) ) ) ∧ ( 𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ ) ) → 𝑏 ∈ ℤ )
130 128 129 zmulcld ⊢ ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝑆 ) ∧ ( 𝑤 ∈ 𝑊 ∧ 𝑛 ∈ ℤ ) ) ∧ 𝑥 = ( 𝑤 ( -g ‘ 𝐺 ) ( 𝑛 · 𝐷 ) ) ) ∧ ( 𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ ) ) → ( 𝑛 · 𝑏 ) ∈ ℤ )
131 63 ad3antrrr ⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝑆 ) ∧ ( 𝑤 ∈ 𝑊 ∧ 𝑛 ∈ ℤ ) ) ∧ 𝑥 = ( 𝑤 ( -g ‘ 𝐺 ) ( 𝑛 · 𝐷 ) ) ) → 𝐷 ∈ 𝐵 )
132 131 adantr ⊢ ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝑆 ) ∧ ( 𝑤 ∈ 𝑊 ∧ 𝑛 ∈ ℤ ) ) ∧ 𝑥 = ( 𝑤 ( -g ‘ 𝐺 ) ( 𝑛 · 𝐷 ) ) ) ∧ ( 𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ ) ) → 𝐷 ∈ 𝐵 )
133 3 19 59 mulgdir ⊢ ( ( 𝐺 ∈ Grp ∧ ( ( 𝑃 · 𝑎 ) ∈ ℤ ∧ ( 𝑛 · 𝑏 ) ∈ ℤ ∧ 𝐷 ∈ 𝐵 ) ) → ( ( ( 𝑃 · 𝑎 ) + ( 𝑛 · 𝑏 ) ) · 𝐷 ) = ( ( ( 𝑃 · 𝑎 ) · 𝐷 ) ( +g ‘ 𝐺 ) ( ( 𝑛 · 𝑏 ) · 𝐷 ) ) )
134 124 127 130 132 133 syl13anc ⊢ ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝑆 ) ∧ ( 𝑤 ∈ 𝑊 ∧ 𝑛 ∈ ℤ ) ) ∧ 𝑥 = ( 𝑤 ( -g ‘ 𝐺 ) ( 𝑛 · 𝐷 ) ) ) ∧ ( 𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ ) ) → ( ( ( 𝑃 · 𝑎 ) + ( 𝑛 · 𝑏 ) ) · 𝐷 ) = ( ( ( 𝑃 · 𝑎 ) · 𝐷 ) ( +g ‘ 𝐺 ) ( ( 𝑛 · 𝑏 ) · 𝐷 ) ) )
135 97 ad3antrrr ⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝑆 ) ∧ ( 𝑤 ∈ 𝑊 ∧ 𝑛 ∈ ℤ ) ) ∧ 𝑥 = ( 𝑤 ( -g ‘ 𝐺 ) ( 𝑛 · 𝐷 ) ) ) → ( 𝑆 ⊕ 𝑊 ) ∈ ( SubGrp ‘ 𝐺 ) )
136 135 adantr ⊢ ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝑆 ) ∧ ( 𝑤 ∈ 𝑊 ∧ 𝑛 ∈ ℤ ) ) ∧ 𝑥 = ( 𝑤 ( -g ‘ 𝐺 ) ( 𝑛 · 𝐷 ) ) ) ∧ ( 𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ ) ) → ( 𝑆 ⊕ 𝑊 ) ∈ ( SubGrp ‘ 𝐺 ) )
137 90 adantr ⊢ ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝑆 ) ∧ ( 𝑤 ∈ 𝑊 ∧ 𝑛 ∈ ℤ ) ) ∧ 𝑥 = ( 𝑤 ( -g ‘ 𝐺 ) ( 𝑛 · 𝐷 ) ) ) ∧ ( 𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ ) ) → 𝑃 ∈ ℂ )
138 zcn ⊢ ( 𝑎 ∈ ℤ → 𝑎 ∈ ℂ )
139 138 ad2antrl ⊢ ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝑆 ) ∧ ( 𝑤 ∈ 𝑊 ∧ 𝑛 ∈ ℤ ) ) ∧ 𝑥 = ( 𝑤 ( -g ‘ 𝐺 ) ( 𝑛 · 𝐷 ) ) ) ∧ ( 𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ ) ) → 𝑎 ∈ ℂ )
140 137 139 mulcomd ⊢ ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝑆 ) ∧ ( 𝑤 ∈ 𝑊 ∧ 𝑛 ∈ ℤ ) ) ∧ 𝑥 = ( 𝑤 ( -g ‘ 𝐺 ) ( 𝑛 · 𝐷 ) ) ) ∧ ( 𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ ) ) → ( 𝑃 · 𝑎 ) = ( 𝑎 · 𝑃 ) )
141 140 oveq1d ⊢ ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝑆 ) ∧ ( 𝑤 ∈ 𝑊 ∧ 𝑛 ∈ ℤ ) ) ∧ 𝑥 = ( 𝑤 ( -g ‘ 𝐺 ) ( 𝑛 · 𝐷 ) ) ) ∧ ( 𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ ) ) → ( ( 𝑃 · 𝑎 ) · 𝐷 ) = ( ( 𝑎 · 𝑃 ) · 𝐷 ) )
142 3 19 mulgass ⊢ ( ( 𝐺 ∈ Grp ∧ ( 𝑎 ∈ ℤ ∧ 𝑃 ∈ ℤ ∧ 𝐷 ∈ 𝐵 ) ) → ( ( 𝑎 · 𝑃 ) · 𝐷 ) = ( 𝑎 · ( 𝑃 · 𝐷 ) ) )
143 124 126 125 132 142 syl13anc ⊢ ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝑆 ) ∧ ( 𝑤 ∈ 𝑊 ∧ 𝑛 ∈ ℤ ) ) ∧ 𝑥 = ( 𝑤 ( -g ‘ 𝐺 ) ( 𝑛 · 𝐷 ) ) ) ∧ ( 𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ ) ) → ( ( 𝑎 · 𝑃 ) · 𝐷 ) = ( 𝑎 · ( 𝑃 · 𝐷 ) ) )
144 141 143 eqtrd ⊢ ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝑆 ) ∧ ( 𝑤 ∈ 𝑊 ∧ 𝑛 ∈ ℤ ) ) ∧ 𝑥 = ( 𝑤 ( -g ‘ 𝐺 ) ( 𝑛 · 𝐷 ) ) ) ∧ ( 𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ ) ) → ( ( 𝑃 · 𝑎 ) · 𝐷 ) = ( 𝑎 · ( 𝑃 · 𝐷 ) ) )
145 7 lsmub2 ⊢ ( ( 𝑆 ∈ ( SubGrp ‘ 𝐺 ) ∧ 𝑊 ∈ ( SubGrp ‘ 𝐺 ) ) → 𝑊 ⊆ ( 𝑆 ⊕ 𝑊 ) )
146 34 14 145 syl2anc ⊢ ( 𝜑 → 𝑊 ⊆ ( 𝑆 ⊕ 𝑊 ) )
147 22 oveq2i ⊢ ( 𝑃 · 𝐷 ) = ( 𝑃 · ( 𝐶 ( +g ‘ 𝐺 ) ( ( 𝑀 / 𝑃 ) · 𝐴 ) ) )
148 3 19 59 mulgdi ⊢ ( ( 𝐺 ∈ Abel ∧ ( 𝑃 ∈ ℤ ∧ 𝐶 ∈ 𝐵 ∧ ( ( 𝑀 / 𝑃 ) · 𝐴 ) ∈ 𝐵 ) ) → ( 𝑃 · ( 𝐶 ( +g ‘ 𝐺 ) ( ( 𝑀 / 𝑃 ) · 𝐴 ) ) ) = ( ( 𝑃 · 𝐶 ) ( +g ‘ 𝐺 ) ( 𝑃 · ( ( 𝑀 / 𝑃 ) · 𝐴 ) ) ) )
149 9 43 104 107 148 syl13anc ⊢ ( 𝜑 → ( 𝑃 · ( 𝐶 ( +g ‘ 𝐺 ) ( ( 𝑀 / 𝑃 ) · 𝐴 ) ) ) = ( ( 𝑃 · 𝐶 ) ( +g ‘ 𝐺 ) ( 𝑃 · ( ( 𝑀 / 𝑃 ) · 𝐴 ) ) ) )
150 147 149 eqtrid ⊢ ( 𝜑 → ( 𝑃 · 𝐷 ) = ( ( 𝑃 · 𝐶 ) ( +g ‘ 𝐺 ) ( 𝑃 · ( ( 𝑀 / 𝑃 ) · 𝐴 ) ) ) )
151 3 19 mulgass ⊢ ( ( 𝐺 ∈ Grp ∧ ( 𝑃 ∈ ℤ ∧ ( 𝑀 / 𝑃 ) ∈ ℤ ∧ 𝐴 ∈ 𝐵 ) ) → ( ( 𝑃 · ( 𝑀 / 𝑃 ) ) · 𝐴 ) = ( 𝑃 · ( ( 𝑀 / 𝑃 ) · 𝐴 ) ) )
152 24 43 49 31 151 syl13anc ⊢ ( 𝜑 → ( ( 𝑃 · ( 𝑀 / 𝑃 ) ) · 𝐴 ) = ( 𝑃 · ( ( 𝑀 / 𝑃 ) · 𝐴 ) ) )
153 20 zcnd ⊢ ( 𝜑 → 𝑀 ∈ ℂ )
154 153 89 46 divcan2d ⊢ ( 𝜑 → ( 𝑃 · ( 𝑀 / 𝑃 ) ) = 𝑀 )
155 154 oveq1d ⊢ ( 𝜑 → ( ( 𝑃 · ( 𝑀 / 𝑃 ) ) · 𝐴 ) = ( 𝑀 · 𝐴 ) )
156 152 155 eqtr3d ⊢ ( 𝜑 → ( 𝑃 · ( ( 𝑀 / 𝑃 ) · 𝐴 ) ) = ( 𝑀 · 𝐴 ) )
157 156 oveq2d ⊢ ( 𝜑 → ( ( 𝑃 · 𝐶 ) ( +g ‘ 𝐺 ) ( 𝑃 · ( ( 𝑀 / 𝑃 ) · 𝐴 ) ) ) = ( ( 𝑃 · 𝐶 ) ( +g ‘ 𝐺 ) ( 𝑀 · 𝐴 ) ) )
158 150 157 eqtrd ⊢ ( 𝜑 → ( 𝑃 · 𝐷 ) = ( ( 𝑃 · 𝐶 ) ( +g ‘ 𝐺 ) ( 𝑀 · 𝐴 ) ) )
159 158 21 eqeltrd ⊢ ( 𝜑 → ( 𝑃 · 𝐷 ) ∈ 𝑊 )
160 146 159 sseldd ⊢ ( 𝜑 → ( 𝑃 · 𝐷 ) ∈ ( 𝑆 ⊕ 𝑊 ) )
161 160 ad3antrrr ⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝑆 ) ∧ ( 𝑤 ∈ 𝑊 ∧ 𝑛 ∈ ℤ ) ) ∧ 𝑥 = ( 𝑤 ( -g ‘ 𝐺 ) ( 𝑛 · 𝐷 ) ) ) → ( 𝑃 · 𝐷 ) ∈ ( 𝑆 ⊕ 𝑊 ) )
162 161 adantr ⊢ ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝑆 ) ∧ ( 𝑤 ∈ 𝑊 ∧ 𝑛 ∈ ℤ ) ) ∧ 𝑥 = ( 𝑤 ( -g ‘ 𝐺 ) ( 𝑛 · 𝐷 ) ) ) ∧ ( 𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ ) ) → ( 𝑃 · 𝐷 ) ∈ ( 𝑆 ⊕ 𝑊 ) )
163 19 subgmulgcl ⊢ ( ( ( 𝑆 ⊕ 𝑊 ) ∈ ( SubGrp ‘ 𝐺 ) ∧ 𝑎 ∈ ℤ ∧ ( 𝑃 · 𝐷 ) ∈ ( 𝑆 ⊕ 𝑊 ) ) → ( 𝑎 · ( 𝑃 · 𝐷 ) ) ∈ ( 𝑆 ⊕ 𝑊 ) )
164 136 126 162 163 syl3anc ⊢ ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝑆 ) ∧ ( 𝑤 ∈ 𝑊 ∧ 𝑛 ∈ ℤ ) ) ∧ 𝑥 = ( 𝑤 ( -g ‘ 𝐺 ) ( 𝑛 · 𝐷 ) ) ) ∧ ( 𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ ) ) → ( 𝑎 · ( 𝑃 · 𝐷 ) ) ∈ ( 𝑆 ⊕ 𝑊 ) )
165 144 164 eqeltrd ⊢ ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝑆 ) ∧ ( 𝑤 ∈ 𝑊 ∧ 𝑛 ∈ ℤ ) ) ∧ 𝑥 = ( 𝑤 ( -g ‘ 𝐺 ) ( 𝑛 · 𝐷 ) ) ) ∧ ( 𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ ) ) → ( ( 𝑃 · 𝑎 ) · 𝐷 ) ∈ ( 𝑆 ⊕ 𝑊 ) )
166 88 adantr ⊢ ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝑆 ) ∧ ( 𝑤 ∈ 𝑊 ∧ 𝑛 ∈ ℤ ) ) ∧ 𝑥 = ( 𝑤 ( -g ‘ 𝐺 ) ( 𝑛 · 𝐷 ) ) ) ∧ ( 𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ ) ) → 𝑛 ∈ ℂ )
167 zcn ⊢ ( 𝑏 ∈ ℤ → 𝑏 ∈ ℂ )
168 167 ad2antll ⊢ ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝑆 ) ∧ ( 𝑤 ∈ 𝑊 ∧ 𝑛 ∈ ℤ ) ) ∧ 𝑥 = ( 𝑤 ( -g ‘ 𝐺 ) ( 𝑛 · 𝐷 ) ) ) ∧ ( 𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ ) ) → 𝑏 ∈ ℂ )
169 166 168 mulcomd ⊢ ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝑆 ) ∧ ( 𝑤 ∈ 𝑊 ∧ 𝑛 ∈ ℤ ) ) ∧ 𝑥 = ( 𝑤 ( -g ‘ 𝐺 ) ( 𝑛 · 𝐷 ) ) ) ∧ ( 𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ ) ) → ( 𝑛 · 𝑏 ) = ( 𝑏 · 𝑛 ) )
170 169 oveq1d ⊢ ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝑆 ) ∧ ( 𝑤 ∈ 𝑊 ∧ 𝑛 ∈ ℤ ) ) ∧ 𝑥 = ( 𝑤 ( -g ‘ 𝐺 ) ( 𝑛 · 𝐷 ) ) ) ∧ ( 𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ ) ) → ( ( 𝑛 · 𝑏 ) · 𝐷 ) = ( ( 𝑏 · 𝑛 ) · 𝐷 ) )
171 3 19 mulgass ⊢ ( ( 𝐺 ∈ Grp ∧ ( 𝑏 ∈ ℤ ∧ 𝑛 ∈ ℤ ∧ 𝐷 ∈ 𝐵 ) ) → ( ( 𝑏 · 𝑛 ) · 𝐷 ) = ( 𝑏 · ( 𝑛 · 𝐷 ) ) )
172 124 129 128 132 171 syl13anc ⊢ ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝑆 ) ∧ ( 𝑤 ∈ 𝑊 ∧ 𝑛 ∈ ℤ ) ) ∧ 𝑥 = ( 𝑤 ( -g ‘ 𝐺 ) ( 𝑛 · 𝐷 ) ) ) ∧ ( 𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ ) ) → ( ( 𝑏 · 𝑛 ) · 𝐷 ) = ( 𝑏 · ( 𝑛 · 𝐷 ) ) )
173 170 172 eqtrd ⊢ ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝑆 ) ∧ ( 𝑤 ∈ 𝑊 ∧ 𝑛 ∈ ℤ ) ) ∧ 𝑥 = ( 𝑤 ( -g ‘ 𝐺 ) ( 𝑛 · 𝐷 ) ) ) ∧ ( 𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ ) ) → ( ( 𝑛 · 𝑏 ) · 𝐷 ) = ( 𝑏 · ( 𝑛 · 𝐷 ) ) )
174 84 oveq2d ⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝑆 ) ∧ ( 𝑤 ∈ 𝑊 ∧ 𝑛 ∈ ℤ ) ) ∧ 𝑥 = ( 𝑤 ( -g ‘ 𝐺 ) ( 𝑛 · 𝐷 ) ) ) → ( 𝑤 ( -g ‘ 𝐺 ) 𝑥 ) = ( 𝑤 ( -g ‘ 𝐺 ) ( 𝑤 ( -g ‘ 𝐺 ) ( 𝑛 · 𝐷 ) ) ) )
175 9 ad3antrrr ⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝑆 ) ∧ ( 𝑤 ∈ 𝑊 ∧ 𝑛 ∈ ℤ ) ) ∧ 𝑥 = ( 𝑤 ( -g ‘ 𝐺 ) ( 𝑛 · 𝐷 ) ) ) → 𝐺 ∈ Abel )
176 3 subgss ⊢ ( 𝑊 ∈ ( SubGrp ‘ 𝐺 ) → 𝑊 ⊆ 𝐵 )
177 85 176 syl ⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝑆 ) ∧ ( 𝑤 ∈ 𝑊 ∧ 𝑛 ∈ ℤ ) ) ∧ 𝑥 = ( 𝑤 ( -g ‘ 𝐺 ) ( 𝑛 · 𝐷 ) ) ) → 𝑊 ⊆ 𝐵 )
178 177 86 sseldd ⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝑆 ) ∧ ( 𝑤 ∈ 𝑊 ∧ 𝑛 ∈ ℤ ) ) ∧ 𝑥 = ( 𝑤 ( -g ‘ 𝐺 ) ( 𝑛 · 𝐷 ) ) ) → 𝑤 ∈ 𝐵 )
179 3 19 mulgcl ⊢ ( ( 𝐺 ∈ Grp ∧ 𝑛 ∈ ℤ ∧ 𝐷 ∈ 𝐵 ) → ( 𝑛 · 𝐷 ) ∈ 𝐵 )
180 94 87 131 179 syl3anc ⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝑆 ) ∧ ( 𝑤 ∈ 𝑊 ∧ 𝑛 ∈ ℤ ) ) ∧ 𝑥 = ( 𝑤 ( -g ‘ 𝐺 ) ( 𝑛 · 𝐷 ) ) ) → ( 𝑛 · 𝐷 ) ∈ 𝐵 )
181 3 68 175 178 180 ablnncan ⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝑆 ) ∧ ( 𝑤 ∈ 𝑊 ∧ 𝑛 ∈ ℤ ) ) ∧ 𝑥 = ( 𝑤 ( -g ‘ 𝐺 ) ( 𝑛 · 𝐷 ) ) ) → ( 𝑤 ( -g ‘ 𝐺 ) ( 𝑤 ( -g ‘ 𝐺 ) ( 𝑛 · 𝐷 ) ) ) = ( 𝑛 · 𝐷 ) )
182 174 181 eqtrd ⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝑆 ) ∧ ( 𝑤 ∈ 𝑊 ∧ 𝑛 ∈ ℤ ) ) ∧ 𝑥 = ( 𝑤 ( -g ‘ 𝐺 ) ( 𝑛 · 𝐷 ) ) ) → ( 𝑤 ( -g ‘ 𝐺 ) 𝑥 ) = ( 𝑛 · 𝐷 ) )
183 146 ad3antrrr ⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝑆 ) ∧ ( 𝑤 ∈ 𝑊 ∧ 𝑛 ∈ ℤ ) ) ∧ 𝑥 = ( 𝑤 ( -g ‘ 𝐺 ) ( 𝑛 · 𝐷 ) ) ) → 𝑊 ⊆ ( 𝑆 ⊕ 𝑊 ) )
184 183 86 sseldd ⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝑆 ) ∧ ( 𝑤 ∈ 𝑊 ∧ 𝑛 ∈ ℤ ) ) ∧ 𝑥 = ( 𝑤 ( -g ‘ 𝐺 ) ( 𝑛 · 𝐷 ) ) ) → 𝑤 ∈ ( 𝑆 ⊕ 𝑊 ) )
185 36 sselda ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑆 ) → 𝑥 ∈ ( 𝑆 ⊕ 𝑊 ) )
186 185 ad2antrr ⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝑆 ) ∧ ( 𝑤 ∈ 𝑊 ∧ 𝑛 ∈ ℤ ) ) ∧ 𝑥 = ( 𝑤 ( -g ‘ 𝐺 ) ( 𝑛 · 𝐷 ) ) ) → 𝑥 ∈ ( 𝑆 ⊕ 𝑊 ) )
187 68 subgsubcl ⊢ ( ( ( 𝑆 ⊕ 𝑊 ) ∈ ( SubGrp ‘ 𝐺 ) ∧ 𝑤 ∈ ( 𝑆 ⊕ 𝑊 ) ∧ 𝑥 ∈ ( 𝑆 ⊕ 𝑊 ) ) → ( 𝑤 ( -g ‘ 𝐺 ) 𝑥 ) ∈ ( 𝑆 ⊕ 𝑊 ) )
188 135 184 186 187 syl3anc ⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝑆 ) ∧ ( 𝑤 ∈ 𝑊 ∧ 𝑛 ∈ ℤ ) ) ∧ 𝑥 = ( 𝑤 ( -g ‘ 𝐺 ) ( 𝑛 · 𝐷 ) ) ) → ( 𝑤 ( -g ‘ 𝐺 ) 𝑥 ) ∈ ( 𝑆 ⊕ 𝑊 ) )
189 182 188 eqeltrrd ⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝑆 ) ∧ ( 𝑤 ∈ 𝑊 ∧ 𝑛 ∈ ℤ ) ) ∧ 𝑥 = ( 𝑤 ( -g ‘ 𝐺 ) ( 𝑛 · 𝐷 ) ) ) → ( 𝑛 · 𝐷 ) ∈ ( 𝑆 ⊕ 𝑊 ) )
190 189 adantr ⊢ ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝑆 ) ∧ ( 𝑤 ∈ 𝑊 ∧ 𝑛 ∈ ℤ ) ) ∧ 𝑥 = ( 𝑤 ( -g ‘ 𝐺 ) ( 𝑛 · 𝐷 ) ) ) ∧ ( 𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ ) ) → ( 𝑛 · 𝐷 ) ∈ ( 𝑆 ⊕ 𝑊 ) )
191 19 subgmulgcl ⊢ ( ( ( 𝑆 ⊕ 𝑊 ) ∈ ( SubGrp ‘ 𝐺 ) ∧ 𝑏 ∈ ℤ ∧ ( 𝑛 · 𝐷 ) ∈ ( 𝑆 ⊕ 𝑊 ) ) → ( 𝑏 · ( 𝑛 · 𝐷 ) ) ∈ ( 𝑆 ⊕ 𝑊 ) )
192 136 129 190 191 syl3anc ⊢ ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝑆 ) ∧ ( 𝑤 ∈ 𝑊 ∧ 𝑛 ∈ ℤ ) ) ∧ 𝑥 = ( 𝑤 ( -g ‘ 𝐺 ) ( 𝑛 · 𝐷 ) ) ) ∧ ( 𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ ) ) → ( 𝑏 · ( 𝑛 · 𝐷 ) ) ∈ ( 𝑆 ⊕ 𝑊 ) )
193 173 192 eqeltrd ⊢ ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝑆 ) ∧ ( 𝑤 ∈ 𝑊 ∧ 𝑛 ∈ ℤ ) ) ∧ 𝑥 = ( 𝑤 ( -g ‘ 𝐺 ) ( 𝑛 · 𝐷 ) ) ) ∧ ( 𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ ) ) → ( ( 𝑛 · 𝑏 ) · 𝐷 ) ∈ ( 𝑆 ⊕ 𝑊 ) )
194 59 subgcl ⊢ ( ( ( 𝑆 ⊕ 𝑊 ) ∈ ( SubGrp ‘ 𝐺 ) ∧ ( ( 𝑃 · 𝑎 ) · 𝐷 ) ∈ ( 𝑆 ⊕ 𝑊 ) ∧ ( ( 𝑛 · 𝑏 ) · 𝐷 ) ∈ ( 𝑆 ⊕ 𝑊 ) ) → ( ( ( 𝑃 · 𝑎 ) · 𝐷 ) ( +g ‘ 𝐺 ) ( ( 𝑛 · 𝑏 ) · 𝐷 ) ) ∈ ( 𝑆 ⊕ 𝑊 ) )
195 136 165 193 194 syl3anc ⊢ ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝑆 ) ∧ ( 𝑤 ∈ 𝑊 ∧ 𝑛 ∈ ℤ ) ) ∧ 𝑥 = ( 𝑤 ( -g ‘ 𝐺 ) ( 𝑛 · 𝐷 ) ) ) ∧ ( 𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ ) ) → ( ( ( 𝑃 · 𝑎 ) · 𝐷 ) ( +g ‘ 𝐺 ) ( ( 𝑛 · 𝑏 ) · 𝐷 ) ) ∈ ( 𝑆 ⊕ 𝑊 ) )
196 134 195 eqeltrd ⊢ ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝑆 ) ∧ ( 𝑤 ∈ 𝑊 ∧ 𝑛 ∈ ℤ ) ) ∧ 𝑥 = ( 𝑤 ( -g ‘ 𝐺 ) ( 𝑛 · 𝐷 ) ) ) ∧ ( 𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ ) ) → ( ( ( 𝑃 · 𝑎 ) + ( 𝑛 · 𝑏 ) ) · 𝐷 ) ∈ ( 𝑆 ⊕ 𝑊 ) )
197 oveq1 ⊢ ( 1 = ( ( 𝑃 · 𝑎 ) + ( 𝑛 · 𝑏 ) ) → ( 1 · 𝐷 ) = ( ( ( 𝑃 · 𝑎 ) + ( 𝑛 · 𝑏 ) ) · 𝐷 ) )
198 197 eleq1d ⊢ ( 1 = ( ( 𝑃 · 𝑎 ) + ( 𝑛 · 𝑏 ) ) → ( ( 1 · 𝐷 ) ∈ ( 𝑆 ⊕ 𝑊 ) ↔ ( ( ( 𝑃 · 𝑎 ) + ( 𝑛 · 𝑏 ) ) · 𝐷 ) ∈ ( 𝑆 ⊕ 𝑊 ) ) )
199 196 198 syl5ibrcom ⊢ ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝑆 ) ∧ ( 𝑤 ∈ 𝑊 ∧ 𝑛 ∈ ℤ ) ) ∧ 𝑥 = ( 𝑤 ( -g ‘ 𝐺 ) ( 𝑛 · 𝐷 ) ) ) ∧ ( 𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ ) ) → ( 1 = ( ( 𝑃 · 𝑎 ) + ( 𝑛 · 𝑏 ) ) → ( 1 · 𝐷 ) ∈ ( 𝑆 ⊕ 𝑊 ) ) )
200 199 rexlimdvva ⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝑆 ) ∧ ( 𝑤 ∈ 𝑊 ∧ 𝑛 ∈ ℤ ) ) ∧ 𝑥 = ( 𝑤 ( -g ‘ 𝐺 ) ( 𝑛 · 𝐷 ) ) ) → ( ∃ 𝑎 ∈ ℤ ∃ 𝑏 ∈ ℤ 1 = ( ( 𝑃 · 𝑎 ) + ( 𝑛 · 𝑏 ) ) → ( 1 · 𝐷 ) ∈ ( 𝑆 ⊕ 𝑊 ) ) )
201 123 200 syld ⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝑆 ) ∧ ( 𝑤 ∈ 𝑊 ∧ 𝑛 ∈ ℤ ) ) ∧ 𝑥 = ( 𝑤 ( -g ‘ 𝐺 ) ( 𝑛 · 𝐷 ) ) ) → ( ( 𝑃 gcd 𝑛 ) = 1 → ( 1 · 𝐷 ) ∈ ( 𝑆 ⊕ 𝑊 ) ) )
202 3 19 mulg1 ⊢ ( 𝐷 ∈ 𝐵 → ( 1 · 𝐷 ) = 𝐷 )
203 131 202 syl ⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝑆 ) ∧ ( 𝑤 ∈ 𝑊 ∧ 𝑛 ∈ ℤ ) ) ∧ 𝑥 = ( 𝑤 ( -g ‘ 𝐺 ) ( 𝑛 · 𝐷 ) ) ) → ( 1 · 𝐷 ) = 𝐷 )
204 203 eleq1d ⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝑆 ) ∧ ( 𝑤 ∈ 𝑊 ∧ 𝑛 ∈ ℤ ) ) ∧ 𝑥 = ( 𝑤 ( -g ‘ 𝐺 ) ( 𝑛 · 𝐷 ) ) ) → ( ( 1 · 𝐷 ) ∈ ( 𝑆 ⊕ 𝑊 ) ↔ 𝐷 ∈ ( 𝑆 ⊕ 𝑊 ) ) )
205 201 204 sylibd ⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝑆 ) ∧ ( 𝑤 ∈ 𝑊 ∧ 𝑛 ∈ ℤ ) ) ∧ 𝑥 = ( 𝑤 ( -g ‘ 𝐺 ) ( 𝑛 · 𝐷 ) ) ) → ( ( 𝑃 gcd 𝑛 ) = 1 → 𝐷 ∈ ( 𝑆 ⊕ 𝑊 ) ) )
206 117 205 sylbid ⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝑆 ) ∧ ( 𝑤 ∈ 𝑊 ∧ 𝑛 ∈ ℤ ) ) ∧ 𝑥 = ( 𝑤 ( -g ‘ 𝐺 ) ( 𝑛 · 𝐷 ) ) ) → ( ¬ 𝑃 ∥ 𝑛 → 𝐷 ∈ ( 𝑆 ⊕ 𝑊 ) ) )
207 114 206 mt3d ⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝑆 ) ∧ ( 𝑤 ∈ 𝑊 ∧ 𝑛 ∈ ℤ ) ) ∧ 𝑥 = ( 𝑤 ( -g ‘ 𝐺 ) ( 𝑛 · 𝐷 ) ) ) → 𝑃 ∥ 𝑛 )
208 dvdsval2 ⊢ ( ( 𝑃 ∈ ℤ ∧ 𝑃 ≠ 0 ∧ 𝑛 ∈ ℤ ) → ( 𝑃 ∥ 𝑛 ↔ ( 𝑛 / 𝑃 ) ∈ ℤ ) )
209 118 91 87 208 syl3anc ⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝑆 ) ∧ ( 𝑤 ∈ 𝑊 ∧ 𝑛 ∈ ℤ ) ) ∧ 𝑥 = ( 𝑤 ( -g ‘ 𝐺 ) ( 𝑛 · 𝐷 ) ) ) → ( 𝑃 ∥ 𝑛 ↔ ( 𝑛 / 𝑃 ) ∈ ℤ ) )
210 207 209 mpbid ⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝑆 ) ∧ ( 𝑤 ∈ 𝑊 ∧ 𝑛 ∈ ℤ ) ) ∧ 𝑥 = ( 𝑤 ( -g ‘ 𝐺 ) ( 𝑛 · 𝐷 ) ) ) → ( 𝑛 / 𝑃 ) ∈ ℤ )
211 3 19 mulgass ⊢ ( ( 𝐺 ∈ Grp ∧ ( ( 𝑛 / 𝑃 ) ∈ ℤ ∧ 𝑃 ∈ ℤ ∧ 𝐷 ∈ 𝐵 ) ) → ( ( ( 𝑛 / 𝑃 ) · 𝑃 ) · 𝐷 ) = ( ( 𝑛 / 𝑃 ) · ( 𝑃 · 𝐷 ) ) )
212 94 210 118 131 211 syl13anc ⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝑆 ) ∧ ( 𝑤 ∈ 𝑊 ∧ 𝑛 ∈ ℤ ) ) ∧ 𝑥 = ( 𝑤 ( -g ‘ 𝐺 ) ( 𝑛 · 𝐷 ) ) ) → ( ( ( 𝑛 / 𝑃 ) · 𝑃 ) · 𝐷 ) = ( ( 𝑛 / 𝑃 ) · ( 𝑃 · 𝐷 ) ) )
213 93 212 eqtr3d ⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝑆 ) ∧ ( 𝑤 ∈ 𝑊 ∧ 𝑛 ∈ ℤ ) ) ∧ 𝑥 = ( 𝑤 ( -g ‘ 𝐺 ) ( 𝑛 · 𝐷 ) ) ) → ( 𝑛 · 𝐷 ) = ( ( 𝑛 / 𝑃 ) · ( 𝑃 · 𝐷 ) ) )
214 159 ad3antrrr ⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝑆 ) ∧ ( 𝑤 ∈ 𝑊 ∧ 𝑛 ∈ ℤ ) ) ∧ 𝑥 = ( 𝑤 ( -g ‘ 𝐺 ) ( 𝑛 · 𝐷 ) ) ) → ( 𝑃 · 𝐷 ) ∈ 𝑊 )
215 19 subgmulgcl ⊢ ( ( 𝑊 ∈ ( SubGrp ‘ 𝐺 ) ∧ ( 𝑛 / 𝑃 ) ∈ ℤ ∧ ( 𝑃 · 𝐷 ) ∈ 𝑊 ) → ( ( 𝑛 / 𝑃 ) · ( 𝑃 · 𝐷 ) ) ∈ 𝑊 )
216 85 210 214 215 syl3anc ⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝑆 ) ∧ ( 𝑤 ∈ 𝑊 ∧ 𝑛 ∈ ℤ ) ) ∧ 𝑥 = ( 𝑤 ( -g ‘ 𝐺 ) ( 𝑛 · 𝐷 ) ) ) → ( ( 𝑛 / 𝑃 ) · ( 𝑃 · 𝐷 ) ) ∈ 𝑊 )
217 213 216 eqeltrd ⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝑆 ) ∧ ( 𝑤 ∈ 𝑊 ∧ 𝑛 ∈ ℤ ) ) ∧ 𝑥 = ( 𝑤 ( -g ‘ 𝐺 ) ( 𝑛 · 𝐷 ) ) ) → ( 𝑛 · 𝐷 ) ∈ 𝑊 )
218 68 subgsubcl ⊢ ( ( 𝑊 ∈ ( SubGrp ‘ 𝐺 ) ∧ 𝑤 ∈ 𝑊 ∧ ( 𝑛 · 𝐷 ) ∈ 𝑊 ) → ( 𝑤 ( -g ‘ 𝐺 ) ( 𝑛 · 𝐷 ) ) ∈ 𝑊 )
219 85 86 217 218 syl3anc ⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝑆 ) ∧ ( 𝑤 ∈ 𝑊 ∧ 𝑛 ∈ ℤ ) ) ∧ 𝑥 = ( 𝑤 ( -g ‘ 𝐺 ) ( 𝑛 · 𝐷 ) ) ) → ( 𝑤 ( -g ‘ 𝐺 ) ( 𝑛 · 𝐷 ) ) ∈ 𝑊 )
220 84 219 eqeltrd ⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝑆 ) ∧ ( 𝑤 ∈ 𝑊 ∧ 𝑛 ∈ ℤ ) ) ∧ 𝑥 = ( 𝑤 ( -g ‘ 𝐺 ) ( 𝑛 · 𝐷 ) ) ) → 𝑥 ∈ 𝑊 )
221 220 ex ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ 𝑆 ) ∧ ( 𝑤 ∈ 𝑊 ∧ 𝑛 ∈ ℤ ) ) → ( 𝑥 = ( 𝑤 ( -g ‘ 𝐺 ) ( 𝑛 · 𝐷 ) ) → 𝑥 ∈ 𝑊 ) )
222 221 rexlimdvva ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑆 ) → ( ∃ 𝑤 ∈ 𝑊 ∃ 𝑛 ∈ ℤ 𝑥 = ( 𝑤 ( -g ‘ 𝐺 ) ( 𝑛 · 𝐷 ) ) → 𝑥 ∈ 𝑊 ) )
223 83 222 sylbid ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑆 ) → ( 𝑥 ∈ ( 𝑊 ⊕ ( 𝐾 ‘ { 𝐷 } ) ) → 𝑥 ∈ 𝑊 ) )
224 223 imdistanda ⊢ ( 𝜑 → ( ( 𝑥 ∈ 𝑆 ∧ 𝑥 ∈ ( 𝑊 ⊕ ( 𝐾 ‘ { 𝐷 } ) ) ) → ( 𝑥 ∈ 𝑆 ∧ 𝑥 ∈ 𝑊 ) ) )
225 elin ⊢ ( 𝑥 ∈ ( 𝑆 ∩ ( 𝑊 ⊕ ( 𝐾 ‘ { 𝐷 } ) ) ) ↔ ( 𝑥 ∈ 𝑆 ∧ 𝑥 ∈ ( 𝑊 ⊕ ( 𝐾 ‘ { 𝐷 } ) ) ) )
226 elin ⊢ ( 𝑥 ∈ ( 𝑆 ∩ 𝑊 ) ↔ ( 𝑥 ∈ 𝑆 ∧ 𝑥 ∈ 𝑊 ) )
227 224 225 226 3imtr4g ⊢ ( 𝜑 → ( 𝑥 ∈ ( 𝑆 ∩ ( 𝑊 ⊕ ( 𝐾 ‘ { 𝐷 } ) ) ) → 𝑥 ∈ ( 𝑆 ∩ 𝑊 ) ) )
228 227 ssrdv ⊢ ( 𝜑 → ( 𝑆 ∩ ( 𝑊 ⊕ ( 𝐾 ‘ { 𝐷 } ) ) ) ⊆ ( 𝑆 ∩ 𝑊 ) )
229 228 15 sseqtrd ⊢ ( 𝜑 → ( 𝑆 ∩ ( 𝑊 ⊕ ( 𝐾 ‘ { 𝐷 } ) ) ) ⊆ { 0 } )
230 6 subg0cl ⊢ ( 𝑆 ∈ ( SubGrp ‘ 𝐺 ) → 0 ∈ 𝑆 )
231 34 230 syl ⊢ ( 𝜑 → 0 ∈ 𝑆 )
232 6 subg0cl ⊢ ( ( 𝑊 ⊕ ( 𝐾 ‘ { 𝐷 } ) ) ∈ ( SubGrp ‘ 𝐺 ) → 0 ∈ ( 𝑊 ⊕ ( 𝐾 ‘ { 𝐷 } ) ) )
233 67 232 syl ⊢ ( 𝜑 → 0 ∈ ( 𝑊 ⊕ ( 𝐾 ‘ { 𝐷 } ) ) )
234 231 233 elind ⊢ ( 𝜑 → 0 ∈ ( 𝑆 ∩ ( 𝑊 ⊕ ( 𝐾 ‘ { 𝐷 } ) ) ) )
235 234 snssd ⊢ ( 𝜑 → { 0 } ⊆ ( 𝑆 ∩ ( 𝑊 ⊕ ( 𝐾 ‘ { 𝐷 } ) ) ) )
236 229 235 eqssd ⊢ ( 𝜑 → ( 𝑆 ∩ ( 𝑊 ⊕ ( 𝐾 ‘ { 𝐷 } ) ) ) = { 0 } )
237 7 lsmass ⊢ ( ( 𝑆 ∈ ( SubGrp ‘ 𝐺 ) ∧ 𝑊 ∈ ( SubGrp ‘ 𝐺 ) ∧ ( 𝐾 ‘ { 𝐷 } ) ∈ ( SubGrp ‘ 𝐺 ) ) → ( ( 𝑆 ⊕ 𝑊 ) ⊕ ( 𝐾 ‘ { 𝐷 } ) ) = ( 𝑆 ⊕ ( 𝑊 ⊕ ( 𝐾 ‘ { 𝐷 } ) ) ) )
238 34 14 65 237 syl3anc ⊢ ( 𝜑 → ( ( 𝑆 ⊕ 𝑊 ) ⊕ ( 𝐾 ‘ { 𝐷 } ) ) = ( 𝑆 ⊕ ( 𝑊 ⊕ ( 𝐾 ‘ { 𝐷 } ) ) ) )
239 62 113 eldifd ⊢ ( 𝜑 → 𝐷 ∈ ( 𝑈 ∖ ( 𝑆 ⊕ 𝑊 ) ) )
240 1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 pgpfac1lem1 ⊢ ( ( 𝜑 ∧ 𝐷 ∈ ( 𝑈 ∖ ( 𝑆 ⊕ 𝑊 ) ) ) → ( ( 𝑆 ⊕ 𝑊 ) ⊕ ( 𝐾 ‘ { 𝐷 } ) ) = 𝑈 )
241 239 240 mpdan ⊢ ( 𝜑 → ( ( 𝑆 ⊕ 𝑊 ) ⊕ ( 𝐾 ‘ { 𝐷 } ) ) = 𝑈 )
242 238 241 eqtr3d ⊢ ( 𝜑 → ( 𝑆 ⊕ ( 𝑊 ⊕ ( 𝐾 ‘ { 𝐷 } ) ) ) = 𝑈 )
243 ineq2 ⊢ ( 𝑡 = ( 𝑊 ⊕ ( 𝐾 ‘ { 𝐷 } ) ) → ( 𝑆 ∩ 𝑡 ) = ( 𝑆 ∩ ( 𝑊 ⊕ ( 𝐾 ‘ { 𝐷 } ) ) ) )
244 243 eqeq1d ⊢ ( 𝑡 = ( 𝑊 ⊕ ( 𝐾 ‘ { 𝐷 } ) ) → ( ( 𝑆 ∩ 𝑡 ) = { 0 } ↔ ( 𝑆 ∩ ( 𝑊 ⊕ ( 𝐾 ‘ { 𝐷 } ) ) ) = { 0 } ) )
245 oveq2 ⊢ ( 𝑡 = ( 𝑊 ⊕ ( 𝐾 ‘ { 𝐷 } ) ) → ( 𝑆 ⊕ 𝑡 ) = ( 𝑆 ⊕ ( 𝑊 ⊕ ( 𝐾 ‘ { 𝐷 } ) ) ) )
246 245 eqeq1d ⊢ ( 𝑡 = ( 𝑊 ⊕ ( 𝐾 ‘ { 𝐷 } ) ) → ( ( 𝑆 ⊕ 𝑡 ) = 𝑈 ↔ ( 𝑆 ⊕ ( 𝑊 ⊕ ( 𝐾 ‘ { 𝐷 } ) ) ) = 𝑈 ) )
247 244 246 anbi12d ⊢ ( 𝑡 = ( 𝑊 ⊕ ( 𝐾 ‘ { 𝐷 } ) ) → ( ( ( 𝑆 ∩ 𝑡 ) = { 0 } ∧ ( 𝑆 ⊕ 𝑡 ) = 𝑈 ) ↔ ( ( 𝑆 ∩ ( 𝑊 ⊕ ( 𝐾 ‘ { 𝐷 } ) ) ) = { 0 } ∧ ( 𝑆 ⊕ ( 𝑊 ⊕ ( 𝐾 ‘ { 𝐷 } ) ) ) = 𝑈 ) ) )
248 247 rspcev ⊢ ( ( ( 𝑊 ⊕ ( 𝐾 ‘ { 𝐷 } ) ) ∈ ( SubGrp ‘ 𝐺 ) ∧ ( ( 𝑆 ∩ ( 𝑊 ⊕ ( 𝐾 ‘ { 𝐷 } ) ) ) = { 0 } ∧ ( 𝑆 ⊕ ( 𝑊 ⊕ ( 𝐾 ‘ { 𝐷 } ) ) ) = 𝑈 ) ) → ∃ 𝑡 ∈ ( SubGrp ‘ 𝐺 ) ( ( 𝑆 ∩ 𝑡 ) = { 0 } ∧ ( 𝑆 ⊕ 𝑡 ) = 𝑈 ) )
249 67 236 242 248 syl12anc ⊢ ( 𝜑 → ∃ 𝑡 ∈ ( SubGrp ‘ 𝐺 ) ( ( 𝑆 ∩ 𝑡 ) = { 0 } ∧ ( 𝑆 ⊕ 𝑡 ) = 𝑈 ) )