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	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	⊢ ( 𝜑 → ( 𝑃 ∥ 𝐸 ∧ 𝑃 ∥ 𝑀 ) )