MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  ablfac1b Structured version   Visualization version   GIF version

Theorem ablfac1b 19992
Description: Any abelian group is the direct product of factors of prime power order (with the exact order further matching the prime factorization of the group order). (Contributed by Mario Carneiro, 21-Apr-2016.)
Hypotheses
Ref Expression
ablfac1.b 𝐡 = (Baseβ€˜πΊ)
ablfac1.o 𝑂 = (odβ€˜πΊ)
ablfac1.s 𝑆 = (𝑝 ∈ 𝐴 ↦ {π‘₯ ∈ 𝐡 ∣ (π‘‚β€˜π‘₯) βˆ₯ (𝑝↑(𝑝 pCnt (β™―β€˜π΅)))})
ablfac1.g (πœ‘ β†’ 𝐺 ∈ Abel)
ablfac1.f (πœ‘ β†’ 𝐡 ∈ Fin)
ablfac1.1 (πœ‘ β†’ 𝐴 βŠ† β„™)
Assertion
Ref Expression
ablfac1b (πœ‘ β†’ 𝐺dom DProd 𝑆)
Distinct variable groups:   π‘₯,𝑝,𝐡   πœ‘,𝑝,π‘₯   𝐴,𝑝,π‘₯   𝑂,𝑝,π‘₯   𝐺,𝑝,π‘₯
Allowed substitution hints:   𝑆(π‘₯,𝑝)

