Metamath Proof Explorer

Theorem pgpfac1lem3a

Description: Lemma for pgpfac1 . (Contributed by Mario Carneiro, 4-Jun-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 ‘ 𝐺 ) ( 𝑀 · 𝐴 ) ) ∈ 𝑊 )
Assertion pgpfac1lem3a ( 𝜑 → ( 𝑃 ∥ 𝐸 ∧ 𝑃 ∥ 𝑀 ) )

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 18 eldifbd ⊢ ( 𝜑 → ¬ 𝐶 ∈ ( 𝑆 ⊕ 𝑊 ) )
23 pgpprm ⊢ ( 𝑃 pGrp 𝐺 → 𝑃 ∈ ℙ )
24 8 23 syl ⊢ ( 𝜑 → 𝑃 ∈ ℙ )
25 ablgrp ⊢ ( 𝐺 ∈ Abel → 𝐺 ∈ Grp )
26 9 25 syl ⊢ ( 𝜑 → 𝐺 ∈ Grp )
27 3 5 gexcl2 ⊢ ( ( 𝐺 ∈ Grp ∧ 𝐵 ∈ Fin ) → 𝐸 ∈ ℕ )
28 26 10 27 syl2anc ⊢ ( 𝜑 → 𝐸 ∈ ℕ )
29 pceq0 ⊢ ( ( 𝑃 ∈ ℙ ∧ 𝐸 ∈ ℕ ) → ( ( 𝑃 pCnt 𝐸 ) = 0 ↔ ¬ 𝑃 ∥ 𝐸 ) )
30 24 28 29 syl2anc ⊢ ( 𝜑 → ( ( 𝑃 pCnt 𝐸 ) = 0 ↔ ¬ 𝑃 ∥ 𝐸 ) )
31 oveq2 ⊢ ( ( 𝑃 pCnt 𝐸 ) = 0 → ( 𝑃 ↑ ( 𝑃 pCnt 𝐸 ) ) = ( 𝑃 ↑ 0 ) )
32 30 31 biimtrrdi ⊢ ( 𝜑 → ( ¬ 𝑃 ∥ 𝐸 → ( 𝑃 ↑ ( 𝑃 pCnt 𝐸 ) ) = ( 𝑃 ↑ 0 ) ) )
33 3 grpbn0 ⊢ ( 𝐺 ∈ Grp → 𝐵 ≠ ∅ )
34 26 33 syl ⊢ ( 𝜑 → 𝐵 ≠ ∅ )
35 hashnncl ⊢ ( 𝐵 ∈ Fin → ( ( ♯ ‘ 𝐵 ) ∈ ℕ ↔ 𝐵 ≠ ∅ ) )
36 10 35 syl ⊢ ( 𝜑 → ( ( ♯ ‘ 𝐵 ) ∈ ℕ ↔ 𝐵 ≠ ∅ ) )
37 34 36 mpbird ⊢ ( 𝜑 → ( ♯ ‘ 𝐵 ) ∈ ℕ )
38 24 37 pccld ⊢ ( 𝜑 → ( 𝑃 pCnt ( ♯ ‘ 𝐵 ) ) ∈ ℕ0 )
39 3 5 gexdvds3 ⊢ ( ( 𝐺 ∈ Grp ∧ 𝐵 ∈ Fin ) → 𝐸 ∥ ( ♯ ‘ 𝐵 ) )
40 26 10 39 syl2anc ⊢ ( 𝜑 → 𝐸 ∥ ( ♯ ‘ 𝐵 ) )
41 3 pgphash ⊢ ( ( 𝑃 pGrp 𝐺 ∧ 𝐵 ∈ Fin ) → ( ♯ ‘ 𝐵 ) = ( 𝑃 ↑ ( 𝑃 pCnt ( ♯ ‘ 𝐵 ) ) ) )
42 8 10 41 syl2anc ⊢ ( 𝜑 → ( ♯ ‘ 𝐵 ) = ( 𝑃 ↑ ( 𝑃 pCnt ( ♯ ‘ 𝐵 ) ) ) )
43 40 42 breqtrd ⊢ ( 𝜑 → 𝐸 ∥ ( 𝑃 ↑ ( 𝑃 pCnt ( ♯ ‘ 𝐵 ) ) ) )
44 oveq2 ⊢ ( 𝑘 = ( 𝑃 pCnt ( ♯ ‘ 𝐵 ) ) → ( 𝑃 ↑ 𝑘 ) = ( 𝑃 ↑ ( 𝑃 pCnt ( ♯ ‘ 𝐵 ) ) ) )
45 44 breq2d ⊢ ( 𝑘 = ( 𝑃 pCnt ( ♯ ‘ 𝐵 ) ) → ( 𝐸 ∥ ( 𝑃 ↑ 𝑘 ) ↔ 𝐸 ∥ ( 𝑃 ↑ ( 𝑃 pCnt ( ♯ ‘ 𝐵 ) ) ) ) )
46 45 rspcev ⊢ ( ( ( 𝑃 pCnt ( ♯ ‘ 𝐵 ) ) ∈ ℕ0 ∧ 𝐸 ∥ ( 𝑃 ↑ ( 𝑃 pCnt ( ♯ ‘ 𝐵 ) ) ) ) → ∃ 𝑘 ∈ ℕ0 𝐸 ∥ ( 𝑃 ↑ 𝑘 ) )
47 38 43 46 syl2anc ⊢ ( 𝜑 → ∃ 𝑘 ∈ ℕ0 𝐸 ∥ ( 𝑃 ↑ 𝑘 ) )
48 pcprmpw2 ⊢ ( ( 𝑃 ∈ ℙ ∧ 𝐸 ∈ ℕ ) → ( ∃ 𝑘 ∈ ℕ0 𝐸 ∥ ( 𝑃 ↑ 𝑘 ) ↔ 𝐸 = ( 𝑃 ↑ ( 𝑃 pCnt 𝐸 ) ) ) )
49 24 28 48 syl2anc ⊢ ( 𝜑 → ( ∃ 𝑘 ∈ ℕ0 𝐸 ∥ ( 𝑃 ↑ 𝑘 ) ↔ 𝐸 = ( 𝑃 ↑ ( 𝑃 pCnt 𝐸 ) ) ) )
50 47 49 mpbid ⊢ ( 𝜑 → 𝐸 = ( 𝑃 ↑ ( 𝑃 pCnt 𝐸 ) ) )
51 50 eqcomd ⊢ ( 𝜑 → ( 𝑃 ↑ ( 𝑃 pCnt 𝐸 ) ) = 𝐸 )
52 prmnn ⊢ ( 𝑃 ∈ ℙ → 𝑃 ∈ ℕ )
53 24 52 syl ⊢ ( 𝜑 → 𝑃 ∈ ℕ )
54 53 nncnd ⊢ ( 𝜑 → 𝑃 ∈ ℂ )
55 54 exp0d ⊢ ( 𝜑 → ( 𝑃 ↑ 0 ) = 1 )
56 51 55 eqeq12d ⊢ ( 𝜑 → ( ( 𝑃 ↑ ( 𝑃 pCnt 𝐸 ) ) = ( 𝑃 ↑ 0 ) ↔ 𝐸 = 1 ) )
57 26 grpmndd ⊢ ( 𝜑 → 𝐺 ∈ Mnd )
58 3 5 gex1 ⊢ ( 𝐺 ∈ Mnd → ( 𝐸 = 1 ↔ 𝐵 ≈ 1o ) )
59 57 58 syl ⊢ ( 𝜑 → ( 𝐸 = 1 ↔ 𝐵 ≈ 1o ) )
60 56 59 bitrd ⊢ ( 𝜑 → ( ( 𝑃 ↑ ( 𝑃 pCnt 𝐸 ) ) = ( 𝑃 ↑ 0 ) ↔ 𝐵 ≈ 1o ) )
61 32 60 sylibd ⊢ ( 𝜑 → ( ¬ 𝑃 ∥ 𝐸 → 𝐵 ≈ 1o ) )
62 3 subgacs ⊢ ( 𝐺 ∈ Grp → ( SubGrp ‘ 𝐺 ) ∈ ( ACS ‘ 𝐵 ) )
63 26 62 syl ⊢ ( 𝜑 → ( SubGrp ‘ 𝐺 ) ∈ ( ACS ‘ 𝐵 ) )
64 63 acsmred ⊢ ( 𝜑 → ( SubGrp ‘ 𝐺 ) ∈ ( Moore ‘ 𝐵 ) )
65 3 subgss ⊢ ( 𝑈 ∈ ( SubGrp ‘ 𝐺 ) → 𝑈 ⊆ 𝐵 )
66 12 65 syl ⊢ ( 𝜑 → 𝑈 ⊆ 𝐵 )
67 66 13 sseldd ⊢ ( 𝜑 → 𝐴 ∈ 𝐵 )
68 1 mrcsncl ⊢ ( ( ( SubGrp ‘ 𝐺 ) ∈ ( Moore ‘ 𝐵 ) ∧ 𝐴 ∈ 𝐵 ) → ( 𝐾 ‘ { 𝐴 } ) ∈ ( SubGrp ‘ 𝐺 ) )
69 64 67 68 syl2anc ⊢ ( 𝜑 → ( 𝐾 ‘ { 𝐴 } ) ∈ ( SubGrp ‘ 𝐺 ) )
70 2 69 eqeltrid ⊢ ( 𝜑 → 𝑆 ∈ ( SubGrp ‘ 𝐺 ) )
71 7 lsmsubg2 ⊢ ( ( 𝐺 ∈ Abel ∧ 𝑆 ∈ ( SubGrp ‘ 𝐺 ) ∧ 𝑊 ∈ ( SubGrp ‘ 𝐺 ) ) → ( 𝑆 ⊕ 𝑊 ) ∈ ( SubGrp ‘ 𝐺 ) )
72 9 70 14 71 syl3anc ⊢ ( 𝜑 → ( 𝑆 ⊕ 𝑊 ) ∈ ( SubGrp ‘ 𝐺 ) )
73 6 subg0cl ⊢ ( ( 𝑆 ⊕ 𝑊 ) ∈ ( SubGrp ‘ 𝐺 ) → 0 ∈ ( 𝑆 ⊕ 𝑊 ) )
74 72 73 syl ⊢ ( 𝜑 → 0 ∈ ( 𝑆 ⊕ 𝑊 ) )
75 74 snssd ⊢ ( 𝜑 → { 0 } ⊆ ( 𝑆 ⊕ 𝑊 ) )
76 75 adantr ⊢ ( ( 𝜑 ∧ 𝐵 ≈ 1o ) → { 0 } ⊆ ( 𝑆 ⊕ 𝑊 ) )
77 18 eldifad ⊢ ( 𝜑 → 𝐶 ∈ 𝑈 )
78 66 77 sseldd ⊢ ( 𝜑 → 𝐶 ∈ 𝐵 )
79 78 adantr ⊢ ( ( 𝜑 ∧ 𝐵 ≈ 1o ) → 𝐶 ∈ 𝐵 )
80 3 6 grpidcl ⊢ ( 𝐺 ∈ Grp → 0 ∈ 𝐵 )
81 26 80 syl ⊢ ( 𝜑 → 0 ∈ 𝐵 )
82 en1eqsn ⊢ ( ( 0 ∈ 𝐵 ∧ 𝐵 ≈ 1o ) → 𝐵 = { 0 } )
83 81 82 sylan ⊢ ( ( 𝜑 ∧ 𝐵 ≈ 1o ) → 𝐵 = { 0 } )
84 79 83 eleqtrd ⊢ ( ( 𝜑 ∧ 𝐵 ≈ 1o ) → 𝐶 ∈ { 0 } )
85 76 84 sseldd ⊢ ( ( 𝜑 ∧ 𝐵 ≈ 1o ) → 𝐶 ∈ ( 𝑆 ⊕ 𝑊 ) )
86 85 ex ⊢ ( 𝜑 → ( 𝐵 ≈ 1o → 𝐶 ∈ ( 𝑆 ⊕ 𝑊 ) ) )
87 61 86 syld ⊢ ( 𝜑 → ( ¬ 𝑃 ∥ 𝐸 → 𝐶 ∈ ( 𝑆 ⊕ 𝑊 ) ) )
88 22 87 mt3d ⊢ ( 𝜑 → 𝑃 ∥ 𝐸 )
89 28 nncnd ⊢ ( 𝜑 → 𝐸 ∈ ℂ )
90 53 nnne0d ⊢ ( 𝜑 → 𝑃 ≠ 0 )
91 89 54 90 divcan1d ⊢ ( 𝜑 → ( ( 𝐸 / 𝑃 ) · 𝑃 ) = 𝐸 )
92 11 91 eqtr4d ⊢ ( 𝜑 → ( 𝑂 ‘ 𝐴 ) = ( ( 𝐸 / 𝑃 ) · 𝑃 ) )
93 nndivdvds ⊢ ( ( 𝐸 ∈ ℕ ∧ 𝑃 ∈ ℕ ) → ( 𝑃 ∥ 𝐸 ↔ ( 𝐸 / 𝑃 ) ∈ ℕ ) )
94 28 53 93 syl2anc ⊢ ( 𝜑 → ( 𝑃 ∥ 𝐸 ↔ ( 𝐸 / 𝑃 ) ∈ ℕ ) )
95 88 94 mpbid ⊢ ( 𝜑 → ( 𝐸 / 𝑃 ) ∈ ℕ )
96 95 nnzd ⊢ ( 𝜑 → ( 𝐸 / 𝑃 ) ∈ ℤ )
97 96 20 zmulcld ⊢ ( 𝜑 → ( ( 𝐸 / 𝑃 ) · 𝑀 ) ∈ ℤ )
98 67 snssd ⊢ ( 𝜑 → { 𝐴 } ⊆ 𝐵 )
99 64 1 98 mrcssidd ⊢ ( 𝜑 → { 𝐴 } ⊆ ( 𝐾 ‘ { 𝐴 } ) )
100 99 2 sseqtrrdi ⊢ ( 𝜑 → { 𝐴 } ⊆ 𝑆 )
101 snssg ⊢ ( 𝐴 ∈ 𝑈 → ( 𝐴 ∈ 𝑆 ↔ { 𝐴 } ⊆ 𝑆 ) )
102 13 101 syl ⊢ ( 𝜑 → ( 𝐴 ∈ 𝑆 ↔ { 𝐴 } ⊆ 𝑆 ) )
103 100 102 mpbird ⊢ ( 𝜑 → 𝐴 ∈ 𝑆 )
104 19 subgmulgcl ⊢ ( ( 𝑆 ∈ ( SubGrp ‘ 𝐺 ) ∧ ( ( 𝐸 / 𝑃 ) · 𝑀 ) ∈ ℤ ∧ 𝐴 ∈ 𝑆 ) → ( ( ( 𝐸 / 𝑃 ) · 𝑀 ) · 𝐴 ) ∈ 𝑆 )
105 70 97 103 104 syl3anc ⊢ ( 𝜑 → ( ( ( 𝐸 / 𝑃 ) · 𝑀 ) · 𝐴 ) ∈ 𝑆 )
106 prmz ⊢ ( 𝑃 ∈ ℙ → 𝑃 ∈ ℤ )
107 24 106 syl ⊢ ( 𝜑 → 𝑃 ∈ ℤ )
108 3 19 mulgcl ⊢ ( ( 𝐺 ∈ Grp ∧ 𝑃 ∈ ℤ ∧ 𝐶 ∈ 𝐵 ) → ( 𝑃 · 𝐶 ) ∈ 𝐵 )
109 26 107 78 108 syl3anc ⊢ ( 𝜑 → ( 𝑃 · 𝐶 ) ∈ 𝐵 )
110 3 19 mulgcl ⊢ ( ( 𝐺 ∈ Grp ∧ 𝑀 ∈ ℤ ∧ 𝐴 ∈ 𝐵 ) → ( 𝑀 · 𝐴 ) ∈ 𝐵 )
111 26 20 67 110 syl3anc ⊢ ( 𝜑 → ( 𝑀 · 𝐴 ) ∈ 𝐵 )
112 eqid ⊢ ( +g ‘ 𝐺 ) = ( +g ‘ 𝐺 )
113 3 19 112 mulgdi ⊢ ( ( 𝐺 ∈ Abel ∧ ( ( 𝐸 / 𝑃 ) ∈ ℤ ∧ ( 𝑃 · 𝐶 ) ∈ 𝐵 ∧ ( 𝑀 · 𝐴 ) ∈ 𝐵 ) ) → ( ( 𝐸 / 𝑃 ) · ( ( 𝑃 · 𝐶 ) ( +g ‘ 𝐺 ) ( 𝑀 · 𝐴 ) ) ) = ( ( ( 𝐸 / 𝑃 ) · ( 𝑃 · 𝐶 ) ) ( +g ‘ 𝐺 ) ( ( 𝐸 / 𝑃 ) · ( 𝑀 · 𝐴 ) ) ) )
114 9 96 109 111 113 syl13anc ⊢ ( 𝜑 → ( ( 𝐸 / 𝑃 ) · ( ( 𝑃 · 𝐶 ) ( +g ‘ 𝐺 ) ( 𝑀 · 𝐴 ) ) ) = ( ( ( 𝐸 / 𝑃 ) · ( 𝑃 · 𝐶 ) ) ( +g ‘ 𝐺 ) ( ( 𝐸 / 𝑃 ) · ( 𝑀 · 𝐴 ) ) ) )
115 91 oveq1d ⊢ ( 𝜑 → ( ( ( 𝐸 / 𝑃 ) · 𝑃 ) · 𝐶 ) = ( 𝐸 · 𝐶 ) )
116 3 19 mulgass ⊢ ( ( 𝐺 ∈ Grp ∧ ( ( 𝐸 / 𝑃 ) ∈ ℤ ∧ 𝑃 ∈ ℤ ∧ 𝐶 ∈ 𝐵 ) ) → ( ( ( 𝐸 / 𝑃 ) · 𝑃 ) · 𝐶 ) = ( ( 𝐸 / 𝑃 ) · ( 𝑃 · 𝐶 ) ) )
117 26 96 107 78 116 syl13anc ⊢ ( 𝜑 → ( ( ( 𝐸 / 𝑃 ) · 𝑃 ) · 𝐶 ) = ( ( 𝐸 / 𝑃 ) · ( 𝑃 · 𝐶 ) ) )
118 3 5 19 6 gexid ⊢ ( 𝐶 ∈ 𝐵 → ( 𝐸 · 𝐶 ) = 0 )
119 78 118 syl ⊢ ( 𝜑 → ( 𝐸 · 𝐶 ) = 0 )
120 115 117 119 3eqtr3rd ⊢ ( 𝜑 → 0 = ( ( 𝐸 / 𝑃 ) · ( 𝑃 · 𝐶 ) ) )
121 3 19 mulgass ⊢ ( ( 𝐺 ∈ Grp ∧ ( ( 𝐸 / 𝑃 ) ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ 𝐴 ∈ 𝐵 ) ) → ( ( ( 𝐸 / 𝑃 ) · 𝑀 ) · 𝐴 ) = ( ( 𝐸 / 𝑃 ) · ( 𝑀 · 𝐴 ) ) )
122 26 96 20 67 121 syl13anc ⊢ ( 𝜑 → ( ( ( 𝐸 / 𝑃 ) · 𝑀 ) · 𝐴 ) = ( ( 𝐸 / 𝑃 ) · ( 𝑀 · 𝐴 ) ) )
123 120 122 oveq12d ⊢ ( 𝜑 → ( 0 ( +g ‘ 𝐺 ) ( ( ( 𝐸 / 𝑃 ) · 𝑀 ) · 𝐴 ) ) = ( ( ( 𝐸 / 𝑃 ) · ( 𝑃 · 𝐶 ) ) ( +g ‘ 𝐺 ) ( ( 𝐸 / 𝑃 ) · ( 𝑀 · 𝐴 ) ) ) )
124 3 subgss ⊢ ( 𝑆 ∈ ( SubGrp ‘ 𝐺 ) → 𝑆 ⊆ 𝐵 )
125 70 124 syl ⊢ ( 𝜑 → 𝑆 ⊆ 𝐵 )
126 125 105 sseldd ⊢ ( 𝜑 → ( ( ( 𝐸 / 𝑃 ) · 𝑀 ) · 𝐴 ) ∈ 𝐵 )
127 3 112 6 grplid ⊢ ( ( 𝐺 ∈ Grp ∧ ( ( ( 𝐸 / 𝑃 ) · 𝑀 ) · 𝐴 ) ∈ 𝐵 ) → ( 0 ( +g ‘ 𝐺 ) ( ( ( 𝐸 / 𝑃 ) · 𝑀 ) · 𝐴 ) ) = ( ( ( 𝐸 / 𝑃 ) · 𝑀 ) · 𝐴 ) )
128 26 126 127 syl2anc ⊢ ( 𝜑 → ( 0 ( +g ‘ 𝐺 ) ( ( ( 𝐸 / 𝑃 ) · 𝑀 ) · 𝐴 ) ) = ( ( ( 𝐸 / 𝑃 ) · 𝑀 ) · 𝐴 ) )
129 114 123 128 3eqtr2d ⊢ ( 𝜑 → ( ( 𝐸 / 𝑃 ) · ( ( 𝑃 · 𝐶 ) ( +g ‘ 𝐺 ) ( 𝑀 · 𝐴 ) ) ) = ( ( ( 𝐸 / 𝑃 ) · 𝑀 ) · 𝐴 ) )
130 19 subgmulgcl ⊢ ( ( 𝑊 ∈ ( SubGrp ‘ 𝐺 ) ∧ ( 𝐸 / 𝑃 ) ∈ ℤ ∧ ( ( 𝑃 · 𝐶 ) ( +g ‘ 𝐺 ) ( 𝑀 · 𝐴 ) ) ∈ 𝑊 ) → ( ( 𝐸 / 𝑃 ) · ( ( 𝑃 · 𝐶 ) ( +g ‘ 𝐺 ) ( 𝑀 · 𝐴 ) ) ) ∈ 𝑊 )
131 14 96 21 130 syl3anc ⊢ ( 𝜑 → ( ( 𝐸 / 𝑃 ) · ( ( 𝑃 · 𝐶 ) ( +g ‘ 𝐺 ) ( 𝑀 · 𝐴 ) ) ) ∈ 𝑊 )
132 129 131 eqeltrrd ⊢ ( 𝜑 → ( ( ( 𝐸 / 𝑃 ) · 𝑀 ) · 𝐴 ) ∈ 𝑊 )
133 105 132 elind ⊢ ( 𝜑 → ( ( ( 𝐸 / 𝑃 ) · 𝑀 ) · 𝐴 ) ∈ ( 𝑆 ∩ 𝑊 ) )
134 133 15 eleqtrd ⊢ ( 𝜑 → ( ( ( 𝐸 / 𝑃 ) · 𝑀 ) · 𝐴 ) ∈ { 0 } )
135 elsni ⊢ ( ( ( ( 𝐸 / 𝑃 ) · 𝑀 ) · 𝐴 ) ∈ { 0 } → ( ( ( 𝐸 / 𝑃 ) · 𝑀 ) · 𝐴 ) = 0 )
136 134 135 syl ⊢ ( 𝜑 → ( ( ( 𝐸 / 𝑃 ) · 𝑀 ) · 𝐴 ) = 0 )
137 3 4 19 6 oddvds ⊢ ( ( 𝐺 ∈ Grp ∧ 𝐴 ∈ 𝐵 ∧ ( ( 𝐸 / 𝑃 ) · 𝑀 ) ∈ ℤ ) → ( ( 𝑂 ‘ 𝐴 ) ∥ ( ( 𝐸 / 𝑃 ) · 𝑀 ) ↔ ( ( ( 𝐸 / 𝑃 ) · 𝑀 ) · 𝐴 ) = 0 ) )
138 26 67 97 137 syl3anc ⊢ ( 𝜑 → ( ( 𝑂 ‘ 𝐴 ) ∥ ( ( 𝐸 / 𝑃 ) · 𝑀 ) ↔ ( ( ( 𝐸 / 𝑃 ) · 𝑀 ) · 𝐴 ) = 0 ) )
139 136 138 mpbird ⊢ ( 𝜑 → ( 𝑂 ‘ 𝐴 ) ∥ ( ( 𝐸 / 𝑃 ) · 𝑀 ) )
140 92 139 eqbrtrrd ⊢ ( 𝜑 → ( ( 𝐸 / 𝑃 ) · 𝑃 ) ∥ ( ( 𝐸 / 𝑃 ) · 𝑀 ) )
141 95 nnne0d ⊢ ( 𝜑 → ( 𝐸 / 𝑃 ) ≠ 0 )
142 dvdscmulr ⊢ ( ( 𝑃 ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ ( ( 𝐸 / 𝑃 ) ∈ ℤ ∧ ( 𝐸 / 𝑃 ) ≠ 0 ) ) → ( ( ( 𝐸 / 𝑃 ) · 𝑃 ) ∥ ( ( 𝐸 / 𝑃 ) · 𝑀 ) ↔ 𝑃 ∥ 𝑀 ) )
143 107 20 96 141 142 syl112anc ⊢ ( 𝜑 → ( ( ( 𝐸 / 𝑃 ) · 𝑃 ) ∥ ( ( 𝐸 / 𝑃 ) · 𝑀 ) ↔ 𝑃 ∥ 𝑀 ) )
144 140 143 mpbid ⊢ ( 𝜑 → 𝑃 ∥ 𝑀 )
145 88 144 jca ⊢ ( 𝜑 → ( 𝑃 ∥ 𝐸 ∧ 𝑃 ∥ 𝑀 ) )