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

Theorem ablfac1eu 20021
Description: The factorization of ablfac1b 20018 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 494 . . . 4 (๐œ‘ โ†’ ๐บdom DProd ๐‘‡)
3 ablfac1eu.2 . . . 4 (๐œ‘ โ†’ dom ๐‘‡ = ๐ด)
42, 3dprdf2 19955 . . 3 (๐œ‘ โ†’ ๐‘‡:๐ดโŸถ(SubGrpโ€˜๐บ))
54ffnd 6717 . 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 20018 . . . 4 (๐œ‘ โ†’ ๐บdom DProd ๐‘†)
136fvexi 6905 . . . . . . 7 ๐ต โˆˆ V
1413rabex 5328 . . . . . 6 {๐‘ฅ โˆˆ ๐ต โˆฃ (๐‘‚โ€˜๐‘ฅ) โˆฅ (๐‘โ†‘(๐‘ pCnt (โ™ฏโ€˜๐ต)))} โˆˆ V
1514, 8dmmpti 6693 . . . . 5 dom ๐‘† = ๐ด
1615a1i 11 . . . 4 (๐œ‘ โ†’ dom ๐‘† = ๐ด)
1712, 16dprdf2 19955 . . 3 (๐œ‘ โ†’ ๐‘†:๐ดโŸถ(SubGrpโ€˜๐บ))
1817ffnd 6717 . 2 (๐œ‘ โ†’ ๐‘† Fn ๐ด)
1910adantr 480 . . . 4 ((๐œ‘ โˆง ๐‘ž โˆˆ ๐ด) โ†’ ๐ต โˆˆ Fin)
2017ffvelcdmda 7088 . . . . 5 ((๐œ‘ โˆง ๐‘ž โˆˆ ๐ด) โ†’ (๐‘†โ€˜๐‘ž) โˆˆ (SubGrpโ€˜๐บ))
216subgss 19073 . . . . 5 ((๐‘†โ€˜๐‘ž) โˆˆ (SubGrpโ€˜๐บ) โ†’ (๐‘†โ€˜๐‘ž) โІ ๐ต)
2220, 21syl 17 . . . 4 ((๐œ‘ โˆง ๐‘ž โˆˆ ๐ด) โ†’ (๐‘†โ€˜๐‘ž) โІ ๐ต)
2319, 22ssfid 9283 . . 3 ((๐œ‘ โˆง ๐‘ž โˆˆ ๐ด) โ†’ (๐‘†โ€˜๐‘ž) โˆˆ Fin)
244ffvelcdmda 7088 . . . . . 6 ((๐œ‘ โˆง ๐‘ž โˆˆ ๐ด) โ†’ (๐‘‡โ€˜๐‘ž) โˆˆ (SubGrpโ€˜๐บ))
256subgss 19073 . . . . . 6 ((๐‘‡โ€˜๐‘ž) โˆˆ (SubGrpโ€˜๐บ) โ†’ (๐‘‡โ€˜๐‘ž) โІ ๐ต)
2624, 25syl 17 . . . . 5 ((๐œ‘ โˆง ๐‘ž โˆˆ ๐ด) โ†’ (๐‘‡โ€˜๐‘ž) โІ ๐ต)
2726sselda 3978 . . . . . . . 8 (((๐œ‘ โˆง ๐‘ž โˆˆ ๐ด) โˆง ๐‘ฅ โˆˆ (๐‘‡โ€˜๐‘ž)) โ†’ ๐‘ฅ โˆˆ ๐ต)
286, 7odcl 19482 . . . . . . . 8 (๐‘ฅ โˆˆ ๐ต โ†’ (๐‘‚โ€˜๐‘ฅ) โˆˆ โ„•0)
2927, 28syl 17 . . . . . . 7 (((๐œ‘ โˆง ๐‘ž โˆˆ ๐ด) โˆง ๐‘ฅ โˆˆ (๐‘‡โ€˜๐‘ž)) โ†’ (๐‘‚โ€˜๐‘ฅ) โˆˆ โ„•0)
3029nn0zd 12606 . . . . . 6 (((๐œ‘ โˆง ๐‘ž โˆˆ ๐ด) โˆง ๐‘ฅ โˆˆ (๐‘‡โ€˜๐‘ž)) โ†’ (๐‘‚โ€˜๐‘ฅ) โˆˆ โ„ค)
3119, 26ssfid 9283 . . . . . . . . 9 ((๐œ‘ โˆง ๐‘ž โˆˆ ๐ด) โ†’ (๐‘‡โ€˜๐‘ž) โˆˆ Fin)
32 hashcl 14339 . . . . . . . . 9 ((๐‘‡โ€˜๐‘ž) โˆˆ Fin โ†’ (โ™ฏโ€˜(๐‘‡โ€˜๐‘ž)) โˆˆ โ„•0)
3331, 32syl 17 . . . . . . . 8 ((๐œ‘ โˆง ๐‘ž โˆˆ ๐ด) โ†’ (โ™ฏโ€˜(๐‘‡โ€˜๐‘ž)) โˆˆ โ„•0)
3433nn0zd 12606 . . . . . . 7 ((๐œ‘ โˆง ๐‘ž โˆˆ ๐ด) โ†’ (โ™ฏโ€˜(๐‘‡โ€˜๐‘ž)) โˆˆ โ„ค)
3534adantr 480 . . . . . 6 (((๐œ‘ โˆง ๐‘ž โˆˆ ๐ด) โˆง ๐‘ฅ โˆˆ (๐‘‡โ€˜๐‘ž)) โ†’ (โ™ฏโ€˜(๐‘‡โ€˜๐‘ž)) โˆˆ โ„ค)
3611sselda 3978 . . . . . . . . . 10 ((๐œ‘ โˆง ๐‘ž โˆˆ ๐ด) โ†’ ๐‘ž โˆˆ โ„™)
37 prmnn 16636 . . . . . . . . . 10 (๐‘ž โˆˆ โ„™ โ†’ ๐‘ž โˆˆ โ„•)
3836, 37syl 17 . . . . . . . . 9 ((๐œ‘ โˆง ๐‘ž โˆˆ ๐ด) โ†’ ๐‘ž โˆˆ โ„•)
39 ablgrp 19731 . . . . . . . . . . . . . 14 (๐บ โˆˆ Abel โ†’ ๐บ โˆˆ Grp)
409, 39syl 17 . . . . . . . . . . . . 13 (๐œ‘ โ†’ ๐บ โˆˆ Grp)
416grpbn0 18914 . . . . . . . . . . . . 13 (๐บ โˆˆ Grp โ†’ ๐ต โ‰  โˆ…)
4240, 41syl 17 . . . . . . . . . . . 12 (๐œ‘ โ†’ ๐ต โ‰  โˆ…)
43 hashnncl 14349 . . . . . . . . . . . . 13 (๐ต โˆˆ Fin โ†’ ((โ™ฏโ€˜๐ต) โˆˆ โ„• โ†” ๐ต โ‰  โˆ…))
4410, 43syl 17 . . . . . . . . . . . 12 (๐œ‘ โ†’ ((โ™ฏโ€˜๐ต) โˆˆ โ„• โ†” ๐ต โ‰  โˆ…))
4542, 44mpbird 257 . . . . . . . . . . 11 (๐œ‘ โ†’ (โ™ฏโ€˜๐ต) โˆˆ โ„•)
4645adantr 480 . . . . . . . . . 10 ((๐œ‘ โˆง ๐‘ž โˆˆ ๐ด) โ†’ (โ™ฏโ€˜๐ต) โˆˆ โ„•)
4736, 46pccld 16810 . . . . . . . . 9 ((๐œ‘ โˆง ๐‘ž โˆˆ ๐ด) โ†’ (๐‘ž pCnt (โ™ฏโ€˜๐ต)) โˆˆ โ„•0)
4838, 47nnexpcld 14231 . . . . . . . 8 ((๐œ‘ โˆง ๐‘ž โˆˆ ๐ด) โ†’ (๐‘žโ†‘(๐‘ž pCnt (โ™ฏโ€˜๐ต))) โˆˆ โ„•)
4948nnzd 12607 . . . . . . 7 ((๐œ‘ โˆง ๐‘ž โˆˆ ๐ด) โ†’ (๐‘žโ†‘(๐‘ž pCnt (โ™ฏโ€˜๐ต))) โˆˆ โ„ค)
5049adantr 480 . . . . . 6 (((๐œ‘ โˆง ๐‘ž โˆˆ ๐ด) โˆง ๐‘ฅ โˆˆ (๐‘‡โ€˜๐‘ž)) โ†’ (๐‘žโ†‘(๐‘ž pCnt (โ™ฏโ€˜๐ต))) โˆˆ โ„ค)
5124adantr 480 . . . . . . 7 (((๐œ‘ โˆง ๐‘ž โˆˆ ๐ด) โˆง ๐‘ฅ โˆˆ (๐‘‡โ€˜๐‘ž)) โ†’ (๐‘‡โ€˜๐‘ž) โˆˆ (SubGrpโ€˜๐บ))
5231adantr 480 . . . . . . 7 (((๐œ‘ โˆง ๐‘ž โˆˆ ๐ด) โˆง ๐‘ฅ โˆˆ (๐‘‡โ€˜๐‘ž)) โ†’ (๐‘‡โ€˜๐‘ž) โˆˆ Fin)
53 simpr 484 . . . . . . 7 (((๐œ‘ โˆง ๐‘ž โˆˆ ๐ด) โˆง ๐‘ฅ โˆˆ (๐‘‡โ€˜๐‘ž)) โ†’ ๐‘ฅ โˆˆ (๐‘‡โ€˜๐‘ž))
547odsubdvds 19517 . . . . . . 7 (((๐‘‡โ€˜๐‘ž) โˆˆ (SubGrpโ€˜๐บ) โˆง (๐‘‡โ€˜๐‘ž) โˆˆ Fin โˆง ๐‘ฅ โˆˆ (๐‘‡โ€˜๐‘ž)) โ†’ (๐‘‚โ€˜๐‘ฅ) โˆฅ (โ™ฏโ€˜(๐‘‡โ€˜๐‘ž)))
5551, 52, 53, 54syl3anc 1369 . . . . . 6 (((๐œ‘ โˆง ๐‘ž โˆˆ ๐ด) โˆง ๐‘ฅ โˆˆ (๐‘‡โ€˜๐‘ž)) โ†’ (๐‘‚โ€˜๐‘ฅ) โˆฅ (โ™ฏโ€˜(๐‘‡โ€˜๐‘ž)))
56 ablfac1eu.4 . . . . . . . 8 ((๐œ‘ โˆง ๐‘ž โˆˆ ๐ด) โ†’ (โ™ฏโ€˜(๐‘‡โ€˜๐‘ž)) = (๐‘žโ†‘๐ถ))
57 prmz 16637 . . . . . . . . . 10 (๐‘ž โˆˆ โ„™ โ†’ ๐‘ž โˆˆ โ„ค)
5836, 57syl 17 . . . . . . . . 9 ((๐œ‘ โˆง ๐‘ž โˆˆ ๐ด) โ†’ ๐‘ž โˆˆ โ„ค)
59 ablfac1eu.3 . . . . . . . . 9 ((๐œ‘ โˆง ๐‘ž โˆˆ ๐ด) โ†’ ๐ถ โˆˆ โ„•0)
6059nn0zd 12606 . . . . . . . . . 10 ((๐œ‘ โˆง ๐‘ž โˆˆ ๐ด) โ†’ ๐ถ โˆˆ โ„ค)
6147nn0zd 12606 . . . . . . . . . 10 ((๐œ‘ โˆง ๐‘ž โˆˆ ๐ด) โ†’ (๐‘ž pCnt (โ™ฏโ€˜๐ต)) โˆˆ โ„ค)
626lagsubg 19141 . . . . . . . . . . . . 13 (((๐‘‡โ€˜๐‘ž) โˆˆ (SubGrpโ€˜๐บ) โˆง ๐ต โˆˆ Fin) โ†’ (โ™ฏโ€˜(๐‘‡โ€˜๐‘ž)) โˆฅ (โ™ฏโ€˜๐ต))
6324, 19, 62syl2anc 583 . . . . . . . . . . . 12 ((๐œ‘ โˆง ๐‘ž โˆˆ ๐ด) โ†’ (โ™ฏโ€˜(๐‘‡โ€˜๐‘ž)) โˆฅ (โ™ฏโ€˜๐ต))
6456, 63eqbrtrrd 5166 . . . . . . . . . . 11 ((๐œ‘ โˆง ๐‘ž โˆˆ ๐ด) โ†’ (๐‘žโ†‘๐ถ) โˆฅ (โ™ฏโ€˜๐ต))
6546nnzd 12607 . . . . . . . . . . . 12 ((๐œ‘ โˆง ๐‘ž โˆˆ ๐ด) โ†’ (โ™ฏโ€˜๐ต) โˆˆ โ„ค)
66 pcdvdsb 16829 . . . . . . . . . . . 12 ((๐‘ž โˆˆ โ„™ โˆง (โ™ฏโ€˜๐ต) โˆˆ โ„ค โˆง ๐ถ โˆˆ โ„•0) โ†’ (๐ถ โ‰ค (๐‘ž pCnt (โ™ฏโ€˜๐ต)) โ†” (๐‘žโ†‘๐ถ) โˆฅ (โ™ฏโ€˜๐ต)))
6736, 65, 59, 66syl3anc 1369 . . . . . . . . . . 11 ((๐œ‘ โˆง ๐‘ž โˆˆ ๐ด) โ†’ (๐ถ โ‰ค (๐‘ž pCnt (โ™ฏโ€˜๐ต)) โ†” (๐‘žโ†‘๐ถ) โˆฅ (โ™ฏโ€˜๐ต)))
6864, 67mpbird 257 . . . . . . . . . 10 ((๐œ‘ โˆง ๐‘ž โˆˆ ๐ด) โ†’ ๐ถ โ‰ค (๐‘ž pCnt (โ™ฏโ€˜๐ต)))
69 eluz2 12850 . . . . . . . . . 10 ((๐‘ž pCnt (โ™ฏโ€˜๐ต)) โˆˆ (โ„คโ‰ฅโ€˜๐ถ) โ†” (๐ถ โˆˆ โ„ค โˆง (๐‘ž pCnt (โ™ฏโ€˜๐ต)) โˆˆ โ„ค โˆง ๐ถ โ‰ค (๐‘ž pCnt (โ™ฏโ€˜๐ต))))
7060, 61, 68, 69syl3anbrc 1341 . . . . . . . . 9 ((๐œ‘ โˆง ๐‘ž โˆˆ ๐ด) โ†’ (๐‘ž pCnt (โ™ฏโ€˜๐ต)) โˆˆ (โ„คโ‰ฅโ€˜๐ถ))
71 dvdsexp 16296 . . . . . . . . 9 ((๐‘ž โˆˆ โ„ค โˆง ๐ถ โˆˆ โ„•0 โˆง (๐‘ž pCnt (โ™ฏโ€˜๐ต)) โˆˆ (โ„คโ‰ฅโ€˜๐ถ)) โ†’ (๐‘žโ†‘๐ถ) โˆฅ (๐‘žโ†‘(๐‘ž pCnt (โ™ฏโ€˜๐ต))))
7258, 59, 70, 71syl3anc 1369 . . . . . . . 8 ((๐œ‘ โˆง ๐‘ž โˆˆ ๐ด) โ†’ (๐‘žโ†‘๐ถ) โˆฅ (๐‘žโ†‘(๐‘ž pCnt (โ™ฏโ€˜๐ต))))
7356, 72eqbrtrd 5164 . . . . . . 7 ((๐œ‘ โˆง ๐‘ž โˆˆ ๐ด) โ†’ (โ™ฏโ€˜(๐‘‡โ€˜๐‘ž)) โˆฅ (๐‘žโ†‘(๐‘ž pCnt (โ™ฏโ€˜๐ต))))
7473adantr 480 . . . . . 6 (((๐œ‘ โˆง ๐‘ž โˆˆ ๐ด) โˆง ๐‘ฅ โˆˆ (๐‘‡โ€˜๐‘ž)) โ†’ (โ™ฏโ€˜(๐‘‡โ€˜๐‘ž)) โˆฅ (๐‘žโ†‘(๐‘ž pCnt (โ™ฏโ€˜๐ต))))
7530, 35, 50, 55, 74dvdstrd 16263 . . . . 5 (((๐œ‘ โˆง ๐‘ž โˆˆ ๐ด) โˆง ๐‘ฅ โˆˆ (๐‘‡โ€˜๐‘ž)) โ†’ (๐‘‚โ€˜๐‘ฅ) โˆฅ (๐‘žโ†‘(๐‘ž pCnt (โ™ฏโ€˜๐ต))))
7626, 75ssrabdv 4067 . . . 4 ((๐œ‘ โˆง ๐‘ž โˆˆ ๐ด) โ†’ (๐‘‡โ€˜๐‘ž) โІ {๐‘ฅ โˆˆ ๐ต โˆฃ (๐‘‚โ€˜๐‘ฅ) โˆฅ (๐‘žโ†‘(๐‘ž pCnt (โ™ฏโ€˜๐ต)))})
77 id 22 . . . . . . . . 9 (๐‘ = ๐‘ž โ†’ ๐‘ = ๐‘ž)
78 oveq1 7421 . . . . . . . . 9 (๐‘ = ๐‘ž โ†’ (๐‘ pCnt (โ™ฏโ€˜๐ต)) = (๐‘ž pCnt (โ™ฏโ€˜๐ต)))
7977, 78oveq12d 7432 . . . . . . . 8 (๐‘ = ๐‘ž โ†’ (๐‘โ†‘(๐‘ pCnt (โ™ฏโ€˜๐ต))) = (๐‘žโ†‘(๐‘ž pCnt (โ™ฏโ€˜๐ต))))
8079breq2d 5154 . . . . . . 7 (๐‘ = ๐‘ž โ†’ ((๐‘‚โ€˜๐‘ฅ) โˆฅ (๐‘โ†‘(๐‘ pCnt (โ™ฏโ€˜๐ต))) โ†” (๐‘‚โ€˜๐‘ฅ) โˆฅ (๐‘žโ†‘(๐‘ž pCnt (โ™ฏโ€˜๐ต)))))
8180rabbidv 3435 . . . . . 6 (๐‘ = ๐‘ž โ†’ {๐‘ฅ โˆˆ ๐ต โˆฃ (๐‘‚โ€˜๐‘ฅ) โˆฅ (๐‘โ†‘(๐‘ pCnt (โ™ฏโ€˜๐ต)))} = {๐‘ฅ โˆˆ ๐ต โˆฃ (๐‘‚โ€˜๐‘ฅ) โˆฅ (๐‘žโ†‘(๐‘ž pCnt (โ™ฏโ€˜๐ต)))})
8281, 8, 14fvmpt3i 7004 . . . . 5 (๐‘ž โˆˆ ๐ด โ†’ (๐‘†โ€˜๐‘ž) = {๐‘ฅ โˆˆ ๐ต โˆฃ (๐‘‚โ€˜๐‘ฅ) โˆฅ (๐‘žโ†‘(๐‘ž pCnt (โ™ฏโ€˜๐ต)))})
8382adantl 481 . . . 4 ((๐œ‘ โˆง ๐‘ž โˆˆ ๐ด) โ†’ (๐‘†โ€˜๐‘ž) = {๐‘ฅ โˆˆ ๐ต โˆฃ (๐‘‚โ€˜๐‘ฅ) โˆฅ (๐‘žโ†‘(๐‘ž pCnt (โ™ฏโ€˜๐ต)))})
8476, 83sseqtrrd 4019 . . 3 ((๐œ‘ โˆง ๐‘ž โˆˆ ๐ด) โ†’ (๐‘‡โ€˜๐‘ž) โІ (๐‘†โ€˜๐‘ž))
8548nnnn0d 12554 . . . . . 6 ((๐œ‘ โˆง ๐‘ž โˆˆ ๐ด) โ†’ (๐‘žโ†‘(๐‘ž pCnt (โ™ฏโ€˜๐ต))) โˆˆ โ„•0)
86 pcdvds 16824 . . . . . . . . . 10 ((๐‘ž โˆˆ โ„™ โˆง (โ™ฏโ€˜๐ต) โˆˆ โ„•) โ†’ (๐‘žโ†‘(๐‘ž pCnt (โ™ฏโ€˜๐ต))) โˆฅ (โ™ฏโ€˜๐ต))
8736, 46, 86syl2anc 583 . . . . . . . . 9 ((๐œ‘ โˆง ๐‘ž โˆˆ ๐ด) โ†’ (๐‘žโ†‘(๐‘ž pCnt (โ™ฏโ€˜๐ต))) โˆฅ (โ™ฏโ€˜๐ต))
882adantr 480 . . . . . . . . . . . . . . 15 ((๐œ‘ โˆง ๐‘ž โˆˆ ๐ด) โ†’ ๐บdom DProd ๐‘‡)
893adantr 480 . . . . . . . . . . . . . . 15 ((๐œ‘ โˆง ๐‘ž โˆˆ ๐ด) โ†’ dom ๐‘‡ = ๐ด)
90 ablfac1.2 . . . . . . . . . . . . . . . 16 (๐œ‘ โ†’ ๐ท โІ ๐ด)
9190adantr 480 . . . . . . . . . . . . . . 15 ((๐œ‘ โˆง ๐‘ž โˆˆ ๐ด) โ†’ ๐ท โІ ๐ด)
9288, 89, 91dprdres 19976 . . . . . . . . . . . . . 14 ((๐œ‘ โˆง ๐‘ž โˆˆ ๐ด) โ†’ (๐บdom DProd (๐‘‡ โ†พ ๐ท) โˆง (๐บ DProd (๐‘‡ โ†พ ๐ท)) โІ (๐บ DProd ๐‘‡)))
9392simpld 494 . . . . . . . . . . . . 13 ((๐œ‘ โˆง ๐‘ž โˆˆ ๐ด) โ†’ ๐บdom DProd (๐‘‡ โ†พ ๐ท))
944adantr 480 . . . . . . . . . . . . . . 15 ((๐œ‘ โˆง ๐‘ž โˆˆ ๐ด) โ†’ ๐‘‡:๐ดโŸถ(SubGrpโ€˜๐บ))
9594, 91fssresd 6758 . . . . . . . . . . . . . 14 ((๐œ‘ โˆง ๐‘ž โˆˆ ๐ด) โ†’ (๐‘‡ โ†พ ๐ท):๐ทโŸถ(SubGrpโ€˜๐บ))
9695fdmd 6727 . . . . . . . . . . . . 13 ((๐œ‘ โˆง ๐‘ž โˆˆ ๐ด) โ†’ dom (๐‘‡ โ†พ ๐ท) = ๐ท)
97 difssd 4128 . . . . . . . . . . . . 13 ((๐œ‘ โˆง ๐‘ž โˆˆ ๐ด) โ†’ (๐ท โˆ– {๐‘ž}) โІ ๐ท)
9893, 96, 97dprdres 19976 . . . . . . . . . . . 12 ((๐œ‘ โˆง ๐‘ž โˆˆ ๐ด) โ†’ (๐บdom DProd ((๐‘‡ โ†พ ๐ท) โ†พ (๐ท โˆ– {๐‘ž})) โˆง (๐บ DProd ((๐‘‡ โ†พ ๐ท) โ†พ (๐ท โˆ– {๐‘ž}))) โІ (๐บ DProd (๐‘‡ โ†พ ๐ท))))
9998simpld 494 . . . . . . . . . . 11 ((๐œ‘ โˆง ๐‘ž โˆˆ ๐ด) โ†’ ๐บdom DProd ((๐‘‡ โ†พ ๐ท) โ†พ (๐ท โˆ– {๐‘ž})))
100 dprdsubg 19972 . . . . . . . . . . 11 (๐บdom DProd ((๐‘‡ โ†พ ๐ท) โ†พ (๐ท โˆ– {๐‘ž})) โ†’ (๐บ DProd ((๐‘‡ โ†พ ๐ท) โ†พ (๐ท โˆ– {๐‘ž}))) โˆˆ (SubGrpโ€˜๐บ))
10199, 100syl 17 . . . . . . . . . 10 ((๐œ‘ โˆง ๐‘ž โˆˆ ๐ด) โ†’ (๐บ DProd ((๐‘‡ โ†พ ๐ท) โ†พ (๐ท โˆ– {๐‘ž}))) โˆˆ (SubGrpโ€˜๐บ))
1026lagsubg 19141 . . . . . . . . . 10 (((๐บ DProd ((๐‘‡ โ†พ ๐ท) โ†พ (๐ท โˆ– {๐‘ž}))) โˆˆ (SubGrpโ€˜๐บ) โˆง ๐ต โˆˆ Fin) โ†’ (โ™ฏโ€˜(๐บ DProd ((๐‘‡ โ†พ ๐ท) โ†พ (๐ท โˆ– {๐‘ž})))) โˆฅ (โ™ฏโ€˜๐ต))
103101, 19, 102syl2anc 583 . . . . . . . . 9 ((๐œ‘ โˆง ๐‘ž โˆˆ ๐ด) โ†’ (โ™ฏโ€˜(๐บ DProd ((๐‘‡ โ†พ ๐ท) โ†พ (๐ท โˆ– {๐‘ž})))) โˆฅ (โ™ฏโ€˜๐ต))
104 eqid 2727 . . . . . . . . . . . . . . 15 (0gโ€˜๐บ) = (0gโ€˜๐บ)
105104subg0cl 19080 . . . . . . . . . . . . . 14 ((๐บ DProd ((๐‘‡ โ†พ ๐ท) โ†พ (๐ท โˆ– {๐‘ž}))) โˆˆ (SubGrpโ€˜๐บ) โ†’ (0gโ€˜๐บ) โˆˆ (๐บ DProd ((๐‘‡ โ†พ ๐ท) โ†พ (๐ท โˆ– {๐‘ž}))))
106101, 105syl 17 . . . . . . . . . . . . 13 ((๐œ‘ โˆง ๐‘ž โˆˆ ๐ด) โ†’ (0gโ€˜๐บ) โˆˆ (๐บ DProd ((๐‘‡ โ†พ ๐ท) โ†พ (๐ท โˆ– {๐‘ž}))))
107106ne0d 4331 . . . . . . . . . . . 12 ((๐œ‘ โˆง ๐‘ž โˆˆ ๐ด) โ†’ (๐บ DProd ((๐‘‡ โ†พ ๐ท) โ†พ (๐ท โˆ– {๐‘ž}))) โ‰  โˆ…)
1086dprdssv 19964 . . . . . . . . . . . . . 14 (๐บ DProd ((๐‘‡ โ†พ ๐ท) โ†พ (๐ท โˆ– {๐‘ž}))) โІ ๐ต
109 ssfi 9189 . . . . . . . . . . . . . 14 ((๐ต โˆˆ Fin โˆง (๐บ DProd ((๐‘‡ โ†พ ๐ท) โ†พ (๐ท โˆ– {๐‘ž}))) โІ ๐ต) โ†’ (๐บ DProd ((๐‘‡ โ†พ ๐ท) โ†พ (๐ท โˆ– {๐‘ž}))) โˆˆ Fin)
11019, 108, 109sylancl 585 . . . . . . . . . . . . 13 ((๐œ‘ โˆง ๐‘ž โˆˆ ๐ด) โ†’ (๐บ DProd ((๐‘‡ โ†พ ๐ท) โ†พ (๐ท โˆ– {๐‘ž}))) โˆˆ Fin)
111 hashnncl 14349 . . . . . . . . . . . . 13 ((๐บ DProd ((๐‘‡ โ†พ ๐ท) โ†พ (๐ท โˆ– {๐‘ž}))) โˆˆ Fin โ†’ ((โ™ฏโ€˜(๐บ DProd ((๐‘‡ โ†พ ๐ท) โ†พ (๐ท โˆ– {๐‘ž})))) โˆˆ โ„• โ†” (๐บ DProd ((๐‘‡ โ†พ ๐ท) โ†พ (๐ท โˆ– {๐‘ž}))) โ‰  โˆ…))
112110, 111syl 17 . . . . . . . . . . . 12 ((๐œ‘ โˆง ๐‘ž โˆˆ ๐ด) โ†’ ((โ™ฏโ€˜(๐บ DProd ((๐‘‡ โ†พ ๐ท) โ†พ (๐ท โˆ– {๐‘ž})))) โˆˆ โ„• โ†” (๐บ DProd ((๐‘‡ โ†พ ๐ท) โ†พ (๐ท โˆ– {๐‘ž}))) โ‰  โˆ…))
113107, 112mpbird 257 . . . . . . . . . . 11 ((๐œ‘ โˆง ๐‘ž โˆˆ ๐ด) โ†’ (โ™ฏโ€˜(๐บ DProd ((๐‘‡ โ†พ ๐ท) โ†พ (๐ท โˆ– {๐‘ž})))) โˆˆ โ„•)
114113nnzd 12607 . . . . . . . . . 10 ((๐œ‘ โˆง ๐‘ž โˆˆ ๐ด) โ†’ (โ™ฏโ€˜(๐บ DProd ((๐‘‡ โ†พ ๐ท) โ†พ (๐ท โˆ– {๐‘ž})))) โˆˆ โ„ค)
115 id 22 . . . . . . . . . . . . . . 15 (๐‘ฅ = ๐‘ž โ†’ ๐‘ฅ = ๐‘ž)
116 sneq 4634 . . . . . . . . . . . . . . . . . . 19 (๐‘ฅ = ๐‘ž โ†’ {๐‘ฅ} = {๐‘ž})
117116difeq2d 4118 . . . . . . . . . . . . . . . . . 18 (๐‘ฅ = ๐‘ž โ†’ (๐ท โˆ– {๐‘ฅ}) = (๐ท โˆ– {๐‘ž}))
118117reseq2d 5979 . . . . . . . . . . . . . . . . 17 (๐‘ฅ = ๐‘ž โ†’ ((๐‘‡ โ†พ ๐ท) โ†พ (๐ท โˆ– {๐‘ฅ})) = ((๐‘‡ โ†พ ๐ท) โ†พ (๐ท โˆ– {๐‘ž})))
119118oveq2d 7430 . . . . . . . . . . . . . . . 16 (๐‘ฅ = ๐‘ž โ†’ (๐บ DProd ((๐‘‡ โ†พ ๐ท) โ†พ (๐ท โˆ– {๐‘ฅ}))) = (๐บ DProd ((๐‘‡ โ†พ ๐ท) โ†พ (๐ท โˆ– {๐‘ž}))))
120119fveq2d 6895 . . . . . . . . . . . . . . 15 (๐‘ฅ = ๐‘ž โ†’ (โ™ฏโ€˜(๐บ DProd ((๐‘‡ โ†พ ๐ท) โ†พ (๐ท โˆ– {๐‘ฅ})))) = (โ™ฏโ€˜(๐บ DProd ((๐‘‡ โ†พ ๐ท) โ†พ (๐ท โˆ– {๐‘ž})))))
121115, 120breq12d 5155 . . . . . . . . . . . . . 14 (๐‘ฅ = ๐‘ž โ†’ (๐‘ฅ โˆฅ (โ™ฏโ€˜(๐บ DProd ((๐‘‡ โ†พ ๐ท) โ†พ (๐ท โˆ– {๐‘ฅ})))) โ†” ๐‘ž โˆฅ (โ™ฏโ€˜(๐บ DProd ((๐‘‡ โ†พ ๐ท) โ†พ (๐ท โˆ– {๐‘ž}))))))
122121notbid 318 . . . . . . . . . . . . 13 (๐‘ฅ = ๐‘ž โ†’ (ยฌ ๐‘ฅ โˆฅ (โ™ฏโ€˜(๐บ DProd ((๐‘‡ โ†พ ๐ท) โ†พ (๐ท โˆ– {๐‘ฅ})))) โ†” ยฌ ๐‘ž โˆฅ (โ™ฏโ€˜(๐บ DProd ((๐‘‡ โ†พ ๐ท) โ†พ (๐ท โˆ– {๐‘ž}))))))
123 eqid 2727 . . . . . . . . . . . . . . . 16 (๐‘ โˆˆ ๐ท โ†ฆ {๐‘ฆ โˆˆ ๐ต โˆฃ (๐‘‚โ€˜๐‘ฆ) โˆฅ (๐‘โ†‘(๐‘ pCnt (โ™ฏโ€˜๐ต)))}) = (๐‘ โˆˆ ๐ท โ†ฆ {๐‘ฆ โˆˆ ๐ต โˆฃ (๐‘‚โ€˜๐‘ฆ) โˆฅ (๐‘โ†‘(๐‘ pCnt (โ™ฏโ€˜๐ต)))})
1249adantr 480 . . . . . . . . . . . . . . . 16 ((๐œ‘ โˆง ๐‘ฅ โˆˆ โ„™) โ†’ ๐บ โˆˆ Abel)
12510adantr 480 . . . . . . . . . . . . . . . 16 ((๐œ‘ โˆง ๐‘ฅ โˆˆ โ„™) โ†’ ๐ต โˆˆ Fin)
126 ablfac1c.d . . . . . . . . . . . . . . . . . 18 ๐ท = {๐‘ค โˆˆ โ„™ โˆฃ ๐‘ค โˆฅ (โ™ฏโ€˜๐ต)}
127126ssrab3 4076 . . . . . . . . . . . . . . . . 17 ๐ท โІ โ„™
128127a1i 11 . . . . . . . . . . . . . . . 16 ((๐œ‘ โˆง ๐‘ฅ โˆˆ โ„™) โ†’ ๐ท โІ โ„™)
129 ssidd 4001 . . . . . . . . . . . . . . . 16 ((๐œ‘ โˆง ๐‘ฅ โˆˆ โ„™) โ†’ ๐ท โІ ๐ท)
1302, 3, 90dprdres 19976 . . . . . . . . . . . . . . . . . . 19 (๐œ‘ โ†’ (๐บdom DProd (๐‘‡ โ†พ ๐ท) โˆง (๐บ DProd (๐‘‡ โ†พ ๐ท)) โІ (๐บ DProd ๐‘‡)))
131130simpld 494 . . . . . . . . . . . . . . . . . 18 (๐œ‘ โ†’ ๐บdom DProd (๐‘‡ โ†พ ๐ท))
132 dprdsubg 19972 . . . . . . . . . . . . . . . . . . . . 21 (๐บdom DProd (๐‘‡ โ†พ ๐ท) โ†’ (๐บ DProd (๐‘‡ โ†พ ๐ท)) โˆˆ (SubGrpโ€˜๐บ))
133131, 132syl 17 . . . . . . . . . . . . . . . . . . . 20 (๐œ‘ โ†’ (๐บ DProd (๐‘‡ โ†พ ๐ท)) โˆˆ (SubGrpโ€˜๐บ))
134 difssd 4128 . . . . . . . . . . . . . . . . . . . . . . 23 (๐œ‘ โ†’ (๐ด โˆ– ๐ท) โІ ๐ด)
1352, 3, 134dprdres 19976 . . . . . . . . . . . . . . . . . . . . . 22 (๐œ‘ โ†’ (๐บdom DProd (๐‘‡ โ†พ (๐ด โˆ– ๐ท)) โˆง (๐บ DProd (๐‘‡ โ†พ (๐ด โˆ– ๐ท))) โІ (๐บ DProd ๐‘‡)))
136135simpld 494 . . . . . . . . . . . . . . . . . . . . 21 (๐œ‘ โ†’ ๐บdom DProd (๐‘‡ โ†พ (๐ด โˆ– ๐ท)))
137 dprdsubg 19972 . . . . . . . . . . . . . . . . . . . . 21 (๐บdom DProd (๐‘‡ โ†พ (๐ด โˆ– ๐ท)) โ†’ (๐บ DProd (๐‘‡ โ†พ (๐ด โˆ– ๐ท))) โˆˆ (SubGrpโ€˜๐บ))
138136, 137syl 17 . . . . . . . . . . . . . . . . . . . 20 (๐œ‘ โ†’ (๐บ DProd (๐‘‡ โ†พ (๐ด โˆ– ๐ท))) โˆˆ (SubGrpโ€˜๐บ))
139 difss 4127 . . . . . . . . . . . . . . . . . . . . . . 23 (๐ด โˆ– ๐ท) โІ ๐ด
140 fssres 6757 . . . . . . . . . . . . . . . . . . . . . . 23 ((๐‘‡:๐ดโŸถ(SubGrpโ€˜๐บ) โˆง (๐ด โˆ– ๐ท) โІ ๐ด) โ†’ (๐‘‡ โ†พ (๐ด โˆ– ๐ท)):(๐ด โˆ– ๐ท)โŸถ(SubGrpโ€˜๐บ))
1414, 139, 140sylancl 585 . . . . . . . . . . . . . . . . . . . . . 22 (๐œ‘ โ†’ (๐‘‡ โ†พ (๐ด โˆ– ๐ท)):(๐ด โˆ– ๐ท)โŸถ(SubGrpโ€˜๐บ))
142141fdmd 6727 . . . . . . . . . . . . . . . . . . . . 21 (๐œ‘ โ†’ dom (๐‘‡ โ†พ (๐ด โˆ– ๐ท)) = (๐ด โˆ– ๐ท))
143 fvres 6910 . . . . . . . . . . . . . . . . . . . . . . 23 (๐‘ž โˆˆ (๐ด โˆ– ๐ท) โ†’ ((๐‘‡ โ†พ (๐ด โˆ– ๐ท))โ€˜๐‘ž) = (๐‘‡โ€˜๐‘ž))
144143adantl 481 . . . . . . . . . . . . . . . . . . . . . 22 ((๐œ‘ โˆง ๐‘ž โˆˆ (๐ด โˆ– ๐ท)) โ†’ ((๐‘‡ โ†พ (๐ด โˆ– ๐ท))โ€˜๐‘ž) = (๐‘‡โ€˜๐‘ž))
145 eldif 3954 . . . . . . . . . . . . . . . . . . . . . . 23 (๐‘ž โˆˆ (๐ด โˆ– ๐ท) โ†” (๐‘ž โˆˆ ๐ด โˆง ยฌ ๐‘ž โˆˆ ๐ท))
14631adantrr 716 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((๐œ‘ โˆง (๐‘ž โˆˆ ๐ด โˆง ยฌ ๐‘ž โˆˆ ๐ท)) โ†’ (๐‘‡โ€˜๐‘ž) โˆˆ Fin)
147104subg0cl 19080 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((๐‘‡โ€˜๐‘ž) โˆˆ (SubGrpโ€˜๐บ) โ†’ (0gโ€˜๐บ) โˆˆ (๐‘‡โ€˜๐‘ž))
14824, 147syl 17 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((๐œ‘ โˆง ๐‘ž โˆˆ ๐ด) โ†’ (0gโ€˜๐บ) โˆˆ (๐‘‡โ€˜๐‘ž))
149148snssd 4808 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((๐œ‘ โˆง ๐‘ž โˆˆ ๐ด) โ†’ {(0gโ€˜๐บ)} โІ (๐‘‡โ€˜๐‘ž))
150149adantrr 716 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((๐œ‘ โˆง (๐‘ž โˆˆ ๐ด โˆง ยฌ ๐‘ž โˆˆ ๐ท)) โ†’ {(0gโ€˜๐บ)} โІ (๐‘‡โ€˜๐‘ž))
151 fvex 6904 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (0gโ€˜๐บ) โˆˆ V
152 hashsng 14352 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((0gโ€˜๐บ) โˆˆ V โ†’ (โ™ฏโ€˜{(0gโ€˜๐บ)}) = 1)
153151, 152ax-mp 5 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (โ™ฏโ€˜{(0gโ€˜๐บ)}) = 1
15456adantrr 716 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((๐œ‘ โˆง (๐‘ž โˆˆ ๐ด โˆง ยฌ ๐‘ž โˆˆ ๐ท)) โ†’ (โ™ฏโ€˜(๐‘‡โ€˜๐‘ž)) = (๐‘žโ†‘๐ถ))
15536adantr 480 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 (((๐œ‘ โˆง ๐‘ž โˆˆ ๐ด) โˆง ๐ถ โˆˆ โ„•) โ†’ ๐‘ž โˆˆ โ„™)
156 iddvdsexp 16248 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 ((๐‘ž โˆˆ โ„ค โˆง ๐ถ โˆˆ โ„•) โ†’ ๐‘ž โˆฅ (๐‘žโ†‘๐ถ))
15758, 156sylan 579 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 (((๐œ‘ โˆง ๐‘ž โˆˆ ๐ด) โˆง ๐ถ โˆˆ โ„•) โ†’ ๐‘ž โˆฅ (๐‘žโ†‘๐ถ))
15864adantr 480 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 (((๐œ‘ โˆง ๐‘ž โˆˆ ๐ด) โˆง ๐ถ โˆˆ โ„•) โ†’ (๐‘žโ†‘๐ถ) โˆฅ (โ™ฏโ€˜๐ต))
15956, 34eqeltrrd 2829 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 ((๐œ‘ โˆง ๐‘ž โˆˆ ๐ด) โ†’ (๐‘žโ†‘๐ถ) โˆˆ โ„ค)
160 dvdstr 16262 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 ((๐‘ž โˆˆ โ„ค โˆง (๐‘žโ†‘๐ถ) โˆˆ โ„ค โˆง (โ™ฏโ€˜๐ต) โˆˆ โ„ค) โ†’ ((๐‘ž โˆฅ (๐‘žโ†‘๐ถ) โˆง (๐‘žโ†‘๐ถ) โˆฅ (โ™ฏโ€˜๐ต)) โ†’ ๐‘ž โˆฅ (โ™ฏโ€˜๐ต)))
16158, 159, 65, 160syl3anc 1369 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 ((๐œ‘ โˆง ๐‘ž โˆˆ ๐ด) โ†’ ((๐‘ž โˆฅ (๐‘žโ†‘๐ถ) โˆง (๐‘žโ†‘๐ถ) โˆฅ (โ™ฏโ€˜๐ต)) โ†’ ๐‘ž โˆฅ (โ™ฏโ€˜๐ต)))
162161adantr 480 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 (((๐œ‘ โˆง ๐‘ž โˆˆ ๐ด) โˆง ๐ถ โˆˆ โ„•) โ†’ ((๐‘ž โˆฅ (๐‘žโ†‘๐ถ) โˆง (๐‘žโ†‘๐ถ) โˆฅ (โ™ฏโ€˜๐ต)) โ†’ ๐‘ž โˆฅ (โ™ฏโ€˜๐ต)))
163157, 158, 162mp2and 698 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 (((๐œ‘ โˆง ๐‘ž โˆˆ ๐ด) โˆง ๐ถ โˆˆ โ„•) โ†’ ๐‘ž โˆฅ (โ™ฏโ€˜๐ต))
164 breq1 5145 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 (๐‘ค = ๐‘ž โ†’ (๐‘ค โˆฅ (โ™ฏโ€˜๐ต) โ†” ๐‘ž โˆฅ (โ™ฏโ€˜๐ต)))
165164, 126elrab2 3683 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 (๐‘ž โˆˆ ๐ท โ†” (๐‘ž โˆˆ โ„™ โˆง ๐‘ž โˆฅ (โ™ฏโ€˜๐ต)))
166155, 163, 165sylanbrc 582 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 (((๐œ‘ โˆง ๐‘ž โˆˆ ๐ด) โˆง ๐ถ โˆˆ โ„•) โ†’ ๐‘ž โˆˆ ๐ท)
167166ex 412 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ((๐œ‘ โˆง ๐‘ž โˆˆ ๐ด) โ†’ (๐ถ โˆˆ โ„• โ†’ ๐‘ž โˆˆ ๐ท))
168167con3d 152 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ((๐œ‘ โˆง ๐‘ž โˆˆ ๐ด) โ†’ (ยฌ ๐‘ž โˆˆ ๐ท โ†’ ยฌ ๐ถ โˆˆ โ„•))
169168impr 454 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ((๐œ‘ โˆง (๐‘ž โˆˆ ๐ด โˆง ยฌ ๐‘ž โˆˆ ๐ท)) โ†’ ยฌ ๐ถ โˆˆ โ„•)
17059adantrr 716 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ((๐œ‘ โˆง (๐‘ž โˆˆ ๐ด โˆง ยฌ ๐‘ž โˆˆ ๐ท)) โ†’ ๐ถ โˆˆ โ„•0)
171 elnn0 12496 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 (๐ถ โˆˆ โ„•0 โ†” (๐ถ โˆˆ โ„• โˆจ ๐ถ = 0))
172170, 171sylib 217 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ((๐œ‘ โˆง (๐‘ž โˆˆ ๐ด โˆง ยฌ ๐‘ž โˆˆ ๐ท)) โ†’ (๐ถ โˆˆ โ„• โˆจ ๐ถ = 0))
173172ord 863 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ((๐œ‘ โˆง (๐‘ž โˆˆ ๐ด โˆง ยฌ ๐‘ž โˆˆ ๐ท)) โ†’ (ยฌ ๐ถ โˆˆ โ„• โ†’ ๐ถ = 0))
174169, 173mpd 15 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ((๐œ‘ โˆง (๐‘ž โˆˆ ๐ด โˆง ยฌ ๐‘ž โˆˆ ๐ท)) โ†’ ๐ถ = 0)
175174oveq2d 7430 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((๐œ‘ โˆง (๐‘ž โˆˆ ๐ด โˆง ยฌ ๐‘ž โˆˆ ๐ท)) โ†’ (๐‘žโ†‘๐ถ) = (๐‘žโ†‘0))
17638adantrr 716 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ((๐œ‘ โˆง (๐‘ž โˆˆ ๐ด โˆง ยฌ ๐‘ž โˆˆ ๐ท)) โ†’ ๐‘ž โˆˆ โ„•)
177176nncnd 12250 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ((๐œ‘ โˆง (๐‘ž โˆˆ ๐ด โˆง ยฌ ๐‘ž โˆˆ ๐ท)) โ†’ ๐‘ž โˆˆ โ„‚)
178177exp0d 14128 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((๐œ‘ โˆง (๐‘ž โˆˆ ๐ด โˆง ยฌ ๐‘ž โˆˆ ๐ท)) โ†’ (๐‘žโ†‘0) = 1)
179154, 175, 1783eqtrd 2771 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((๐œ‘ โˆง (๐‘ž โˆˆ ๐ด โˆง ยฌ ๐‘ž โˆˆ ๐ท)) โ†’ (โ™ฏโ€˜(๐‘‡โ€˜๐‘ž)) = 1)
180153, 179eqtr4id 2786 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((๐œ‘ โˆง (๐‘ž โˆˆ ๐ด โˆง ยฌ ๐‘ž โˆˆ ๐ท)) โ†’ (โ™ฏโ€˜{(0gโ€˜๐บ)}) = (โ™ฏโ€˜(๐‘‡โ€˜๐‘ž)))
181 snfi 9060 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 {(0gโ€˜๐บ)} โˆˆ Fin
182 hashen 14330 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (({(0gโ€˜๐บ)} โˆˆ Fin โˆง (๐‘‡โ€˜๐‘ž) โˆˆ Fin) โ†’ ((โ™ฏโ€˜{(0gโ€˜๐บ)}) = (โ™ฏโ€˜(๐‘‡โ€˜๐‘ž)) โ†” {(0gโ€˜๐บ)} โ‰ˆ (๐‘‡โ€˜๐‘ž)))
183181, 146, 182sylancr 586 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((๐œ‘ โˆง (๐‘ž โˆˆ ๐ด โˆง ยฌ ๐‘ž โˆˆ ๐ท)) โ†’ ((โ™ฏโ€˜{(0gโ€˜๐บ)}) = (โ™ฏโ€˜(๐‘‡โ€˜๐‘ž)) โ†” {(0gโ€˜๐บ)} โ‰ˆ (๐‘‡โ€˜๐‘ž)))
184180, 183mpbid 231 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((๐œ‘ โˆง (๐‘ž โˆˆ ๐ด โˆง ยฌ ๐‘ž โˆˆ ๐ท)) โ†’ {(0gโ€˜๐บ)} โ‰ˆ (๐‘‡โ€˜๐‘ž))
185 fisseneq 9273 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((๐‘‡โ€˜๐‘ž) โˆˆ Fin โˆง {(0gโ€˜๐บ)} โІ (๐‘‡โ€˜๐‘ž) โˆง {(0gโ€˜๐บ)} โ‰ˆ (๐‘‡โ€˜๐‘ž)) โ†’ {(0gโ€˜๐บ)} = (๐‘‡โ€˜๐‘ž))
186146, 150, 184, 185syl3anc 1369 . . . . . . . . . . . . . . . . . . . . . . . 24 ((๐œ‘ โˆง (๐‘ž โˆˆ ๐ด โˆง ยฌ ๐‘ž โˆˆ ๐ท)) โ†’ {(0gโ€˜๐บ)} = (๐‘‡โ€˜๐‘ž))
187104subg0cl 19080 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((๐บ DProd (๐‘‡ โ†พ ๐ท)) โˆˆ (SubGrpโ€˜๐บ) โ†’ (0gโ€˜๐บ) โˆˆ (๐บ DProd (๐‘‡ โ†พ ๐ท)))
188133, 187syl 17 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (๐œ‘ โ†’ (0gโ€˜๐บ) โˆˆ (๐บ DProd (๐‘‡ โ†พ ๐ท)))
189188adantr 480 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((๐œ‘ โˆง (๐‘ž โˆˆ ๐ด โˆง ยฌ ๐‘ž โˆˆ ๐ท)) โ†’ (0gโ€˜๐บ) โˆˆ (๐บ DProd (๐‘‡ โ†พ ๐ท)))
190189snssd 4808 . . . . . . . . . . . . . . . . . . . . . . . 24 ((๐œ‘ โˆง (๐‘ž โˆˆ ๐ด โˆง ยฌ ๐‘ž โˆˆ ๐ท)) โ†’ {(0gโ€˜๐บ)} โІ (๐บ DProd (๐‘‡ โ†พ ๐ท)))
191186, 190eqsstrrd 4017 . . . . . . . . . . . . . . . . . . . . . . 23 ((๐œ‘ โˆง (๐‘ž โˆˆ ๐ด โˆง ยฌ ๐‘ž โˆˆ ๐ท)) โ†’ (๐‘‡โ€˜๐‘ž) โІ (๐บ DProd (๐‘‡ โ†พ ๐ท)))
192145, 191sylan2b 593 . . . . . . . . . . . . . . . . . . . . . 22 ((๐œ‘ โˆง ๐‘ž โˆˆ (๐ด โˆ– ๐ท)) โ†’ (๐‘‡โ€˜๐‘ž) โІ (๐บ DProd (๐‘‡ โ†พ ๐ท)))
193144, 192eqsstrd 4016 . . . . . . . . . . . . . . . . . . . . 21 ((๐œ‘ โˆง ๐‘ž โˆˆ (๐ด โˆ– ๐ท)) โ†’ ((๐‘‡ โ†พ (๐ด โˆ– ๐ท))โ€˜๐‘ž) โІ (๐บ DProd (๐‘‡ โ†พ ๐ท)))
194136, 142, 133, 193dprdlub 19974 . . . . . . . . . . . . . . . . . . . 20 (๐œ‘ โ†’ (๐บ DProd (๐‘‡ โ†พ (๐ด โˆ– ๐ท))) โІ (๐บ DProd (๐‘‡ โ†พ ๐ท)))
195 eqid 2727 . . . . . . . . . . . . . . . . . . . . 21 (LSSumโ€˜๐บ) = (LSSumโ€˜๐บ)
196195lsmss2 19613 . . . . . . . . . . . . . . . . . . . 20 (((๐บ DProd (๐‘‡ โ†พ ๐ท)) โˆˆ (SubGrpโ€˜๐บ) โˆง (๐บ DProd (๐‘‡ โ†พ (๐ด โˆ– ๐ท))) โˆˆ (SubGrpโ€˜๐บ) โˆง (๐บ DProd (๐‘‡ โ†พ (๐ด โˆ– ๐ท))) โІ (๐บ DProd (๐‘‡ โ†พ ๐ท))) โ†’ ((๐บ DProd (๐‘‡ โ†พ ๐ท))(LSSumโ€˜๐บ)(๐บ DProd (๐‘‡ โ†พ (๐ด โˆ– ๐ท)))) = (๐บ DProd (๐‘‡ โ†พ ๐ท)))
197133, 138, 194, 196syl3anc 1369 . . . . . . . . . . . . . . . . . . 19 (๐œ‘ โ†’ ((๐บ DProd (๐‘‡ โ†พ ๐ท))(LSSumโ€˜๐บ)(๐บ DProd (๐‘‡ โ†พ (๐ด โˆ– ๐ท)))) = (๐บ DProd (๐‘‡ โ†พ ๐ท)))
198 disjdif 4467 . . . . . . . . . . . . . . . . . . . . . 22 (๐ท โˆฉ (๐ด โˆ– ๐ท)) = โˆ…
199198a1i 11 . . . . . . . . . . . . . . . . . . . . 21 (๐œ‘ โ†’ (๐ท โˆฉ (๐ด โˆ– ๐ท)) = โˆ…)
200 undif2 4472 . . . . . . . . . . . . . . . . . . . . . 22 (๐ท โˆช (๐ด โˆ– ๐ท)) = (๐ท โˆช ๐ด)
201 ssequn1 4176 . . . . . . . . . . . . . . . . . . . . . . 23 (๐ท โІ ๐ด โ†” (๐ท โˆช ๐ด) = ๐ด)
20290, 201sylib 217 . . . . . . . . . . . . . . . . . . . . . 22 (๐œ‘ โ†’ (๐ท โˆช ๐ด) = ๐ด)
203200, 202eqtr2id 2780 . . . . . . . . . . . . . . . . . . . . 21 (๐œ‘ โ†’ ๐ด = (๐ท โˆช (๐ด โˆ– ๐ท)))
2044, 199, 203, 195, 2dprdsplit 19996 . . . . . . . . . . . . . . . . . . . 20 (๐œ‘ โ†’ (๐บ DProd ๐‘‡) = ((๐บ DProd (๐‘‡ โ†พ ๐ท))(LSSumโ€˜๐บ)(๐บ DProd (๐‘‡ โ†พ (๐ด โˆ– ๐ท)))))
2051simprd 495 . . . . . . . . . . . . . . . . . . . 20 (๐œ‘ โ†’ (๐บ DProd ๐‘‡) = ๐ต)
206204, 205eqtr3d 2769 . . . . . . . . . . . . . . . . . . 19 (๐œ‘ โ†’ ((๐บ DProd (๐‘‡ โ†พ ๐ท))(LSSumโ€˜๐บ)(๐บ DProd (๐‘‡ โ†พ (๐ด โˆ– ๐ท)))) = ๐ต)
207197, 206eqtr3d 2769 . . . . . . . . . . . . . . . . . 18 (๐œ‘ โ†’ (๐บ DProd (๐‘‡ โ†พ ๐ท)) = ๐ต)
208131, 207jca 511 . . . . . . . . . . . . . . . . 17 (๐œ‘ โ†’ (๐บdom DProd (๐‘‡ โ†พ ๐ท) โˆง (๐บ DProd (๐‘‡ โ†พ ๐ท)) = ๐ต))
209208adantr 480 . . . . . . . . . . . . . . . 16 ((๐œ‘ โˆง ๐‘ฅ โˆˆ โ„™) โ†’ (๐บdom DProd (๐‘‡ โ†พ ๐ท) โˆง (๐บ DProd (๐‘‡ โ†พ ๐ท)) = ๐ต))
2104, 90fssresd 6758 . . . . . . . . . . . . . . . . . 18 (๐œ‘ โ†’ (๐‘‡ โ†พ ๐ท):๐ทโŸถ(SubGrpโ€˜๐บ))
211210fdmd 6727 . . . . . . . . . . . . . . . . 17 (๐œ‘ โ†’ dom (๐‘‡ โ†พ ๐ท) = ๐ท)
212211adantr 480 . . . . . . . . . . . . . . . 16 ((๐œ‘ โˆง ๐‘ฅ โˆˆ โ„™) โ†’ dom (๐‘‡ โ†พ ๐ท) = ๐ท)
21390sselda 3978 . . . . . . . . . . . . . . . . . 18 ((๐œ‘ โˆง ๐‘ž โˆˆ ๐ท) โ†’ ๐‘ž โˆˆ ๐ด)
214213, 59syldan 590 . . . . . . . . . . . . . . . . 17 ((๐œ‘ โˆง ๐‘ž โˆˆ ๐ท) โ†’ ๐ถ โˆˆ โ„•0)
215214adantlr 714 . . . . . . . . . . . . . . . 16 (((๐œ‘ โˆง ๐‘ฅ โˆˆ โ„™) โˆง ๐‘ž โˆˆ ๐ท) โ†’ ๐ถ โˆˆ โ„•0)
216 fvres 6910 . . . . . . . . . . . . . . . . . . . 20 (๐‘ž โˆˆ ๐ท โ†’ ((๐‘‡ โ†พ ๐ท)โ€˜๐‘ž) = (๐‘‡โ€˜๐‘ž))
217216adantl 481 . . . . . . . . . . . . . . . . . . 19 ((๐œ‘ โˆง ๐‘ž โˆˆ ๐ท) โ†’ ((๐‘‡ โ†พ ๐ท)โ€˜๐‘ž) = (๐‘‡โ€˜๐‘ž))
218217fveq2d 6895 . . . . . . . . . . . . . . . . . 18 ((๐œ‘ โˆง ๐‘ž โˆˆ ๐ท) โ†’ (โ™ฏโ€˜((๐‘‡ โ†พ ๐ท)โ€˜๐‘ž)) = (โ™ฏโ€˜(๐‘‡โ€˜๐‘ž)))
219213, 56syldan 590 . . . . . . . . . . . . . . . . . 18 ((๐œ‘ โˆง ๐‘ž โˆˆ ๐ท) โ†’ (โ™ฏโ€˜(๐‘‡โ€˜๐‘ž)) = (๐‘žโ†‘๐ถ))
220218, 219eqtrd 2767 . . . . . . . . . . . . . . . . 17 ((๐œ‘ โˆง ๐‘ž โˆˆ ๐ท) โ†’ (โ™ฏโ€˜((๐‘‡ โ†พ ๐ท)โ€˜๐‘ž)) = (๐‘žโ†‘๐ถ))
221220adantlr 714 . . . . . . . . . . . . . . . 16 (((๐œ‘ โˆง ๐‘ฅ โˆˆ โ„™) โˆง ๐‘ž โˆˆ ๐ท) โ†’ (โ™ฏโ€˜((๐‘‡ โ†พ ๐ท)โ€˜๐‘ž)) = (๐‘žโ†‘๐ถ))
222 simpr 484 . . . . . . . . . . . . . . . 16 ((๐œ‘ โˆง ๐‘ฅ โˆˆ โ„™) โ†’ ๐‘ฅ โˆˆ โ„™)
223 fzfid 13962 . . . . . . . . . . . . . . . . . 18 (๐œ‘ โ†’ (1...(โ™ฏโ€˜๐ต)) โˆˆ Fin)
224 prmnn 16636 . . . . . . . . . . . . . . . . . . . . . 22 (๐‘ค โˆˆ โ„™ โ†’ ๐‘ค โˆˆ โ„•)
2252243ad2ant2 1132 . . . . . . . . . . . . . . . . . . . . 21 ((๐œ‘ โˆง ๐‘ค โˆˆ โ„™ โˆง ๐‘ค โˆฅ (โ™ฏโ€˜๐ต)) โ†’ ๐‘ค โˆˆ โ„•)
226 prmz 16637 . . . . . . . . . . . . . . . . . . . . . . 23 (๐‘ค โˆˆ โ„™ โ†’ ๐‘ค โˆˆ โ„ค)
227 dvdsle 16278 . . . . . . . . . . . . . . . . . . . . . . 23 ((๐‘ค โˆˆ โ„ค โˆง (โ™ฏโ€˜๐ต) โˆˆ โ„•) โ†’ (๐‘ค โˆฅ (โ™ฏโ€˜๐ต) โ†’ ๐‘ค โ‰ค (โ™ฏโ€˜๐ต)))
228226, 45, 227syl2anr 596 . . . . . . . . . . . . . . . . . . . . . 22 ((๐œ‘ โˆง ๐‘ค โˆˆ โ„™) โ†’ (๐‘ค โˆฅ (โ™ฏโ€˜๐ต) โ†’ ๐‘ค โ‰ค (โ™ฏโ€˜๐ต)))
2292283impia 1115 . . . . . . . . . . . . . . . . . . . . 21 ((๐œ‘ โˆง ๐‘ค โˆˆ โ„™ โˆง ๐‘ค โˆฅ (โ™ฏโ€˜๐ต)) โ†’ ๐‘ค โ‰ค (โ™ฏโ€˜๐ต))
23045nnzd 12607 . . . . . . . . . . . . . . . . . . . . . . 23 (๐œ‘ โ†’ (โ™ฏโ€˜๐ต) โˆˆ โ„ค)
2312303ad2ant1 1131 . . . . . . . . . . . . . . . . . . . . . 22 ((๐œ‘ โˆง ๐‘ค โˆˆ โ„™ โˆง ๐‘ค โˆฅ (โ™ฏโ€˜๐ต)) โ†’ (โ™ฏโ€˜๐ต) โˆˆ โ„ค)
232 fznn 13593 . . . . . . . . . . . . . . . . . . . . . 22 ((โ™ฏโ€˜๐ต) โˆˆ โ„ค โ†’ (๐‘ค โˆˆ (1...(โ™ฏโ€˜๐ต)) โ†” (๐‘ค โˆˆ โ„• โˆง ๐‘ค โ‰ค (โ™ฏโ€˜๐ต))))
233231, 232syl 17 . . . . . . . . . . . . . . . . . . . . 21 ((๐œ‘ โˆง ๐‘ค โˆˆ โ„™ โˆง ๐‘ค โˆฅ (โ™ฏโ€˜๐ต)) โ†’ (๐‘ค โˆˆ (1...(โ™ฏโ€˜๐ต)) โ†” (๐‘ค โˆˆ โ„• โˆง ๐‘ค โ‰ค (โ™ฏโ€˜๐ต))))
234225, 229, 233mpbir2and 712 . . . . . . . . . . . . . . . . . . . 20 ((๐œ‘ โˆง ๐‘ค โˆˆ โ„™ โˆง ๐‘ค โˆฅ (โ™ฏโ€˜๐ต)) โ†’ ๐‘ค โˆˆ (1...(โ™ฏโ€˜๐ต)))
235234rabssdv 4068 . . . . . . . . . . . . . . . . . . 19 (๐œ‘ โ†’ {๐‘ค โˆˆ โ„™ โˆฃ ๐‘ค โˆฅ (โ™ฏโ€˜๐ต)} โІ (1...(โ™ฏโ€˜๐ต)))
236126, 235eqsstrid 4026 . . . . . . . . . . . . . . . . . 18 (๐œ‘ โ†’ ๐ท โІ (1...(โ™ฏโ€˜๐ต)))
237223, 236ssfid 9283 . . . . . . . . . . . . . . . . 17 (๐œ‘ โ†’ ๐ท โˆˆ Fin)
238237adantr 480 . . . . . . . . . . . . . . . 16 ((๐œ‘ โˆง ๐‘ฅ โˆˆ โ„™) โ†’ ๐ท โˆˆ Fin)
2396, 7, 123, 124, 125, 128, 126, 129, 209, 212, 215, 221, 222, 238ablfac1eulem 20020 . . . . . . . . . . . . . . 15 ((๐œ‘ โˆง ๐‘ฅ โˆˆ โ„™) โ†’ ยฌ ๐‘ฅ โˆฅ (โ™ฏโ€˜(๐บ DProd ((๐‘‡ โ†พ ๐ท) โ†พ (๐ท โˆ– {๐‘ฅ})))))
240239ralrimiva 3141 . . . . . . . . . . . . . 14 (๐œ‘ โ†’ โˆ€๐‘ฅ โˆˆ โ„™ ยฌ ๐‘ฅ โˆฅ (โ™ฏโ€˜(๐บ DProd ((๐‘‡ โ†พ ๐ท) โ†พ (๐ท โˆ– {๐‘ฅ})))))
241240adantr 480 . . . . . . . . . . . . 13 ((๐œ‘ โˆง ๐‘ž โˆˆ ๐ด) โ†’ โˆ€๐‘ฅ โˆˆ โ„™ ยฌ ๐‘ฅ โˆฅ (โ™ฏโ€˜(๐บ DProd ((๐‘‡ โ†พ ๐ท) โ†พ (๐ท โˆ– {๐‘ฅ})))))
242122, 241, 36rspcdva 3608 . . . . . . . . . . . 12 ((๐œ‘ โˆง ๐‘ž โˆˆ ๐ด) โ†’ ยฌ ๐‘ž โˆฅ (โ™ฏโ€˜(๐บ DProd ((๐‘‡ โ†พ ๐ท) โ†พ (๐ท โˆ– {๐‘ž})))))
243 coprm 16673 . . . . . . . . . . . . 13 ((๐‘ž โˆˆ โ„™ โˆง (โ™ฏโ€˜(๐บ DProd ((๐‘‡ โ†พ ๐ท) โ†พ (๐ท โˆ– {๐‘ž})))) โˆˆ โ„ค) โ†’ (ยฌ ๐‘ž โˆฅ (โ™ฏโ€˜(๐บ DProd ((๐‘‡ โ†พ ๐ท) โ†พ (๐ท โˆ– {๐‘ž})))) โ†” (๐‘ž gcd (โ™ฏโ€˜(๐บ DProd ((๐‘‡ โ†พ ๐ท) โ†พ (๐ท โˆ– {๐‘ž}))))) = 1))
24436, 114, 243syl2anc 583 . . . . . . . . . . . 12 ((๐œ‘ โˆง ๐‘ž โˆˆ ๐ด) โ†’ (ยฌ ๐‘ž โˆฅ (โ™ฏโ€˜(๐บ DProd ((๐‘‡ โ†พ ๐ท) โ†พ (๐ท โˆ– {๐‘ž})))) โ†” (๐‘ž gcd (โ™ฏโ€˜(๐บ DProd ((๐‘‡ โ†พ ๐ท) โ†พ (๐ท โˆ– {๐‘ž}))))) = 1))
245242, 244mpbid 231 . . . . . . . . . . 11 ((๐œ‘ โˆง ๐‘ž โˆˆ ๐ด) โ†’ (๐‘ž gcd (โ™ฏโ€˜(๐บ DProd ((๐‘‡ โ†พ ๐ท) โ†พ (๐ท โˆ– {๐‘ž}))))) = 1)
246 rpexp1i 16686 . . . . . . . . . . . 12 ((๐‘ž โˆˆ โ„ค โˆง (โ™ฏโ€˜(๐บ DProd ((๐‘‡ โ†พ ๐ท) โ†พ (๐ท โˆ– {๐‘ž})))) โˆˆ โ„ค โˆง (๐‘ž pCnt (โ™ฏโ€˜๐ต)) โˆˆ โ„•0) โ†’ ((๐‘ž gcd (โ™ฏโ€˜(๐บ DProd ((๐‘‡ โ†พ ๐ท) โ†พ (๐ท โˆ– {๐‘ž}))))) = 1 โ†’ ((๐‘žโ†‘(๐‘ž pCnt (โ™ฏโ€˜๐ต))) gcd (โ™ฏโ€˜(๐บ DProd ((๐‘‡ โ†พ ๐ท) โ†พ (๐ท โˆ– {๐‘ž}))))) = 1))
24758, 114, 47, 246syl3anc 1369 . . . . . . . . . . 11 ((๐œ‘ โˆง ๐‘ž โˆˆ ๐ด) โ†’ ((๐‘ž gcd (โ™ฏโ€˜(๐บ DProd ((๐‘‡ โ†พ ๐ท) โ†พ (๐ท โˆ– {๐‘ž}))))) = 1 โ†’ ((๐‘žโ†‘(๐‘ž pCnt (โ™ฏโ€˜๐ต))) gcd (โ™ฏโ€˜(๐บ DProd ((๐‘‡ โ†พ ๐ท) โ†พ (๐ท โˆ– {๐‘ž}))))) = 1))
248245, 247mpd 15 . . . . . . . . . 10 ((๐œ‘ โˆง ๐‘ž โˆˆ ๐ด) โ†’ ((๐‘žโ†‘(๐‘ž pCnt (โ™ฏโ€˜๐ต))) gcd (โ™ฏโ€˜(๐บ DProd ((๐‘‡ โ†พ ๐ท) โ†พ (๐ท โˆ– {๐‘ž}))))) = 1)
249 coprmdvds2 16616 . . . . . . . . . 10 ((((๐‘žโ†‘(๐‘ž pCnt (โ™ฏโ€˜๐ต))) โˆˆ โ„ค โˆง (โ™ฏโ€˜(๐บ DProd ((๐‘‡ โ†พ ๐ท) โ†พ (๐ท โˆ– {๐‘ž})))) โˆˆ โ„ค โˆง (โ™ฏโ€˜๐ต) โˆˆ โ„ค) โˆง ((๐‘žโ†‘(๐‘ž pCnt (โ™ฏโ€˜๐ต))) gcd (โ™ฏโ€˜(๐บ DProd ((๐‘‡ โ†พ ๐ท) โ†พ (๐ท โˆ– {๐‘ž}))))) = 1) โ†’ (((๐‘žโ†‘(๐‘ž pCnt (โ™ฏโ€˜๐ต))) โˆฅ (โ™ฏโ€˜๐ต) โˆง (โ™ฏโ€˜(๐บ DProd ((๐‘‡ โ†พ ๐ท) โ†พ (๐ท โˆ– {๐‘ž})))) โˆฅ (โ™ฏโ€˜๐ต)) โ†’ ((๐‘žโ†‘(๐‘ž pCnt (โ™ฏโ€˜๐ต))) ยท (โ™ฏโ€˜(๐บ DProd ((๐‘‡ โ†พ ๐ท) โ†พ (๐ท โˆ– {๐‘ž}))))) โˆฅ (โ™ฏโ€˜๐ต)))
25049, 114, 65, 248, 249syl31anc 1371 . . . . . . . . 9 ((๐œ‘ โˆง ๐‘ž โˆˆ ๐ด) โ†’ (((๐‘žโ†‘(๐‘ž pCnt (โ™ฏโ€˜๐ต))) โˆฅ (โ™ฏโ€˜๐ต) โˆง (โ™ฏโ€˜(๐บ DProd ((๐‘‡ โ†พ ๐ท) โ†พ (๐ท โˆ– {๐‘ž})))) โˆฅ (โ™ฏโ€˜๐ต)) โ†’ ((๐‘žโ†‘(๐‘ž pCnt (โ™ฏโ€˜๐ต))) ยท (โ™ฏโ€˜(๐บ DProd ((๐‘‡ โ†พ ๐ท) โ†พ (๐ท โˆ– {๐‘ž}))))) โˆฅ (โ™ฏโ€˜๐ต)))
25187, 103, 250mp2and 698 . . . . . . . 8 ((๐œ‘ โˆง ๐‘ž โˆˆ ๐ด) โ†’ ((๐‘žโ†‘(๐‘ž pCnt (โ™ฏโ€˜๐ต))) ยท (โ™ฏโ€˜(๐บ DProd ((๐‘‡ โ†พ ๐ท) โ†พ (๐ท โˆ– {๐‘ž}))))) โˆฅ (โ™ฏโ€˜๐ต))
252 eqid 2727 . . . . . . . . . 10 (Cntzโ€˜๐บ) = (Cntzโ€˜๐บ)
253 inss1 4224 . . . . . . . . . . . . . 14 (๐ท โˆฉ {๐‘ž}) โІ ๐ท
254253a1i 11 . . . . . . . . . . . . 13 ((๐œ‘ โˆง ๐‘ž โˆˆ ๐ด) โ†’ (๐ท โˆฉ {๐‘ž}) โІ ๐ท)
25593, 96, 254dprdres 19976 . . . . . . . . . . . 12 ((๐œ‘ โˆง ๐‘ž โˆˆ ๐ด) โ†’ (๐บdom DProd ((๐‘‡ โ†พ ๐ท) โ†พ (๐ท โˆฉ {๐‘ž})) โˆง (๐บ DProd ((๐‘‡ โ†พ ๐ท) โ†พ (๐ท โˆฉ {๐‘ž}))) โІ (๐บ DProd (๐‘‡ โ†พ ๐ท))))
256255simpld 494 . . . . . . . . . . 11 ((๐œ‘ โˆง ๐‘ž โˆˆ ๐ด) โ†’ ๐บdom DProd ((๐‘‡ โ†พ ๐ท) โ†พ (๐ท โˆฉ {๐‘ž})))
257 dprdsubg 19972 . . . . . . . . . . 11 (๐บdom DProd ((๐‘‡ โ†พ ๐ท) โ†พ (๐ท โˆฉ {๐‘ž})) โ†’ (๐บ DProd ((๐‘‡ โ†พ ๐ท) โ†พ (๐ท โˆฉ {๐‘ž}))) โˆˆ (SubGrpโ€˜๐บ))
258256, 257syl 17 . . . . . . . . . 10 ((๐œ‘ โˆง ๐‘ž โˆˆ ๐ด) โ†’ (๐บ DProd ((๐‘‡ โ†พ ๐ท) โ†พ (๐ท โˆฉ {๐‘ž}))) โˆˆ (SubGrpโ€˜๐บ))
259 inass 4215 . . . . . . . . . . . . 13 ((๐ท โˆฉ {๐‘ž}) โˆฉ (๐ท โˆ– {๐‘ž})) = (๐ท โˆฉ ({๐‘ž} โˆฉ (๐ท โˆ– {๐‘ž})))
260 disjdif 4467 . . . . . . . . . . . . . 14 ({๐‘ž} โˆฉ (๐ท โˆ– {๐‘ž})) = โˆ…
261260ineq2i 4205 . . . . . . . . . . . . 13 (๐ท โˆฉ ({๐‘ž} โˆฉ (๐ท โˆ– {๐‘ž}))) = (๐ท โˆฉ โˆ…)
262 in0 4387 . . . . . . . . . . . . 13 (๐ท โˆฉ โˆ…) = โˆ…
263259, 261, 2623eqtri 2759 . . . . . . . . . . . 12 ((๐ท โˆฉ {๐‘ž}) โˆฉ (๐ท โˆ– {๐‘ž})) = โˆ…
264263a1i 11 . . . . . . . . . . 11 ((๐œ‘ โˆง ๐‘ž โˆˆ ๐ด) โ†’ ((๐ท โˆฉ {๐‘ž}) โˆฉ (๐ท โˆ– {๐‘ž})) = โˆ…)
26593, 96, 254, 97, 264, 104dprddisj2 19987 . . . . . . . . . 10 ((๐œ‘ โˆง ๐‘ž โˆˆ ๐ด) โ†’ ((๐บ DProd ((๐‘‡ โ†พ ๐ท) โ†พ (๐ท โˆฉ {๐‘ž}))) โˆฉ (๐บ DProd ((๐‘‡ โ†พ ๐ท) โ†พ (๐ท โˆ– {๐‘ž})))) = {(0gโ€˜๐บ)})
26693, 96, 254, 97, 264, 252dprdcntz2 19986 . . . . . . . . . 10 ((๐œ‘ โˆง ๐‘ž โˆˆ ๐ด) โ†’ (๐บ DProd ((๐‘‡ โ†พ ๐ท) โ†พ (๐ท โˆฉ {๐‘ž}))) โІ ((Cntzโ€˜๐บ)โ€˜(๐บ DProd ((๐‘‡ โ†พ ๐ท) โ†พ (๐ท โˆ– {๐‘ž})))))
2676dprdssv 19964 . . . . . . . . . . 11 (๐บ DProd ((๐‘‡ โ†พ ๐ท) โ†พ (๐ท โˆฉ {๐‘ž}))) โІ ๐ต
268 ssfi 9189 . . . . . . . . . . 11 ((๐ต โˆˆ Fin โˆง (๐บ DProd ((๐‘‡ โ†พ ๐ท) โ†พ (๐ท โˆฉ {๐‘ž}))) โІ ๐ต) โ†’ (๐บ DProd ((๐‘‡ โ†พ ๐ท) โ†พ (๐ท โˆฉ {๐‘ž}))) โˆˆ Fin)
26919, 267, 268sylancl 585 . . . . . . . . . 10 ((๐œ‘ โˆง ๐‘ž โˆˆ ๐ด) โ†’ (๐บ DProd ((๐‘‡ โ†พ ๐ท) โ†พ (๐ท โˆฉ {๐‘ž}))) โˆˆ Fin)
270195, 104, 252, 258, 101, 265, 266, 269, 110lsmhash 19651 . . . . . . . . 9 ((๐œ‘ โˆง ๐‘ž โˆˆ ๐ด) โ†’ (โ™ฏโ€˜((๐บ DProd ((๐‘‡ โ†พ ๐ท) โ†พ (๐ท โˆฉ {๐‘ž})))(LSSumโ€˜๐บ)(๐บ DProd ((๐‘‡ โ†พ ๐ท) โ†พ (๐ท โˆ– {๐‘ž}))))) = ((โ™ฏโ€˜(๐บ DProd ((๐‘‡ โ†พ ๐ท) โ†พ (๐ท โˆฉ {๐‘ž})))) ยท (โ™ฏโ€˜(๐บ DProd ((๐‘‡ โ†พ ๐ท) โ†พ (๐ท โˆ– {๐‘ž}))))))
271 inundif 4474 . . . . . . . . . . . . . 14 ((๐ท โˆฉ {๐‘ž}) โˆช (๐ท โˆ– {๐‘ž})) = ๐ท
272271eqcomi 2736 . . . . . . . . . . . . 13 ๐ท = ((๐ท โˆฉ {๐‘ž}) โˆช (๐ท โˆ– {๐‘ž}))
273272a1i 11 . . . . . . . . . . . 12 ((๐œ‘ โˆง ๐‘ž โˆˆ ๐ด) โ†’ ๐ท = ((๐ท โˆฉ {๐‘ž}) โˆช (๐ท โˆ– {๐‘ž})))
27495, 264, 273, 195, 93dprdsplit 19996 . . . . . . . . . . 11 ((๐œ‘ โˆง ๐‘ž โˆˆ ๐ด) โ†’ (๐บ DProd (๐‘‡ โ†พ ๐ท)) = ((๐บ DProd ((๐‘‡ โ†พ ๐ท) โ†พ (๐ท โˆฉ {๐‘ž})))(LSSumโ€˜๐บ)(๐บ DProd ((๐‘‡ โ†พ ๐ท) โ†พ (๐ท โˆ– {๐‘ž})))))
275207adantr 480 . . . . . . . . . . 11 ((๐œ‘ โˆง ๐‘ž โˆˆ ๐ด) โ†’ (๐บ DProd (๐‘‡ โ†พ ๐ท)) = ๐ต)
276274, 275eqtr3d 2769 . . . . . . . . . 10 ((๐œ‘ โˆง ๐‘ž โˆˆ ๐ด) โ†’ ((๐บ DProd ((๐‘‡ โ†พ ๐ท) โ†พ (๐ท โˆฉ {๐‘ž})))(LSSumโ€˜๐บ)(๐บ DProd ((๐‘‡ โ†พ ๐ท) โ†พ (๐ท โˆ– {๐‘ž})))) = ๐ต)
277276fveq2d 6895 . . . . . . . . 9 ((๐œ‘ โˆง ๐‘ž โˆˆ ๐ด) โ†’ (โ™ฏโ€˜((๐บ DProd ((๐‘‡ โ†พ ๐ท) โ†พ (๐ท โˆฉ {๐‘ž})))(LSSumโ€˜๐บ)(๐บ DProd ((๐‘‡ โ†พ ๐ท) โ†พ (๐ท โˆ– {๐‘ž}))))) = (โ™ฏโ€˜๐ต))
278 snssi 4807 . . . . . . . . . . . . . . . . 17 (๐‘ž โˆˆ ๐ท โ†’ {๐‘ž} โІ ๐ท)
279278adantl 481 . . . . . . . . . . . . . . . 16 (((๐œ‘ โˆง ๐‘ž โˆˆ ๐ด) โˆง ๐‘ž โˆˆ ๐ท) โ†’ {๐‘ž} โІ ๐ท)
280 sseqin2 4211 . . . . . . . . . . . . . . . 16 ({๐‘ž} โІ ๐ท โ†” (๐ท โˆฉ {๐‘ž}) = {๐‘ž})
281279, 280sylib 217 . . . . . . . . . . . . . . 15 (((๐œ‘ โˆง ๐‘ž โˆˆ ๐ด) โˆง ๐‘ž โˆˆ ๐ท) โ†’ (๐ท โˆฉ {๐‘ž}) = {๐‘ž})
282281reseq2d 5979 . . . . . . . . . . . . . 14 (((๐œ‘ โˆง ๐‘ž โˆˆ ๐ด) โˆง ๐‘ž โˆˆ ๐ท) โ†’ ((๐‘‡ โ†พ ๐ท) โ†พ (๐ท โˆฉ {๐‘ž})) = ((๐‘‡ โ†พ ๐ท) โ†พ {๐‘ž}))
283282oveq2d 7430 . . . . . . . . . . . . 13 (((๐œ‘ โˆง ๐‘ž โˆˆ ๐ด) โˆง ๐‘ž โˆˆ ๐ท) โ†’ (๐บ DProd ((๐‘‡ โ†พ ๐ท) โ†พ (๐ท โˆฉ {๐‘ž}))) = (๐บ DProd ((๐‘‡ โ†พ ๐ท) โ†พ {๐‘ž})))
28493adantr 480 . . . . . . . . . . . . . 14 (((๐œ‘ โˆง ๐‘ž โˆˆ ๐ด) โˆง ๐‘ž โˆˆ ๐ท) โ†’ ๐บdom DProd (๐‘‡ โ†พ ๐ท))
285211ad2antrr 725 . . . . . . . . . . . . . 14 (((๐œ‘ โˆง ๐‘ž โˆˆ ๐ด) โˆง ๐‘ž โˆˆ ๐ท) โ†’ dom (๐‘‡ โ†พ ๐ท) = ๐ท)
286 simpr 484 . . . . . . . . . . . . . 14 (((๐œ‘ โˆง ๐‘ž โˆˆ ๐ด) โˆง ๐‘ž โˆˆ ๐ท) โ†’ ๐‘ž โˆˆ ๐ท)
287284, 285, 286dpjlem 19999 . . . . . . . . . . . . 13 (((๐œ‘ โˆง ๐‘ž โˆˆ ๐ด) โˆง ๐‘ž โˆˆ ๐ท) โ†’ (๐บ DProd ((๐‘‡ โ†พ ๐ท) โ†พ {๐‘ž})) = ((๐‘‡ โ†พ ๐ท)โ€˜๐‘ž))
288216adantl 481 . . . . . . . . . . . . 13 (((๐œ‘ โˆง ๐‘ž โˆˆ ๐ด) โˆง ๐‘ž โˆˆ ๐ท) โ†’ ((๐‘‡ โ†พ ๐ท)โ€˜๐‘ž) = (๐‘‡โ€˜๐‘ž))
289283, 287, 2883eqtrd 2771 . . . . . . . . . . . 12 (((๐œ‘ โˆง ๐‘ž โˆˆ ๐ด) โˆง ๐‘ž โˆˆ ๐ท) โ†’ (๐บ DProd ((๐‘‡ โ†พ ๐ท) โ†พ (๐ท โˆฉ {๐‘ž}))) = (๐‘‡โ€˜๐‘ž))
290 simprr 772 . . . . . . . . . . . . . . . . . 18 ((๐œ‘ โˆง (๐‘ž โˆˆ ๐ด โˆง ยฌ ๐‘ž โˆˆ ๐ท)) โ†’ ยฌ ๐‘ž โˆˆ ๐ท)
291 disjsn 4711 . . . . . . . . . . . . . . . . . 18 ((๐ท โˆฉ {๐‘ž}) = โˆ… โ†” ยฌ ๐‘ž โˆˆ ๐ท)
292290, 291sylibr 233 . . . . . . . . . . . . . . . . 17 ((๐œ‘ โˆง (๐‘ž โˆˆ ๐ด โˆง ยฌ ๐‘ž โˆˆ ๐ท)) โ†’ (๐ท โˆฉ {๐‘ž}) = โˆ…)
293292reseq2d 5979 . . . . . . . . . . . . . . . 16 ((๐œ‘ โˆง (๐‘ž โˆˆ ๐ด โˆง ยฌ ๐‘ž โˆˆ ๐ท)) โ†’ ((๐‘‡ โ†พ ๐ท) โ†พ (๐ท โˆฉ {๐‘ž})) = ((๐‘‡ โ†พ ๐ท) โ†พ โˆ…))
294 res0 5983 . . . . . . . . . . . . . . . 16 ((๐‘‡ โ†พ ๐ท) โ†พ โˆ…) = โˆ…
295293, 294eqtrdi 2783 . . . . . . . . . . . . . . 15 ((๐œ‘ โˆง (๐‘ž โˆˆ ๐ด โˆง ยฌ ๐‘ž โˆˆ ๐ท)) โ†’ ((๐‘‡ โ†พ ๐ท) โ†พ (๐ท โˆฉ {๐‘ž})) = โˆ…)
296295oveq2d 7430 . . . . . . . . . . . . . 14 ((๐œ‘ โˆง (๐‘ž โˆˆ ๐ด โˆง ยฌ ๐‘ž โˆˆ ๐ท)) โ†’ (๐บ DProd ((๐‘‡ โ†พ ๐ท) โ†พ (๐ท โˆฉ {๐‘ž}))) = (๐บ DProd โˆ…))
297104dprd0 19979 . . . . . . . . . . . . . . . . 17 (๐บ โˆˆ Grp โ†’ (๐บdom DProd โˆ… โˆง (๐บ DProd โˆ…) = {(0gโ€˜๐บ)}))
29840, 297syl 17 . . . . . . . . . . . . . . . 16 (๐œ‘ โ†’ (๐บdom DProd โˆ… โˆง (๐บ DProd โˆ…) = {(0gโ€˜๐บ)}))
299298simprd 495 . . . . . . . . . . . . . . 15 (๐œ‘ โ†’ (๐บ DProd โˆ…) = {(0gโ€˜๐บ)})
300299adantr 480 . . . . . . . . . . . . . 14 ((๐œ‘ โˆง (๐‘ž โˆˆ ๐ด โˆง ยฌ ๐‘ž โˆˆ ๐ท)) โ†’ (๐บ DProd โˆ…) = {(0gโ€˜๐บ)})
301296, 300, 1863eqtrd 2771 . . . . . . . . . . . . 13 ((๐œ‘ โˆง (๐‘ž โˆˆ ๐ด โˆง ยฌ ๐‘ž โˆˆ ๐ท)) โ†’ (๐บ DProd ((๐‘‡ โ†พ ๐ท) โ†พ (๐ท โˆฉ {๐‘ž}))) = (๐‘‡โ€˜๐‘ž))
302301anassrs 467 . . . . . . . . . . . 12 (((๐œ‘ โˆง ๐‘ž โˆˆ ๐ด) โˆง ยฌ ๐‘ž โˆˆ ๐ท) โ†’ (๐บ DProd ((๐‘‡ โ†พ ๐ท) โ†พ (๐ท โˆฉ {๐‘ž}))) = (๐‘‡โ€˜๐‘ž))
303289, 302pm2.61dan 812 . . . . . . . . . . 11 ((๐œ‘ โˆง ๐‘ž โˆˆ ๐ด) โ†’ (๐บ DProd ((๐‘‡ โ†พ ๐ท) โ†พ (๐ท โˆฉ {๐‘ž}))) = (๐‘‡โ€˜๐‘ž))
304303fveq2d 6895 . . . . . . . . . 10 ((๐œ‘ โˆง ๐‘ž โˆˆ ๐ด) โ†’ (โ™ฏโ€˜(๐บ DProd ((๐‘‡ โ†พ ๐ท) โ†พ (๐ท โˆฉ {๐‘ž})))) = (โ™ฏโ€˜(๐‘‡โ€˜๐‘ž)))
305304oveq1d 7429 . . . . . . . . 9 ((๐œ‘ โˆง ๐‘ž โˆˆ ๐ด) โ†’ ((โ™ฏโ€˜(๐บ DProd ((๐‘‡ โ†พ ๐ท) โ†พ (๐ท โˆฉ {๐‘ž})))) ยท (โ™ฏโ€˜(๐บ DProd ((๐‘‡ โ†พ ๐ท) โ†พ (๐ท โˆ– {๐‘ž}))))) = ((โ™ฏโ€˜(๐‘‡โ€˜๐‘ž)) ยท (โ™ฏโ€˜(๐บ DProd ((๐‘‡ โ†พ ๐ท) โ†พ (๐ท โˆ– {๐‘ž}))))))
306270, 277, 3053eqtr3d 2775 . . . . . . . 8 ((๐œ‘ โˆง ๐‘ž โˆˆ ๐ด) โ†’ (โ™ฏโ€˜๐ต) = ((โ™ฏโ€˜(๐‘‡โ€˜๐‘ž)) ยท (โ™ฏโ€˜(๐บ DProd ((๐‘‡ โ†พ ๐ท) โ†พ (๐ท โˆ– {๐‘ž}))))))
307251, 306breqtrd 5168 . . . . . . 7 ((๐œ‘ โˆง ๐‘ž โˆˆ ๐ด) โ†’ ((๐‘žโ†‘(๐‘ž pCnt (โ™ฏโ€˜๐ต))) ยท (โ™ฏโ€˜(๐บ DProd ((๐‘‡ โ†พ ๐ท) โ†พ (๐ท โˆ– {๐‘ž}))))) โˆฅ ((โ™ฏโ€˜(๐‘‡โ€˜๐‘ž)) ยท (โ™ฏโ€˜(๐บ DProd ((๐‘‡ โ†พ ๐ท) โ†พ (๐ท โˆ– {๐‘ž}))))))
308113nnne0d 12284 . . . . . . . 8 ((๐œ‘ โˆง ๐‘ž โˆˆ ๐ด) โ†’ (โ™ฏโ€˜(๐บ DProd ((๐‘‡ โ†พ ๐ท) โ†พ (๐ท โˆ– {๐‘ž})))) โ‰  0)
309 dvdsmulcr 16254 . . . . . . . 8 (((๐‘žโ†‘(๐‘ž pCnt (โ™ฏโ€˜๐ต))) โˆˆ โ„ค โˆง (โ™ฏโ€˜(๐‘‡โ€˜๐‘ž)) โˆˆ โ„ค โˆง ((โ™ฏโ€˜(๐บ DProd ((๐‘‡ โ†พ ๐ท) โ†พ (๐ท โˆ– {๐‘ž})))) โˆˆ โ„ค โˆง (โ™ฏโ€˜(๐บ DProd ((๐‘‡ โ†พ ๐ท) โ†พ (๐ท โˆ– {๐‘ž})))) โ‰  0)) โ†’ (((๐‘žโ†‘(๐‘ž pCnt (โ™ฏโ€˜๐ต))) ยท (โ™ฏโ€˜(๐บ DProd ((๐‘‡ โ†พ ๐ท) โ†พ (๐ท โˆ– {๐‘ž}))))) โˆฅ ((โ™ฏโ€˜(๐‘‡โ€˜๐‘ž)) ยท (โ™ฏโ€˜(๐บ DProd ((๐‘‡ โ†พ ๐ท) โ†พ (๐ท โˆ– {๐‘ž}))))) โ†” (๐‘žโ†‘(๐‘ž pCnt (โ™ฏโ€˜๐ต))) โˆฅ (โ™ฏโ€˜(๐‘‡โ€˜๐‘ž))))
31049, 34, 114, 308, 309syl112anc 1372 . . . . . . 7 ((๐œ‘ โˆง ๐‘ž โˆˆ ๐ด) โ†’ (((๐‘žโ†‘(๐‘ž pCnt (โ™ฏโ€˜๐ต))) ยท (โ™ฏโ€˜(๐บ DProd ((๐‘‡ โ†พ ๐ท) โ†พ (๐ท โˆ– {๐‘ž}))))) โˆฅ ((โ™ฏโ€˜(๐‘‡โ€˜๐‘ž)) ยท (โ™ฏโ€˜(๐บ DProd ((๐‘‡ โ†พ ๐ท) โ†พ (๐ท โˆ– {๐‘ž}))))) โ†” (๐‘žโ†‘(๐‘ž pCnt (โ™ฏโ€˜๐ต))) โˆฅ (โ™ฏโ€˜(๐‘‡โ€˜๐‘ž))))
311307, 310mpbid 231 . . . . . 6 ((๐œ‘ โˆง ๐‘ž โˆˆ ๐ด) โ†’ (๐‘žโ†‘(๐‘ž pCnt (โ™ฏโ€˜๐ต))) โˆฅ (โ™ฏโ€˜(๐‘‡โ€˜๐‘ž)))
312 dvdseq 16282 . . . . . 6 ((((โ™ฏโ€˜(๐‘‡โ€˜๐‘ž)) โˆˆ โ„•0 โˆง (๐‘žโ†‘(๐‘ž pCnt (โ™ฏโ€˜๐ต))) โˆˆ โ„•0) โˆง ((โ™ฏโ€˜(๐‘‡โ€˜๐‘ž)) โˆฅ (๐‘žโ†‘(๐‘ž pCnt (โ™ฏโ€˜๐ต))) โˆง (๐‘žโ†‘(๐‘ž pCnt (โ™ฏโ€˜๐ต))) โˆฅ (โ™ฏโ€˜(๐‘‡โ€˜๐‘ž)))) โ†’ (โ™ฏโ€˜(๐‘‡โ€˜๐‘ž)) = (๐‘žโ†‘(๐‘ž pCnt (โ™ฏโ€˜๐ต))))
31333, 85, 73, 311, 312syl22anc 838 . . . . 5 ((๐œ‘ โˆง ๐‘ž โˆˆ ๐ด) โ†’ (โ™ฏโ€˜(๐‘‡โ€˜๐‘ž)) = (๐‘žโ†‘(๐‘ž pCnt (โ™ฏโ€˜๐ต))))
3146, 7, 8, 9, 10, 11ablfac1a 20017 . . . . 5 ((๐œ‘ โˆง ๐‘ž โˆˆ ๐ด) โ†’ (โ™ฏโ€˜(๐‘†โ€˜๐‘ž)) = (๐‘žโ†‘(๐‘ž pCnt (โ™ฏโ€˜๐ต))))
315313, 314eqtr4d 2770 . . . 4 ((๐œ‘ โˆง ๐‘ž โˆˆ ๐ด) โ†’ (โ™ฏโ€˜(๐‘‡โ€˜๐‘ž)) = (โ™ฏโ€˜(๐‘†โ€˜๐‘ž)))
316 hashen 14330 . . . . 5 (((๐‘‡โ€˜๐‘ž) โˆˆ Fin โˆง (๐‘†โ€˜๐‘ž) โˆˆ Fin) โ†’ ((โ™ฏโ€˜(๐‘‡โ€˜๐‘ž)) = (โ™ฏโ€˜(๐‘†โ€˜๐‘ž)) โ†” (๐‘‡โ€˜๐‘ž) โ‰ˆ (๐‘†โ€˜๐‘ž)))
31731, 23, 316syl2anc 583 . . . 4 ((๐œ‘ โˆง ๐‘ž โˆˆ ๐ด) โ†’ ((โ™ฏโ€˜(๐‘‡โ€˜๐‘ž)) = (โ™ฏโ€˜(๐‘†โ€˜๐‘ž)) โ†” (๐‘‡โ€˜๐‘ž) โ‰ˆ (๐‘†โ€˜๐‘ž)))
318315, 317mpbid 231 . . 3 ((๐œ‘ โˆง ๐‘ž โˆˆ ๐ด) โ†’ (๐‘‡โ€˜๐‘ž) โ‰ˆ (๐‘†โ€˜๐‘ž))
319 fisseneq 9273 . . 3 (((๐‘†โ€˜๐‘ž) โˆˆ Fin โˆง (๐‘‡โ€˜๐‘ž) โІ (๐‘†โ€˜๐‘ž) โˆง (๐‘‡โ€˜๐‘ž) โ‰ˆ (๐‘†โ€˜๐‘ž)) โ†’ (๐‘‡โ€˜๐‘ž) = (๐‘†โ€˜๐‘ž))
32023, 84, 318, 319syl3anc 1369 . 2 ((๐œ‘ โˆง ๐‘ž โˆˆ ๐ด) โ†’ (๐‘‡โ€˜๐‘ž) = (๐‘†โ€˜๐‘ž))
3215, 18, 320eqfnfvd 7037 1 (๐œ‘ โ†’ ๐‘‡ = ๐‘†)
Colors of variables: wff setvar class
Syntax hints:  ยฌ wn 3   โ†’ wi 4   โ†” wb 205   โˆง wa 395   โˆจ wo 846   โˆง w3a 1085   = wceq 1534   โˆˆ wcel 2099   โ‰  wne 2935  โˆ€wral 3056  {crab 3427  Vcvv 3469   โˆ– cdif 3941   โˆช cun 3942   โˆฉ cin 3943   โІ wss 3944  โˆ…c0 4318  {csn 4624   class class class wbr 5142   โ†ฆ cmpt 5225  dom cdm 5672   โ†พ cres 5674  โŸถwf 6538  โ€˜cfv 6542  (class class class)co 7414   โ‰ˆ cen 8952  Fincfn 8955  0cc0 11130  1c1 11131   ยท cmul 11135   โ‰ค cle 11271  โ„•cn 12234  โ„•0cn0 12494  โ„คcz 12580  โ„คโ‰ฅcuz 12844  ...cfz 13508  โ†‘cexp 14050  โ™ฏchash 14313   โˆฅ cdvds 16222   gcd cgcd 16460  โ„™cprime 16633   pCnt cpc 16796  Basecbs 17171  0gc0g 17412  Grpcgrp 18881  SubGrpcsubg 19066  Cntzccntz 19257  odcod 19470  LSSumclsm 19580  Abelcabl 19727   DProd cdprd 19941
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1790  ax-4 1804  ax-5 1906  ax-6 1964  ax-7 2004  ax-8 2101  ax-9 2109  ax-10 2130  ax-11 2147  ax-12 2164  ax-ext 2698  ax-rep 5279  ax-sep 5293  ax-nul 5300  ax-pow 5359  ax-pr 5423  ax-un 7734  ax-inf2 9656  ax-cnex 11186  ax-resscn 11187  ax-1cn 11188  ax-icn 11189  ax-addcl 11190  ax-addrcl 11191  ax-mulcl 11192  ax-mulrcl 11193  ax-mulcom 11194  ax-addass 11195  ax-mulass 11196  ax-distr 11197  ax-i2m1 11198  ax-1ne0 11199  ax-1rid 11200  ax-rnegex 11201  ax-rrecex 11202  ax-cnre 11203  ax-pre-lttri 11204  ax-pre-lttrn 11205  ax-pre-ltadd 11206  ax-pre-mulgt0 11207  ax-pre-sup 11208
This theorem depends on definitions:  df-bi 206  df-an 396  df-or 847  df-3or 1086  df-3an 1087  df-tru 1537  df-fal 1547  df-ex 1775  df-nf 1779  df-sb 2061  df-mo 2529  df-eu 2558  df-clab 2705  df-cleq 2719  df-clel 2805  df-nfc 2880  df-ne 2936  df-nel 3042  df-ral 3057  df-rex 3066  df-rmo 3371  df-reu 3372  df-rab 3428  df-v 3471  df-sbc 3775  df-csb 3890  df-dif 3947  df-un 3949  df-in 3951  df-ss 3961  df-pss 3963  df-nul 4319  df-if 4525  df-pw 4600  df-sn 4625  df-pr 4627  df-op 4631  df-uni 4904  df-int 4945  df-iun 4993  df-iin 4994  df-disj 5108  df-br 5143  df-opab 5205  df-mpt 5226  df-tr 5260  df-id 5570  df-eprel 5576  df-po 5584  df-so 5585  df-fr 5627  df-se 5628  df-we 5629  df-xp 5678  df-rel 5679  df-cnv 5680  df-co 5681  df-dm 5682  df-rn 5683  df-res 5684  df-ima 5685  df-pred 6299  df-ord 6366  df-on 6367  df-lim 6368  df-suc 6369  df-iota 6494  df-fun 6544  df-fn 6545  df-f 6546  df-f1 6547  df-fo 6548  df-f1o 6549  df-fv 6550  df-isom 6551  df-riota 7370  df-ov 7417  df-oprab 7418  df-mpo 7419  df-of 7679  df-om 7865  df-1st 7987  df-2nd 7988  df-supp 8160  df-tpos 8225  df-frecs 8280  df-wrecs 8311  df-recs 8385  df-rdg 8424  df-1o 8480  df-2o 8481  df-oadd 8484  df-omul 8485  df-er 8718  df-ec 8720  df-qs 8724  df-map 8838  df-ixp 8908  df-en 8956  df-dom 8957  df-sdom 8958  df-fin 8959  df-fsupp 9378  df-sup 9457  df-inf 9458  df-oi 9525  df-dju 9916  df-card 9954  df-acn 9957  df-pnf 11272  df-mnf 11273  df-xr 11274  df-ltxr 11275  df-le 11276  df-sub 11468  df-neg 11469  df-div 11894  df-nn 12235  df-2 12297  df-3 12298  df-n0 12495  df-xnn0 12567  df-z 12581  df-uz 12845  df-q 12955  df-rp 12999  df-fz 13509  df-fzo 13652  df-fl 13781  df-mod 13859  df-seq 13991  df-exp 14051  df-fac 14257  df-bc 14286  df-hash 14314  df-cj 15070  df-re 15071  df-im 15072  df-sqrt 15206  df-abs 15207  df-clim 15456  df-sum 15657  df-dvds 16223  df-gcd 16461  df-prm 16634  df-pc 16797  df-sets 17124  df-slot 17142  df-ndx 17154  df-base 17172  df-ress 17201  df-plusg 17237  df-0g 17414  df-gsum 17415  df-mre 17557  df-mrc 17558  df-acs 17560  df-mgm 18591  df-sgrp 18670  df-mnd 18686  df-mhm 18731  df-submnd 18732  df-grp 18884  df-minusg 18885  df-sbg 18886  df-mulg 19015  df-subg 19069  df-eqg 19071  df-ghm 19159  df-gim 19204  df-ga 19232  df-cntz 19259  df-oppg 19288  df-od 19474  df-lsm 19582  df-pj1 19583  df-cmn 19728  df-abl 19729  df-dprd 19943
This theorem is referenced by: (None)
  Copyright terms: Public domain W3C validator