Proof of Theorem ablfac1b
Dummy variables π‘Ž 𝑏 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 eqid 2726 . 2 (Cntzβ€˜πΊ) = (Cntzβ€˜πΊ)
2 eqid 2726 . 2 (0gβ€˜πΊ) = (0gβ€˜πΊ)
3 eqid 2726 . 2 (mrClsβ€˜(SubGrpβ€˜πΊ)) = (mrClsβ€˜(SubGrpβ€˜πΊ))
4 ablfac1.g . . 3 (πœ‘ β†’ 𝐺 ∈ Abel)
5 ablgrp 19705 . . 3 (𝐺 ∈ Abel β†’ 𝐺 ∈ Grp)
64, 5syl 17 . 2 (πœ‘ β†’ 𝐺 ∈ Grp)
7 ablfac1.1 . . 3 (πœ‘ β†’ 𝐴 βŠ† β„™)
8 prmex 16621 . . . 4 β„™ ∈ V
98ssex 5314 . . 3 (𝐴 βŠ† β„™ β†’ 𝐴 ∈ V)
107, 9syl 17 . 2 (πœ‘ β†’ 𝐴 ∈ V)
114adantr 480 . . . 4 ((πœ‘ ∧ 𝑝 ∈ 𝐴) β†’ 𝐺 ∈ Abel)
127sselda 3977 . . . . . . 7 ((πœ‘ ∧ 𝑝 ∈ 𝐴) β†’ 𝑝 ∈ β„™)
13 prmnn 16618 . . . . . . 7 (𝑝 ∈ β„™ β†’ 𝑝 ∈ β„•)
1412, 13syl 17 . . . . . 6 ((πœ‘ ∧ 𝑝 ∈ 𝐴) β†’ 𝑝 ∈ β„•)
15 ablfac1.b . . . . . . . . . . 11 𝐡 = (Baseβ€˜πΊ)
1615grpbn0 18896 . . . . . . . . . 10 (𝐺 ∈ Grp β†’ 𝐡 β‰  βˆ…)
176, 16syl 17 . . . . . . . . 9 (πœ‘ β†’ 𝐡 β‰  βˆ…)
18 ablfac1.f . . . . . . . . . 10 (πœ‘ β†’ 𝐡 ∈ Fin)
19 hashnncl 14331 . . . . . . . . . 10 (𝐡 ∈ Fin β†’ ((β™―β€˜π΅) ∈ β„• ↔ 𝐡 β‰  βˆ…))
2018, 19syl 17 . . . . . . . . 9 (πœ‘ β†’ ((β™―β€˜π΅) ∈ β„• ↔ 𝐡 β‰  βˆ…))
2117, 20mpbird 257 . . . . . . . 8 (πœ‘ β†’ (β™―β€˜π΅) ∈ β„•)
2221adantr 480 . . . . . . 7 ((πœ‘ ∧ 𝑝 ∈ 𝐴) β†’ (β™―β€˜π΅) ∈ β„•)
2312, 22pccld 16792 . . . . . 6 ((πœ‘ ∧ 𝑝 ∈ 𝐴) β†’ (𝑝 pCnt (β™―β€˜π΅)) ∈ β„•0)
2414, 23nnexpcld 14213 . . . . 5 ((πœ‘ ∧ 𝑝 ∈ 𝐴) β†’ (𝑝↑(𝑝 pCnt (β™―β€˜π΅))) ∈ β„•)
2524nnzd 12589 . . . 4 ((πœ‘ ∧ 𝑝 ∈ 𝐴) β†’ (𝑝↑(𝑝 pCnt (β™―β€˜π΅))) ∈ β„€)
26 ablfac1.o . . . . 5 𝑂 = (odβ€˜πΊ)
2726, 15oddvdssubg 19775 . . . 4 ((𝐺 ∈ Abel ∧ (𝑝↑(𝑝 pCnt (β™―β€˜π΅))) ∈ β„€) β†’ {π‘₯ ∈ 𝐡 ∣ (π‘‚β€˜π‘₯) βˆ₯ (𝑝↑(𝑝 pCnt (β™―β€˜π΅)))} ∈ (SubGrpβ€˜πΊ))
2811, 25, 27syl2anc 583 . . 3 ((πœ‘ ∧ 𝑝 ∈ 𝐴) β†’ {π‘₯ ∈ 𝐡 ∣ (π‘‚β€˜π‘₯) βˆ₯ (𝑝↑(𝑝 pCnt (β™―β€˜π΅)))} ∈ (SubGrpβ€˜πΊ))
29 ablfac1.s . . 3 𝑆 = (𝑝 ∈ 𝐴 ↦ {π‘₯ ∈ 𝐡 ∣ (π‘‚β€˜π‘₯) βˆ₯ (𝑝↑(𝑝 pCnt (β™―β€˜π΅)))})
3028, 29fmptd 7109 . 2 (πœ‘ β†’ 𝑆:𝐴⟢(SubGrpβ€˜πΊ))
314adantr 480 . . 3 ((πœ‘ ∧ (π‘Ž ∈ 𝐴 ∧ 𝑏 ∈ 𝐴 ∧ π‘Ž β‰  𝑏)) β†’ 𝐺 ∈ Abel)
3230adantr 480 . . . 4 ((πœ‘ ∧ (π‘Ž ∈ 𝐴 ∧ 𝑏 ∈ 𝐴 ∧ π‘Ž β‰  𝑏)) β†’ 𝑆:𝐴⟢(SubGrpβ€˜πΊ))
33 simpr1 1191 . . . 4 ((πœ‘ ∧ (π‘Ž ∈ 𝐴 ∧ 𝑏 ∈ 𝐴 ∧ π‘Ž β‰  𝑏)) β†’ π‘Ž ∈ 𝐴)
3432, 33ffvelcdmd 7081 . . 3 ((πœ‘ ∧ (π‘Ž ∈ 𝐴 ∧ 𝑏 ∈ 𝐴 ∧ π‘Ž β‰  𝑏)) β†’ (π‘†β€˜π‘Ž) ∈ (SubGrpβ€˜πΊ))
35 simpr2 1192 . . . 4 ((πœ‘ ∧ (π‘Ž ∈ 𝐴 ∧ 𝑏 ∈ 𝐴 ∧ π‘Ž β‰  𝑏)) β†’ 𝑏 ∈ 𝐴)
3632, 35ffvelcdmd 7081 . . 3 ((πœ‘ ∧ (π‘Ž ∈ 𝐴 ∧ 𝑏 ∈ 𝐴 ∧ π‘Ž β‰  𝑏)) β†’ (π‘†β€˜π‘) ∈ (SubGrpβ€˜πΊ))
371, 31, 34, 36ablcntzd 19777 . 2 ((πœ‘ ∧ (π‘Ž ∈ 𝐴 ∧ 𝑏 ∈ 𝐴 ∧ π‘Ž β‰  𝑏)) β†’ (π‘†β€˜π‘Ž) βŠ† ((Cntzβ€˜πΊ)β€˜(π‘†β€˜π‘)))
38 id 22 . . . . . . . . . 10 (𝑝 = π‘Ž β†’ 𝑝 = π‘Ž)
39 oveq1 7412 . . . . . . . . . 10 (𝑝 = π‘Ž β†’ (𝑝 pCnt (β™―β€˜π΅)) = (π‘Ž pCnt (β™―β€˜π΅)))
4038, 39oveq12d 7423 . . . . . . . . 9 (𝑝 = π‘Ž β†’ (𝑝↑(𝑝 pCnt (β™―β€˜π΅))) = (π‘Žβ†‘(π‘Ž pCnt (β™―β€˜π΅))))
4140breq2d 5153 . . . . . . . 8 (𝑝 = π‘Ž β†’ ((π‘‚β€˜π‘₯) βˆ₯ (𝑝↑(𝑝 pCnt (β™―β€˜π΅))) ↔ (π‘‚β€˜π‘₯) βˆ₯ (π‘Žβ†‘(π‘Ž pCnt (β™―β€˜π΅)))))
4241rabbidv 3434 . . . . . . 7 (𝑝 = π‘Ž β†’ {π‘₯ ∈ 𝐡 ∣ (π‘‚β€˜π‘₯) βˆ₯ (𝑝↑(𝑝 pCnt (β™―β€˜π΅)))} = {π‘₯ ∈ 𝐡 ∣ (π‘‚β€˜π‘₯) βˆ₯ (π‘Žβ†‘(π‘Ž pCnt (β™―β€˜π΅)))})
4315fvexi 6899 . . . . . . . 8 𝐡 ∈ V
4443rabex 5325 . . . . . . 7 {π‘₯ ∈ 𝐡 ∣ (π‘‚β€˜π‘₯) βˆ₯ (𝑝↑(𝑝 pCnt (β™―β€˜π΅)))} ∈ V
4542, 29, 44fvmpt3i 6997 . . . . . 6 (π‘Ž ∈ 𝐴 β†’ (π‘†β€˜π‘Ž) = {π‘₯ ∈ 𝐡 ∣ (π‘‚β€˜π‘₯) βˆ₯ (π‘Žβ†‘(π‘Ž pCnt (β™―β€˜π΅)))})
4645adantl 481 . . . . 5 ((πœ‘ ∧ π‘Ž ∈ 𝐴) β†’ (π‘†β€˜π‘Ž) = {π‘₯ ∈ 𝐡 ∣ (π‘‚β€˜π‘₯) βˆ₯ (π‘Žβ†‘(π‘Ž pCnt (β™―β€˜π΅)))})
47 eqimss 4035 . . . . 5 ((π‘†β€˜π‘Ž) = {π‘₯ ∈ 𝐡 ∣ (π‘‚β€˜π‘₯) βˆ₯ (π‘Žβ†‘(π‘Ž pCnt (β™―β€˜π΅)))} β†’ (π‘†β€˜π‘Ž) βŠ† {π‘₯ ∈ 𝐡 ∣ (π‘‚β€˜π‘₯) βˆ₯ (π‘Žβ†‘(π‘Ž pCnt (β™―β€˜π΅)))})
4846, 47syl 17 . . . 4 ((πœ‘ ∧ π‘Ž ∈ 𝐴) β†’ (π‘†β€˜π‘Ž) βŠ† {π‘₯ ∈ 𝐡 ∣ (π‘‚β€˜π‘₯) βˆ₯ (π‘Žβ†‘(π‘Ž pCnt (β™―β€˜π΅)))})
494adantr 480 . . . . . 6 ((πœ‘ ∧ π‘Ž ∈ 𝐴) β†’ 𝐺 ∈ Abel)
50 eqid 2726 . . . . . . 7 (Baseβ€˜πΊ) = (Baseβ€˜πΊ)
5150subgacs 19088 . . . . . 6 (𝐺 ∈ Grp β†’ (SubGrpβ€˜πΊ) ∈ (ACSβ€˜(Baseβ€˜πΊ)))
52 acsmre 17605 . . . . . 6 ((SubGrpβ€˜πΊ) ∈ (ACSβ€˜(Baseβ€˜πΊ)) β†’ (SubGrpβ€˜πΊ) ∈ (Mooreβ€˜(Baseβ€˜πΊ)))
5349, 5, 51, 524syl 19 . . . . 5 ((πœ‘ ∧ π‘Ž ∈ 𝐴) β†’ (SubGrpβ€˜πΊ) ∈ (Mooreβ€˜(Baseβ€˜πΊ)))
54 df-ima 5682 . . . . . . 7 (𝑆 β€œ (𝐴 βˆ– {π‘Ž})) = ran (𝑆 β†Ύ (𝐴 βˆ– {π‘Ž}))
557sselda 3977 . . . . . . . . . . . . . . . . 17 ((πœ‘ ∧ π‘Ž ∈ 𝐴) β†’ π‘Ž ∈ β„™)
5655ad2antrr 723 . . . . . . . . . . . . . . . 16 ((((πœ‘ ∧ π‘Ž ∈ 𝐴) ∧ 𝑝 ∈ (𝐴 βˆ– {π‘Ž})) ∧ π‘₯ ∈ 𝐡) β†’ π‘Ž ∈ β„™)
5721ad3antrrr 727 . . . . . . . . . . . . . . . 16 ((((πœ‘ ∧ π‘Ž ∈ 𝐴) ∧ 𝑝 ∈ (𝐴 βˆ– {π‘Ž})) ∧ π‘₯ ∈ 𝐡) β†’ (β™―β€˜π΅) ∈ β„•)
58 pcdvds 16806 . . . . . . . . . . . . . . . 16 ((π‘Ž ∈ β„™ ∧ (β™―β€˜π΅) ∈ β„•) β†’ (π‘Žβ†‘(π‘Ž pCnt (β™―β€˜π΅))) βˆ₯ (β™―β€˜π΅))
5956, 57, 58syl2anc 583 . . . . . . . . . . . . . . 15 ((((πœ‘ ∧ π‘Ž ∈ 𝐴) ∧ 𝑝 ∈ (𝐴 βˆ– {π‘Ž})) ∧ π‘₯ ∈ 𝐡) β†’ (π‘Žβ†‘(π‘Ž pCnt (β™―β€˜π΅))) βˆ₯ (β™―β€˜π΅))
607ad3antrrr 727 . . . . . . . . . . . . . . . . 17 ((((πœ‘ ∧ π‘Ž ∈ 𝐴) ∧ 𝑝 ∈ (𝐴 βˆ– {π‘Ž})) ∧ π‘₯ ∈ 𝐡) β†’ 𝐴 βŠ† β„™)
61 eldifi 4121 . . . . . . . . . . . . . . . . . 18 (𝑝 ∈ (𝐴 βˆ– {π‘Ž}) β†’ 𝑝 ∈ 𝐴)
6261ad2antlr 724 . . . . . . . . . . . . . . . . 17 ((((πœ‘ ∧ π‘Ž ∈ 𝐴) ∧ 𝑝 ∈ (𝐴 βˆ– {π‘Ž})) ∧ π‘₯ ∈ 𝐡) β†’ 𝑝 ∈ 𝐴)
6360, 62sseldd 3978 . . . . . . . . . . . . . . . 16 ((((πœ‘ ∧ π‘Ž ∈ 𝐴) ∧ 𝑝 ∈ (𝐴 βˆ– {π‘Ž})) ∧ π‘₯ ∈ 𝐡) β†’ 𝑝 ∈ β„™)
64 pcdvds 16806 . . . . . . . . . . . . . . . 16 ((𝑝 ∈ β„™ ∧ (β™―β€˜π΅) ∈ β„•) β†’ (𝑝↑(𝑝 pCnt (β™―β€˜π΅))) βˆ₯ (β™―β€˜π΅))
6563, 57, 64syl2anc 583 . . . . . . . . . . . . . . 15 ((((πœ‘ ∧ π‘Ž ∈ 𝐴) ∧ 𝑝 ∈ (𝐴 βˆ– {π‘Ž})) ∧ π‘₯ ∈ 𝐡) β†’ (𝑝↑(𝑝 pCnt (β™―β€˜π΅))) βˆ₯ (β™―β€˜π΅))
66 eqid 2726 . . . . . . . . . . . . . . . . . . . . 21 (π‘Žβ†‘(π‘Ž pCnt (β™―β€˜π΅))) = (π‘Žβ†‘(π‘Ž pCnt (β™―β€˜π΅)))
67 eqid 2726 . . . . . . . . . . . . . . . . . . . . 21 ((β™―β€˜π΅) / (π‘Žβ†‘(π‘Ž pCnt (β™―β€˜π΅)))) = ((β™―β€˜π΅) / (π‘Žβ†‘(π‘Ž pCnt (β™―β€˜π΅))))
6815, 26, 29, 4, 18, 7, 66, 67ablfac1lem 19990 . . . . . . . . . . . . . . . . . . . 20 ((πœ‘ ∧ π‘Ž ∈ 𝐴) β†’ (((π‘Žβ†‘(π‘Ž pCnt (β™―β€˜π΅))) ∈ β„• ∧ ((β™―β€˜π΅) / (π‘Žβ†‘(π‘Ž pCnt (β™―β€˜π΅)))) ∈ β„•) ∧ ((π‘Žβ†‘(π‘Ž pCnt (β™―β€˜π΅))) gcd ((β™―β€˜π΅) / (π‘Žβ†‘(π‘Ž pCnt (β™―β€˜π΅))))) = 1 ∧ (β™―β€˜π΅) = ((π‘Žβ†‘(π‘Ž pCnt (β™―β€˜π΅))) Β· ((β™―β€˜π΅) / (π‘Žβ†‘(π‘Ž pCnt (β™―β€˜π΅)))))))
6968simp1d 1139 . . . . . . . . . . . . . . . . . . 19 ((πœ‘ ∧ π‘Ž ∈ 𝐴) β†’ ((π‘Žβ†‘(π‘Ž pCnt (β™―β€˜π΅))) ∈ β„• ∧ ((β™―β€˜π΅) / (π‘Žβ†‘(π‘Ž pCnt (β™―β€˜π΅)))) ∈ β„•))
7069simpld 494 . . . . . . . . . . . . . . . . . 18 ((πœ‘ ∧ π‘Ž ∈ 𝐴) β†’ (π‘Žβ†‘(π‘Ž pCnt (β™―β€˜π΅))) ∈ β„•)
7170ad2antrr 723 . . . . . . . . . . . . . . . . 17 ((((πœ‘ ∧ π‘Ž ∈ 𝐴) ∧ 𝑝 ∈ (𝐴 βˆ– {π‘Ž})) ∧ π‘₯ ∈ 𝐡) β†’ (π‘Žβ†‘(π‘Ž pCnt (β™―β€˜π΅))) ∈ β„•)
7271nnzd 12589 . . . . . . . . . . . . . . . 16 ((((πœ‘ ∧ π‘Ž ∈ 𝐴) ∧ 𝑝 ∈ (𝐴 βˆ– {π‘Ž})) ∧ π‘₯ ∈ 𝐡) β†’ (π‘Žβ†‘(π‘Ž pCnt (β™―β€˜π΅))) ∈ β„€)
7363, 13syl 17 . . . . . . . . . . . . . . . . . 18 ((((πœ‘ ∧ π‘Ž ∈ 𝐴) ∧ 𝑝 ∈ (𝐴 βˆ– {π‘Ž})) ∧ π‘₯ ∈ 𝐡) β†’ 𝑝 ∈ β„•)
7463, 57pccld 16792 . . . . . . . . . . . . . . . . . 18 ((((πœ‘ ∧ π‘Ž ∈ 𝐴) ∧ 𝑝 ∈ (𝐴 βˆ– {π‘Ž})) ∧ π‘₯ ∈ 𝐡) β†’ (𝑝 pCnt (β™―β€˜π΅)) ∈ β„•0)
7573, 74nnexpcld 14213 . . . . . . . . . . . . . . . . 17 ((((πœ‘ ∧ π‘Ž ∈ 𝐴) ∧ 𝑝 ∈ (𝐴 βˆ– {π‘Ž})) ∧ π‘₯ ∈ 𝐡) β†’ (𝑝↑(𝑝 pCnt (β™―β€˜π΅))) ∈ β„•)
7675nnzd 12589 . . . . . . . . . . . . . . . 16 ((((πœ‘ ∧ π‘Ž ∈ 𝐴) ∧ 𝑝 ∈ (𝐴 βˆ– {π‘Ž})) ∧ π‘₯ ∈ 𝐡) β†’ (𝑝↑(𝑝 pCnt (β™―β€˜π΅))) ∈ β„€)
7757nnzd 12589 . . . . . . . . . . . . . . . 16 ((((πœ‘ ∧ π‘Ž ∈ 𝐴) ∧ 𝑝 ∈ (𝐴 βˆ– {π‘Ž})) ∧ π‘₯ ∈ 𝐡) β†’ (β™―β€˜π΅) ∈ β„€)
78 eldifsni 4788 . . . . . . . . . . . . . . . . . . . 20 (𝑝 ∈ (𝐴 βˆ– {π‘Ž}) β†’ 𝑝 β‰  π‘Ž)
7978ad2antlr 724 . . . . . . . . . . . . . . . . . . 19 ((((πœ‘ ∧ π‘Ž ∈ 𝐴) ∧ 𝑝 ∈ (𝐴 βˆ– {π‘Ž})) ∧ π‘₯ ∈ 𝐡) β†’ 𝑝 β‰  π‘Ž)
8079necomd 2990 . . . . . . . . . . . . . . . . . 18 ((((πœ‘ ∧ π‘Ž ∈ 𝐴) ∧ 𝑝 ∈ (𝐴 βˆ– {π‘Ž})) ∧ π‘₯ ∈ 𝐡) β†’ π‘Ž β‰  𝑝)
81 prmrp 16656 . . . . . . . . . . . . . . . . . . 19 ((π‘Ž ∈ β„™ ∧ 𝑝 ∈ β„™) β†’ ((π‘Ž gcd 𝑝) = 1 ↔ π‘Ž β‰  𝑝))
8256, 63, 81syl2anc 583 . . . . . . . . . . . . . . . . . 18 ((((πœ‘ ∧ π‘Ž ∈ 𝐴) ∧ 𝑝 ∈ (𝐴 βˆ– {π‘Ž})) ∧ π‘₯ ∈ 𝐡) β†’ ((π‘Ž gcd 𝑝) = 1 ↔ π‘Ž β‰  𝑝))
8380, 82mpbird 257 . . . . . . . . . . . . . . . . 17 ((((πœ‘ ∧ π‘Ž ∈ 𝐴) ∧ 𝑝 ∈ (𝐴 βˆ– {π‘Ž})) ∧ π‘₯ ∈ 𝐡) β†’ (π‘Ž gcd 𝑝) = 1)
84 prmz 16619 . . . . . . . . . . . . . . . . . . 19 (π‘Ž ∈ β„™ β†’ π‘Ž ∈ β„€)
8556, 84syl 17 . . . . . . . . . . . . . . . . . 18 ((((πœ‘ ∧ π‘Ž ∈ 𝐴) ∧ 𝑝 ∈ (𝐴 βˆ– {π‘Ž})) ∧ π‘₯ ∈ 𝐡) β†’ π‘Ž ∈ β„€)
86 prmz 16619 . . . . . . . . . . . . . . . . . . 19 (𝑝 ∈ β„™ β†’ 𝑝 ∈ β„€)
8763, 86syl 17 . . . . . . . . . . . . . . . . . 18 ((((πœ‘ ∧ π‘Ž ∈ 𝐴) ∧ 𝑝 ∈ (𝐴 βˆ– {π‘Ž})) ∧ π‘₯ ∈ 𝐡) β†’ 𝑝 ∈ β„€)
8856, 57pccld 16792 . . . . . . . . . . . . . . . . . 18 ((((πœ‘ ∧ π‘Ž ∈ 𝐴) ∧ 𝑝 ∈ (𝐴 βˆ– {π‘Ž})) ∧ π‘₯ ∈ 𝐡) β†’ (π‘Ž pCnt (β™―β€˜π΅)) ∈ β„•0)
89 rpexp12i 16669 . . . . . . . . . . . . . . . . . 18 ((π‘Ž ∈ β„€ ∧ 𝑝 ∈ β„€ ∧ ((π‘Ž pCnt (β™―β€˜π΅)) ∈ β„•0 ∧ (𝑝 pCnt (β™―β€˜π΅)) ∈ β„•0)) β†’ ((π‘Ž gcd 𝑝) = 1 β†’ ((π‘Žβ†‘(π‘Ž pCnt (β™―β€˜π΅))) gcd (𝑝↑(𝑝 pCnt (β™―β€˜π΅)))) = 1))
9085, 87, 88, 74, 89syl112anc 1371 . . . . . . . . . . . . . . . . 17 ((((πœ‘ ∧ π‘Ž ∈ 𝐴) ∧ 𝑝 ∈ (𝐴 βˆ– {π‘Ž})) ∧ π‘₯ ∈ 𝐡) β†’ ((π‘Ž gcd 𝑝) = 1 β†’ ((π‘Žβ†‘(π‘Ž pCnt (β™―β€˜π΅))) gcd (𝑝↑(𝑝 pCnt (β™―β€˜π΅)))) = 1))
9183, 90mpd 15 . . . . . . . . . . . . . . . 16 ((((πœ‘ ∧ π‘Ž ∈ 𝐴) ∧ 𝑝 ∈ (𝐴 βˆ– {π‘Ž})) ∧ π‘₯ ∈ 𝐡) β†’ ((π‘Žβ†‘(π‘Ž pCnt (β™―β€˜π΅))) gcd (𝑝↑(𝑝 pCnt (β™―β€˜π΅)))) = 1)
92 coprmdvds2 16598 . . . . . . . . . . . . . . . 16 ((((π‘Žβ†‘(π‘Ž pCnt (β™―β€˜π΅))) ∈ β„€ ∧ (𝑝↑(𝑝 pCnt (β™―β€˜π΅))) ∈ β„€ ∧ (β™―β€˜π΅) ∈ β„€) ∧ ((π‘Žβ†‘(π‘Ž pCnt (β™―β€˜π΅))) gcd (𝑝↑(𝑝 pCnt (β™―β€˜π΅)))) = 1) β†’ (((π‘Žβ†‘(π‘Ž pCnt (β™―β€˜π΅))) βˆ₯ (β™―β€˜π΅) ∧ (𝑝↑(𝑝 pCnt (β™―β€˜π΅))) βˆ₯ (β™―β€˜π΅)) β†’ ((π‘Žβ†‘(π‘Ž pCnt (β™―β€˜π΅))) Β· (𝑝↑(𝑝 pCnt (β™―β€˜π΅)))) βˆ₯ (β™―β€˜π΅)))
9372, 76, 77, 91, 92syl31anc 1370 . . . . . . . . . . . . . . 15 ((((πœ‘ ∧ π‘Ž ∈ 𝐴) ∧ 𝑝 ∈ (𝐴 βˆ– {π‘Ž})) ∧ π‘₯ ∈ 𝐡) β†’ (((π‘Žβ†‘(π‘Ž pCnt (β™―β€˜π΅))) βˆ₯ (β™―β€˜π΅) ∧ (𝑝↑(𝑝 pCnt (β™―β€˜π΅))) βˆ₯ (β™―β€˜π΅)) β†’ ((π‘Žβ†‘(π‘Ž pCnt (β™―β€˜π΅))) Β· (𝑝↑(𝑝 pCnt (β™―β€˜π΅)))) βˆ₯ (β™―β€˜π΅)))
9459, 65, 93mp2and 696 . . . . . . . . . . . . . 14 ((((πœ‘ ∧ π‘Ž ∈ 𝐴) ∧ 𝑝 ∈ (𝐴 βˆ– {π‘Ž})) ∧ π‘₯ ∈ 𝐡) β†’ ((π‘Žβ†‘(π‘Ž pCnt (β™―β€˜π΅))) Β· (𝑝↑(𝑝 pCnt (β™―β€˜π΅)))) βˆ₯ (β™―β€˜π΅))
9568simp3d 1141 . . . . . . . . . . . . . . 15 ((πœ‘ ∧ π‘Ž ∈ 𝐴) β†’ (β™―β€˜π΅) = ((π‘Žβ†‘(π‘Ž pCnt (β™―β€˜π΅))) Β· ((β™―β€˜π΅) / (π‘Žβ†‘(π‘Ž pCnt (β™―β€˜π΅))))))
9695ad2antrr 723 . . . . . . . . . . . . . 14 ((((πœ‘ ∧ π‘Ž ∈ 𝐴) ∧ 𝑝 ∈ (𝐴 βˆ– {π‘Ž})) ∧ π‘₯ ∈ 𝐡) β†’ (β™―β€˜π΅) = ((π‘Žβ†‘(π‘Ž pCnt (β™―β€˜π΅))) Β· ((β™―β€˜π΅) / (π‘Žβ†‘(π‘Ž pCnt (β™―β€˜π΅))))))
9794, 96breqtrd 5167 . . . . . . . . . . . . 13 ((((πœ‘ ∧ π‘Ž ∈ 𝐴) ∧ 𝑝 ∈ (𝐴 βˆ– {π‘Ž})) ∧ π‘₯ ∈ 𝐡) β†’ ((π‘Žβ†‘(π‘Ž pCnt (β™―β€˜π΅))) Β· (𝑝↑(𝑝 pCnt (β™―β€˜π΅)))) βˆ₯ ((π‘Žβ†‘(π‘Ž pCnt (β™―β€˜π΅))) Β· ((β™―β€˜π΅) / (π‘Žβ†‘(π‘Ž pCnt (β™―β€˜π΅))))))
9869simprd 495 . . . . . . . . . . . . . . . 16 ((πœ‘ ∧ π‘Ž ∈ 𝐴) β†’ ((β™―β€˜π΅) / (π‘Žβ†‘(π‘Ž pCnt (β™―β€˜π΅)))) ∈ β„•)
9998ad2antrr 723 . . . . . . . . . . . . . . 15 ((((πœ‘ ∧ π‘Ž ∈ 𝐴) ∧ 𝑝 ∈ (𝐴 βˆ– {π‘Ž})) ∧ π‘₯ ∈ 𝐡) β†’ ((β™―β€˜π΅) / (π‘Žβ†‘(π‘Ž pCnt (β™―β€˜π΅)))) ∈ β„•)
10099nnzd 12589 . . . . . . . . . . . . . 14 ((((πœ‘ ∧ π‘Ž ∈ 𝐴) ∧ 𝑝 ∈ (𝐴 βˆ– {π‘Ž})) ∧ π‘₯ ∈ 𝐡) β†’ ((β™―β€˜π΅) / (π‘Žβ†‘(π‘Ž pCnt (β™―β€˜π΅)))) ∈ β„€)
10171nnne0d 12266 . . . . . . . . . . . . . 14 ((((πœ‘ ∧ π‘Ž ∈ 𝐴) ∧ 𝑝 ∈ (𝐴 βˆ– {π‘Ž})) ∧ π‘₯ ∈ 𝐡) β†’ (π‘Žβ†‘(π‘Ž pCnt (β™―β€˜π΅))) β‰  0)
102 dvdscmulr 16235 . . . . . . . . . . . . . 14 (((𝑝↑(𝑝 pCnt (β™―β€˜π΅))) ∈ β„€ ∧ ((β™―β€˜π΅) / (π‘Žβ†‘(π‘Ž pCnt (β™―β€˜π΅)))) ∈ β„€ ∧ ((π‘Žβ†‘(π‘Ž pCnt (β™―β€˜π΅))) ∈ β„€ ∧ (π‘Žβ†‘(π‘Ž pCnt (β™―β€˜π΅))) β‰  0)) β†’ (((π‘Žβ†‘(π‘Ž pCnt (β™―β€˜π΅))) Β· (𝑝↑(𝑝 pCnt (β™―β€˜π΅)))) βˆ₯ ((π‘Žβ†‘(π‘Ž pCnt (β™―β€˜π΅))) Β· ((β™―β€˜π΅) / (π‘Žβ†‘(π‘Ž pCnt (β™―β€˜π΅))))) ↔ (𝑝↑(𝑝 pCnt (β™―β€˜π΅))) βˆ₯ ((β™―β€˜π΅) / (π‘Žβ†‘(π‘Ž pCnt (β™―β€˜π΅))))))
10376, 100, 72, 101, 102syl112anc 1371 . . . . . . . . . . . . 13 ((((πœ‘ ∧ π‘Ž ∈ 𝐴) ∧ 𝑝 ∈ (𝐴 βˆ– {π‘Ž})) ∧ π‘₯ ∈ 𝐡) β†’ (((π‘Žβ†‘(π‘Ž pCnt (β™―β€˜π΅))) Β· (𝑝↑(𝑝 pCnt (β™―β€˜π΅)))) βˆ₯ ((π‘Žβ†‘(π‘Ž pCnt (β™―β€˜π΅))) Β· ((β™―β€˜π΅) / (π‘Žβ†‘(π‘Ž pCnt (β™―β€˜π΅))))) ↔ (𝑝↑(𝑝 pCnt (β™―β€˜π΅))) βˆ₯ ((β™―β€˜π΅) / (π‘Žβ†‘(π‘Ž pCnt (β™―β€˜π΅))))))
10497, 103mpbid 231 . . . . . . . . . . . 12 ((((πœ‘ ∧ π‘Ž ∈ 𝐴) ∧ 𝑝 ∈ (𝐴 βˆ– {π‘Ž})) ∧ π‘₯ ∈ 𝐡) β†’ (𝑝↑(𝑝 pCnt (β™―β€˜π΅))) βˆ₯ ((β™―β€˜π΅) / (π‘Žβ†‘(π‘Ž pCnt (β™―β€˜π΅)))))
10515, 26odcl 19456 . . . . . . . . . . . . . . 15 (π‘₯ ∈ 𝐡 β†’ (π‘‚β€˜π‘₯) ∈ β„•0)
106105adantl 481 . . . . . . . . . . . . . 14 ((((πœ‘ ∧ π‘Ž ∈ 𝐴) ∧ 𝑝 ∈ (𝐴 βˆ– {π‘Ž})) ∧ π‘₯ ∈ 𝐡) β†’ (π‘‚β€˜π‘₯) ∈ β„•0)
107106nn0zd 12588 . . . . . . . . . . . . 13 ((((πœ‘ ∧ π‘Ž ∈ 𝐴) ∧ 𝑝 ∈ (𝐴 βˆ– {π‘Ž})) ∧ π‘₯ ∈ 𝐡) β†’ (π‘‚β€˜π‘₯) ∈ β„€)
108 dvdstr 16244 . . . . . . . . . . . . 13 (((π‘‚β€˜π‘₯) ∈ β„€ ∧ (𝑝↑(𝑝 pCnt (β™―β€˜π΅))) ∈ β„€ ∧ ((β™―β€˜π΅) / (π‘Žβ†‘(π‘Ž pCnt (β™―β€˜π΅)))) ∈ β„€) β†’ (((π‘‚β€˜π‘₯) βˆ₯ (𝑝↑(𝑝 pCnt (β™―β€˜π΅))) ∧ (𝑝↑(𝑝 pCnt (β™―β€˜π΅))) βˆ₯ ((β™―β€˜π΅) / (π‘Žβ†‘(π‘Ž pCnt (β™―β€˜π΅))))) β†’ (π‘‚β€˜π‘₯) βˆ₯ ((β™―β€˜π΅) / (π‘Žβ†‘(π‘Ž pCnt (β™―β€˜π΅))))))
109107, 76, 100, 108syl3anc 1368 . . . . . . . . . . . 12 ((((πœ‘ ∧ π‘Ž ∈ 𝐴) ∧ 𝑝 ∈ (𝐴 βˆ– {π‘Ž})) ∧ π‘₯ ∈ 𝐡) β†’ (((π‘‚β€˜π‘₯) βˆ₯ (𝑝↑(𝑝 pCnt (β™―β€˜π΅))) ∧ (𝑝↑(𝑝 pCnt (β™―β€˜π΅))) βˆ₯ ((β™―β€˜π΅) / (π‘Žβ†‘(π‘Ž pCnt (β™―β€˜π΅))))) β†’ (π‘‚β€˜π‘₯) βˆ₯ ((β™―β€˜π΅) / (π‘Žβ†‘(π‘Ž pCnt (β™―β€˜π΅))))))
110104, 109mpan2d 691 . . . . . . . . . . 11 ((((πœ‘ ∧ π‘Ž ∈ 𝐴) ∧ 𝑝 ∈ (𝐴 βˆ– {π‘Ž})) ∧ π‘₯ ∈ 𝐡) β†’ ((π‘‚β€˜π‘₯) βˆ₯ (𝑝↑(𝑝 pCnt (β™―β€˜π΅))) β†’ (π‘‚β€˜π‘₯) βˆ₯ ((β™―β€˜π΅) / (π‘Žβ†‘(π‘Ž pCnt (β™―β€˜π΅))))))
111110ss2rabdv 4068 . . . . . . . . . 10 (((πœ‘ ∧ π‘Ž ∈ 𝐴) ∧ 𝑝 ∈ (𝐴 βˆ– {π‘Ž})) β†’ {π‘₯ ∈ 𝐡 ∣ (π‘‚β€˜π‘₯) βˆ₯ (𝑝↑(𝑝 pCnt (β™―β€˜π΅)))} βŠ† {π‘₯ ∈ 𝐡 ∣ (π‘‚β€˜π‘₯) βˆ₯ ((β™―β€˜π΅) / (π‘Žβ†‘(π‘Ž pCnt (β™―β€˜π΅))))})
11244elpw 4601 . . . . . . . . . 10 ({π‘₯ ∈ 𝐡 ∣ (π‘‚β€˜π‘₯) βˆ₯ (𝑝↑(𝑝 pCnt (β™―β€˜π΅)))} ∈ 𝒫 {π‘₯ ∈ 𝐡 ∣ (π‘‚β€˜π‘₯) βˆ₯ ((β™―β€˜π΅) / (π‘Žβ†‘(π‘Ž pCnt (β™―β€˜π΅))))} ↔ {π‘₯ ∈ 𝐡 ∣ (π‘‚β€˜π‘₯) βˆ₯ (𝑝↑(𝑝 pCnt (β™―β€˜π΅)))} βŠ† {π‘₯ ∈ 𝐡 ∣ (π‘‚β€˜π‘₯) βˆ₯ ((β™―β€˜π΅) / (π‘Žβ†‘(π‘Ž pCnt (β™―β€˜π΅))))})
113111, 112sylibr 233 . . . . . . . . 9 (((πœ‘ ∧ π‘Ž ∈ 𝐴) ∧ 𝑝 ∈ (𝐴 βˆ– {π‘Ž})) β†’ {π‘₯ ∈ 𝐡 ∣ (π‘‚β€˜π‘₯) βˆ₯ (𝑝↑(𝑝 pCnt (β™―β€˜π΅)))} ∈ 𝒫 {π‘₯ ∈ 𝐡 ∣ (π‘‚β€˜π‘₯) βˆ₯ ((β™―β€˜π΅) / (π‘Žβ†‘(π‘Ž pCnt (β™―β€˜π΅))))})
11429reseq1i 5971 . . . . . . . . . 10 (𝑆 β†Ύ (𝐴 βˆ– {π‘Ž})) = ((𝑝 ∈ 𝐴 ↦ {π‘₯ ∈ 𝐡 ∣ (π‘‚β€˜π‘₯) βˆ₯ (𝑝↑(𝑝 pCnt (β™―β€˜π΅)))}) β†Ύ (𝐴 βˆ– {π‘Ž}))
115 difss 4126 . . . . . . . . . . 11 (𝐴 βˆ– {π‘Ž}) βŠ† 𝐴
116 resmpt 6031 . . . . . . . . . . 11 ((𝐴 βˆ– {π‘Ž}) βŠ† 𝐴 β†’ ((𝑝 ∈ 𝐴 ↦ {π‘₯ ∈ 𝐡 ∣ (π‘‚β€˜π‘₯) βˆ₯ (𝑝↑(𝑝 pCnt (β™―β€˜π΅)))}) β†Ύ (𝐴 βˆ– {π‘Ž})) = (𝑝 ∈ (𝐴 βˆ– {π‘Ž}) ↦ {π‘₯ ∈ 𝐡 ∣ (π‘‚β€˜π‘₯) βˆ₯ (𝑝↑(𝑝 pCnt (β™―β€˜π΅)))}))
117115, 116ax-mp 5 . . . . . . . . . 10 ((𝑝 ∈ 𝐴 ↦ {π‘₯ ∈ 𝐡 ∣ (π‘‚β€˜π‘₯) βˆ₯ (𝑝↑(𝑝 pCnt (β™―β€˜π΅)))}) β†Ύ (𝐴 βˆ– {π‘Ž})) = (𝑝 ∈ (𝐴 βˆ– {π‘Ž}) ↦ {π‘₯ ∈ 𝐡 ∣ (π‘‚β€˜π‘₯) βˆ₯ (𝑝↑(𝑝 pCnt (β™―β€˜π΅)))})
118114, 117eqtri 2754 . . . . . . . . 9 (𝑆 β†Ύ (𝐴 βˆ– {π‘Ž})) = (𝑝 ∈ (𝐴 βˆ– {π‘Ž}) ↦ {π‘₯ ∈ 𝐡 ∣ (π‘‚β€˜π‘₯) βˆ₯ (𝑝↑(𝑝 pCnt (β™―β€˜π΅)))})
119113, 118fmptd 7109 . . . . . . . 8 ((πœ‘ ∧ π‘Ž ∈ 𝐴) β†’ (𝑆 β†Ύ (𝐴 βˆ– {π‘Ž})):(𝐴 βˆ– {π‘Ž})βŸΆπ’« {π‘₯ ∈ 𝐡 ∣ (π‘‚β€˜π‘₯) βˆ₯ ((β™―β€˜π΅) / (π‘Žβ†‘(π‘Ž pCnt (β™―β€˜π΅))))})
120119frnd 6719 . . . . . . 7 ((πœ‘ ∧ π‘Ž ∈ 𝐴) β†’ ran (𝑆 β†Ύ (𝐴 βˆ– {π‘Ž})) βŠ† 𝒫 {π‘₯ ∈ 𝐡 ∣ (π‘‚β€˜π‘₯) βˆ₯ ((β™―β€˜π΅) / (π‘Žβ†‘(π‘Ž pCnt (β™―β€˜π΅))))})
12154, 120eqsstrid 4025 . . . . . 6 ((πœ‘ ∧ π‘Ž ∈ 𝐴) β†’ (𝑆 β€œ (𝐴 βˆ– {π‘Ž})) βŠ† 𝒫 {π‘₯ ∈ 𝐡 ∣ (π‘‚β€˜π‘₯) βˆ₯ ((β™―β€˜π΅) / (π‘Žβ†‘(π‘Ž pCnt (β™―β€˜π΅))))})
122 sspwuni 5096 . . . . . 6 ((𝑆 β€œ (𝐴 βˆ– {π‘Ž})) βŠ† 𝒫 {π‘₯ ∈ 𝐡 ∣ (π‘‚β€˜π‘₯) βˆ₯ ((β™―β€˜π΅) / (π‘Žβ†‘(π‘Ž pCnt (β™―β€˜π΅))))} ↔ βˆͺ (𝑆 β€œ (𝐴 βˆ– {π‘Ž})) βŠ† {π‘₯ ∈ 𝐡 ∣ (π‘‚β€˜π‘₯) βˆ₯ ((β™―β€˜π΅) / (π‘Žβ†‘(π‘Ž pCnt (β™―β€˜π΅))))})
123121, 122sylib 217 . . . . 5 ((πœ‘ ∧ π‘Ž ∈ 𝐴) β†’ βˆͺ (𝑆 β€œ (𝐴 βˆ– {π‘Ž})) βŠ† {π‘₯ ∈ 𝐡 ∣ (π‘‚β€˜π‘₯) βˆ₯ ((β™―β€˜π΅) / (π‘Žβ†‘(π‘Ž pCnt (β™―β€˜π΅))))})
12498nnzd 12589 . . . . . 6 ((πœ‘ ∧ π‘Ž ∈ 𝐴) β†’ ((β™―β€˜π΅) / (π‘Žβ†‘(π‘Ž pCnt (β™―β€˜π΅)))) ∈ β„€)
12526, 15oddvdssubg 19775 . . . . . 6 ((𝐺 ∈ Abel ∧ ((β™―β€˜π΅) / (π‘Žβ†‘(π‘Ž pCnt (β™―β€˜π΅)))) ∈ β„€) β†’ {π‘₯ ∈ 𝐡 ∣ (π‘‚β€˜π‘₯) βˆ₯ ((β™―β€˜π΅) / (π‘Žβ†‘(π‘Ž pCnt (β™―β€˜π΅))))} ∈ (SubGrpβ€˜πΊ))
12649, 124, 125syl2anc 583 . . . . 5 ((πœ‘ ∧ π‘Ž ∈ 𝐴) β†’ {π‘₯ ∈ 𝐡 ∣ (π‘‚β€˜π‘₯) βˆ₯ ((β™―β€˜π΅) / (π‘Žβ†‘(π‘Ž pCnt (β™―β€˜π΅))))} ∈ (SubGrpβ€˜πΊ))
1273mrcsscl 17573 . . . . 5 (((SubGrpβ€˜πΊ) ∈ (Mooreβ€˜(Baseβ€˜πΊ)) ∧ βˆͺ (𝑆 β€œ (𝐴 βˆ– {π‘Ž})) βŠ† {π‘₯ ∈ 𝐡 ∣ (π‘‚β€˜π‘₯) βˆ₯ ((β™―β€˜π΅) / (π‘Žβ†‘(π‘Ž pCnt (β™―β€˜π΅))))} ∧ {π‘₯ ∈ 𝐡 ∣ (π‘‚β€˜π‘₯) βˆ₯ ((β™―β€˜π΅) / (π‘Žβ†‘(π‘Ž pCnt (β™―β€˜π΅))))} ∈ (SubGrpβ€˜πΊ)) β†’ ((mrClsβ€˜(SubGrpβ€˜πΊ))β€˜βˆͺ (𝑆 β€œ (𝐴 βˆ– {π‘Ž}))) βŠ† {π‘₯ ∈ 𝐡 ∣ (π‘‚β€˜π‘₯) βˆ₯ ((β™―β€˜π΅) / (π‘Žβ†‘(π‘Ž pCnt (β™―β€˜π΅))))})
12853, 123, 126, 127syl3anc 1368 . . . 4 ((πœ‘ ∧ π‘Ž ∈ 𝐴) β†’ ((mrClsβ€˜(SubGrpβ€˜πΊ))β€˜βˆͺ (𝑆 β€œ (𝐴 βˆ– {π‘Ž}))) βŠ† {π‘₯ ∈ 𝐡 ∣ (π‘‚β€˜π‘₯) βˆ₯ ((β™―β€˜π΅) / (π‘Žβ†‘(π‘Ž pCnt (β™―β€˜π΅))))})
129 ss2in 4231 . . . 4 (((π‘†β€˜π‘Ž) βŠ† {π‘₯ ∈ 𝐡 ∣ (π‘‚β€˜π‘₯) βˆ₯ (π‘Žβ†‘(π‘Ž pCnt (β™―β€˜π΅)))} ∧ ((mrClsβ€˜(SubGrpβ€˜πΊ))β€˜βˆͺ (𝑆 β€œ (𝐴 βˆ– {π‘Ž}))) βŠ† {π‘₯ ∈ 𝐡 ∣ (π‘‚β€˜π‘₯) βˆ₯ ((β™―β€˜π΅) / (π‘Žβ†‘(π‘Ž pCnt (β™―β€˜π΅))))}) β†’ ((π‘†β€˜π‘Ž) ∩ ((mrClsβ€˜(SubGrpβ€˜πΊ))β€˜βˆͺ (𝑆 β€œ (𝐴 βˆ– {π‘Ž})))) βŠ† ({π‘₯ ∈ 𝐡 ∣ (π‘‚β€˜π‘₯) βˆ₯ (π‘Žβ†‘(π‘Ž pCnt (β™―β€˜π΅)))} ∩ {π‘₯ ∈ 𝐡 ∣ (π‘‚β€˜π‘₯) βˆ₯ ((β™―β€˜π΅) / (π‘Žβ†‘(π‘Ž pCnt (β™―β€˜π΅))))}))
13048, 128, 129syl2anc 583 . . 3 ((πœ‘ ∧ π‘Ž ∈ 𝐴) β†’ ((π‘†β€˜π‘Ž) ∩ ((mrClsβ€˜(SubGrpβ€˜πΊ))β€˜βˆͺ (𝑆 β€œ (𝐴 βˆ– {π‘Ž})))) βŠ† ({π‘₯ ∈ 𝐡 ∣ (π‘‚β€˜π‘₯) βˆ₯ (π‘Žβ†‘(π‘Ž pCnt (β™―β€˜π΅)))} ∩ {π‘₯ ∈ 𝐡 ∣ (π‘‚β€˜π‘₯) βˆ₯ ((β™―β€˜π΅) / (π‘Žβ†‘(π‘Ž pCnt (β™―β€˜π΅))))}))
131 eqid 2726 . . . . 5 {π‘₯ ∈ 𝐡 ∣ (π‘‚β€˜π‘₯) βˆ₯ (π‘Žβ†‘(π‘Ž pCnt (β™―β€˜π΅)))} = {π‘₯ ∈ 𝐡 ∣ (π‘‚β€˜π‘₯) βˆ₯ (π‘Žβ†‘(π‘Ž pCnt (β™―β€˜π΅)))}
132 eqid 2726 . . . . 5 {π‘₯ ∈ 𝐡 ∣ (π‘‚β€˜π‘₯) βˆ₯ ((β™―β€˜π΅) / (π‘Žβ†‘(π‘Ž pCnt (β™―β€˜π΅))))} = {π‘₯ ∈ 𝐡 ∣ (π‘‚β€˜π‘₯) βˆ₯ ((β™―β€˜π΅) / (π‘Žβ†‘(π‘Ž pCnt (β™―β€˜π΅))))}
13368simp2d 1140 . . . . 5 ((πœ‘ ∧ π‘Ž ∈ 𝐴) β†’ ((π‘Žβ†‘(π‘Ž pCnt (β™―β€˜π΅))) gcd ((β™―β€˜π΅) / (π‘Žβ†‘(π‘Ž pCnt (β™―β€˜π΅))))) = 1)
134 eqid 2726 . . . . 5 (LSSumβ€˜πΊ) = (LSSumβ€˜πΊ)
13515, 26, 131, 132, 49, 70, 98, 133, 95, 2, 134ablfacrp 19988 . . . 4 ((πœ‘ ∧ π‘Ž ∈ 𝐴) β†’ (({π‘₯ ∈ 𝐡 ∣ (π‘‚β€˜π‘₯) βˆ₯ (π‘Žβ†‘(π‘Ž pCnt (β™―β€˜π΅)))} ∩ {π‘₯ ∈ 𝐡 ∣ (π‘‚β€˜π‘₯) βˆ₯ ((β™―β€˜π΅) / (π‘Žβ†‘(π‘Ž pCnt (β™―β€˜π΅))))}) = {(0gβ€˜πΊ)} ∧ ({π‘₯ ∈ 𝐡 ∣ (π‘‚β€˜π‘₯) βˆ₯ (π‘Žβ†‘(π‘Ž pCnt (β™―β€˜π΅)))} (LSSumβ€˜πΊ){π‘₯ ∈ 𝐡 ∣ (π‘‚β€˜π‘₯) βˆ₯ ((β™―β€˜π΅) / (π‘Žβ†‘(π‘Ž pCnt (β™―β€˜π΅))))}) = 𝐡))
136135simpld 494 . . 3 ((πœ‘ ∧ π‘Ž ∈ 𝐴) β†’ ({π‘₯ ∈ 𝐡 ∣ (π‘‚β€˜π‘₯) βˆ₯ (π‘Žβ†‘(π‘Ž pCnt (β™―β€˜π΅)))} ∩ {π‘₯ ∈ 𝐡 ∣ (π‘‚β€˜π‘₯) βˆ₯ ((β™―β€˜π΅) / (π‘Žβ†‘(π‘Ž pCnt (β™―β€˜π΅))))}) = {(0gβ€˜πΊ)})
137130, 136sseqtrd 4017 . 2 ((πœ‘ ∧ π‘Ž ∈ 𝐴) β†’ ((π‘†β€˜π‘Ž) ∩ ((mrClsβ€˜(SubGrpβ€˜πΊ))β€˜βˆͺ (𝑆 β€œ (𝐴 βˆ– {π‘Ž})))) βŠ† {(0gβ€˜πΊ)})
1381, 2, 3, 6, 10, 30, 37, 137dmdprdd 19921 1 (πœ‘ β†’ 𝐺dom DProd 𝑆)
Colors of variables: wff setvar class
Syntax hints:   β†’ wi 4   ↔ wb 205   ∧ wa 395   ∧ w3a 1084   = wceq 1533   ∈ wcel 2098   β‰  wne 2934  {crab 3426  Vcvv 3468   βˆ– cdif 3940   ∩ cin 3942   βŠ† wss 3943  βˆ…c0 4317  π’« cpw 4597  {csn 4623  βˆͺ cuni 4902   class class class wbr 5141   ↦ cmpt 5224  dom cdm 5669  ran crn 5670   β†Ύ cres 5671   β€œ cima 5672  βŸΆwf 6533  β€˜cfv 6537  (class class class)co 7405  Fincfn 8941  0cc0 11112  1c1 11113   Β· cmul 11117   / cdiv 11875  β„•cn 12216  β„•0cn0 12476  β„€cz 12562  β†‘cexp 14032  β™―chash 14295   βˆ₯ cdvds 16204   gcd cgcd 16442  β„™cprime 16615   pCnt cpc 16778  Basecbs 17153  0gc0g 17394  Moorecmre 17535  mrClscmrc 17536  ACScacs 17538  Grpcgrp 18863  SubGrpcsubg 19047  Cntzccntz 19231  odcod 19444  LSSumclsm 19554  Abelcabl 19701   DProd cdprd 19915
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1789  ax-4 1803  ax-5 1905  ax-6 1963  ax-7 2003  ax-8 2100  ax-9 2108  ax-10 2129  ax-11 2146  ax-12 2163  ax-ext 2697  ax-rep 5278  ax-sep 5292  ax-nul 5299  ax-pow 5356  ax-pr 5420  ax-un 7722  ax-inf2 9638  ax-cnex 11168  ax-resscn 11169  ax-1cn 11170  ax-icn 11171  ax-addcl 11172  ax-addrcl 11173  ax-mulcl 11174  ax-mulrcl 11175  ax-mulcom 11176  ax-addass 11177  ax-mulass 11178  ax-distr 11179  ax-i2m1 11180  ax-1ne0 11181  ax-1rid 11182  ax-rnegex 11183  ax-rrecex 11184  ax-cnre 11185  ax-pre-lttri 11186  ax-pre-lttrn 11187  ax-pre-ltadd 11188  ax-pre-mulgt0 11189  ax-pre-sup 11190
This theorem depends on definitions:  df-bi 206  df-an 396  df-or 845  df-3or 1085  df-3an 1086  df-tru 1536  df-fal 1546  df-ex 1774  df-nf 1778  df-sb 2060  df-mo 2528  df-eu 2557  df-clab 2704  df-cleq 2718  df-clel 2804  df-nfc 2879  df-ne 2935  df-nel 3041  df-ral 3056  df-rex 3065  df-rmo 3370  df-reu 3371  df-rab 3427  df-v 3470  df-sbc 3773  df-csb 3889  df-dif 3946  df-un 3948  df-in 3950  df-ss 3960  df-pss 3962  df-nul 4318  df-if 4524  df-pw 4599  df-sn 4624  df-pr 4626  df-op 4630  df-uni 4903  df-int 4944  df-iun 4992  df-iin 4993  df-disj 5107  df-br 5142  df-opab 5204  df-mpt 5225  df-tr 5259  df-id 5567  df-eprel 5573  df-po 5581  df-so 5582  df-fr 5624  df-se 5625  df-we 5626  df-xp 5675  df-rel 5676  df-cnv 5677  df-co 5678  df-dm 5679  df-rn 5680  df-res 5681  df-ima 5682  df-pred 6294  df-ord 6361  df-on 6362  df-lim 6363  df-suc 6364  df-iota 6489  df-fun 6539  df-fn 6540  df-f 6541  df-f1 6542  df-fo 6543  df-f1o 6544  df-fv 6545  df-isom 6546  df-riota 7361  df-ov 7408  df-oprab 7409  df-mpo 7410  df-om 7853  df-1st 7974  df-2nd 7975  df-frecs 8267  df-wrecs 8298  df-recs 8372  df-rdg 8411  df-1o 8467  df-2o 8468  df-oadd 8471  df-omul 8472  df-er 8705  df-ec 8707  df-qs 8711  df-map 8824  df-ixp 8894  df-en 8942  df-dom 8943  df-sdom 8944  df-fin 8945  df-sup 9439  df-inf 9440  df-oi 9507  df-card 9936  df-acn 9939  df-pnf 11254  df-mnf 11255  df-xr 11256  df-ltxr 11257  df-le 11258  df-sub 11450  df-neg 11451  df-div 11876  df-nn 12217  df-2 12279  df-3 12280  df-n0 12477  df-z 12563  df-uz 12827  df-q 12937  df-rp 12981  df-fz 13491  df-fzo 13634  df-fl 13763  df-mod 13841  df-seq 13973  df-exp 14033  df-hash 14296  df-cj 15052  df-re 15053  df-im 15054  df-sqrt 15188  df-abs 15189  df-clim 15438  df-sum 15639  df-dvds 16205  df-gcd 16443  df-prm 16616  df-pc 16779  df-sets 17106  df-slot 17124  df-ndx 17136  df-base 17154  df-ress 17183  df-plusg 17219  df-0g 17396  df-mre 17539  df-mrc 17540  df-acs 17542  df-mgm 18573  df-sgrp 18652  df-mnd 18668  df-submnd 18714  df-grp 18866  df-minusg 18867  df-sbg 18868  df-mulg 18996  df-subg 19050  df-eqg 19052  df-cntz 19233  df-od 19448  df-lsm 19556  df-cmn 19702  df-abl 19703  df-dprd 19917
This theorem is referenced by:  ablfac1c  19993  ablfac1eu  19995  ablfaclem2  20008  ablfaclem3  20009
  Copyright terms: Public domain W3C validator