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 } ∧ ( 𝑆 ⊕ 𝑡 ) = 𝑈 ) )