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

Theorem ablfac1eu 19853
Description: The factorization of ablfac1b 19850 is unique, in that any other factorization into prime power factors (even if the exponents are different) must be equal to ๐‘†. (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 (๐œ‘ โ†’ ๐ด โŠ† โ„™)
ablfac1c.d ๐ท = {๐‘ค โˆˆ โ„™ โˆฃ ๐‘ค โˆฅ (โ™ฏโ€˜๐ต)}
ablfac1.2 (๐œ‘ โ†’ ๐ท โŠ† ๐ด)
ablfac1eu.1 (๐œ‘ โ†’ (๐บdom DProd ๐‘‡ โˆง (๐บ DProd ๐‘‡) = ๐ต))
ablfac1eu.2 (๐œ‘ โ†’ dom ๐‘‡ = ๐ด)
ablfac1eu.3 ((๐œ‘ โˆง ๐‘ž โˆˆ ๐ด) โ†’ ๐ถ โˆˆ โ„•0)
ablfac1eu.4 ((๐œ‘ โˆง ๐‘ž โˆˆ ๐ด) โ†’ (โ™ฏโ€˜(๐‘‡โ€˜๐‘ž)) = (๐‘žโ†‘๐ถ))
Assertion
Ref Expression
ablfac1eu (๐œ‘ โ†’ ๐‘‡ = ๐‘†)
Distinct variable groups:   ๐‘ž,๐‘,๐‘ค,๐‘ฅ,๐ต   ๐ท,๐‘,๐‘ž,๐‘ฅ   ๐œ‘,๐‘,๐‘ž,๐‘ค,๐‘ฅ   ๐‘†,๐‘ž   ๐ด,๐‘,๐‘ž,๐‘ฅ   ๐‘‚,๐‘,๐‘ž,๐‘ฅ   ๐‘‡,๐‘ž,๐‘ฅ   ๐บ,๐‘,๐‘ž,๐‘ฅ
Allowed substitution hints:   ๐ด(๐‘ค)   ๐ถ(๐‘ฅ,๐‘ค,๐‘ž,๐‘)   ๐ท(๐‘ค)   ๐‘†(๐‘ฅ,๐‘ค,๐‘)   ๐‘‡(๐‘ค,๐‘)   ๐บ(๐‘ค)   ๐‘‚(๐‘ค)

Proof of Theorem ablfac1eu
Dummy variable ๐‘ฆ is distinct from all other variables.
StepHypRef Expression
1 ablfac1eu.1 . . . . 5 (๐œ‘ โ†’ (๐บdom DProd ๐‘‡ โˆง (๐บ DProd ๐‘‡) = ๐ต))
21simpld 496 . . . 4 (๐œ‘ โ†’ ๐บdom DProd ๐‘‡)
3 ablfac1eu.2 . . . 4 (๐œ‘ โ†’ dom ๐‘‡ = ๐ด)
42, 3dprdf2 19787 . . 3 (๐œ‘ โ†’ ๐‘‡:๐ดโŸถ(SubGrpโ€˜๐บ))
54ffnd 6670 . 2 (๐œ‘ โ†’ ๐‘‡ Fn ๐ด)
6 ablfac1.b . . . . 5 ๐ต = (Baseโ€˜๐บ)
7 ablfac1.o . . . . 5 ๐‘‚ = (odโ€˜๐บ)
8 ablfac1.s . . . . 5 ๐‘† = (๐‘ โˆˆ ๐ด โ†ฆ {๐‘ฅ โˆˆ ๐ต โˆฃ (๐‘‚โ€˜๐‘ฅ) โˆฅ (๐‘โ†‘(๐‘ pCnt (โ™ฏโ€˜๐ต)))})
9 ablfac1.g . . . . 5 (๐œ‘ โ†’ ๐บ โˆˆ Abel)
10 ablfac1.f . . . . 5 (๐œ‘ โ†’ ๐ต โˆˆ Fin)
11 ablfac1.1 . . . . 5 (๐œ‘ โ†’ ๐ด โŠ† โ„™)
126, 7, 8, 9, 10, 11ablfac1b 19850 . . . 4 (๐œ‘ โ†’ ๐บdom DProd ๐‘†)
136fvexi 6857 . . . . . . 7 ๐ต โˆˆ V
1413rabex 5290 . . . . . 6 {๐‘ฅ โˆˆ ๐ต โˆฃ (๐‘‚โ€˜๐‘ฅ) โˆฅ (๐‘โ†‘(๐‘ pCnt (โ™ฏโ€˜๐ต)))} โˆˆ V
1514, 8dmmpti 6646 . . . . 5 dom ๐‘† = ๐ด
1615a1i 11 . . . 4 (๐œ‘ โ†’ dom ๐‘† = ๐ด)
1712, 16dprdf2 19787 . . 3 (๐œ‘ โ†’ ๐‘†:๐ดโŸถ(SubGrpโ€˜๐บ))
1817ffnd 6670 . 2 (๐œ‘ โ†’ ๐‘† Fn ๐ด)
1910adantr 482 . . . 4 ((๐œ‘ โˆง ๐‘ž โˆˆ ๐ด) โ†’ ๐ต โˆˆ Fin)
2017ffvelcdmda 7036 . . . . 5 ((๐œ‘ โˆง ๐‘ž โˆˆ ๐ด) โ†’ (๐‘†โ€˜๐‘ž) โˆˆ (SubGrpโ€˜๐บ))
216subgss 18930 . . . . 5 ((๐‘†โ€˜๐‘ž) โˆˆ (SubGrpโ€˜๐บ) โ†’ (๐‘†โ€˜๐‘ž) โŠ† ๐ต)
2220, 21syl 17 . . . 4 ((๐œ‘ โˆง ๐‘ž โˆˆ ๐ด) โ†’ (๐‘†โ€˜๐‘ž) โŠ† ๐ต)
2319, 22ssfid 9212 . . 3 ((๐œ‘ โˆง ๐‘ž โˆˆ ๐ด) โ†’ (๐‘†โ€˜๐‘ž) โˆˆ Fin)
244ffvelcdmda 7036 . . . . . 6 ((๐œ‘ โˆง ๐‘ž โˆˆ ๐ด) โ†’ (๐‘‡โ€˜๐‘ž) โˆˆ (SubGrpโ€˜๐บ))
256subgss 18930 . . . . . 6 ((๐‘‡โ€˜๐‘ž) โˆˆ (SubGrpโ€˜๐บ) โ†’ (๐‘‡โ€˜๐‘ž) โŠ† ๐ต)
2624, 25syl 17 . . . . 5 ((๐œ‘ โˆง ๐‘ž โˆˆ ๐ด) โ†’ (๐‘‡โ€˜๐‘ž) โŠ† ๐ต)
2726sselda 3945 . . . . . . . 8 (((๐œ‘ โˆง ๐‘ž โˆˆ ๐ด) โˆง ๐‘ฅ โˆˆ (๐‘‡โ€˜๐‘ž)) โ†’ ๐‘ฅ โˆˆ ๐ต)
286, 7odcl 19319 . . . . . . . 8 (๐‘ฅ โˆˆ ๐ต โ†’ (๐‘‚โ€˜๐‘ฅ) โˆˆ โ„•0)
2927, 28syl 17 . . . . . . 7 (((๐œ‘ โˆง ๐‘ž โˆˆ ๐ด) โˆง ๐‘ฅ โˆˆ (๐‘‡โ€˜๐‘ž)) โ†’ (๐‘‚โ€˜๐‘ฅ) โˆˆ โ„•0)
3029nn0zd 12526 . . . . . 6 (((๐œ‘ โˆง ๐‘ž โˆˆ ๐ด) โˆง ๐‘ฅ โˆˆ (๐‘‡โ€˜๐‘ž)) โ†’ (๐‘‚โ€˜๐‘ฅ) โˆˆ โ„ค)
3119, 26ssfid 9212 . . . . . . . . 9 ((๐œ‘ โˆง ๐‘ž โˆˆ ๐ด) โ†’ (๐‘‡โ€˜๐‘ž) โˆˆ Fin)
32 hashcl 14257 . . . . . . . . 9 ((๐‘‡โ€˜๐‘ž) โˆˆ Fin โ†’ (โ™ฏโ€˜(๐‘‡โ€˜๐‘ž)) โˆˆ โ„•0)
3331, 32syl 17 . . . . . . . 8 ((๐œ‘ โˆง ๐‘ž โˆˆ ๐ด) โ†’ (โ™ฏโ€˜(๐‘‡โ€˜๐‘ž)) โˆˆ โ„•0)
3433nn0zd 12526 . . . . . . 7 ((๐œ‘ โˆง ๐‘ž โˆˆ ๐ด) โ†’ (โ™ฏโ€˜(๐‘‡โ€˜๐‘ž)) โˆˆ โ„ค)
3534adantr 482 . . . . . 6 (((๐œ‘ โˆง ๐‘ž โˆˆ ๐ด) โˆง ๐‘ฅ โˆˆ (๐‘‡โ€˜๐‘ž)) โ†’ (โ™ฏโ€˜(๐‘‡โ€˜๐‘ž)) โˆˆ โ„ค)
3611sselda 3945 . . . . . . . . . 10 ((๐œ‘ โˆง ๐‘ž โˆˆ ๐ด) โ†’ ๐‘ž โˆˆ โ„™)
37 prmnn 16551 . . . . . . . . . 10 (๐‘ž โˆˆ โ„™ โ†’ ๐‘ž โˆˆ โ„•)
3836, 37syl 17 . . . . . . . . 9 ((๐œ‘ โˆง ๐‘ž โˆˆ ๐ด) โ†’ ๐‘ž โˆˆ โ„•)
39 ablgrp 19568 . . . . . . . . . . . . . 14 (๐บ โˆˆ Abel โ†’ ๐บ โˆˆ Grp)
409, 39syl 17 . . . . . . . . . . . . 13 (๐œ‘ โ†’ ๐บ โˆˆ Grp)
416grpbn0 18780 . . . . . . . . . . . . 13 (๐บ โˆˆ Grp โ†’ ๐ต โ‰  โˆ…)
4240, 41syl 17 . . . . . . . . . . . 12 (๐œ‘ โ†’ ๐ต โ‰  โˆ…)
43 hashnncl 14267 . . . . . . . . . . . . 13 (๐ต โˆˆ Fin โ†’ ((โ™ฏโ€˜๐ต) โˆˆ โ„• โ†” ๐ต โ‰  โˆ…))
4410, 43syl 17 . . . . . . . . . . . 12 (๐œ‘ โ†’ ((โ™ฏโ€˜๐ต) โˆˆ โ„• โ†” ๐ต โ‰  โˆ…))
4542, 44mpbird 257 . . . . . . . . . . 11 (๐œ‘ โ†’ (โ™ฏโ€˜๐ต) โˆˆ โ„•)
4645adantr 482 . . . . . . . . . 10 ((๐œ‘ โˆง ๐‘ž โˆˆ ๐ด) โ†’ (โ™ฏโ€˜๐ต) โˆˆ โ„•)
4736, 46pccld 16723 . . . . . . . . 9 ((๐œ‘ โˆง ๐‘ž โˆˆ ๐ด) โ†’ (๐‘ž pCnt (โ™ฏโ€˜๐ต)) โˆˆ โ„•0)
4838, 47nnexpcld 14149 . . . . . . . 8 ((๐œ‘ โˆง ๐‘ž โˆˆ ๐ด) โ†’ (๐‘žโ†‘(๐‘ž pCnt (โ™ฏโ€˜๐ต))) โˆˆ โ„•)
4948nnzd 12527 . . . . . . 7 ((๐œ‘ โˆง ๐‘ž โˆˆ ๐ด) โ†’ (๐‘žโ†‘(๐‘ž pCnt (โ™ฏโ€˜๐ต))) โˆˆ โ„ค)
5049adantr 482 . . . . . 6 (((๐œ‘ โˆง ๐‘ž โˆˆ ๐ด) โˆง ๐‘ฅ โˆˆ (๐‘‡โ€˜๐‘ž)) โ†’ (๐‘žโ†‘(๐‘ž pCnt (โ™ฏโ€˜๐ต))) โˆˆ โ„ค)
5124adantr 482 . . . . . . 7 (((๐œ‘ โˆง ๐‘ž โˆˆ ๐ด) โˆง ๐‘ฅ โˆˆ (๐‘‡โ€˜๐‘ž)) โ†’ (๐‘‡โ€˜๐‘ž) โˆˆ (SubGrpโ€˜๐บ))
5231adantr 482 . . . . . . 7 (((๐œ‘ โˆง ๐‘ž โˆˆ ๐ด) โˆง ๐‘ฅ โˆˆ (๐‘‡โ€˜๐‘ž)) โ†’ (๐‘‡โ€˜๐‘ž) โˆˆ Fin)
53 simpr 486 . . . . . . 7 (((๐œ‘ โˆง ๐‘ž โˆˆ ๐ด) โˆง ๐‘ฅ โˆˆ (๐‘‡โ€˜๐‘ž)) โ†’ ๐‘ฅ โˆˆ (๐‘‡โ€˜๐‘ž))
547odsubdvds 19354 . . . . . . 7 (((๐‘‡โ€˜๐‘ž) โˆˆ (SubGrpโ€˜๐บ) โˆง (๐‘‡โ€˜๐‘ž) โˆˆ Fin โˆง ๐‘ฅ โˆˆ (๐‘‡โ€˜๐‘ž)) โ†’ (๐‘‚โ€˜๐‘ฅ) โˆฅ (โ™ฏโ€˜(๐‘‡โ€˜๐‘ž)))
5551, 52, 53, 54syl3anc 1372 . . . . . 6 (((๐œ‘ โˆง ๐‘ž โˆˆ ๐ด) โˆง ๐‘ฅ โˆˆ (๐‘‡โ€˜๐‘ž)) โ†’ (๐‘‚โ€˜๐‘ฅ) โˆฅ (โ™ฏโ€˜(๐‘‡โ€˜๐‘ž)))
56 ablfac1eu.4 . . . . . . . 8 ((๐œ‘ โˆง ๐‘ž โˆˆ ๐ด) โ†’ (โ™ฏโ€˜(๐‘‡โ€˜๐‘ž)) = (๐‘žโ†‘๐ถ))
57 prmz 16552 . . . . . . . . . 10 (๐‘ž โˆˆ โ„™ โ†’ ๐‘ž โˆˆ โ„ค)
5836, 57syl 17 . . . . . . . . 9 ((๐œ‘ โˆง ๐‘ž โˆˆ ๐ด) โ†’ ๐‘ž โˆˆ โ„ค)
59 ablfac1eu.3 . . . . . . . . 9 ((๐œ‘ โˆง ๐‘ž โˆˆ ๐ด) โ†’ ๐ถ โˆˆ โ„•0)
6059nn0zd 12526 . . . . . . . . . 10 ((๐œ‘ โˆง ๐‘ž โˆˆ ๐ด) โ†’ ๐ถ โˆˆ โ„ค)
6147nn0zd 12526 . . . . . . . . . 10 ((๐œ‘ โˆง ๐‘ž โˆˆ ๐ด) โ†’ (๐‘ž pCnt (โ™ฏโ€˜๐ต)) โˆˆ โ„ค)
626lagsubg 18993 . . . . . . . . . . . . 13 (((๐‘‡โ€˜๐‘ž) โˆˆ (SubGrpโ€˜๐บ) โˆง ๐ต โˆˆ Fin) โ†’ (โ™ฏโ€˜(๐‘‡โ€˜๐‘ž)) โˆฅ (โ™ฏโ€˜๐ต))
6324, 19, 62syl2anc 585 . . . . . . . . . . . 12 ((๐œ‘ โˆง ๐‘ž โˆˆ ๐ด) โ†’ (โ™ฏโ€˜(๐‘‡โ€˜๐‘ž)) โˆฅ (โ™ฏโ€˜๐ต))
6456, 63eqbrtrrd 5130 . . . . . . . . . . 11 ((๐œ‘ โˆง ๐‘ž โˆˆ ๐ด) โ†’ (๐‘žโ†‘๐ถ) โˆฅ (โ™ฏโ€˜๐ต))
6546nnzd 12527 . . . . . . . . . . . 12 ((๐œ‘ โˆง ๐‘ž โˆˆ ๐ด) โ†’ (โ™ฏโ€˜๐ต) โˆˆ โ„ค)
66 pcdvdsb 16742 . . . . . . . . . . . 12 ((๐‘ž โˆˆ โ„™ โˆง (โ™ฏโ€˜๐ต) โˆˆ โ„ค โˆง ๐ถ โˆˆ โ„•0) โ†’ (๐ถ โ‰ค (๐‘ž pCnt (โ™ฏโ€˜๐ต)) โ†” (๐‘žโ†‘๐ถ) โˆฅ (โ™ฏโ€˜๐ต)))
6736, 65, 59, 66syl3anc 1372 . . . . . . . . . . 11 ((๐œ‘ โˆง ๐‘ž โˆˆ ๐ด) โ†’ (๐ถ โ‰ค (๐‘ž pCnt (โ™ฏโ€˜๐ต)) โ†” (๐‘žโ†‘๐ถ) โˆฅ (โ™ฏโ€˜๐ต)))
6864, 67mpbird 257 . . . . . . . . . 10 ((๐œ‘ โˆง ๐‘ž โˆˆ ๐ด) โ†’ ๐ถ โ‰ค (๐‘ž pCnt (โ™ฏโ€˜๐ต)))
69 eluz2 12770 . . . . . . . . . 10 ((๐‘ž pCnt (โ™ฏโ€˜๐ต)) โˆˆ (โ„คโ‰ฅโ€˜๐ถ) โ†” (๐ถ โˆˆ โ„ค โˆง (๐‘ž pCnt (โ™ฏโ€˜๐ต)) โˆˆ โ„ค โˆง ๐ถ โ‰ค (๐‘ž pCnt (โ™ฏโ€˜๐ต))))
7060, 61, 68, 69syl3anbrc 1344 . . . . . . . . 9 ((๐œ‘ โˆง ๐‘ž โˆˆ ๐ด) โ†’ (๐‘ž pCnt (โ™ฏโ€˜๐ต)) โˆˆ (โ„คโ‰ฅโ€˜๐ถ))
71 dvdsexp 16211 . . . . . . . . 9 ((๐‘ž โˆˆ โ„ค โˆง ๐ถ โˆˆ โ„•0 โˆง (๐‘ž pCnt (โ™ฏโ€˜๐ต)) โˆˆ (โ„คโ‰ฅโ€˜๐ถ)) โ†’ (๐‘žโ†‘๐ถ) โˆฅ (๐‘žโ†‘(๐‘ž pCnt (โ™ฏโ€˜๐ต))))
7258, 59, 70, 71syl3anc 1372 . . . . . . . 8 ((๐œ‘ โˆง ๐‘ž โˆˆ ๐ด) โ†’ (๐‘žโ†‘๐ถ) โˆฅ (๐‘žโ†‘(๐‘ž pCnt (โ™ฏโ€˜๐ต))))
7356, 72eqbrtrd 5128 . . . . . . 7 ((๐œ‘ โˆง ๐‘ž โˆˆ ๐ด) โ†’ (โ™ฏโ€˜(๐‘‡โ€˜๐‘ž)) โˆฅ (๐‘žโ†‘(๐‘ž pCnt (โ™ฏโ€˜๐ต))))
7473adantr 482 . . . . . 6 (((๐œ‘ โˆง ๐‘ž โˆˆ ๐ด) โˆง ๐‘ฅ โˆˆ (๐‘‡โ€˜๐‘ž)) โ†’ (โ™ฏโ€˜(๐‘‡โ€˜๐‘ž)) โˆฅ (๐‘žโ†‘(๐‘ž pCnt (โ™ฏโ€˜๐ต))))
7530, 35, 50, 55, 74dvdstrd 16178 . . . . 5 (((๐œ‘ โˆง ๐‘ž โˆˆ ๐ด) โˆง ๐‘ฅ โˆˆ (๐‘‡โ€˜๐‘ž)) โ†’ (๐‘‚โ€˜๐‘ฅ) โˆฅ (๐‘žโ†‘(๐‘ž pCnt (โ™ฏโ€˜๐ต))))
7626, 75ssrabdv 4032 . . . 4 ((๐œ‘ โˆง ๐‘ž โˆˆ ๐ด) โ†’ (๐‘‡โ€˜๐‘ž) โŠ† {๐‘ฅ โˆˆ ๐ต โˆฃ (๐‘‚โ€˜๐‘ฅ) โˆฅ (๐‘žโ†‘(๐‘ž pCnt (โ™ฏโ€˜๐ต)))})
77 id 22 . . . . . . . . 9 (๐‘ = ๐‘ž โ†’ ๐‘ = ๐‘ž)
78 oveq1 7365 . . . . . . . . 9 (๐‘ = ๐‘ž โ†’ (๐‘ pCnt (โ™ฏโ€˜๐ต)) = (๐‘ž pCnt (โ™ฏโ€˜๐ต)))
7977, 78oveq12d 7376 . . . . . . . 8 (๐‘ = ๐‘ž โ†’ (๐‘โ†‘(๐‘ pCnt (โ™ฏโ€˜๐ต))) = (๐‘žโ†‘(๐‘ž pCnt (โ™ฏโ€˜๐ต))))
8079breq2d 5118 . . . . . . 7 (๐‘ = ๐‘ž โ†’ ((๐‘‚โ€˜๐‘ฅ) โˆฅ (๐‘โ†‘(๐‘ pCnt (โ™ฏโ€˜๐ต))) โ†” (๐‘‚โ€˜๐‘ฅ) โˆฅ (๐‘žโ†‘(๐‘ž pCnt (โ™ฏโ€˜๐ต)))))
8180rabbidv 3416 . . . . . 6 (๐‘ = ๐‘ž โ†’ {๐‘ฅ โˆˆ ๐ต โˆฃ (๐‘‚โ€˜๐‘ฅ) โˆฅ (๐‘โ†‘(๐‘ pCnt (โ™ฏโ€˜๐ต)))} = {๐‘ฅ โˆˆ ๐ต โˆฃ (๐‘‚โ€˜๐‘ฅ) โˆฅ (๐‘žโ†‘(๐‘ž pCnt (โ™ฏโ€˜๐ต)))})
8281, 8, 14fvmpt3i 6954 . . . . 5 (๐‘ž โˆˆ ๐ด โ†’ (๐‘†โ€˜๐‘ž) = {๐‘ฅ โˆˆ ๐ต โˆฃ (๐‘‚โ€˜๐‘ฅ) โˆฅ (๐‘žโ†‘(๐‘ž pCnt (โ™ฏโ€˜๐ต)))})
8382adantl 483 . . . 4 ((๐œ‘ โˆง ๐‘ž โˆˆ ๐ด) โ†’ (๐‘†โ€˜๐‘ž) = {๐‘ฅ โˆˆ ๐ต โˆฃ (๐‘‚โ€˜๐‘ฅ) โˆฅ (๐‘žโ†‘(๐‘ž pCnt (โ™ฏโ€˜๐ต)))})
8476, 83sseqtrrd 3986 . . 3 ((๐œ‘ โˆง ๐‘ž โˆˆ ๐ด) โ†’ (๐‘‡โ€˜๐‘ž) โŠ† (๐‘†โ€˜๐‘ž))
8548nnnn0d 12474 . . . . . 6 ((๐œ‘ โˆง ๐‘ž โˆˆ ๐ด) โ†’ (๐‘žโ†‘(๐‘ž pCnt (โ™ฏโ€˜๐ต))) โˆˆ โ„•0)
86 pcdvds 16737 . . . . . . . . . 10 ((๐‘ž โˆˆ โ„™ โˆง (โ™ฏโ€˜๐ต) โˆˆ โ„•) โ†’ (๐‘žโ†‘(๐‘ž pCnt (โ™ฏโ€˜๐ต))) โˆฅ (โ™ฏโ€˜๐ต))
8736, 46, 86syl2anc 585 . . . . . . . . 9 ((๐œ‘ โˆง ๐‘ž โˆˆ ๐ด) โ†’ (๐‘žโ†‘(๐‘ž pCnt (โ™ฏโ€˜๐ต))) โˆฅ (โ™ฏโ€˜๐ต))
882adantr 482 . . . . . . . . . . . . . . 15 ((๐œ‘ โˆง ๐‘ž โˆˆ ๐ด) โ†’ ๐บdom DProd ๐‘‡)
893adantr 482 . . . . . . . . . . . . . . 15 ((๐œ‘ โˆง ๐‘ž โˆˆ ๐ด) โ†’ dom ๐‘‡ = ๐ด)
90 ablfac1.2 . . . . . . . . . . . . . . . 16 (๐œ‘ โ†’ ๐ท โŠ† ๐ด)
9190adantr 482 . . . . . . . . . . . . . . 15 ((๐œ‘ โˆง ๐‘ž โˆˆ ๐ด) โ†’ ๐ท โŠ† ๐ด)
9288, 89, 91dprdres 19808 . . . . . . . . . . . . . 14 ((๐œ‘ โˆง ๐‘ž โˆˆ ๐ด) โ†’ (๐บdom DProd (๐‘‡ โ†พ ๐ท) โˆง (๐บ DProd (๐‘‡ โ†พ ๐ท)) โŠ† (๐บ DProd ๐‘‡)))
9392simpld 496 . . . . . . . . . . . . 13 ((๐œ‘ โˆง ๐‘ž โˆˆ ๐ด) โ†’ ๐บdom DProd (๐‘‡ โ†พ ๐ท))
944adantr 482 . . . . . . . . . . . . . . 15 ((๐œ‘ โˆง ๐‘ž โˆˆ ๐ด) โ†’ ๐‘‡:๐ดโŸถ(SubGrpโ€˜๐บ))
9594, 91fssresd 6710 . . . . . . . . . . . . . 14 ((๐œ‘ โˆง ๐‘ž โˆˆ ๐ด) โ†’ (๐‘‡ โ†พ ๐ท):๐ทโŸถ(SubGrpโ€˜๐บ))
9695fdmd 6680 . . . . . . . . . . . . 13 ((๐œ‘ โˆง ๐‘ž โˆˆ ๐ด) โ†’ dom (๐‘‡ โ†พ ๐ท) = ๐ท)
97 difssd 4093 . . . . . . . . . . . . 13 ((๐œ‘ โˆง ๐‘ž โˆˆ ๐ด) โ†’ (๐ท โˆ– {๐‘ž}) โŠ† ๐ท)
9893, 96, 97dprdres 19808 . . . . . . . . . . . 12 ((๐œ‘ โˆง ๐‘ž โˆˆ ๐ด) โ†’ (๐บdom DProd ((๐‘‡ โ†พ ๐ท) โ†พ (๐ท โˆ– {๐‘ž})) โˆง (๐บ DProd ((๐‘‡ โ†พ ๐ท) โ†พ (๐ท โˆ– {๐‘ž}))) โŠ† (๐บ DProd (๐‘‡ โ†พ ๐ท))))
9998simpld 496 . . . . . . . . . . 11 ((๐œ‘ โˆง ๐‘ž โˆˆ ๐ด) โ†’ ๐บdom DProd ((๐‘‡ โ†พ ๐ท) โ†พ (๐ท โˆ– {๐‘ž})))
100 dprdsubg 19804 . . . . . . . . . . 11 (๐บdom DProd ((๐‘‡ โ†พ ๐ท) โ†พ (๐ท โˆ– {๐‘ž})) โ†’ (๐บ DProd ((๐‘‡ โ†พ ๐ท) โ†พ (๐ท โˆ– {๐‘ž}))) โˆˆ (SubGrpโ€˜๐บ))
10199, 100syl 17 . . . . . . . . . 10 ((๐œ‘ โˆง ๐‘ž โˆˆ ๐ด) โ†’ (๐บ DProd ((๐‘‡ โ†พ ๐ท) โ†พ (๐ท โˆ– {๐‘ž}))) โˆˆ (SubGrpโ€˜๐บ))
1026lagsubg 18993 . . . . . . . . . 10 (((๐บ DProd ((๐‘‡ โ†พ ๐ท) โ†พ (๐ท โˆ– {๐‘ž}))) โˆˆ (SubGrpโ€˜๐บ) โˆง ๐ต โˆˆ Fin) โ†’ (โ™ฏโ€˜(๐บ DProd ((๐‘‡ โ†พ ๐ท) โ†พ (๐ท โˆ– {๐‘ž})))) โˆฅ (โ™ฏโ€˜๐ต))
103101, 19, 102syl2anc 585 . . . . . . . . 9 ((๐œ‘ โˆง ๐‘ž โˆˆ ๐ด) โ†’ (โ™ฏโ€˜(๐บ DProd ((๐‘‡ โ†พ ๐ท) โ†พ (๐ท โˆ– {๐‘ž})))) โˆฅ (โ™ฏโ€˜๐ต))
104 eqid 2737 . . . . . . . . . . . . . . 15 (0gโ€˜๐บ) = (0gโ€˜๐บ)
105104subg0cl 18937 . . . . . . . . . . . . . 14 ((๐บ DProd ((๐‘‡ โ†พ ๐ท) โ†พ (๐ท โˆ– {๐‘ž}))) โˆˆ (SubGrpโ€˜๐บ) โ†’ (0gโ€˜๐บ) โˆˆ (๐บ DProd ((๐‘‡ โ†พ ๐ท) โ†พ (๐ท โˆ– {๐‘ž}))))
106101, 105syl 17 . . . . . . . . . . . . 13 ((๐œ‘ โˆง ๐‘ž โˆˆ ๐ด) โ†’ (0gโ€˜๐บ) โˆˆ (๐บ DProd ((๐‘‡ โ†พ ๐ท) โ†พ (๐ท โˆ– {๐‘ž}))))
107106ne0d 4296 . . . . . . . . . . . 12 ((๐œ‘ โˆง ๐‘ž โˆˆ ๐ด) โ†’ (๐บ DProd ((๐‘‡ โ†พ ๐ท) โ†พ (๐ท โˆ– {๐‘ž}))) โ‰  โˆ…)
1086dprdssv 19796 . . . . . . . . . . . . . 14 (๐บ DProd ((๐‘‡ โ†พ ๐ท) โ†พ (๐ท โˆ– {๐‘ž}))) โŠ† ๐ต
109 ssfi 9118 . . . . . . . . . . . . . 14 ((๐ต โˆˆ Fin โˆง (๐บ DProd ((๐‘‡ โ†พ ๐ท) โ†พ (๐ท โˆ– {๐‘ž}))) โŠ† ๐ต) โ†’ (๐บ DProd ((๐‘‡ โ†พ ๐ท) โ†พ (๐ท โˆ– {๐‘ž}))) โˆˆ Fin)
11019, 108, 109sylancl 587 . . . . . . . . . . . . 13 ((๐œ‘ โˆง ๐‘ž โˆˆ ๐ด) โ†’ (๐บ DProd ((๐‘‡ โ†พ ๐ท) โ†พ (๐ท โˆ– {๐‘ž}))) โˆˆ Fin)
111 hashnncl 14267 . . . . . . . . . . . . 13 ((๐บ DProd ((๐‘‡ โ†พ ๐ท) โ†พ (๐ท โˆ– {๐‘ž}))) โˆˆ Fin โ†’ ((โ™ฏโ€˜(๐บ DProd ((๐‘‡ โ†พ ๐ท) โ†พ (๐ท โˆ– {๐‘ž})))) โˆˆ โ„• โ†” (๐บ DProd ((๐‘‡ โ†พ ๐ท) โ†พ (๐ท โˆ– {๐‘ž}))) โ‰  โˆ…))
112110, 111syl 17 . . . . . . . . . . . 12 ((๐œ‘ โˆง ๐‘ž โˆˆ ๐ด) โ†’ ((โ™ฏโ€˜(๐บ DProd ((๐‘‡ โ†พ ๐ท) โ†พ (๐ท โˆ– {๐‘ž})))) โˆˆ โ„• โ†” (๐บ DProd ((๐‘‡ โ†พ ๐ท) โ†พ (๐ท โˆ– {๐‘ž}))) โ‰  โˆ…))
113107, 112mpbird 257 . . . . . . . . . . 11 ((๐œ‘ โˆง ๐‘ž โˆˆ ๐ด) โ†’ (โ™ฏโ€˜(๐บ DProd ((๐‘‡ โ†พ ๐ท) โ†พ (๐ท โˆ– {๐‘ž})))) โˆˆ โ„•)
114113nnzd 12527 . . . . . . . . . 10 ((๐œ‘ โˆง ๐‘ž โˆˆ ๐ด) โ†’ (โ™ฏโ€˜(๐บ DProd ((๐‘‡ โ†พ ๐ท) โ†พ (๐ท โˆ– {๐‘ž})))) โˆˆ โ„ค)
115 id 22 . . . . . . . . . . . . . . 15 (๐‘ฅ = ๐‘ž โ†’ ๐‘ฅ = ๐‘ž)
116 sneq 4597 . . . . . . . . . . . . . . . . . . 19 (๐‘ฅ = ๐‘ž โ†’ {๐‘ฅ} = {๐‘ž})
117116difeq2d 4083 . . . . . . . . . . . . . . . . . 18 (๐‘ฅ = ๐‘ž โ†’ (๐ท โˆ– {๐‘ฅ}) = (๐ท โˆ– {๐‘ž}))
118117reseq2d 5938 . . . . . . . . . . . . . . . . 17 (๐‘ฅ = ๐‘ž โ†’ ((๐‘‡ โ†พ ๐ท) โ†พ (๐ท โˆ– {๐‘ฅ})) = ((๐‘‡ โ†พ ๐ท) โ†พ (๐ท โˆ– {๐‘ž})))
119118oveq2d 7374 . . . . . . . . . . . . . . . 16 (๐‘ฅ = ๐‘ž โ†’ (๐บ DProd ((๐‘‡ โ†พ ๐ท) โ†พ (๐ท โˆ– {๐‘ฅ}))) = (๐บ DProd ((๐‘‡ โ†พ ๐ท) โ†พ (๐ท โˆ– {๐‘ž}))))
120119fveq2d 6847 . . . . . . . . . . . . . . 15 (๐‘ฅ = ๐‘ž โ†’ (โ™ฏโ€˜(๐บ DProd ((๐‘‡ โ†พ ๐ท) โ†พ (๐ท โˆ– {๐‘ฅ})))) = (โ™ฏโ€˜(๐บ DProd ((๐‘‡ โ†พ ๐ท) โ†พ (๐ท โˆ– {๐‘ž})))))
121115, 120breq12d 5119 . . . . . . . . . . . . . 14 (๐‘ฅ = ๐‘ž โ†’ (๐‘ฅ โˆฅ (โ™ฏโ€˜(๐บ DProd ((๐‘‡ โ†พ ๐ท) โ†พ (๐ท โˆ– {๐‘ฅ})))) โ†” ๐‘ž โˆฅ (โ™ฏโ€˜(๐บ DProd ((๐‘‡ โ†พ ๐ท) โ†พ (๐ท โˆ– {๐‘ž}))))))
122121notbid 318 . . . . . . . . . . . . 13 (๐‘ฅ = ๐‘ž โ†’ (ยฌ ๐‘ฅ โˆฅ (โ™ฏโ€˜(๐บ DProd ((๐‘‡ โ†พ ๐ท) โ†พ (๐ท โˆ– {๐‘ฅ})))) โ†” ยฌ ๐‘ž โˆฅ (โ™ฏโ€˜(๐บ DProd ((๐‘‡ โ†พ ๐ท) โ†พ (๐ท โˆ– {๐‘ž}))))))
123 eqid 2737 . . . . . . . . . . . . . . . 16 (๐‘ โˆˆ ๐ท โ†ฆ {๐‘ฆ โˆˆ ๐ต โˆฃ (๐‘‚โ€˜๐‘ฆ) โˆฅ (๐‘โ†‘(๐‘ pCnt (โ™ฏโ€˜๐ต)))}) = (๐‘ โˆˆ ๐ท โ†ฆ {๐‘ฆ โˆˆ ๐ต โˆฃ (๐‘‚โ€˜๐‘ฆ) โˆฅ (๐‘โ†‘(๐‘ pCnt (โ™ฏโ€˜๐ต)))})
1249adantr 482 . . . . . . . . . . . . . . . 16 ((๐œ‘ โˆง ๐‘ฅ โˆˆ โ„™) โ†’ ๐บ โˆˆ Abel)
12510adantr 482 . . . . . . . . . . . . . . . 16 ((๐œ‘ โˆง ๐‘ฅ โˆˆ โ„™) โ†’ ๐ต โˆˆ Fin)
126 ablfac1c.d . . . . . . . . . . . . . . . . . 18 ๐ท = {๐‘ค โˆˆ โ„™ โˆฃ ๐‘ค โˆฅ (โ™ฏโ€˜๐ต)}
127126ssrab3 4041 . . . . . . . . . . . . . . . . 17 ๐ท โŠ† โ„™
128127a1i 11 . . . . . . . . . . . . . . . 16 ((๐œ‘ โˆง ๐‘ฅ โˆˆ โ„™) โ†’ ๐ท โŠ† โ„™)
129 ssidd 3968 . . . . . . . . . . . . . . . 16 ((๐œ‘ โˆง ๐‘ฅ โˆˆ โ„™) โ†’ ๐ท โŠ† ๐ท)
1302, 3, 90dprdres 19808 . . . . . . . . . . . . . . . . . . 19 (๐œ‘ โ†’ (๐บdom DProd (๐‘‡ โ†พ ๐ท) โˆง (๐บ DProd (๐‘‡ โ†พ ๐ท)) โŠ† (๐บ DProd ๐‘‡)))
131130simpld 496 . . . . . . . . . . . . . . . . . 18 (๐œ‘ โ†’ ๐บdom DProd (๐‘‡ โ†พ ๐ท))
132 dprdsubg 19804 . . . . . . . . . . . . . . . . . . . . 21 (๐บdom DProd (๐‘‡ โ†พ ๐ท) โ†’ (๐บ DProd (๐‘‡ โ†พ ๐ท)) โˆˆ (SubGrpโ€˜๐บ))
133131, 132syl 17 . . . . . . . . . . . . . . . . . . . 20 (๐œ‘ โ†’ (๐บ DProd (๐‘‡ โ†พ ๐ท)) โˆˆ (SubGrpโ€˜๐บ))
134 difssd 4093 . . . . . . . . . . . . . . . . . . . . . . 23 (๐œ‘ โ†’ (๐ด โˆ– ๐ท) โŠ† ๐ด)
1352, 3, 134dprdres 19808 . . . . . . . . . . . . . . . . . . . . . 22 (๐œ‘ โ†’ (๐บdom DProd (๐‘‡ โ†พ (๐ด โˆ– ๐ท)) โˆง (๐บ DProd (๐‘‡ โ†พ (๐ด โˆ– ๐ท))) โŠ† (๐บ DProd ๐‘‡)))
136135simpld 496 . . . . . . . . . . . . . . . . . . . . 21 (๐œ‘ โ†’ ๐บdom DProd (๐‘‡ โ†พ (๐ด โˆ– ๐ท)))
137 dprdsubg 19804 . . . . . . . . . . . . . . . . . . . . 21 (๐บdom DProd (๐‘‡ โ†พ (๐ด โˆ– ๐ท)) โ†’ (๐บ DProd (๐‘‡ โ†พ (๐ด โˆ– ๐ท))) โˆˆ (SubGrpโ€˜๐บ))
138136, 137syl 17 . . . . . . . . . . . . . . . . . . . 20 (๐œ‘ โ†’ (๐บ DProd (๐‘‡ โ†พ (๐ด โˆ– ๐ท))) โˆˆ (SubGrpโ€˜๐บ))
139 difss 4092 . . . . . . . . . . . . . . . . . . . . . . 23 (๐ด โˆ– ๐ท) โŠ† ๐ด
140 fssres 6709 . . . . . . . . . . . . . . . . . . . . . . 23 ((๐‘‡:๐ดโŸถ(SubGrpโ€˜๐บ) โˆง (๐ด โˆ– ๐ท) โŠ† ๐ด) โ†’ (๐‘‡ โ†พ (๐ด โˆ– ๐ท)):(๐ด โˆ– ๐ท)โŸถ(SubGrpโ€˜๐บ))
1414, 139, 140sylancl 587 . . . . . . . . . . . . . . . . . . . . . 22 (๐œ‘ โ†’ (๐‘‡ โ†พ (๐ด โˆ– ๐ท)):(๐ด โˆ– ๐ท)โŸถ(SubGrpโ€˜๐บ))
142141fdmd 6680 . . . . . . . . . . . . . . . . . . . . 21 (๐œ‘ โ†’ dom (๐‘‡ โ†พ (๐ด โˆ– ๐ท)) = (๐ด โˆ– ๐ท))
143 fvres 6862 . . . . . . . . . . . . . . . . . . . . . . 23 (๐‘ž โˆˆ (๐ด โˆ– ๐ท) โ†’ ((๐‘‡ โ†พ (๐ด โˆ– ๐ท))โ€˜๐‘ž) = (๐‘‡โ€˜๐‘ž))
144143adantl 483 . . . . . . . . . . . . . . . . . . . . . 22 ((๐œ‘ โˆง ๐‘ž โˆˆ (๐ด โˆ– ๐ท)) โ†’ ((๐‘‡ โ†พ (๐ด โˆ– ๐ท))โ€˜๐‘ž) = (๐‘‡โ€˜๐‘ž))
145 eldif 3921 . . . . . . . . . . . . . . . . . . . . . . 23 (๐‘ž โˆˆ (๐ด โˆ– ๐ท) โ†” (๐‘ž โˆˆ ๐ด โˆง ยฌ ๐‘ž โˆˆ ๐ท))
14631adantrr 716 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((๐œ‘ โˆง (๐‘ž โˆˆ ๐ด โˆง ยฌ ๐‘ž โˆˆ ๐ท)) โ†’ (๐‘‡โ€˜๐‘ž) โˆˆ Fin)
147104subg0cl 18937 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((๐‘‡โ€˜๐‘ž) โˆˆ (SubGrpโ€˜๐บ) โ†’ (0gโ€˜๐บ) โˆˆ (๐‘‡โ€˜๐‘ž))
14824, 147syl 17 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((๐œ‘ โˆง ๐‘ž โˆˆ ๐ด) โ†’ (0gโ€˜๐บ) โˆˆ (๐‘‡โ€˜๐‘ž))
149148snssd 4770 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((๐œ‘ โˆง ๐‘ž โˆˆ ๐ด) โ†’ {(0gโ€˜๐บ)} โŠ† (๐‘‡โ€˜๐‘ž))
150149adantrr 716 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((๐œ‘ โˆง (๐‘ž โˆˆ ๐ด โˆง ยฌ ๐‘ž โˆˆ ๐ท)) โ†’ {(0gโ€˜๐บ)} โŠ† (๐‘‡โ€˜๐‘ž))
151 fvex 6856 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (0gโ€˜๐บ) โˆˆ V
152 hashsng 14270 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((0gโ€˜๐บ) โˆˆ V โ†’ (โ™ฏโ€˜{(0gโ€˜๐บ)}) = 1)
153151, 152ax-mp 5 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (โ™ฏโ€˜{(0gโ€˜๐บ)}) = 1
15456adantrr 716 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((๐œ‘ โˆง (๐‘ž โˆˆ ๐ด โˆง ยฌ ๐‘ž โˆˆ ๐ท)) โ†’ (โ™ฏโ€˜(๐‘‡โ€˜๐‘ž)) = (๐‘žโ†‘๐ถ))
15536adantr 482 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 (((๐œ‘ โˆง ๐‘ž โˆˆ ๐ด) โˆง ๐ถ โˆˆ โ„•) โ†’ ๐‘ž โˆˆ โ„™)
156 iddvdsexp 16163 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 ((๐‘ž โˆˆ โ„ค โˆง ๐ถ โˆˆ โ„•) โ†’ ๐‘ž โˆฅ (๐‘žโ†‘๐ถ))
15758, 156sylan 581 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 (((๐œ‘ โˆง ๐‘ž โˆˆ ๐ด) โˆง ๐ถ โˆˆ โ„•) โ†’ ๐‘ž โˆฅ (๐‘žโ†‘๐ถ))
15864adantr 482 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 (((๐œ‘ โˆง ๐‘ž โˆˆ ๐ด) โˆง ๐ถ โˆˆ โ„•) โ†’ (๐‘žโ†‘๐ถ) โˆฅ (โ™ฏโ€˜๐ต))
15956, 34eqeltrrd 2839 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 ((๐œ‘ โˆง ๐‘ž โˆˆ ๐ด) โ†’ (๐‘žโ†‘๐ถ) โˆˆ โ„ค)
160 dvdstr 16177 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 ((๐‘ž โˆˆ โ„ค โˆง (๐‘žโ†‘๐ถ) โˆˆ โ„ค โˆง (โ™ฏโ€˜๐ต) โˆˆ โ„ค) โ†’ ((๐‘ž โˆฅ (๐‘žโ†‘๐ถ) โˆง (๐‘žโ†‘๐ถ) โˆฅ (โ™ฏโ€˜๐ต)) โ†’ ๐‘ž โˆฅ (โ™ฏโ€˜๐ต)))
16158, 159, 65, 160syl3anc 1372 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 ((๐œ‘ โˆง ๐‘ž โˆˆ ๐ด) โ†’ ((๐‘ž โˆฅ (๐‘žโ†‘๐ถ) โˆง (๐‘žโ†‘๐ถ) โˆฅ (โ™ฏโ€˜๐ต)) โ†’ ๐‘ž โˆฅ (โ™ฏโ€˜๐ต)))
162161adantr 482 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 (((๐œ‘ โˆง ๐‘ž โˆˆ ๐ด) โˆง ๐ถ โˆˆ โ„•) โ†’ ((๐‘ž โˆฅ (๐‘žโ†‘๐ถ) โˆง (๐‘žโ†‘๐ถ) โˆฅ (โ™ฏโ€˜๐ต)) โ†’ ๐‘ž โˆฅ (โ™ฏโ€˜๐ต)))
163157, 158, 162mp2and 698 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 (((๐œ‘ โˆง ๐‘ž โˆˆ ๐ด) โˆง ๐ถ โˆˆ โ„•) โ†’ ๐‘ž โˆฅ (โ™ฏโ€˜๐ต))
164 breq1 5109 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 (๐‘ค = ๐‘ž โ†’ (๐‘ค โˆฅ (โ™ฏโ€˜๐ต) โ†” ๐‘ž โˆฅ (โ™ฏโ€˜๐ต)))
165164, 126elrab2 3649 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 (๐‘ž โˆˆ ๐ท โ†” (๐‘ž โˆˆ โ„™ โˆง ๐‘ž โˆฅ (โ™ฏโ€˜๐ต)))
166155, 163, 165sylanbrc 584 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 (((๐œ‘ โˆง ๐‘ž โˆˆ ๐ด) โˆง ๐ถ โˆˆ โ„•) โ†’ ๐‘ž โˆˆ ๐ท)
167166ex 414 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ((๐œ‘ โˆง ๐‘ž โˆˆ ๐ด) โ†’ (๐ถ โˆˆ โ„• โ†’ ๐‘ž โˆˆ ๐ท))
168167con3d 152 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ((๐œ‘ โˆง ๐‘ž โˆˆ ๐ด) โ†’ (ยฌ ๐‘ž โˆˆ ๐ท โ†’ ยฌ ๐ถ โˆˆ โ„•))
169168impr 456 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ((๐œ‘ โˆง (๐‘ž โˆˆ ๐ด โˆง ยฌ ๐‘ž โˆˆ ๐ท)) โ†’ ยฌ ๐ถ โˆˆ โ„•)
17059adantrr 716 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ((๐œ‘ โˆง (๐‘ž โˆˆ ๐ด โˆง ยฌ ๐‘ž โˆˆ ๐ท)) โ†’ ๐ถ โˆˆ โ„•0)
171 elnn0 12416 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 (๐ถ โˆˆ โ„•0 โ†” (๐ถ โˆˆ โ„• โˆจ ๐ถ = 0))
172170, 171sylib 217 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ((๐œ‘ โˆง (๐‘ž โˆˆ ๐ด โˆง ยฌ ๐‘ž โˆˆ ๐ท)) โ†’ (๐ถ โˆˆ โ„• โˆจ ๐ถ = 0))
173172ord 863 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ((๐œ‘ โˆง (๐‘ž โˆˆ ๐ด โˆง ยฌ ๐‘ž โˆˆ ๐ท)) โ†’ (ยฌ ๐ถ โˆˆ โ„• โ†’ ๐ถ = 0))
174169, 173mpd 15 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ((๐œ‘ โˆง (๐‘ž โˆˆ ๐ด โˆง ยฌ ๐‘ž โˆˆ ๐ท)) โ†’ ๐ถ = 0)
175174oveq2d 7374 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((๐œ‘ โˆง (๐‘ž โˆˆ ๐ด โˆง ยฌ ๐‘ž โˆˆ ๐ท)) โ†’ (๐‘žโ†‘๐ถ) = (๐‘žโ†‘0))
17638adantrr 716 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ((๐œ‘ โˆง (๐‘ž โˆˆ ๐ด โˆง ยฌ ๐‘ž โˆˆ ๐ท)) โ†’ ๐‘ž โˆˆ โ„•)
177176nncnd 12170 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ((๐œ‘ โˆง (๐‘ž โˆˆ ๐ด โˆง ยฌ ๐‘ž โˆˆ ๐ท)) โ†’ ๐‘ž โˆˆ โ„‚)
178177exp0d 14046 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((๐œ‘ โˆง (๐‘ž โˆˆ ๐ด โˆง ยฌ ๐‘ž โˆˆ ๐ท)) โ†’ (๐‘žโ†‘0) = 1)
179154, 175, 1783eqtrd 2781 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((๐œ‘ โˆง (๐‘ž โˆˆ ๐ด โˆง ยฌ ๐‘ž โˆˆ ๐ท)) โ†’ (โ™ฏโ€˜(๐‘‡โ€˜๐‘ž)) = 1)
180153, 179eqtr4id 2796 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((๐œ‘ โˆง (๐‘ž โˆˆ ๐ด โˆง ยฌ ๐‘ž โˆˆ ๐ท)) โ†’ (โ™ฏโ€˜{(0gโ€˜๐บ)}) = (โ™ฏโ€˜(๐‘‡โ€˜๐‘ž)))
181 snfi 8989 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 {(0gโ€˜๐บ)} โˆˆ Fin
182 hashen 14248 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (({(0gโ€˜๐บ)} โˆˆ Fin โˆง (๐‘‡โ€˜๐‘ž) โˆˆ Fin) โ†’ ((โ™ฏโ€˜{(0gโ€˜๐บ)}) = (โ™ฏโ€˜(๐‘‡โ€˜๐‘ž)) โ†” {(0gโ€˜๐บ)} โ‰ˆ (๐‘‡โ€˜๐‘ž)))
183181, 146, 182sylancr 588 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((๐œ‘ โˆง (๐‘ž โˆˆ ๐ด โˆง ยฌ ๐‘ž โˆˆ ๐ท)) โ†’ ((โ™ฏโ€˜{(0gโ€˜๐บ)}) = (โ™ฏโ€˜(๐‘‡โ€˜๐‘ž)) โ†” {(0gโ€˜๐บ)} โ‰ˆ (๐‘‡โ€˜๐‘ž)))
184180, 183mpbid 231 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((๐œ‘ โˆง (๐‘ž โˆˆ ๐ด โˆง ยฌ ๐‘ž โˆˆ ๐ท)) โ†’ {(0gโ€˜๐บ)} โ‰ˆ (๐‘‡โ€˜๐‘ž))
185 fisseneq 9202 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((๐‘‡โ€˜๐‘ž) โˆˆ Fin โˆง {(0gโ€˜๐บ)} โŠ† (๐‘‡โ€˜๐‘ž) โˆง {(0gโ€˜๐บ)} โ‰ˆ (๐‘‡โ€˜๐‘ž)) โ†’ {(0gโ€˜๐บ)} = (๐‘‡โ€˜๐‘ž))
186146, 150, 184, 185syl3anc 1372 . . . . . . . . . . . . . . . . . . . . . . . 24 ((๐œ‘ โˆง (๐‘ž โˆˆ ๐ด โˆง ยฌ ๐‘ž โˆˆ ๐ท)) โ†’ {(0gโ€˜๐บ)} = (๐‘‡โ€˜๐‘ž))
187104subg0cl 18937 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((๐บ DProd (๐‘‡ โ†พ ๐ท)) โˆˆ (SubGrpโ€˜๐บ) โ†’ (0gโ€˜๐บ) โˆˆ (๐บ DProd (๐‘‡ โ†พ ๐ท)))
188133, 187syl 17 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (๐œ‘ โ†’ (0gโ€˜๐บ) โˆˆ (๐บ DProd (๐‘‡ โ†พ ๐ท)))
189188adantr 482 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((๐œ‘ โˆง (๐‘ž โˆˆ ๐ด โˆง ยฌ ๐‘ž โˆˆ ๐ท)) โ†’ (0gโ€˜๐บ) โˆˆ (๐บ DProd (๐‘‡ โ†พ ๐ท)))
190189snssd 4770 . . . . . . . . . . . . . . . . . . . . . . . 24 ((๐œ‘ โˆง (๐‘ž โˆˆ ๐ด โˆง ยฌ ๐‘ž โˆˆ ๐ท)) โ†’ {(0gโ€˜๐บ)} โŠ† (๐บ DProd (๐‘‡ โ†พ ๐ท)))
191186, 190eqsstrrd 3984 . . . . . . . . . . . . . . . . . . . . . . 23 ((๐œ‘ โˆง (๐‘ž โˆˆ ๐ด โˆง ยฌ ๐‘ž โˆˆ ๐ท)) โ†’ (๐‘‡โ€˜๐‘ž) โŠ† (๐บ DProd (๐‘‡ โ†พ ๐ท)))
192145, 191sylan2b 595 . . . . . . . . . . . . . . . . . . . . . 22 ((๐œ‘ โˆง ๐‘ž โˆˆ (๐ด โˆ– ๐ท)) โ†’ (๐‘‡โ€˜๐‘ž) โŠ† (๐บ DProd (๐‘‡ โ†พ ๐ท)))
193144, 192eqsstrd 3983 . . . . . . . . . . . . . . . . . . . . 21 ((๐œ‘ โˆง ๐‘ž โˆˆ (๐ด โˆ– ๐ท)) โ†’ ((๐‘‡ โ†พ (๐ด โˆ– ๐ท))โ€˜๐‘ž) โŠ† (๐บ DProd (๐‘‡ โ†พ ๐ท)))
194136, 142, 133, 193dprdlub 19806 . . . . . . . . . . . . . . . . . . . 20 (๐œ‘ โ†’ (๐บ DProd (๐‘‡ โ†พ (๐ด โˆ– ๐ท))) โŠ† (๐บ DProd (๐‘‡ โ†พ ๐ท)))
195 eqid 2737 . . . . . . . . . . . . . . . . . . . . 21 (LSSumโ€˜๐บ) = (LSSumโ€˜๐บ)
196195lsmss2 19450 . . . . . . . . . . . . . . . . . . . 20 (((๐บ DProd (๐‘‡ โ†พ ๐ท)) โˆˆ (SubGrpโ€˜๐บ) โˆง (๐บ DProd (๐‘‡ โ†พ (๐ด โˆ– ๐ท))) โˆˆ (SubGrpโ€˜๐บ) โˆง (๐บ DProd (๐‘‡ โ†พ (๐ด โˆ– ๐ท))) โŠ† (๐บ DProd (๐‘‡ โ†พ ๐ท))) โ†’ ((๐บ DProd (๐‘‡ โ†พ ๐ท))(LSSumโ€˜๐บ)(๐บ DProd (๐‘‡ โ†พ (๐ด โˆ– ๐ท)))) = (๐บ DProd (๐‘‡ โ†พ ๐ท)))
197133, 138, 194, 196syl3anc 1372 . . . . . . . . . . . . . . . . . . 19 (๐œ‘ โ†’ ((๐บ DProd (๐‘‡ โ†พ ๐ท))(LSSumโ€˜๐บ)(๐บ DProd (๐‘‡ โ†พ (๐ด โˆ– ๐ท)))) = (๐บ DProd (๐‘‡ โ†พ ๐ท)))
198 disjdif 4432 . . . . . . . . . . . . . . . . . . . . . 22 (๐ท โˆฉ (๐ด โˆ– ๐ท)) = โˆ…
199198a1i 11 . . . . . . . . . . . . . . . . . . . . 21 (๐œ‘ โ†’ (๐ท โˆฉ (๐ด โˆ– ๐ท)) = โˆ…)
200 undif2 4437 . . . . . . . . . . . . . . . . . . . . . 22 (๐ท โˆช (๐ด โˆ– ๐ท)) = (๐ท โˆช ๐ด)
201 ssequn1 4141 . . . . . . . . . . . . . . . . . . . . . . 23 (๐ท โŠ† ๐ด โ†” (๐ท โˆช ๐ด) = ๐ด)
20290, 201sylib 217 . . . . . . . . . . . . . . . . . . . . . 22 (๐œ‘ โ†’ (๐ท โˆช ๐ด) = ๐ด)
203200, 202eqtr2id 2790 . . . . . . . . . . . . . . . . . . . . 21 (๐œ‘ โ†’ ๐ด = (๐ท โˆช (๐ด โˆ– ๐ท)))
2044, 199, 203, 195, 2dprdsplit 19828 . . . . . . . . . . . . . . . . . . . 20 (๐œ‘ โ†’ (๐บ DProd ๐‘‡) = ((๐บ DProd (๐‘‡ โ†พ ๐ท))(LSSumโ€˜๐บ)(๐บ DProd (๐‘‡ โ†พ (๐ด โˆ– ๐ท)))))
2051simprd 497 . . . . . . . . . . . . . . . . . . . 20 (๐œ‘ โ†’ (๐บ DProd ๐‘‡) = ๐ต)
206204, 205eqtr3d 2779 . . . . . . . . . . . . . . . . . . 19 (๐œ‘ โ†’ ((๐บ DProd (๐‘‡ โ†พ ๐ท))(LSSumโ€˜๐บ)(๐บ DProd (๐‘‡ โ†พ (๐ด โˆ– ๐ท)))) = ๐ต)
207197, 206eqtr3d 2779 . . . . . . . . . . . . . . . . . 18 (๐œ‘ โ†’ (๐บ DProd (๐‘‡ โ†พ ๐ท)) = ๐ต)
208131, 207jca 513 . . . . . . . . . . . . . . . . 17 (๐œ‘ โ†’ (๐บdom DProd (๐‘‡ โ†พ ๐ท) โˆง (๐บ DProd (๐‘‡ โ†พ ๐ท)) = ๐ต))
209208adantr 482 . . . . . . . . . . . . . . . 16 ((๐œ‘ โˆง ๐‘ฅ โˆˆ โ„™) โ†’ (๐บdom DProd (๐‘‡ โ†พ ๐ท) โˆง (๐บ DProd (๐‘‡ โ†พ ๐ท)) = ๐ต))
2104, 90fssresd 6710 . . . . . . . . . . . . . . . . . 18 (๐œ‘ โ†’ (๐‘‡ โ†พ ๐ท):๐ทโŸถ(SubGrpโ€˜๐บ))
211210fdmd 6680 . . . . . . . . . . . . . . . . 17 (๐œ‘ โ†’ dom (๐‘‡ โ†พ ๐ท) = ๐ท)
212211adantr 482 . . . . . . . . . . . . . . . 16 ((๐œ‘ โˆง ๐‘ฅ โˆˆ โ„™) โ†’ dom (๐‘‡ โ†พ ๐ท) = ๐ท)
21390sselda 3945 . . . . . . . . . . . . . . . . . 18 ((๐œ‘ โˆง ๐‘ž โˆˆ ๐ท) โ†’ ๐‘ž โˆˆ ๐ด)
214213, 59syldan 592 . . . . . . . . . . . . . . . . 17 ((๐œ‘ โˆง ๐‘ž โˆˆ ๐ท) โ†’ ๐ถ โˆˆ โ„•0)
215214adantlr 714 . . . . . . . . . . . . . . . 16 (((๐œ‘ โˆง ๐‘ฅ โˆˆ โ„™) โˆง ๐‘ž โˆˆ ๐ท) โ†’ ๐ถ โˆˆ โ„•0)
216 fvres 6862 . . . . . . . . . . . . . . . . . . . 20 (๐‘ž โˆˆ ๐ท โ†’ ((๐‘‡ โ†พ ๐ท)โ€˜๐‘ž) = (๐‘‡โ€˜๐‘ž))
217216adantl 483 . . . . . . . . . . . . . . . . . . 19 ((๐œ‘ โˆง ๐‘ž โˆˆ ๐ท) โ†’ ((๐‘‡ โ†พ ๐ท)โ€˜๐‘ž) = (๐‘‡โ€˜๐‘ž))
218217fveq2d 6847 . . . . . . . . . . . . . . . . . 18 ((๐œ‘ โˆง ๐‘ž โˆˆ ๐ท) โ†’ (โ™ฏโ€˜((๐‘‡ โ†พ ๐ท)โ€˜๐‘ž)) = (โ™ฏโ€˜(๐‘‡โ€˜๐‘ž)))
219213, 56syldan 592 . . . . . . . . . . . . . . . . . 18 ((๐œ‘ โˆง ๐‘ž โˆˆ ๐ท) โ†’ (โ™ฏโ€˜(๐‘‡โ€˜๐‘ž)) = (๐‘žโ†‘๐ถ))
220218, 219eqtrd 2777 . . . . . . . . . . . . . . . . 17 ((๐œ‘ โˆง ๐‘ž โˆˆ ๐ท) โ†’ (โ™ฏโ€˜((๐‘‡ โ†พ ๐ท)โ€˜๐‘ž)) = (๐‘žโ†‘๐ถ))
221220adantlr 714 . . . . . . . . . . . . . . . 16 (((๐œ‘ โˆง ๐‘ฅ โˆˆ โ„™) โˆง ๐‘ž โˆˆ ๐ท) โ†’ (โ™ฏโ€˜((๐‘‡ โ†พ ๐ท)โ€˜๐‘ž)) = (๐‘žโ†‘๐ถ))
222 simpr 486 . . . . . . . . . . . . . . . 16 ((๐œ‘ โˆง ๐‘ฅ โˆˆ โ„™) โ†’ ๐‘ฅ โˆˆ โ„™)
223 fzfid 13879 . . . . . . . . . . . . . . . . . 18 (๐œ‘ โ†’ (1...(โ™ฏโ€˜๐ต)) โˆˆ Fin)
224 prmnn 16551 . . . . . . . . . . . . . . . . . . . . . 22 (๐‘ค โˆˆ โ„™ โ†’ ๐‘ค โˆˆ โ„•)
2252243ad2ant2 1135 . . . . . . . . . . . . . . . . . . . . 21 ((๐œ‘ โˆง ๐‘ค โˆˆ โ„™ โˆง ๐‘ค โˆฅ (โ™ฏโ€˜๐ต)) โ†’ ๐‘ค โˆˆ โ„•)
226 prmz 16552 . . . . . . . . . . . . . . . . . . . . . . 23 (๐‘ค โˆˆ โ„™ โ†’ ๐‘ค โˆˆ โ„ค)
227 dvdsle 16193 . . . . . . . . . . . . . . . . . . . . . . 23 ((๐‘ค โˆˆ โ„ค โˆง (โ™ฏโ€˜๐ต) โˆˆ โ„•) โ†’ (๐‘ค โˆฅ (โ™ฏโ€˜๐ต) โ†’ ๐‘ค โ‰ค (โ™ฏโ€˜๐ต)))
228226, 45, 227syl2anr 598 . . . . . . . . . . . . . . . . . . . . . 22 ((๐œ‘ โˆง ๐‘ค โˆˆ โ„™) โ†’ (๐‘ค โˆฅ (โ™ฏโ€˜๐ต) โ†’ ๐‘ค โ‰ค (โ™ฏโ€˜๐ต)))
2292283impia 1118 . . . . . . . . . . . . . . . . . . . . 21 ((๐œ‘ โˆง ๐‘ค โˆˆ โ„™ โˆง ๐‘ค โˆฅ (โ™ฏโ€˜๐ต)) โ†’ ๐‘ค โ‰ค (โ™ฏโ€˜๐ต))
23045nnzd 12527 . . . . . . . . . . . . . . . . . . . . . . 23 (๐œ‘ โ†’ (โ™ฏโ€˜๐ต) โˆˆ โ„ค)
2312303ad2ant1 1134 . . . . . . . . . . . . . . . . . . . . . 22 ((๐œ‘ โˆง ๐‘ค โˆˆ โ„™ โˆง ๐‘ค โˆฅ (โ™ฏโ€˜๐ต)) โ†’ (โ™ฏโ€˜๐ต) โˆˆ โ„ค)
232 fznn 13510 . . . . . . . . . . . . . . . . . . . . . 22 ((โ™ฏโ€˜๐ต) โˆˆ โ„ค โ†’ (๐‘ค โˆˆ (1...(โ™ฏโ€˜๐ต)) โ†” (๐‘ค โˆˆ โ„• โˆง ๐‘ค โ‰ค (โ™ฏโ€˜๐ต))))
233231, 232syl 17 . . . . . . . . . . . . . . . . . . . . 21 ((๐œ‘ โˆง ๐‘ค โˆˆ โ„™ โˆง ๐‘ค โˆฅ (โ™ฏโ€˜๐ต)) โ†’ (๐‘ค โˆˆ (1...(โ™ฏโ€˜๐ต)) โ†” (๐‘ค โˆˆ โ„• โˆง ๐‘ค โ‰ค (โ™ฏโ€˜๐ต))))
234225, 229, 233mpbir2and 712 . . . . . . . . . . . . . . . . . . . 20 ((๐œ‘ โˆง ๐‘ค โˆˆ โ„™ โˆง ๐‘ค โˆฅ (โ™ฏโ€˜๐ต)) โ†’ ๐‘ค โˆˆ (1...(โ™ฏโ€˜๐ต)))
235234rabssdv 4033 . . . . . . . . . . . . . . . . . . 19 (๐œ‘ โ†’ {๐‘ค โˆˆ โ„™ โˆฃ ๐‘ค โˆฅ (โ™ฏโ€˜๐ต)} โŠ† (1...(โ™ฏโ€˜๐ต)))
236126, 235eqsstrid 3993 . . . . . . . . . . . . . . . . . 18 (๐œ‘ โ†’ ๐ท โŠ† (1...(โ™ฏโ€˜๐ต)))
237223, 236ssfid 9212 . . . . . . . . . . . . . . . . 17 (๐œ‘ โ†’ ๐ท โˆˆ Fin)
238237adantr 482 . . . . . . . . . . . . . . . 16 ((๐œ‘ โˆง ๐‘ฅ โˆˆ โ„™) โ†’ ๐ท โˆˆ Fin)
2396, 7, 123, 124, 125, 128, 126, 129, 209, 212, 215, 221, 222, 238ablfac1eulem 19852 . . . . . . . . . . . . . . 15 ((๐œ‘ โˆง ๐‘ฅ โˆˆ โ„™) โ†’ ยฌ ๐‘ฅ โˆฅ (โ™ฏโ€˜(๐บ DProd ((๐‘‡ โ†พ ๐ท) โ†พ (๐ท โˆ– {๐‘ฅ})))))
240239ralrimiva 3144 . . . . . . . . . . . . . 14 (๐œ‘ โ†’ โˆ€๐‘ฅ โˆˆ โ„™ ยฌ ๐‘ฅ โˆฅ (โ™ฏโ€˜(๐บ DProd ((๐‘‡ โ†พ ๐ท) โ†พ (๐ท โˆ– {๐‘ฅ})))))
241240adantr 482 . . . . . . . . . . . . 13 ((๐œ‘ โˆง ๐‘ž โˆˆ ๐ด) โ†’ โˆ€๐‘ฅ โˆˆ โ„™ ยฌ ๐‘ฅ โˆฅ (โ™ฏโ€˜(๐บ DProd ((๐‘‡ โ†พ ๐ท) โ†พ (๐ท โˆ– {๐‘ฅ})))))
242122, 241, 36rspcdva 3583 . . . . . . . . . . . 12 ((๐œ‘ โˆง ๐‘ž โˆˆ ๐ด) โ†’ ยฌ ๐‘ž โˆฅ (โ™ฏโ€˜(๐บ DProd ((๐‘‡ โ†พ ๐ท) โ†พ (๐ท โˆ– {๐‘ž})))))
243 coprm 16588 . . . . . . . . . . . . 13 ((๐‘ž โˆˆ โ„™ โˆง (โ™ฏโ€˜(๐บ DProd ((๐‘‡ โ†พ ๐ท) โ†พ (๐ท โˆ– {๐‘ž})))) โˆˆ โ„ค) โ†’ (ยฌ ๐‘ž โˆฅ (โ™ฏโ€˜(๐บ DProd ((๐‘‡ โ†พ ๐ท) โ†พ (๐ท โˆ– {๐‘ž})))) โ†” (๐‘ž gcd (โ™ฏโ€˜(๐บ DProd ((๐‘‡ โ†พ ๐ท) โ†พ (๐ท โˆ– {๐‘ž}))))) = 1))
24436, 114, 243syl2anc 585 . . . . . . . . . . . 12 ((๐œ‘ โˆง ๐‘ž โˆˆ ๐ด) โ†’ (ยฌ ๐‘ž โˆฅ (โ™ฏโ€˜(๐บ DProd ((๐‘‡ โ†พ ๐ท) โ†พ (๐ท โˆ– {๐‘ž})))) โ†” (๐‘ž gcd (โ™ฏโ€˜(๐บ DProd ((๐‘‡ โ†พ ๐ท) โ†พ (๐ท โˆ– {๐‘ž}))))) = 1))
245242, 244mpbid 231 . . . . . . . . . . 11 ((๐œ‘ โˆง ๐‘ž โˆˆ ๐ด) โ†’ (๐‘ž gcd (โ™ฏโ€˜(๐บ DProd ((๐‘‡ โ†พ ๐ท) โ†พ (๐ท โˆ– {๐‘ž}))))) = 1)
246 rpexp1i 16600 . . . . . . . . . . . 12 ((๐‘ž โˆˆ โ„ค โˆง (โ™ฏโ€˜(๐บ DProd ((๐‘‡ โ†พ ๐ท) โ†พ (๐ท โˆ– {๐‘ž})))) โˆˆ โ„ค โˆง (๐‘ž pCnt (โ™ฏโ€˜๐ต)) โˆˆ โ„•0) โ†’ ((๐‘ž gcd (โ™ฏโ€˜(๐บ DProd ((๐‘‡ โ†พ ๐ท) โ†พ (๐ท โˆ– {๐‘ž}))))) = 1 โ†’ ((๐‘žโ†‘(๐‘ž pCnt (โ™ฏโ€˜๐ต))) gcd (โ™ฏโ€˜(๐บ DProd ((๐‘‡ โ†พ ๐ท) โ†พ (๐ท โˆ– {๐‘ž}))))) = 1))
24758, 114, 47, 246syl3anc 1372 . . . . . . . . . . 11 ((๐œ‘ โˆง ๐‘ž โˆˆ ๐ด) โ†’ ((๐‘ž gcd (โ™ฏโ€˜(๐บ DProd ((๐‘‡ โ†พ ๐ท) โ†พ (๐ท โˆ– {๐‘ž}))))) = 1 โ†’ ((๐‘žโ†‘(๐‘ž pCnt (โ™ฏโ€˜๐ต))) gcd (โ™ฏโ€˜(๐บ DProd ((๐‘‡ โ†พ ๐ท) โ†พ (๐ท โˆ– {๐‘ž}))))) = 1))
248245, 247mpd 15 . . . . . . . . . 10 ((๐œ‘ โˆง ๐‘ž โˆˆ ๐ด) โ†’ ((๐‘žโ†‘(๐‘ž pCnt (โ™ฏโ€˜๐ต))) gcd (โ™ฏโ€˜(๐บ DProd ((๐‘‡ โ†พ ๐ท) โ†พ (๐ท โˆ– {๐‘ž}))))) = 1)
249 coprmdvds2 16531 . . . . . . . . . 10 ((((๐‘žโ†‘(๐‘ž pCnt (โ™ฏโ€˜๐ต))) โˆˆ โ„ค โˆง (โ™ฏโ€˜(๐บ DProd ((๐‘‡ โ†พ ๐ท) โ†พ (๐ท โˆ– {๐‘ž})))) โˆˆ โ„ค โˆง (โ™ฏโ€˜๐ต) โˆˆ โ„ค) โˆง ((๐‘žโ†‘(๐‘ž pCnt (โ™ฏโ€˜๐ต))) gcd (โ™ฏโ€˜(๐บ DProd ((๐‘‡ โ†พ ๐ท) โ†พ (๐ท โˆ– {๐‘ž}))))) = 1) โ†’ (((๐‘žโ†‘(๐‘ž pCnt (โ™ฏโ€˜๐ต))) โˆฅ (โ™ฏโ€˜๐ต) โˆง (โ™ฏโ€˜(๐บ DProd ((๐‘‡ โ†พ ๐ท) โ†พ (๐ท โˆ– {๐‘ž})))) โˆฅ (โ™ฏโ€˜๐ต)) โ†’ ((๐‘žโ†‘(๐‘ž pCnt (โ™ฏโ€˜๐ต))) ยท (โ™ฏโ€˜(๐บ DProd ((๐‘‡ โ†พ ๐ท) โ†พ (๐ท โˆ– {๐‘ž}))))) โˆฅ (โ™ฏโ€˜๐ต)))
25049, 114, 65, 248, 249syl31anc 1374 . . . . . . . . 9 ((๐œ‘ โˆง ๐‘ž โˆˆ ๐ด) โ†’ (((๐‘žโ†‘(๐‘ž pCnt (โ™ฏโ€˜๐ต))) โˆฅ (โ™ฏโ€˜๐ต) โˆง (โ™ฏโ€˜(๐บ DProd ((๐‘‡ โ†พ ๐ท) โ†พ (๐ท โˆ– {๐‘ž})))) โˆฅ (โ™ฏโ€˜๐ต)) โ†’ ((๐‘žโ†‘(๐‘ž pCnt (โ™ฏโ€˜๐ต))) ยท (โ™ฏโ€˜(๐บ DProd ((๐‘‡ โ†พ ๐ท) โ†พ (๐ท โˆ– {๐‘ž}))))) โˆฅ (โ™ฏโ€˜๐ต)))
25187, 103, 250mp2and 698 . . . . . . . 8 ((๐œ‘ โˆง ๐‘ž โˆˆ ๐ด) โ†’ ((๐‘žโ†‘(๐‘ž pCnt (โ™ฏโ€˜๐ต))) ยท (โ™ฏโ€˜(๐บ DProd ((๐‘‡ โ†พ ๐ท) โ†พ (๐ท โˆ– {๐‘ž}))))) โˆฅ (โ™ฏโ€˜๐ต))
252 eqid 2737 . . . . . . . . . 10 (Cntzโ€˜๐บ) = (Cntzโ€˜๐บ)
253 inss1 4189 . . . . . . . . . . . . . 14 (๐ท โˆฉ {๐‘ž}) โŠ† ๐ท
254253a1i 11 . . . . . . . . . . . . 13 ((๐œ‘ โˆง ๐‘ž โˆˆ ๐ด) โ†’ (๐ท โˆฉ {๐‘ž}) โŠ† ๐ท)
25593, 96, 254dprdres 19808 . . . . . . . . . . . 12 ((๐œ‘ โˆง ๐‘ž โˆˆ ๐ด) โ†’ (๐บdom DProd ((๐‘‡ โ†พ ๐ท) โ†พ (๐ท โˆฉ {๐‘ž})) โˆง (๐บ DProd ((๐‘‡ โ†พ ๐ท) โ†พ (๐ท โˆฉ {๐‘ž}))) โŠ† (๐บ DProd (๐‘‡ โ†พ ๐ท))))
256255simpld 496 . . . . . . . . . . 11 ((๐œ‘ โˆง ๐‘ž โˆˆ ๐ด) โ†’ ๐บdom DProd ((๐‘‡ โ†พ ๐ท) โ†พ (๐ท โˆฉ {๐‘ž})))
257 dprdsubg 19804 . . . . . . . . . . 11 (๐บdom DProd ((๐‘‡ โ†พ ๐ท) โ†พ (๐ท โˆฉ {๐‘ž})) โ†’ (๐บ DProd ((๐‘‡ โ†พ ๐ท) โ†พ (๐ท โˆฉ {๐‘ž}))) โˆˆ (SubGrpโ€˜๐บ))
258256, 257syl 17 . . . . . . . . . 10 ((๐œ‘ โˆง ๐‘ž โˆˆ ๐ด) โ†’ (๐บ DProd ((๐‘‡ โ†พ ๐ท) โ†พ (๐ท โˆฉ {๐‘ž}))) โˆˆ (SubGrpโ€˜๐บ))
259 inass 4180 . . . . . . . . . . . . 13 ((๐ท โˆฉ {๐‘ž}) โˆฉ (๐ท โˆ– {๐‘ž})) = (๐ท โˆฉ ({๐‘ž} โˆฉ (๐ท โˆ– {๐‘ž})))
260 disjdif 4432 . . . . . . . . . . . . . 14 ({๐‘ž} โˆฉ (๐ท โˆ– {๐‘ž})) = โˆ…
261260ineq2i 4170 . . . . . . . . . . . . 13 (๐ท โˆฉ ({๐‘ž} โˆฉ (๐ท โˆ– {๐‘ž}))) = (๐ท โˆฉ โˆ…)
262 in0 4352 . . . . . . . . . . . . 13 (๐ท โˆฉ โˆ…) = โˆ…
263259, 261, 2623eqtri 2769 . . . . . . . . . . . 12 ((๐ท โˆฉ {๐‘ž}) โˆฉ (๐ท โˆ– {๐‘ž})) = โˆ…
264263a1i 11 . . . . . . . . . . 11 ((๐œ‘ โˆง ๐‘ž โˆˆ ๐ด) โ†’ ((๐ท โˆฉ {๐‘ž}) โˆฉ (๐ท โˆ– {๐‘ž})) = โˆ…)
26593, 96, 254, 97, 264, 104dprddisj2 19819 . . . . . . . . . 10 ((๐œ‘ โˆง ๐‘ž โˆˆ ๐ด) โ†’ ((๐บ DProd ((๐‘‡ โ†พ ๐ท) โ†พ (๐ท โˆฉ {๐‘ž}))) โˆฉ (๐บ DProd ((๐‘‡ โ†พ ๐ท) โ†พ (๐ท โˆ– {๐‘ž})))) = {(0gโ€˜๐บ)})
26693, 96, 254, 97, 264, 252dprdcntz2 19818 . . . . . . . . . 10 ((๐œ‘ โˆง ๐‘ž โˆˆ ๐ด) โ†’ (๐บ DProd ((๐‘‡ โ†พ ๐ท) โ†พ (๐ท โˆฉ {๐‘ž}))) โŠ† ((Cntzโ€˜๐บ)โ€˜(๐บ DProd ((๐‘‡ โ†พ ๐ท) โ†พ (๐ท โˆ– {๐‘ž})))))
2676dprdssv 19796 . . . . . . . . . . 11 (๐บ DProd ((๐‘‡ โ†พ ๐ท) โ†พ (๐ท โˆฉ {๐‘ž}))) โŠ† ๐ต
268 ssfi 9118 . . . . . . . . . . 11 ((๐ต โˆˆ Fin โˆง (๐บ DProd ((๐‘‡ โ†พ ๐ท) โ†พ (๐ท โˆฉ {๐‘ž}))) โŠ† ๐ต) โ†’ (๐บ DProd ((๐‘‡ โ†พ ๐ท) โ†พ (๐ท โˆฉ {๐‘ž}))) โˆˆ Fin)
26919, 267, 268sylancl 587 . . . . . . . . . 10 ((๐œ‘ โˆง ๐‘ž โˆˆ ๐ด) โ†’ (๐บ DProd ((๐‘‡ โ†พ ๐ท) โ†พ (๐ท โˆฉ {๐‘ž}))) โˆˆ Fin)
270195, 104, 252, 258, 101, 265, 266, 269, 110lsmhash 19488 . . . . . . . . 9 ((๐œ‘ โˆง ๐‘ž โˆˆ ๐ด) โ†’ (โ™ฏโ€˜((๐บ DProd ((๐‘‡ โ†พ ๐ท) โ†พ (๐ท โˆฉ {๐‘ž})))(LSSumโ€˜๐บ)(๐บ DProd ((๐‘‡ โ†พ ๐ท) โ†พ (๐ท โˆ– {๐‘ž}))))) = ((โ™ฏโ€˜(๐บ DProd ((๐‘‡ โ†พ ๐ท) โ†พ (๐ท โˆฉ {๐‘ž})))) ยท (โ™ฏโ€˜(๐บ DProd ((๐‘‡ โ†พ ๐ท) โ†พ (๐ท โˆ– {๐‘ž}))))))
271 inundif 4439 . . . . . . . . . . . . . 14 ((๐ท โˆฉ {๐‘ž}) โˆช (๐ท โˆ– {๐‘ž})) = ๐ท
272271eqcomi 2746 . . . . . . . . . . . . 13 ๐ท = ((๐ท โˆฉ {๐‘ž}) โˆช (๐ท โˆ– {๐‘ž}))
273272a1i 11 . . . . . . . . . . . 12 ((๐œ‘ โˆง ๐‘ž โˆˆ ๐ด) โ†’ ๐ท = ((๐ท โˆฉ {๐‘ž}) โˆช (๐ท โˆ– {๐‘ž})))
27495, 264, 273, 195, 93dprdsplit 19828 . . . . . . . . . . 11 ((๐œ‘ โˆง ๐‘ž โˆˆ ๐ด) โ†’ (๐บ DProd (๐‘‡ โ†พ ๐ท)) = ((๐บ DProd ((๐‘‡ โ†พ ๐ท) โ†พ (๐ท โˆฉ {๐‘ž})))(LSSumโ€˜๐บ)(๐บ DProd ((๐‘‡ โ†พ ๐ท) โ†พ (๐ท โˆ– {๐‘ž})))))
275207adantr 482 . . . . . . . . . . 11 ((๐œ‘ โˆง ๐‘ž โˆˆ ๐ด) โ†’ (๐บ DProd (๐‘‡ โ†พ ๐ท)) = ๐ต)
276274, 275eqtr3d 2779 . . . . . . . . . 10 ((๐œ‘ โˆง ๐‘ž โˆˆ ๐ด) โ†’ ((๐บ DProd ((๐‘‡ โ†พ ๐ท) โ†พ (๐ท โˆฉ {๐‘ž})))(LSSumโ€˜๐บ)(๐บ DProd ((๐‘‡ โ†พ ๐ท) โ†พ (๐ท โˆ– {๐‘ž})))) = ๐ต)
277276fveq2d 6847 . . . . . . . . 9 ((๐œ‘ โˆง ๐‘ž โˆˆ ๐ด) โ†’ (โ™ฏโ€˜((๐บ DProd ((๐‘‡ โ†พ ๐ท) โ†พ (๐ท โˆฉ {๐‘ž})))(LSSumโ€˜๐บ)(๐บ DProd ((๐‘‡ โ†พ ๐ท) โ†พ (๐ท โˆ– {๐‘ž}))))) = (โ™ฏโ€˜๐ต))
278 snssi 4769 . . . . . . . . . . . . . . . . 17 (๐‘ž โˆˆ ๐ท โ†’ {๐‘ž} โŠ† ๐ท)
279278adantl 483 . . . . . . . . . . . . . . . 16 (((๐œ‘ โˆง ๐‘ž โˆˆ ๐ด) โˆง ๐‘ž โˆˆ ๐ท) โ†’ {๐‘ž} โŠ† ๐ท)
280 sseqin2 4176 . . . . . . . . . . . . . . . 16 ({๐‘ž} โŠ† ๐ท โ†” (๐ท โˆฉ {๐‘ž}) = {๐‘ž})
281279, 280sylib 217 . . . . . . . . . . . . . . 15 (((๐œ‘ โˆง ๐‘ž โˆˆ ๐ด) โˆง ๐‘ž โˆˆ ๐ท) โ†’ (๐ท โˆฉ {๐‘ž}) = {๐‘ž})
282281reseq2d 5938 . . . . . . . . . . . . . 14 (((๐œ‘ โˆง ๐‘ž โˆˆ ๐ด) โˆง ๐‘ž โˆˆ ๐ท) โ†’ ((๐‘‡ โ†พ ๐ท) โ†พ (๐ท โˆฉ {๐‘ž})) = ((๐‘‡ โ†พ ๐ท) โ†พ {๐‘ž}))
283282oveq2d 7374 . . . . . . . . . . . . 13 (((๐œ‘ โˆง ๐‘ž โˆˆ ๐ด) โˆง ๐‘ž โˆˆ ๐ท) โ†’ (๐บ DProd ((๐‘‡ โ†พ ๐ท) โ†พ (๐ท โˆฉ {๐‘ž}))) = (๐บ DProd ((๐‘‡ โ†พ ๐ท) โ†พ {๐‘ž})))
28493adantr 482 . . . . . . . . . . . . . 14 (((๐œ‘ โˆง ๐‘ž โˆˆ ๐ด) โˆง ๐‘ž โˆˆ ๐ท) โ†’ ๐บdom DProd (๐‘‡ โ†พ ๐ท))
285211ad2antrr 725 . . . . . . . . . . . . . 14 (((๐œ‘ โˆง ๐‘ž โˆˆ ๐ด) โˆง ๐‘ž โˆˆ ๐ท) โ†’ dom (๐‘‡ โ†พ ๐ท) = ๐ท)
286 simpr 486 . . . . . . . . . . . . . 14 (((๐œ‘ โˆง ๐‘ž โˆˆ ๐ด) โˆง ๐‘ž โˆˆ ๐ท) โ†’ ๐‘ž โˆˆ ๐ท)
287284, 285, 286dpjlem 19831 . . . . . . . . . . . . 13 (((๐œ‘ โˆง ๐‘ž โˆˆ ๐ด) โˆง ๐‘ž โˆˆ ๐ท) โ†’ (๐บ DProd ((๐‘‡ โ†พ ๐ท) โ†พ {๐‘ž})) = ((๐‘‡ โ†พ ๐ท)โ€˜๐‘ž))
288216adantl 483 . . . . . . . . . . . . 13 (((๐œ‘ โˆง ๐‘ž โˆˆ ๐ด) โˆง ๐‘ž โˆˆ ๐ท) โ†’ ((๐‘‡ โ†พ ๐ท)โ€˜๐‘ž) = (๐‘‡โ€˜๐‘ž))
289283, 287, 2883eqtrd 2781 . . . . . . . . . . . 12 (((๐œ‘ โˆง ๐‘ž โˆˆ ๐ด) โˆง ๐‘ž โˆˆ ๐ท) โ†’ (๐บ DProd ((๐‘‡ โ†พ ๐ท) โ†พ (๐ท โˆฉ {๐‘ž}))) = (๐‘‡โ€˜๐‘ž))
290 simprr 772 . . . . . . . . . . . . . . . . . 18 ((๐œ‘ โˆง (๐‘ž โˆˆ ๐ด โˆง ยฌ ๐‘ž โˆˆ ๐ท)) โ†’ ยฌ ๐‘ž โˆˆ ๐ท)
291 disjsn 4673 . . . . . . . . . . . . . . . . . 18 ((๐ท โˆฉ {๐‘ž}) = โˆ… โ†” ยฌ ๐‘ž โˆˆ ๐ท)
292290, 291sylibr 233 . . . . . . . . . . . . . . . . 17 ((๐œ‘ โˆง (๐‘ž โˆˆ ๐ด โˆง ยฌ ๐‘ž โˆˆ ๐ท)) โ†’ (๐ท โˆฉ {๐‘ž}) = โˆ…)
293292reseq2d 5938 . . . . . . . . . . . . . . . 16 ((๐œ‘ โˆง (๐‘ž โˆˆ ๐ด โˆง ยฌ ๐‘ž โˆˆ ๐ท)) โ†’ ((๐‘‡ โ†พ ๐ท) โ†พ (๐ท โˆฉ {๐‘ž})) = ((๐‘‡ โ†พ ๐ท) โ†พ โˆ…))
294 res0 5942 . . . . . . . . . . . . . . . 16 ((๐‘‡ โ†พ ๐ท) โ†พ โˆ…) = โˆ…
295293, 294eqtrdi 2793 . . . . . . . . . . . . . . 15 ((๐œ‘ โˆง (๐‘ž โˆˆ ๐ด โˆง ยฌ ๐‘ž โˆˆ ๐ท)) โ†’ ((๐‘‡ โ†พ ๐ท) โ†พ (๐ท โˆฉ {๐‘ž})) = โˆ…)
296295oveq2d 7374 . . . . . . . . . . . . . 14 ((๐œ‘ โˆง (๐‘ž โˆˆ ๐ด โˆง ยฌ ๐‘ž โˆˆ ๐ท)) โ†’ (๐บ DProd ((๐‘‡ โ†พ ๐ท) โ†พ (๐ท โˆฉ {๐‘ž}))) = (๐บ DProd โˆ…))
297104dprd0 19811 . . . . . . . . . . . . . . . . 17 (๐บ โˆˆ Grp โ†’ (๐บdom DProd โˆ… โˆง (๐บ DProd โˆ…) = {(0gโ€˜๐บ)}))
29840, 297syl 17 . . . . . . . . . . . . . . . 16 (๐œ‘ โ†’ (๐บdom DProd โˆ… โˆง (๐บ DProd โˆ…) = {(0gโ€˜๐บ)}))
299298simprd 497 . . . . . . . . . . . . . . 15 (๐œ‘ โ†’ (๐บ DProd โˆ…) = {(0gโ€˜๐บ)})
300299adantr 482 . . . . . . . . . . . . . 14 ((๐œ‘ โˆง (๐‘ž โˆˆ ๐ด โˆง ยฌ ๐‘ž โˆˆ ๐ท)) โ†’ (๐บ DProd โˆ…) = {(0gโ€˜๐บ)})
301296, 300, 1863eqtrd 2781 . . . . . . . . . . . . 13 ((๐œ‘ โˆง (๐‘ž โˆˆ ๐ด โˆง ยฌ ๐‘ž โˆˆ ๐ท)) โ†’ (๐บ DProd ((๐‘‡ โ†พ ๐ท) โ†พ (๐ท โˆฉ {๐‘ž}))) = (๐‘‡โ€˜๐‘ž))
302301anassrs 469 . . . . . . . . . . . 12 (((๐œ‘ โˆง ๐‘ž โˆˆ ๐ด) โˆง ยฌ ๐‘ž โˆˆ ๐ท) โ†’ (๐บ DProd ((๐‘‡ โ†พ ๐ท) โ†พ (๐ท โˆฉ {๐‘ž}))) = (๐‘‡โ€˜๐‘ž))
303289, 302pm2.61dan 812 . . . . . . . . . . 11 ((๐œ‘ โˆง ๐‘ž โˆˆ ๐ด) โ†’ (๐บ DProd ((๐‘‡ โ†พ ๐ท) โ†พ (๐ท โˆฉ {๐‘ž}))) = (๐‘‡โ€˜๐‘ž))
304303fveq2d 6847 . . . . . . . . . 10 ((๐œ‘ โˆง ๐‘ž โˆˆ ๐ด) โ†’ (โ™ฏโ€˜(๐บ DProd ((๐‘‡ โ†พ ๐ท) โ†พ (๐ท โˆฉ {๐‘ž})))) = (โ™ฏโ€˜(๐‘‡โ€˜๐‘ž)))
305304oveq1d 7373 . . . . . . . . 9 ((๐œ‘ โˆง ๐‘ž โˆˆ ๐ด) โ†’ ((โ™ฏโ€˜(๐บ DProd ((๐‘‡ โ†พ ๐ท) โ†พ (๐ท โˆฉ {๐‘ž})))) ยท (โ™ฏโ€˜(๐บ DProd ((๐‘‡ โ†พ ๐ท) โ†พ (๐ท โˆ– {๐‘ž}))))) = ((โ™ฏโ€˜(๐‘‡โ€˜๐‘ž)) ยท (โ™ฏโ€˜(๐บ DProd ((๐‘‡ โ†พ ๐ท) โ†พ (๐ท โˆ– {๐‘ž}))))))
306270, 277, 3053eqtr3d 2785 . . . . . . . 8 ((๐œ‘ โˆง ๐‘ž โˆˆ ๐ด) โ†’ (โ™ฏโ€˜๐ต) = ((โ™ฏโ€˜(๐‘‡โ€˜๐‘ž)) ยท (โ™ฏโ€˜(๐บ DProd ((๐‘‡ โ†พ ๐ท) โ†พ (๐ท โˆ– {๐‘ž}))))))
307251, 306breqtrd 5132 . . . . . . 7 ((๐œ‘ โˆง ๐‘ž โˆˆ ๐ด) โ†’ ((๐‘žโ†‘(๐‘ž pCnt (โ™ฏโ€˜๐ต))) ยท (โ™ฏโ€˜(๐บ DProd ((๐‘‡ โ†พ ๐ท) โ†พ (๐ท โˆ– {๐‘ž}))))) โˆฅ ((โ™ฏโ€˜(๐‘‡โ€˜๐‘ž)) ยท (โ™ฏโ€˜(๐บ DProd ((๐‘‡ โ†พ ๐ท) โ†พ (๐ท โˆ– {๐‘ž}))))))
308113nnne0d 12204 . . . . . . . 8 ((๐œ‘ โˆง ๐‘ž โˆˆ ๐ด) โ†’ (โ™ฏโ€˜(๐บ DProd ((๐‘‡ โ†พ ๐ท) โ†พ (๐ท โˆ– {๐‘ž})))) โ‰  0)
309 dvdsmulcr 16169 . . . . . . . 8 (((๐‘žโ†‘(๐‘ž pCnt (โ™ฏโ€˜๐ต))) โˆˆ โ„ค โˆง (โ™ฏโ€˜(๐‘‡โ€˜๐‘ž)) โˆˆ โ„ค โˆง ((โ™ฏโ€˜(๐บ DProd ((๐‘‡ โ†พ ๐ท) โ†พ (๐ท โˆ– {๐‘ž})))) โˆˆ โ„ค โˆง (โ™ฏโ€˜(๐บ DProd ((๐‘‡ โ†พ ๐ท) โ†พ (๐ท โˆ– {๐‘ž})))) โ‰  0)) โ†’ (((๐‘žโ†‘(๐‘ž pCnt (โ™ฏโ€˜๐ต))) ยท (โ™ฏโ€˜(๐บ DProd ((๐‘‡ โ†พ ๐ท) โ†พ (๐ท โˆ– {๐‘ž}))))) โˆฅ ((โ™ฏโ€˜(๐‘‡โ€˜๐‘ž)) ยท (โ™ฏโ€˜(๐บ DProd ((๐‘‡ โ†พ ๐ท) โ†พ (๐ท โˆ– {๐‘ž}))))) โ†” (๐‘žโ†‘(๐‘ž pCnt (โ™ฏโ€˜๐ต))) โˆฅ (โ™ฏโ€˜(๐‘‡โ€˜๐‘ž))))
31049, 34, 114, 308, 309syl112anc 1375 . . . . . . 7 ((๐œ‘ โˆง ๐‘ž โˆˆ ๐ด) โ†’ (((๐‘žโ†‘(๐‘ž pCnt (โ™ฏโ€˜๐ต))) ยท (โ™ฏโ€˜(๐บ DProd ((๐‘‡ โ†พ ๐ท) โ†พ (๐ท โˆ– {๐‘ž}))))) โˆฅ ((โ™ฏโ€˜(๐‘‡โ€˜๐‘ž)) ยท (โ™ฏโ€˜(๐บ DProd ((๐‘‡ โ†พ ๐ท) โ†พ (๐ท โˆ– {๐‘ž}))))) โ†” (๐‘žโ†‘(๐‘ž pCnt (โ™ฏโ€˜๐ต))) โˆฅ (โ™ฏโ€˜(๐‘‡โ€˜๐‘ž))))
311307, 310mpbid 231 . . . . . 6 ((๐œ‘ โˆง ๐‘ž โˆˆ ๐ด) โ†’ (๐‘žโ†‘(๐‘ž pCnt (โ™ฏโ€˜๐ต))) โˆฅ (โ™ฏโ€˜(๐‘‡โ€˜๐‘ž)))
312 dvdseq 16197 . . . . . 6 ((((โ™ฏโ€˜(๐‘‡โ€˜๐‘ž)) โˆˆ โ„•0 โˆง (๐‘žโ†‘(๐‘ž pCnt (โ™ฏโ€˜๐ต))) โˆˆ โ„•0) โˆง ((โ™ฏโ€˜(๐‘‡โ€˜๐‘ž)) โˆฅ (๐‘žโ†‘(๐‘ž pCnt (โ™ฏโ€˜๐ต))) โˆง (๐‘žโ†‘(๐‘ž pCnt (โ™ฏโ€˜๐ต))) โˆฅ (โ™ฏโ€˜(๐‘‡โ€˜๐‘ž)))) โ†’ (โ™ฏโ€˜(๐‘‡โ€˜๐‘ž)) = (๐‘žโ†‘(๐‘ž pCnt (โ™ฏโ€˜๐ต))))
31333, 85, 73, 311, 312syl22anc 838 . . . . 5 ((๐œ‘ โˆง ๐‘ž โˆˆ ๐ด) โ†’ (โ™ฏโ€˜(๐‘‡โ€˜๐‘ž)) = (๐‘žโ†‘(๐‘ž pCnt (โ™ฏโ€˜๐ต))))
3146, 7, 8, 9, 10, 11ablfac1a 19849 . . . . 5 ((๐œ‘ โˆง ๐‘ž โˆˆ ๐ด) โ†’ (โ™ฏโ€˜(๐‘†โ€˜๐‘ž)) = (๐‘žโ†‘(๐‘ž pCnt (โ™ฏโ€˜๐ต))))
315313, 314eqtr4d 2780 . . . 4 ((๐œ‘ โˆง ๐‘ž โˆˆ ๐ด) โ†’ (โ™ฏโ€˜(๐‘‡โ€˜๐‘ž)) = (โ™ฏโ€˜(๐‘†โ€˜๐‘ž)))
316 hashen 14248 . . . . 5 (((๐‘‡โ€˜๐‘ž) โˆˆ Fin โˆง (๐‘†โ€˜๐‘ž) โˆˆ Fin) โ†’ ((โ™ฏโ€˜(๐‘‡โ€˜๐‘ž)) = (โ™ฏโ€˜(๐‘†โ€˜๐‘ž)) โ†” (๐‘‡โ€˜๐‘ž) โ‰ˆ (๐‘†โ€˜๐‘ž)))
31731, 23, 316syl2anc 585 . . . 4 ((๐œ‘ โˆง ๐‘ž โˆˆ ๐ด) โ†’ ((โ™ฏโ€˜(๐‘‡โ€˜๐‘ž)) = (โ™ฏโ€˜(๐‘†โ€˜๐‘ž)) โ†” (๐‘‡โ€˜๐‘ž) โ‰ˆ (๐‘†โ€˜๐‘ž)))
318315, 317mpbid 231 . . 3 ((๐œ‘ โˆง ๐‘ž โˆˆ ๐ด) โ†’ (๐‘‡โ€˜๐‘ž) โ‰ˆ (๐‘†โ€˜๐‘ž))
319 fisseneq 9202 . . 3 (((๐‘†โ€˜๐‘ž) โˆˆ Fin โˆง (๐‘‡โ€˜๐‘ž) โŠ† (๐‘†โ€˜๐‘ž) โˆง (๐‘‡โ€˜๐‘ž) โ‰ˆ (๐‘†โ€˜๐‘ž)) โ†’ (๐‘‡โ€˜๐‘ž) = (๐‘†โ€˜๐‘ž))
32023, 84, 318, 319syl3anc 1372 . 2 ((๐œ‘ โˆง ๐‘ž โˆˆ ๐ด) โ†’ (๐‘‡โ€˜๐‘ž) = (๐‘†โ€˜๐‘ž))
3215, 18, 320eqfnfvd 6986 1 (๐œ‘ โ†’ ๐‘‡ = ๐‘†)
Colors of variables: wff setvar class
Syntax hints:  ยฌ wn 3   โ†’ wi 4   โ†” wb 205   โˆง wa 397   โˆจ wo 846   โˆง w3a 1088   = wceq 1542   โˆˆ wcel 2107   โ‰  wne 2944  โˆ€wral 3065  {crab 3408  Vcvv 3446   โˆ– cdif 3908   โˆช cun 3909   โˆฉ cin 3910   โŠ† wss 3911  โˆ…c0 4283  {csn 4587   class class class wbr 5106   โ†ฆ cmpt 5189  dom cdm 5634   โ†พ cres 5636  โŸถwf 6493  โ€˜cfv 6497  (class class class)co 7358   โ‰ˆ cen 8881  Fincfn 8884  0cc0 11052  1c1 11053   ยท cmul 11057   โ‰ค cle 11191  โ„•cn 12154  โ„•0cn0 12414  โ„คcz 12500  โ„คโ‰ฅcuz 12764  ...cfz 13425  โ†‘cexp 13968  โ™ฏchash 14231   โˆฅ cdvds 16137   gcd cgcd 16375  โ„™cprime 16548   pCnt cpc 16709  Basecbs 17084  0gc0g 17322  Grpcgrp 18749  SubGrpcsubg 18923  Cntzccntz 19096  odcod 19307  LSSumclsm 19417  Abelcabl 19564   DProd cdprd 19773
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-10 2138  ax-11 2155  ax-12 2172  ax-ext 2708  ax-rep 5243  ax-sep 5257  ax-nul 5264  ax-pow 5321  ax-pr 5385  ax-un 7673  ax-inf2 9578  ax-cnex 11108  ax-resscn 11109  ax-1cn 11110  ax-icn 11111  ax-addcl 11112  ax-addrcl 11113  ax-mulcl 11114  ax-mulrcl 11115  ax-mulcom 11116  ax-addass 11117  ax-mulass 11118  ax-distr 11119  ax-i2m1 11120  ax-1ne0 11121  ax-1rid 11122  ax-rnegex 11123  ax-rrecex 11124  ax-cnre 11125  ax-pre-lttri 11126  ax-pre-lttrn 11127  ax-pre-ltadd 11128  ax-pre-mulgt0 11129  ax-pre-sup 11130
This theorem depends on definitions:  df-bi 206  df-an 398  df-or 847  df-3or 1089  df-3an 1090  df-tru 1545  df-fal 1555  df-ex 1783  df-nf 1787  df-sb 2069  df-mo 2539  df-eu 2568  df-clab 2715  df-cleq 2729  df-clel 2815  df-nfc 2890  df-ne 2945  df-nel 3051  df-ral 3066  df-rex 3075  df-rmo 3354  df-reu 3355  df-rab 3409  df-v 3448  df-sbc 3741  df-csb 3857  df-dif 3914  df-un 3916  df-in 3918  df-ss 3928  df-pss 3930  df-nul 4284  df-if 4488  df-pw 4563  df-sn 4588  df-pr 4590  df-op 4594  df-uni 4867  df-int 4909  df-iun 4957  df-iin 4958  df-disj 5072  df-br 5107  df-opab 5169  df-mpt 5190  df-tr 5224  df-id 5532  df-eprel 5538  df-po 5546  df-so 5547  df-fr 5589  df-se 5590  df-we 5591  df-xp 5640  df-rel 5641  df-cnv 5642  df-co 5643  df-dm 5644  df-rn 5645  df-res 5646  df-ima 5647  df-pred 6254  df-ord 6321  df-on 6322  df-lim 6323  df-suc 6324  df-iota 6449  df-fun 6499  df-fn 6500  df-f 6501  df-f1 6502  df-fo 6503  df-f1o 6504  df-fv 6505  df-isom 6506  df-riota 7314  df-ov 7361  df-oprab 7362  df-mpo 7363  df-of 7618  df-om 7804  df-1st 7922  df-2nd 7923  df-supp 8094  df-tpos 8158  df-frecs 8213  df-wrecs 8244  df-recs 8318  df-rdg 8357  df-1o 8413  df-2o 8414  df-oadd 8417  df-omul 8418  df-er 8649  df-ec 8651  df-qs 8655  df-map 8768  df-ixp 8837  df-en 8885  df-dom 8886  df-sdom 8887  df-fin 8888  df-fsupp 9307  df-sup 9379  df-inf 9380  df-oi 9447  df-dju 9838  df-card 9876  df-acn 9879  df-pnf 11192  df-mnf 11193  df-xr 11194  df-ltxr 11195  df-le 11196  df-sub 11388  df-neg 11389  df-div 11814  df-nn 12155  df-2 12217  df-3 12218  df-n0 12415  df-xnn0 12487  df-z 12501  df-uz 12765  df-q 12875  df-rp 12917  df-fz 13426  df-fzo 13569  df-fl 13698  df-mod 13776  df-seq 13908  df-exp 13969  df-fac 14175  df-bc 14204  df-hash 14232  df-cj 14985  df-re 14986  df-im 14987  df-sqrt 15121  df-abs 15122  df-clim 15371  df-sum 15572  df-dvds 16138  df-gcd 16376  df-prm 16549  df-pc 16710  df-sets 17037  df-slot 17055  df-ndx 17067  df-base 17085  df-ress 17114  df-plusg 17147  df-0g 17324  df-gsum 17325  df-mre 17467  df-mrc 17468  df-acs 17470  df-mgm 18498  df-sgrp 18547  df-mnd 18558  df-mhm 18602  df-submnd 18603  df-grp 18752  df-minusg 18753  df-sbg 18754  df-mulg 18874  df-subg 18926  df-eqg 18928  df-ghm 19007  df-gim 19050  df-ga 19071  df-cntz 19098  df-oppg 19125  df-od 19311  df-lsm 19419  df-pj1 19420  df-cmn 19565  df-abl 19566  df-dprd 19775
This theorem is referenced by: (None)
  Copyright terms: Public domain W3C validator