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 syl6bir ⊢ ( 𝜑 → ( ¬ 𝑃 ∥ 𝐸 → ( 𝑃 ↑ ( 𝑃 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 grpmnd ⊢ ( 𝐺 ∈ Grp → 𝐺 ∈ Mnd )
58 26 57 syl ⊢ ( 𝜑 → 𝐺 ∈ Mnd )
59 3 5 gex1 ⊢ ( 𝐺 ∈ Mnd → ( 𝐸 = 1 ↔ 𝐵 ≈ 1o ) )
60 58 59 syl ⊢ ( 𝜑 → ( 𝐸 = 1 ↔ 𝐵 ≈ 1o ) )
61 56 60 bitrd ⊢ ( 𝜑 → ( ( 𝑃 ↑ ( 𝑃 pCnt 𝐸 ) ) = ( 𝑃 ↑ 0 ) ↔ 𝐵 ≈ 1o ) )
62 32 61 sylibd ⊢ ( 𝜑 → ( ¬ 𝑃 ∥ 𝐸 → 𝐵 ≈ 1o ) )
63 3 subgacs ⊢ ( 𝐺 ∈ Grp → ( SubGrp ‘ 𝐺 ) ∈ ( ACS ‘ 𝐵 ) )
64 26 63 syl ⊢ ( 𝜑 → ( SubGrp ‘ 𝐺 ) ∈ ( ACS ‘ 𝐵 ) )
65 64 acsmred ⊢ ( 𝜑 → ( SubGrp ‘ 𝐺 ) ∈ ( Moore ‘ 𝐵 ) )
66 3 subgss ⊢ ( 𝑈 ∈ ( SubGrp ‘ 𝐺 ) → 𝑈 ⊆ 𝐵 )
67 12 66 syl ⊢ ( 𝜑 → 𝑈 ⊆ 𝐵 )
68 67 13 sseldd ⊢ ( 𝜑 → 𝐴 ∈ 𝐵 )
69 1 mrcsncl ⊢ ( ( ( SubGrp ‘ 𝐺 ) ∈ ( Moore ‘ 𝐵 ) ∧ 𝐴 ∈ 𝐵 ) → ( 𝐾 ‘ { 𝐴 } ) ∈ ( SubGrp ‘ 𝐺 ) )
70 65 68 69 syl2anc ⊢ ( 𝜑 → ( 𝐾 ‘ { 𝐴 } ) ∈ ( SubGrp ‘ 𝐺 ) )
71 2 70 eqeltrid ⊢ ( 𝜑 → 𝑆 ∈ ( SubGrp ‘ 𝐺 ) )
72 7 lsmsubg2 ⊢ ( ( 𝐺 ∈ Abel ∧ 𝑆 ∈ ( SubGrp ‘ 𝐺 ) ∧ 𝑊 ∈ ( SubGrp ‘ 𝐺 ) ) → ( 𝑆 ⊕ 𝑊 ) ∈ ( SubGrp ‘ 𝐺 ) )
73 9 71 14 72 syl3anc ⊢ ( 𝜑 → ( 𝑆 ⊕ 𝑊 ) ∈ ( SubGrp ‘ 𝐺 ) )
74 6 subg0cl ⊢ ( ( 𝑆 ⊕ 𝑊 ) ∈ ( SubGrp ‘ 𝐺 ) → 0 ∈ ( 𝑆 ⊕ 𝑊 ) )
75 73 74 syl ⊢ ( 𝜑 → 0 ∈ ( 𝑆 ⊕ 𝑊 ) )
76 75 snssd ⊢ ( 𝜑 → { 0 } ⊆ ( 𝑆 ⊕ 𝑊 ) )
77 76 adantr ⊢ ( ( 𝜑 ∧ 𝐵 ≈ 1o ) → { 0 } ⊆ ( 𝑆 ⊕ 𝑊 ) )
78 18 eldifad ⊢ ( 𝜑 → 𝐶 ∈ 𝑈 )
79 67 78 sseldd ⊢ ( 𝜑 → 𝐶 ∈ 𝐵 )
80 79 adantr ⊢ ( ( 𝜑 ∧ 𝐵 ≈ 1o ) → 𝐶 ∈ 𝐵 )
81 3 6 grpidcl ⊢ ( 𝐺 ∈ Grp → 0 ∈ 𝐵 )
82 26 81 syl ⊢ ( 𝜑 → 0 ∈ 𝐵 )
83 en1eqsn ⊢ ( ( 0 ∈ 𝐵 ∧ 𝐵 ≈ 1o ) → 𝐵 = { 0 } )
84 82 83 sylan ⊢ ( ( 𝜑 ∧ 𝐵 ≈ 1o ) → 𝐵 = { 0 } )
85 80 84 eleqtrd ⊢ ( ( 𝜑 ∧ 𝐵 ≈ 1o ) → 𝐶 ∈ { 0 } )
86 77 85 sseldd ⊢ ( ( 𝜑 ∧ 𝐵 ≈ 1o ) → 𝐶 ∈ ( 𝑆 ⊕ 𝑊 ) )
87 86 ex ⊢ ( 𝜑 → ( 𝐵 ≈ 1o → 𝐶 ∈ ( 𝑆 ⊕ 𝑊 ) ) )
88 62 87 syld ⊢ ( 𝜑 → ( ¬ 𝑃 ∥ 𝐸 → 𝐶 ∈ ( 𝑆 ⊕ 𝑊 ) ) )
89 22 88 mt3d ⊢ ( 𝜑 → 𝑃 ∥ 𝐸 )
90 28 nncnd ⊢ ( 𝜑 → 𝐸 ∈ ℂ )
91 53 nnne0d ⊢ ( 𝜑 → 𝑃 ≠ 0 )
92 90 54 91 divcan1d ⊢ ( 𝜑 → ( ( 𝐸 / 𝑃 ) · 𝑃 ) = 𝐸 )
93 11 92 eqtr4d ⊢ ( 𝜑 → ( 𝑂 ‘ 𝐴 ) = ( ( 𝐸 / 𝑃 ) · 𝑃 ) )
94 nndivdvds ⊢ ( ( 𝐸 ∈ ℕ ∧ 𝑃 ∈ ℕ ) → ( 𝑃 ∥ 𝐸 ↔ ( 𝐸 / 𝑃 ) ∈ ℕ ) )
95 28 53 94 syl2anc ⊢ ( 𝜑 → ( 𝑃 ∥ 𝐸 ↔ ( 𝐸 / 𝑃 ) ∈ ℕ ) )
96 89 95 mpbid ⊢ ( 𝜑 → ( 𝐸 / 𝑃 ) ∈ ℕ )
97 96 nnzd ⊢ ( 𝜑 → ( 𝐸 / 𝑃 ) ∈ ℤ )
98 97 20 zmulcld ⊢ ( 𝜑 → ( ( 𝐸 / 𝑃 ) · 𝑀 ) ∈ ℤ )
99 68 snssd ⊢ ( 𝜑 → { 𝐴 } ⊆ 𝐵 )
100 65 1 99 mrcssidd ⊢ ( 𝜑 → { 𝐴 } ⊆ ( 𝐾 ‘ { 𝐴 } ) )
101 100 2 sseqtrrdi ⊢ ( 𝜑 → { 𝐴 } ⊆ 𝑆 )
102 snssg ⊢ ( 𝐴 ∈ 𝑈 → ( 𝐴 ∈ 𝑆 ↔ { 𝐴 } ⊆ 𝑆 ) )
103 13 102 syl ⊢ ( 𝜑 → ( 𝐴 ∈ 𝑆 ↔ { 𝐴 } ⊆ 𝑆 ) )
104 101 103 mpbird ⊢ ( 𝜑 → 𝐴 ∈ 𝑆 )
105 19 subgmulgcl ⊢ ( ( 𝑆 ∈ ( SubGrp ‘ 𝐺 ) ∧ ( ( 𝐸 / 𝑃 ) · 𝑀 ) ∈ ℤ ∧ 𝐴 ∈ 𝑆 ) → ( ( ( 𝐸 / 𝑃 ) · 𝑀 ) · 𝐴 ) ∈ 𝑆 )
106 71 98 104 105 syl3anc ⊢ ( 𝜑 → ( ( ( 𝐸 / 𝑃 ) · 𝑀 ) · 𝐴 ) ∈ 𝑆 )
107 prmz ⊢ ( 𝑃 ∈ ℙ → 𝑃 ∈ ℤ )
108 24 107 syl ⊢ ( 𝜑 → 𝑃 ∈ ℤ )
109 3 19 mulgcl ⊢ ( ( 𝐺 ∈ Grp ∧ 𝑃 ∈ ℤ ∧ 𝐶 ∈ 𝐵 ) → ( 𝑃 · 𝐶 ) ∈ 𝐵 )
110 26 108 79 109 syl3anc ⊢ ( 𝜑 → ( 𝑃 · 𝐶 ) ∈ 𝐵 )
111 3 19 mulgcl ⊢ ( ( 𝐺 ∈ Grp ∧ 𝑀 ∈ ℤ ∧ 𝐴 ∈ 𝐵 ) → ( 𝑀 · 𝐴 ) ∈ 𝐵 )
112 26 20 68 111 syl3anc ⊢ ( 𝜑 → ( 𝑀 · 𝐴 ) ∈ 𝐵 )
113 eqid ⊢ ( +g ‘ 𝐺 ) = ( +g ‘ 𝐺 )
114 3 19 113 mulgdi ⊢ ( ( 𝐺 ∈ Abel ∧ ( ( 𝐸 / 𝑃 ) ∈ ℤ ∧ ( 𝑃 · 𝐶 ) ∈ 𝐵 ∧ ( 𝑀 · 𝐴 ) ∈ 𝐵 ) ) → ( ( 𝐸 / 𝑃 ) · ( ( 𝑃 · 𝐶 ) ( +g ‘ 𝐺 ) ( 𝑀 · 𝐴 ) ) ) = ( ( ( 𝐸 / 𝑃 ) · ( 𝑃 · 𝐶 ) ) ( +g ‘ 𝐺 ) ( ( 𝐸 / 𝑃 ) · ( 𝑀 · 𝐴 ) ) ) )
115 9 97 110 112 114 syl13anc ⊢ ( 𝜑 → ( ( 𝐸 / 𝑃 ) · ( ( 𝑃 · 𝐶 ) ( +g ‘ 𝐺 ) ( 𝑀 · 𝐴 ) ) ) = ( ( ( 𝐸 / 𝑃 ) · ( 𝑃 · 𝐶 ) ) ( +g ‘ 𝐺 ) ( ( 𝐸 / 𝑃 ) · ( 𝑀 · 𝐴 ) ) ) )
116 92 oveq1d ⊢ ( 𝜑 → ( ( ( 𝐸 / 𝑃 ) · 𝑃 ) · 𝐶 ) = ( 𝐸 · 𝐶 ) )
117 3 19 mulgass ⊢ ( ( 𝐺 ∈ Grp ∧ ( ( 𝐸 / 𝑃 ) ∈ ℤ ∧ 𝑃 ∈ ℤ ∧ 𝐶 ∈ 𝐵 ) ) → ( ( ( 𝐸 / 𝑃 ) · 𝑃 ) · 𝐶 ) = ( ( 𝐸 / 𝑃 ) · ( 𝑃 · 𝐶 ) ) )
118 26 97 108 79 117 syl13anc ⊢ ( 𝜑 → ( ( ( 𝐸 / 𝑃 ) · 𝑃 ) · 𝐶 ) = ( ( 𝐸 / 𝑃 ) · ( 𝑃 · 𝐶 ) ) )
119 3 5 19 6 gexid ⊢ ( 𝐶 ∈ 𝐵 → ( 𝐸 · 𝐶 ) = 0 )
120 79 119 syl ⊢ ( 𝜑 → ( 𝐸 · 𝐶 ) = 0 )
121 116 118 120 3eqtr3rd ⊢ ( 𝜑 → 0 = ( ( 𝐸 / 𝑃 ) · ( 𝑃 · 𝐶 ) ) )
122 3 19 mulgass ⊢ ( ( 𝐺 ∈ Grp ∧ ( ( 𝐸 / 𝑃 ) ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ 𝐴 ∈ 𝐵 ) ) → ( ( ( 𝐸 / 𝑃 ) · 𝑀 ) · 𝐴 ) = ( ( 𝐸 / 𝑃 ) · ( 𝑀 · 𝐴 ) ) )
123 26 97 20 68 122 syl13anc ⊢ ( 𝜑 → ( ( ( 𝐸 / 𝑃 ) · 𝑀 ) · 𝐴 ) = ( ( 𝐸 / 𝑃 ) · ( 𝑀 · 𝐴 ) ) )
124 121 123 oveq12d ⊢ ( 𝜑 → ( 0 ( +g ‘ 𝐺 ) ( ( ( 𝐸 / 𝑃 ) · 𝑀 ) · 𝐴 ) ) = ( ( ( 𝐸 / 𝑃 ) · ( 𝑃 · 𝐶 ) ) ( +g ‘ 𝐺 ) ( ( 𝐸 / 𝑃 ) · ( 𝑀 · 𝐴 ) ) ) )
125 3 subgss ⊢ ( 𝑆 ∈ ( SubGrp ‘ 𝐺 ) → 𝑆 ⊆ 𝐵 )
126 71 125 syl ⊢ ( 𝜑 → 𝑆 ⊆ 𝐵 )
127 126 106 sseldd ⊢ ( 𝜑 → ( ( ( 𝐸 / 𝑃 ) · 𝑀 ) · 𝐴 ) ∈ 𝐵 )
128 3 113 6 grplid ⊢ ( ( 𝐺 ∈ Grp ∧ ( ( ( 𝐸 / 𝑃 ) · 𝑀 ) · 𝐴 ) ∈ 𝐵 ) → ( 0 ( +g ‘ 𝐺 ) ( ( ( 𝐸 / 𝑃 ) · 𝑀 ) · 𝐴 ) ) = ( ( ( 𝐸 / 𝑃 ) · 𝑀 ) · 𝐴 ) )
129 26 127 128 syl2anc ⊢ ( 𝜑 → ( 0 ( +g ‘ 𝐺 ) ( ( ( 𝐸 / 𝑃 ) · 𝑀 ) · 𝐴 ) ) = ( ( ( 𝐸 / 𝑃 ) · 𝑀 ) · 𝐴 ) )
130 115 124 129 3eqtr2d ⊢ ( 𝜑 → ( ( 𝐸 / 𝑃 ) · ( ( 𝑃 · 𝐶 ) ( +g ‘ 𝐺 ) ( 𝑀 · 𝐴 ) ) ) = ( ( ( 𝐸 / 𝑃 ) · 𝑀 ) · 𝐴 ) )
131 19 subgmulgcl ⊢ ( ( 𝑊 ∈ ( SubGrp ‘ 𝐺 ) ∧ ( 𝐸 / 𝑃 ) ∈ ℤ ∧ ( ( 𝑃 · 𝐶 ) ( +g ‘ 𝐺 ) ( 𝑀 · 𝐴 ) ) ∈ 𝑊 ) → ( ( 𝐸 / 𝑃 ) · ( ( 𝑃 · 𝐶 ) ( +g ‘ 𝐺 ) ( 𝑀 · 𝐴 ) ) ) ∈ 𝑊 )
132 14 97 21 131 syl3anc ⊢ ( 𝜑 → ( ( 𝐸 / 𝑃 ) · ( ( 𝑃 · 𝐶 ) ( +g ‘ 𝐺 ) ( 𝑀 · 𝐴 ) ) ) ∈ 𝑊 )
133 130 132 eqeltrrd ⊢ ( 𝜑 → ( ( ( 𝐸 / 𝑃 ) · 𝑀 ) · 𝐴 ) ∈ 𝑊 )
134 106 133 elind ⊢ ( 𝜑 → ( ( ( 𝐸 / 𝑃 ) · 𝑀 ) · 𝐴 ) ∈ ( 𝑆 ∩ 𝑊 ) )
135 134 15 eleqtrd ⊢ ( 𝜑 → ( ( ( 𝐸 / 𝑃 ) · 𝑀 ) · 𝐴 ) ∈ { 0 } )
136 elsni ⊢ ( ( ( ( 𝐸 / 𝑃 ) · 𝑀 ) · 𝐴 ) ∈ { 0 } → ( ( ( 𝐸 / 𝑃 ) · 𝑀 ) · 𝐴 ) = 0 )
137 135 136 syl ⊢ ( 𝜑 → ( ( ( 𝐸 / 𝑃 ) · 𝑀 ) · 𝐴 ) = 0 )
138 3 4 19 6 oddvds ⊢ ( ( 𝐺 ∈ Grp ∧ 𝐴 ∈ 𝐵 ∧ ( ( 𝐸 / 𝑃 ) · 𝑀 ) ∈ ℤ ) → ( ( 𝑂 ‘ 𝐴 ) ∥ ( ( 𝐸 / 𝑃 ) · 𝑀 ) ↔ ( ( ( 𝐸 / 𝑃 ) · 𝑀 ) · 𝐴 ) = 0 ) )
139 26 68 98 138 syl3anc ⊢ ( 𝜑 → ( ( 𝑂 ‘ 𝐴 ) ∥ ( ( 𝐸 / 𝑃 ) · 𝑀 ) ↔ ( ( ( 𝐸 / 𝑃 ) · 𝑀 ) · 𝐴 ) = 0 ) )
140 137 139 mpbird ⊢ ( 𝜑 → ( 𝑂 ‘ 𝐴 ) ∥ ( ( 𝐸 / 𝑃 ) · 𝑀 ) )
141 93 140 eqbrtrrd ⊢ ( 𝜑 → ( ( 𝐸 / 𝑃 ) · 𝑃 ) ∥ ( ( 𝐸 / 𝑃 ) · 𝑀 ) )
142 96 nnne0d ⊢ ( 𝜑 → ( 𝐸 / 𝑃 ) ≠ 0 )
143 dvdscmulr ⊢ ( ( 𝑃 ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ ( ( 𝐸 / 𝑃 ) ∈ ℤ ∧ ( 𝐸 / 𝑃 ) ≠ 0 ) ) → ( ( ( 𝐸 / 𝑃 ) · 𝑃 ) ∥ ( ( 𝐸 / 𝑃 ) · 𝑀 ) ↔ 𝑃 ∥ 𝑀 ) )
144 108 20 97 142 143 syl112anc ⊢ ( 𝜑 → ( ( ( 𝐸 / 𝑃 ) · 𝑃 ) ∥ ( ( 𝐸 / 𝑃 ) · 𝑀 ) ↔ 𝑃 ∥ 𝑀 ) )
145 141 144 mpbid ⊢ ( 𝜑 → 𝑃 ∥ 𝑀 )
146 89 145 jca ⊢ ( 𝜑 → ( 𝑃 ∥ 𝐸 ∧ 𝑃 ∥ 𝑀 ) )