Users' Mathboxes Mathbox for Thierry Arnoux < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  gsumhashmul Structured version   Visualization version   GIF version

Theorem gsumhashmul 32208
Description: Express a group sum by grouping by nonzero values. (Contributed by Thierry Arnoux, 22-Jun-2024.)
Hypotheses
Ref Expression
gsumhashmul.b ๐ต = (Baseโ€˜๐บ)
gsumhashmul.z 0 = (0gโ€˜๐บ)
gsumhashmul.x ยท = (.gโ€˜๐บ)
gsumhashmul.g (๐œ‘ โ†’ ๐บ โˆˆ CMnd)
gsumhashmul.f (๐œ‘ โ†’ ๐น:๐ดโŸถ๐ต)
gsumhashmul.1 (๐œ‘ โ†’ ๐น finSupp 0 )
Assertion
Ref Expression
gsumhashmul (๐œ‘ โ†’ (๐บ ฮฃg ๐น) = (๐บ ฮฃg (๐‘ฅ โˆˆ (ran ๐น โˆ– { 0 }) โ†ฆ ((โ™ฏโ€˜(โ—ก๐น โ€œ {๐‘ฅ})) ยท ๐‘ฅ))))
Distinct variable groups:   ๐‘ฅ, 0   ๐‘ฅ,๐ด   ๐‘ฅ,๐ต   ๐‘ฅ,๐น   ๐‘ฅ,๐บ   ๐œ‘,๐‘ฅ
Allowed substitution hint:   ยท (๐‘ฅ)

Proof of Theorem gsumhashmul
Dummy variables ๐‘ก ๐‘ข ๐‘ฃ ๐‘ฆ ๐‘ง are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 gsumhashmul.f . . . . . . 7 (๐œ‘ โ†’ ๐น:๐ดโŸถ๐ต)
2 suppssdm 8162 . . . . . . . 8 (๐น supp 0 ) โŠ† dom ๐น
32, 1fssdm 6738 . . . . . . 7 (๐œ‘ โ†’ (๐น supp 0 ) โŠ† ๐ด)
41, 3feqresmpt 6962 . . . . . 6 (๐œ‘ โ†’ (๐น โ†พ (๐น supp 0 )) = (๐‘ฅ โˆˆ (๐น supp 0 ) โ†ฆ (๐นโ€˜๐‘ฅ)))
54oveq2d 7425 . . . . 5 (๐œ‘ โ†’ (๐บ ฮฃg (๐น โ†พ (๐น supp 0 ))) = (๐บ ฮฃg (๐‘ฅ โˆˆ (๐น supp 0 ) โ†ฆ (๐นโ€˜๐‘ฅ))))
6 gsumhashmul.b . . . . . 6 ๐ต = (Baseโ€˜๐บ)
7 gsumhashmul.z . . . . . 6 0 = (0gโ€˜๐บ)
8 gsumhashmul.g . . . . . 6 (๐œ‘ โ†’ ๐บ โˆˆ CMnd)
9 gsumhashmul.1 . . . . . . . 8 (๐œ‘ โ†’ ๐น finSupp 0 )
10 relfsupp 9363 . . . . . . . . 9 Rel finSupp
1110brrelex1i 5733 . . . . . . . 8 (๐น finSupp 0 โ†’ ๐น โˆˆ V)
129, 11syl 17 . . . . . . 7 (๐œ‘ โ†’ ๐น โˆˆ V)
131ffnd 6719 . . . . . . 7 (๐œ‘ โ†’ ๐น Fn ๐ด)
1412, 13fndmexd 7897 . . . . . 6 (๐œ‘ โ†’ ๐ด โˆˆ V)
15 ssidd 4006 . . . . . 6 (๐œ‘ โ†’ (๐น supp 0 ) โŠ† (๐น supp 0 ))
166, 7, 8, 14, 1, 15, 9gsumres 19781 . . . . 5 (๐œ‘ โ†’ (๐บ ฮฃg (๐น โ†พ (๐น supp 0 ))) = (๐บ ฮฃg ๐น))
17 nfcv 2904 . . . . . 6 โ„ฒ๐‘ฅ(๐นโ€˜(1st โ€˜๐‘ง))
18 fveq2 6892 . . . . . 6 (๐‘ฅ = (1st โ€˜๐‘ง) โ†’ (๐นโ€˜๐‘ฅ) = (๐นโ€˜(1st โ€˜๐‘ง)))
199fsuppimpd 9369 . . . . . 6 (๐œ‘ โ†’ (๐น supp 0 ) โˆˆ Fin)
20 ssidd 4006 . . . . . 6 (๐œ‘ โ†’ ๐ต โŠ† ๐ต)
211adantr 482 . . . . . . 7 ((๐œ‘ โˆง ๐‘ฅ โˆˆ (๐น supp 0 )) โ†’ ๐น:๐ดโŸถ๐ต)
223sselda 3983 . . . . . . 7 ((๐œ‘ โˆง ๐‘ฅ โˆˆ (๐น supp 0 )) โ†’ ๐‘ฅ โˆˆ ๐ด)
2321, 22ffvelcdmd 7088 . . . . . 6 ((๐œ‘ โˆง ๐‘ฅ โˆˆ (๐น supp 0 )) โ†’ (๐นโ€˜๐‘ฅ) โˆˆ ๐ต)
241ffund 6722 . . . . . . . . 9 (๐œ‘ โ†’ Fun ๐น)
25 funrel 6566 . . . . . . . . 9 (Fun ๐น โ†’ Rel ๐น)
26 reldif 5816 . . . . . . . . 9 (Rel ๐น โ†’ Rel (๐น โˆ– (V ร— { 0 })))
2724, 25, 263syl 18 . . . . . . . 8 (๐œ‘ โ†’ Rel (๐น โˆ– (V ร— { 0 })))
28 1stdm 8026 . . . . . . . 8 ((Rel (๐น โˆ– (V ร— { 0 })) โˆง ๐‘ง โˆˆ (๐น โˆ– (V ร— { 0 }))) โ†’ (1st โ€˜๐‘ง) โˆˆ dom (๐น โˆ– (V ร— { 0 })))
2927, 28sylan 581 . . . . . . 7 ((๐œ‘ โˆง ๐‘ง โˆˆ (๐น โˆ– (V ร— { 0 }))) โ†’ (1st โ€˜๐‘ง) โˆˆ dom (๐น โˆ– (V ร— { 0 })))
307fvexi 6906 . . . . . . . . . . . 12 0 โˆˆ V
3130a1i 11 . . . . . . . . . . 11 (๐œ‘ โ†’ 0 โˆˆ V)
32 fressupp 31910 . . . . . . . . . . 11 ((Fun ๐น โˆง ๐น โˆˆ V โˆง 0 โˆˆ V) โ†’ (๐น โ†พ (๐น supp 0 )) = (๐น โˆ– (V ร— { 0 })))
3324, 12, 31, 32syl3anc 1372 . . . . . . . . . 10 (๐œ‘ โ†’ (๐น โ†พ (๐น supp 0 )) = (๐น โˆ– (V ร— { 0 })))
3433dmeqd 5906 . . . . . . . . 9 (๐œ‘ โ†’ dom (๐น โ†พ (๐น supp 0 )) = dom (๐น โˆ– (V ร— { 0 })))
352a1i 11 . . . . . . . . . 10 (๐œ‘ โ†’ (๐น supp 0 ) โŠ† dom ๐น)
36 ssdmres 6005 . . . . . . . . . 10 ((๐น supp 0 ) โŠ† dom ๐น โ†” dom (๐น โ†พ (๐น supp 0 )) = (๐น supp 0 ))
3735, 36sylib 217 . . . . . . . . 9 (๐œ‘ โ†’ dom (๐น โ†พ (๐น supp 0 )) = (๐น supp 0 ))
3834, 37eqtr3d 2775 . . . . . . . 8 (๐œ‘ โ†’ dom (๐น โˆ– (V ร— { 0 })) = (๐น supp 0 ))
3938adantr 482 . . . . . . 7 ((๐œ‘ โˆง ๐‘ง โˆˆ (๐น โˆ– (V ร— { 0 }))) โ†’ dom (๐น โˆ– (V ร— { 0 })) = (๐น supp 0 ))
4029, 39eleqtrd 2836 . . . . . 6 ((๐œ‘ โˆง ๐‘ง โˆˆ (๐น โˆ– (V ร— { 0 }))) โ†’ (1st โ€˜๐‘ง) โˆˆ (๐น supp 0 ))
4124funresd 6592 . . . . . . . . . . 11 (๐œ‘ โ†’ Fun (๐น โ†พ (๐น supp 0 )))
4241adantr 482 . . . . . . . . . 10 ((๐œ‘ โˆง ๐‘ฅ โˆˆ (๐น supp 0 )) โ†’ Fun (๐น โ†พ (๐น supp 0 )))
4337eleq2d 2820 . . . . . . . . . . 11 (๐œ‘ โ†’ (๐‘ฅ โˆˆ dom (๐น โ†พ (๐น supp 0 )) โ†” ๐‘ฅ โˆˆ (๐น supp 0 )))
4443biimpar 479 . . . . . . . . . 10 ((๐œ‘ โˆง ๐‘ฅ โˆˆ (๐น supp 0 )) โ†’ ๐‘ฅ โˆˆ dom (๐น โ†พ (๐น supp 0 )))
45 simpr 486 . . . . . . . . . . 11 ((๐œ‘ โˆง ๐‘ฅ โˆˆ (๐น supp 0 )) โ†’ ๐‘ฅ โˆˆ (๐น supp 0 ))
4645fvresd 6912 . . . . . . . . . 10 ((๐œ‘ โˆง ๐‘ฅ โˆˆ (๐น supp 0 )) โ†’ ((๐น โ†พ (๐น supp 0 ))โ€˜๐‘ฅ) = (๐นโ€˜๐‘ฅ))
47 funopfvb 6948 . . . . . . . . . . 11 ((Fun (๐น โ†พ (๐น supp 0 )) โˆง ๐‘ฅ โˆˆ dom (๐น โ†พ (๐น supp 0 ))) โ†’ (((๐น โ†พ (๐น supp 0 ))โ€˜๐‘ฅ) = (๐นโ€˜๐‘ฅ) โ†” โŸจ๐‘ฅ, (๐นโ€˜๐‘ฅ)โŸฉ โˆˆ (๐น โ†พ (๐น supp 0 ))))
4847biimpa 478 . . . . . . . . . 10 (((Fun (๐น โ†พ (๐น supp 0 )) โˆง ๐‘ฅ โˆˆ dom (๐น โ†พ (๐น supp 0 ))) โˆง ((๐น โ†พ (๐น supp 0 ))โ€˜๐‘ฅ) = (๐นโ€˜๐‘ฅ)) โ†’ โŸจ๐‘ฅ, (๐นโ€˜๐‘ฅ)โŸฉ โˆˆ (๐น โ†พ (๐น supp 0 )))
4942, 44, 46, 48syl21anc 837 . . . . . . . . 9 ((๐œ‘ โˆง ๐‘ฅ โˆˆ (๐น supp 0 )) โ†’ โŸจ๐‘ฅ, (๐นโ€˜๐‘ฅ)โŸฉ โˆˆ (๐น โ†พ (๐น supp 0 )))
5033adantr 482 . . . . . . . . 9 ((๐œ‘ โˆง ๐‘ฅ โˆˆ (๐น supp 0 )) โ†’ (๐น โ†พ (๐น supp 0 )) = (๐น โˆ– (V ร— { 0 })))
5149, 50eleqtrd 2836 . . . . . . . 8 ((๐œ‘ โˆง ๐‘ฅ โˆˆ (๐น supp 0 )) โ†’ โŸจ๐‘ฅ, (๐นโ€˜๐‘ฅ)โŸฉ โˆˆ (๐น โˆ– (V ร— { 0 })))
52 eqeq2 2745 . . . . . . . . . . 11 (๐‘ฃ = โŸจ๐‘ฅ, (๐นโ€˜๐‘ฅ)โŸฉ โ†’ (๐‘ง = ๐‘ฃ โ†” ๐‘ง = โŸจ๐‘ฅ, (๐นโ€˜๐‘ฅ)โŸฉ))
5352bibi2d 343 . . . . . . . . . 10 (๐‘ฃ = โŸจ๐‘ฅ, (๐นโ€˜๐‘ฅ)โŸฉ โ†’ ((๐‘ฅ = (1st โ€˜๐‘ง) โ†” ๐‘ง = ๐‘ฃ) โ†” (๐‘ฅ = (1st โ€˜๐‘ง) โ†” ๐‘ง = โŸจ๐‘ฅ, (๐นโ€˜๐‘ฅ)โŸฉ)))
5453ralbidv 3178 . . . . . . . . 9 (๐‘ฃ = โŸจ๐‘ฅ, (๐นโ€˜๐‘ฅ)โŸฉ โ†’ (โˆ€๐‘ง โˆˆ (๐น โˆ– (V ร— { 0 }))(๐‘ฅ = (1st โ€˜๐‘ง) โ†” ๐‘ง = ๐‘ฃ) โ†” โˆ€๐‘ง โˆˆ (๐น โˆ– (V ร— { 0 }))(๐‘ฅ = (1st โ€˜๐‘ง) โ†” ๐‘ง = โŸจ๐‘ฅ, (๐นโ€˜๐‘ฅ)โŸฉ)))
5554adantl 483 . . . . . . . 8 (((๐œ‘ โˆง ๐‘ฅ โˆˆ (๐น supp 0 )) โˆง ๐‘ฃ = โŸจ๐‘ฅ, (๐นโ€˜๐‘ฅ)โŸฉ) โ†’ (โˆ€๐‘ง โˆˆ (๐น โˆ– (V ร— { 0 }))(๐‘ฅ = (1st โ€˜๐‘ง) โ†” ๐‘ง = ๐‘ฃ) โ†” โˆ€๐‘ง โˆˆ (๐น โˆ– (V ร— { 0 }))(๐‘ฅ = (1st โ€˜๐‘ง) โ†” ๐‘ง = โŸจ๐‘ฅ, (๐นโ€˜๐‘ฅ)โŸฉ)))
56 fvexd 6907 . . . . . . . . . . . . . 14 ((((๐œ‘ โˆง ๐‘ฅ โˆˆ (๐น supp 0 )) โˆง ๐‘ง โˆˆ (๐น โˆ– (V ร— { 0 }))) โˆง ๐‘ฅ = (1st โ€˜๐‘ง)) โ†’ (2nd โ€˜๐‘ง) โˆˆ V)
5727ad3antrrr 729 . . . . . . . . . . . . . . . . 17 ((((๐œ‘ โˆง ๐‘ฅ โˆˆ (๐น supp 0 )) โˆง ๐‘ง โˆˆ (๐น โˆ– (V ร— { 0 }))) โˆง ๐‘ฅ = (1st โ€˜๐‘ง)) โ†’ Rel (๐น โˆ– (V ร— { 0 })))
58 simplr 768 . . . . . . . . . . . . . . . . 17 ((((๐œ‘ โˆง ๐‘ฅ โˆˆ (๐น supp 0 )) โˆง ๐‘ง โˆˆ (๐น โˆ– (V ร— { 0 }))) โˆง ๐‘ฅ = (1st โ€˜๐‘ง)) โ†’ ๐‘ง โˆˆ (๐น โˆ– (V ร— { 0 })))
59 1st2nd 8025 . . . . . . . . . . . . . . . . 17 ((Rel (๐น โˆ– (V ร— { 0 })) โˆง ๐‘ง โˆˆ (๐น โˆ– (V ร— { 0 }))) โ†’ ๐‘ง = โŸจ(1st โ€˜๐‘ง), (2nd โ€˜๐‘ง)โŸฉ)
6057, 58, 59syl2anc 585 . . . . . . . . . . . . . . . 16 ((((๐œ‘ โˆง ๐‘ฅ โˆˆ (๐น supp 0 )) โˆง ๐‘ง โˆˆ (๐น โˆ– (V ร— { 0 }))) โˆง ๐‘ฅ = (1st โ€˜๐‘ง)) โ†’ ๐‘ง = โŸจ(1st โ€˜๐‘ง), (2nd โ€˜๐‘ง)โŸฉ)
61 opeq1 4874 . . . . . . . . . . . . . . . . 17 (๐‘ฅ = (1st โ€˜๐‘ง) โ†’ โŸจ๐‘ฅ, (2nd โ€˜๐‘ง)โŸฉ = โŸจ(1st โ€˜๐‘ง), (2nd โ€˜๐‘ง)โŸฉ)
6261adantl 483 . . . . . . . . . . . . . . . 16 ((((๐œ‘ โˆง ๐‘ฅ โˆˆ (๐น supp 0 )) โˆง ๐‘ง โˆˆ (๐น โˆ– (V ร— { 0 }))) โˆง ๐‘ฅ = (1st โ€˜๐‘ง)) โ†’ โŸจ๐‘ฅ, (2nd โ€˜๐‘ง)โŸฉ = โŸจ(1st โ€˜๐‘ง), (2nd โ€˜๐‘ง)โŸฉ)
6360, 62eqtr4d 2776 . . . . . . . . . . . . . . 15 ((((๐œ‘ โˆง ๐‘ฅ โˆˆ (๐น supp 0 )) โˆง ๐‘ง โˆˆ (๐น โˆ– (V ร— { 0 }))) โˆง ๐‘ฅ = (1st โ€˜๐‘ง)) โ†’ ๐‘ง = โŸจ๐‘ฅ, (2nd โ€˜๐‘ง)โŸฉ)
64 difssd 4133 . . . . . . . . . . . . . . . . . 18 ((๐œ‘ โˆง ๐‘ฅ โˆˆ (๐น supp 0 )) โ†’ (๐น โˆ– (V ร— { 0 })) โŠ† ๐น)
6564sselda 3983 . . . . . . . . . . . . . . . . 17 (((๐œ‘ โˆง ๐‘ฅ โˆˆ (๐น supp 0 )) โˆง ๐‘ง โˆˆ (๐น โˆ– (V ร— { 0 }))) โ†’ ๐‘ง โˆˆ ๐น)
6665adantr 482 . . . . . . . . . . . . . . . 16 ((((๐œ‘ โˆง ๐‘ฅ โˆˆ (๐น supp 0 )) โˆง ๐‘ง โˆˆ (๐น โˆ– (V ร— { 0 }))) โˆง ๐‘ฅ = (1st โ€˜๐‘ง)) โ†’ ๐‘ง โˆˆ ๐น)
6763, 66eqeltrrd 2835 . . . . . . . . . . . . . . 15 ((((๐œ‘ โˆง ๐‘ฅ โˆˆ (๐น supp 0 )) โˆง ๐‘ง โˆˆ (๐น โˆ– (V ร— { 0 }))) โˆง ๐‘ฅ = (1st โ€˜๐‘ง)) โ†’ โŸจ๐‘ฅ, (2nd โ€˜๐‘ง)โŸฉ โˆˆ ๐น)
6863, 67jca 513 . . . . . . . . . . . . . 14 ((((๐œ‘ โˆง ๐‘ฅ โˆˆ (๐น supp 0 )) โˆง ๐‘ง โˆˆ (๐น โˆ– (V ร— { 0 }))) โˆง ๐‘ฅ = (1st โ€˜๐‘ง)) โ†’ (๐‘ง = โŸจ๐‘ฅ, (2nd โ€˜๐‘ง)โŸฉ โˆง โŸจ๐‘ฅ, (2nd โ€˜๐‘ง)โŸฉ โˆˆ ๐น))
69 opeq2 4875 . . . . . . . . . . . . . . . 16 (๐‘ฆ = (2nd โ€˜๐‘ง) โ†’ โŸจ๐‘ฅ, ๐‘ฆโŸฉ = โŸจ๐‘ฅ, (2nd โ€˜๐‘ง)โŸฉ)
7069eqeq2d 2744 . . . . . . . . . . . . . . 15 (๐‘ฆ = (2nd โ€˜๐‘ง) โ†’ (๐‘ง = โŸจ๐‘ฅ, ๐‘ฆโŸฉ โ†” ๐‘ง = โŸจ๐‘ฅ, (2nd โ€˜๐‘ง)โŸฉ))
7169eleq1d 2819 . . . . . . . . . . . . . . 15 (๐‘ฆ = (2nd โ€˜๐‘ง) โ†’ (โŸจ๐‘ฅ, ๐‘ฆโŸฉ โˆˆ ๐น โ†” โŸจ๐‘ฅ, (2nd โ€˜๐‘ง)โŸฉ โˆˆ ๐น))
7270, 71anbi12d 632 . . . . . . . . . . . . . 14 (๐‘ฆ = (2nd โ€˜๐‘ง) โ†’ ((๐‘ง = โŸจ๐‘ฅ, ๐‘ฆโŸฉ โˆง โŸจ๐‘ฅ, ๐‘ฆโŸฉ โˆˆ ๐น) โ†” (๐‘ง = โŸจ๐‘ฅ, (2nd โ€˜๐‘ง)โŸฉ โˆง โŸจ๐‘ฅ, (2nd โ€˜๐‘ง)โŸฉ โˆˆ ๐น)))
7356, 68, 72spcedv 3589 . . . . . . . . . . . . 13 ((((๐œ‘ โˆง ๐‘ฅ โˆˆ (๐น supp 0 )) โˆง ๐‘ง โˆˆ (๐น โˆ– (V ร— { 0 }))) โˆง ๐‘ฅ = (1st โ€˜๐‘ง)) โ†’ โˆƒ๐‘ฆ(๐‘ง = โŸจ๐‘ฅ, ๐‘ฆโŸฉ โˆง โŸจ๐‘ฅ, ๐‘ฆโŸฉ โˆˆ ๐น))
74 vex 3479 . . . . . . . . . . . . . 14 ๐‘ฅ โˆˆ V
7574elsnres 6022 . . . . . . . . . . . . 13 (๐‘ง โˆˆ (๐น โ†พ {๐‘ฅ}) โ†” โˆƒ๐‘ฆ(๐‘ง = โŸจ๐‘ฅ, ๐‘ฆโŸฉ โˆง โŸจ๐‘ฅ, ๐‘ฆโŸฉ โˆˆ ๐น))
7673, 75sylibr 233 . . . . . . . . . . . 12 ((((๐œ‘ โˆง ๐‘ฅ โˆˆ (๐น supp 0 )) โˆง ๐‘ง โˆˆ (๐น โˆ– (V ร— { 0 }))) โˆง ๐‘ฅ = (1st โ€˜๐‘ง)) โ†’ ๐‘ง โˆˆ (๐น โ†พ {๐‘ฅ}))
7713ad3antrrr 729 . . . . . . . . . . . . 13 ((((๐œ‘ โˆง ๐‘ฅ โˆˆ (๐น supp 0 )) โˆง ๐‘ง โˆˆ (๐น โˆ– (V ร— { 0 }))) โˆง ๐‘ฅ = (1st โ€˜๐‘ง)) โ†’ ๐น Fn ๐ด)
7822ad2antrr 725 . . . . . . . . . . . . 13 ((((๐œ‘ โˆง ๐‘ฅ โˆˆ (๐น supp 0 )) โˆง ๐‘ง โˆˆ (๐น โˆ– (V ร— { 0 }))) โˆง ๐‘ฅ = (1st โ€˜๐‘ง)) โ†’ ๐‘ฅ โˆˆ ๐ด)
79 fnressn 7156 . . . . . . . . . . . . 13 ((๐น Fn ๐ด โˆง ๐‘ฅ โˆˆ ๐ด) โ†’ (๐น โ†พ {๐‘ฅ}) = {โŸจ๐‘ฅ, (๐นโ€˜๐‘ฅ)โŸฉ})
8077, 78, 79syl2anc 585 . . . . . . . . . . . 12 ((((๐œ‘ โˆง ๐‘ฅ โˆˆ (๐น supp 0 )) โˆง ๐‘ง โˆˆ (๐น โˆ– (V ร— { 0 }))) โˆง ๐‘ฅ = (1st โ€˜๐‘ง)) โ†’ (๐น โ†พ {๐‘ฅ}) = {โŸจ๐‘ฅ, (๐นโ€˜๐‘ฅ)โŸฉ})
8176, 80eleqtrd 2836 . . . . . . . . . . 11 ((((๐œ‘ โˆง ๐‘ฅ โˆˆ (๐น supp 0 )) โˆง ๐‘ง โˆˆ (๐น โˆ– (V ร— { 0 }))) โˆง ๐‘ฅ = (1st โ€˜๐‘ง)) โ†’ ๐‘ง โˆˆ {โŸจ๐‘ฅ, (๐นโ€˜๐‘ฅ)โŸฉ})
82 elsni 4646 . . . . . . . . . . 11 (๐‘ง โˆˆ {โŸจ๐‘ฅ, (๐นโ€˜๐‘ฅ)โŸฉ} โ†’ ๐‘ง = โŸจ๐‘ฅ, (๐นโ€˜๐‘ฅ)โŸฉ)
8381, 82syl 17 . . . . . . . . . 10 ((((๐œ‘ โˆง ๐‘ฅ โˆˆ (๐น supp 0 )) โˆง ๐‘ง โˆˆ (๐น โˆ– (V ร— { 0 }))) โˆง ๐‘ฅ = (1st โ€˜๐‘ง)) โ†’ ๐‘ง = โŸจ๐‘ฅ, (๐นโ€˜๐‘ฅ)โŸฉ)
84 simpr 486 . . . . . . . . . . . 12 ((((๐œ‘ โˆง ๐‘ฅ โˆˆ (๐น supp 0 )) โˆง ๐‘ง โˆˆ (๐น โˆ– (V ร— { 0 }))) โˆง ๐‘ง = โŸจ๐‘ฅ, (๐นโ€˜๐‘ฅ)โŸฉ) โ†’ ๐‘ง = โŸจ๐‘ฅ, (๐นโ€˜๐‘ฅ)โŸฉ)
8584fveq2d 6896 . . . . . . . . . . 11 ((((๐œ‘ โˆง ๐‘ฅ โˆˆ (๐น supp 0 )) โˆง ๐‘ง โˆˆ (๐น โˆ– (V ร— { 0 }))) โˆง ๐‘ง = โŸจ๐‘ฅ, (๐นโ€˜๐‘ฅ)โŸฉ) โ†’ (1st โ€˜๐‘ง) = (1st โ€˜โŸจ๐‘ฅ, (๐นโ€˜๐‘ฅ)โŸฉ))
86 fvex 6905 . . . . . . . . . . . 12 (๐นโ€˜๐‘ฅ) โˆˆ V
8774, 86op1st 7983 . . . . . . . . . . 11 (1st โ€˜โŸจ๐‘ฅ, (๐นโ€˜๐‘ฅ)โŸฉ) = ๐‘ฅ
8885, 87eqtr2di 2790 . . . . . . . . . 10 ((((๐œ‘ โˆง ๐‘ฅ โˆˆ (๐น supp 0 )) โˆง ๐‘ง โˆˆ (๐น โˆ– (V ร— { 0 }))) โˆง ๐‘ง = โŸจ๐‘ฅ, (๐นโ€˜๐‘ฅ)โŸฉ) โ†’ ๐‘ฅ = (1st โ€˜๐‘ง))
8983, 88impbida 800 . . . . . . . . 9 (((๐œ‘ โˆง ๐‘ฅ โˆˆ (๐น supp 0 )) โˆง ๐‘ง โˆˆ (๐น โˆ– (V ร— { 0 }))) โ†’ (๐‘ฅ = (1st โ€˜๐‘ง) โ†” ๐‘ง = โŸจ๐‘ฅ, (๐นโ€˜๐‘ฅ)โŸฉ))
9089ralrimiva 3147 . . . . . . . 8 ((๐œ‘ โˆง ๐‘ฅ โˆˆ (๐น supp 0 )) โ†’ โˆ€๐‘ง โˆˆ (๐น โˆ– (V ร— { 0 }))(๐‘ฅ = (1st โ€˜๐‘ง) โ†” ๐‘ง = โŸจ๐‘ฅ, (๐นโ€˜๐‘ฅ)โŸฉ))
9151, 55, 90rspcedvd 3615 . . . . . . 7 ((๐œ‘ โˆง ๐‘ฅ โˆˆ (๐น supp 0 )) โ†’ โˆƒ๐‘ฃ โˆˆ (๐น โˆ– (V ร— { 0 }))โˆ€๐‘ง โˆˆ (๐น โˆ– (V ร— { 0 }))(๐‘ฅ = (1st โ€˜๐‘ง) โ†” ๐‘ง = ๐‘ฃ))
92 reu6 3723 . . . . . . 7 (โˆƒ!๐‘ง โˆˆ (๐น โˆ– (V ร— { 0 }))๐‘ฅ = (1st โ€˜๐‘ง) โ†” โˆƒ๐‘ฃ โˆˆ (๐น โˆ– (V ร— { 0 }))โˆ€๐‘ง โˆˆ (๐น โˆ– (V ร— { 0 }))(๐‘ฅ = (1st โ€˜๐‘ง) โ†” ๐‘ง = ๐‘ฃ))
9391, 92sylibr 233 . . . . . 6 ((๐œ‘ โˆง ๐‘ฅ โˆˆ (๐น supp 0 )) โ†’ โˆƒ!๐‘ง โˆˆ (๐น โˆ– (V ร— { 0 }))๐‘ฅ = (1st โ€˜๐‘ง))
9417, 6, 7, 18, 8, 19, 20, 23, 40, 93gsummptf1o 19831 . . . . 5 (๐œ‘ โ†’ (๐บ ฮฃg (๐‘ฅ โˆˆ (๐น supp 0 ) โ†ฆ (๐นโ€˜๐‘ฅ))) = (๐บ ฮฃg (๐‘ง โˆˆ (๐น โˆ– (V ร— { 0 })) โ†ฆ (๐นโ€˜(1st โ€˜๐‘ง)))))
955, 16, 943eqtr3d 2781 . . . 4 (๐œ‘ โ†’ (๐บ ฮฃg ๐น) = (๐บ ฮฃg (๐‘ง โˆˆ (๐น โˆ– (V ร— { 0 })) โ†ฆ (๐นโ€˜(1st โ€˜๐‘ง)))))
96 simpr 486 . . . . . . . 8 ((๐œ‘ โˆง ๐‘ง โˆˆ (๐น โˆ– (V ร— { 0 }))) โ†’ ๐‘ง โˆˆ (๐น โˆ– (V ร— { 0 })))
9796eldifad 3961 . . . . . . 7 ((๐œ‘ โˆง ๐‘ง โˆˆ (๐น โˆ– (V ร— { 0 }))) โ†’ ๐‘ง โˆˆ ๐น)
98 funfv1st2nd 8032 . . . . . . 7 ((Fun ๐น โˆง ๐‘ง โˆˆ ๐น) โ†’ (๐นโ€˜(1st โ€˜๐‘ง)) = (2nd โ€˜๐‘ง))
9924, 97, 98syl2an2r 684 . . . . . 6 ((๐œ‘ โˆง ๐‘ง โˆˆ (๐น โˆ– (V ร— { 0 }))) โ†’ (๐นโ€˜(1st โ€˜๐‘ง)) = (2nd โ€˜๐‘ง))
10099mpteq2dva 5249 . . . . 5 (๐œ‘ โ†’ (๐‘ง โˆˆ (๐น โˆ– (V ร— { 0 })) โ†ฆ (๐นโ€˜(1st โ€˜๐‘ง))) = (๐‘ง โˆˆ (๐น โˆ– (V ร— { 0 })) โ†ฆ (2nd โ€˜๐‘ง)))
101100oveq2d 7425 . . . 4 (๐œ‘ โ†’ (๐บ ฮฃg (๐‘ง โˆˆ (๐น โˆ– (V ร— { 0 })) โ†ฆ (๐นโ€˜(1st โ€˜๐‘ง)))) = (๐บ ฮฃg (๐‘ง โˆˆ (๐น โˆ– (V ร— { 0 })) โ†ฆ (2nd โ€˜๐‘ง))))
10295, 101eqtrd 2773 . . 3 (๐œ‘ โ†’ (๐บ ฮฃg ๐น) = (๐บ ฮฃg (๐‘ง โˆˆ (๐น โˆ– (V ร— { 0 })) โ†ฆ (2nd โ€˜๐‘ง))))
103 nfcv 2904 . . . 4 โ„ฒ๐‘ง(1st โ€˜๐‘ก)
104 fvex 6905 . . . . 5 (2nd โ€˜๐‘ก) โˆˆ V
105 fvex 6905 . . . . 5 (1st โ€˜๐‘ก) โˆˆ V
106104, 105op2ndd 7986 . . . 4 (๐‘ง = โŸจ(2nd โ€˜๐‘ก), (1st โ€˜๐‘ก)โŸฉ โ†’ (2nd โ€˜๐‘ง) = (1st โ€˜๐‘ก))
107 resfnfinfin 9332 . . . . . 6 ((๐น Fn ๐ด โˆง (๐น supp 0 ) โˆˆ Fin) โ†’ (๐น โ†พ (๐น supp 0 )) โˆˆ Fin)
10813, 19, 107syl2anc 585 . . . . 5 (๐œ‘ โ†’ (๐น โ†พ (๐น supp 0 )) โˆˆ Fin)
10933, 108eqeltrrd 2835 . . . 4 (๐œ‘ โ†’ (๐น โˆ– (V ร— { 0 })) โˆˆ Fin)
11033rneqd 5938 . . . . 5 (๐œ‘ โ†’ ran (๐น โ†พ (๐น supp 0 )) = ran (๐น โˆ– (V ร— { 0 })))
111 rnresss 6018 . . . . . 6 ran (๐น โ†พ (๐น supp 0 )) โŠ† ran ๐น
1121frnd 6726 . . . . . 6 (๐œ‘ โ†’ ran ๐น โŠ† ๐ต)
113111, 112sstrid 3994 . . . . 5 (๐œ‘ โ†’ ran (๐น โ†พ (๐น supp 0 )) โŠ† ๐ต)
114110, 113eqsstrrd 4022 . . . 4 (๐œ‘ โ†’ ran (๐น โˆ– (V ร— { 0 })) โŠ† ๐ต)
115 2ndrn 8027 . . . . 5 ((Rel (๐น โˆ– (V ร— { 0 })) โˆง ๐‘ง โˆˆ (๐น โˆ– (V ร— { 0 }))) โ†’ (2nd โ€˜๐‘ง) โˆˆ ran (๐น โˆ– (V ร— { 0 })))
11627, 115sylan 581 . . . 4 ((๐œ‘ โˆง ๐‘ง โˆˆ (๐น โˆ– (V ร— { 0 }))) โ†’ (2nd โ€˜๐‘ง) โˆˆ ran (๐น โˆ– (V ร— { 0 })))
117 relcnv 6104 . . . . . . . 8 Rel โ—ก๐น
118 reldif 5816 . . . . . . . 8 (Rel โ—ก๐น โ†’ Rel (โ—ก๐น โˆ– ({ 0 } ร— V)))
119117, 118mp1i 13 . . . . . . 7 (๐œ‘ โ†’ Rel (โ—ก๐น โˆ– ({ 0 } ร— V)))
120 1st2nd 8025 . . . . . . 7 ((Rel (โ—ก๐น โˆ– ({ 0 } ร— V)) โˆง ๐‘ก โˆˆ (โ—ก๐น โˆ– ({ 0 } ร— V))) โ†’ ๐‘ก = โŸจ(1st โ€˜๐‘ก), (2nd โ€˜๐‘ก)โŸฉ)
121119, 120sylan 581 . . . . . 6 ((๐œ‘ โˆง ๐‘ก โˆˆ (โ—ก๐น โˆ– ({ 0 } ร— V))) โ†’ ๐‘ก = โŸจ(1st โ€˜๐‘ก), (2nd โ€˜๐‘ก)โŸฉ)
122 cnvdif 6144 . . . . . . . . . 10 โ—ก(๐น โˆ– (V ร— { 0 })) = (โ—ก๐น โˆ– โ—ก(V ร— { 0 }))
123 cnvxp 6157 . . . . . . . . . . 11 โ—ก(V ร— { 0 }) = ({ 0 } ร— V)
124123difeq2i 4120 . . . . . . . . . 10 (โ—ก๐น โˆ– โ—ก(V ร— { 0 })) = (โ—ก๐น โˆ– ({ 0 } ร— V))
125122, 124eqtri 2761 . . . . . . . . 9 โ—ก(๐น โˆ– (V ร— { 0 })) = (โ—ก๐น โˆ– ({ 0 } ร— V))
126125eqimss2i 4044 . . . . . . . 8 (โ—ก๐น โˆ– ({ 0 } ร— V)) โŠ† โ—ก(๐น โˆ– (V ร— { 0 }))
127126a1i 11 . . . . . . 7 (๐œ‘ โ†’ (โ—ก๐น โˆ– ({ 0 } ร— V)) โŠ† โ—ก(๐น โˆ– (V ร— { 0 })))
128127sselda 3983 . . . . . 6 ((๐œ‘ โˆง ๐‘ก โˆˆ (โ—ก๐น โˆ– ({ 0 } ร— V))) โ†’ ๐‘ก โˆˆ โ—ก(๐น โˆ– (V ร— { 0 })))
129121, 128eqeltrrd 2835 . . . . 5 ((๐œ‘ โˆง ๐‘ก โˆˆ (โ—ก๐น โˆ– ({ 0 } ร— V))) โ†’ โŸจ(1st โ€˜๐‘ก), (2nd โ€˜๐‘ก)โŸฉ โˆˆ โ—ก(๐น โˆ– (V ร— { 0 })))
130105, 104opelcnv 5882 . . . . 5 (โŸจ(1st โ€˜๐‘ก), (2nd โ€˜๐‘ก)โŸฉ โˆˆ โ—ก(๐น โˆ– (V ร— { 0 })) โ†” โŸจ(2nd โ€˜๐‘ก), (1st โ€˜๐‘ก)โŸฉ โˆˆ (๐น โˆ– (V ร— { 0 })))
131129, 130sylib 217 . . . 4 ((๐œ‘ โˆง ๐‘ก โˆˆ (โ—ก๐น โˆ– ({ 0 } ร— V))) โ†’ โŸจ(2nd โ€˜๐‘ก), (1st โ€˜๐‘ก)โŸฉ โˆˆ (๐น โˆ– (V ร— { 0 })))
13227adantr 482 . . . . . . . 8 ((๐œ‘ โˆง ๐‘ง โˆˆ (๐น โˆ– (V ร— { 0 }))) โ†’ Rel (๐น โˆ– (V ร— { 0 })))
133 eqidd 2734 . . . . . . . 8 ((๐œ‘ โˆง ๐‘ง โˆˆ (๐น โˆ– (V ร— { 0 }))) โ†’ โˆช โ—ก{๐‘ง} = โˆช โ—ก{๐‘ง})
134 cnvf1olem 8096 . . . . . . . . 9 ((Rel (๐น โˆ– (V ร— { 0 })) โˆง (๐‘ง โˆˆ (๐น โˆ– (V ร— { 0 })) โˆง โˆช โ—ก{๐‘ง} = โˆช โ—ก{๐‘ง})) โ†’ (โˆช โ—ก{๐‘ง} โˆˆ โ—ก(๐น โˆ– (V ร— { 0 })) โˆง ๐‘ง = โˆช โ—ก{โˆช โ—ก{๐‘ง}}))
135134simpld 496 . . . . . . . 8 ((Rel (๐น โˆ– (V ร— { 0 })) โˆง (๐‘ง โˆˆ (๐น โˆ– (V ร— { 0 })) โˆง โˆช โ—ก{๐‘ง} = โˆช โ—ก{๐‘ง})) โ†’ โˆช โ—ก{๐‘ง} โˆˆ โ—ก(๐น โˆ– (V ร— { 0 })))
136132, 96, 133, 135syl12anc 836 . . . . . . 7 ((๐œ‘ โˆง ๐‘ง โˆˆ (๐น โˆ– (V ร— { 0 }))) โ†’ โˆช โ—ก{๐‘ง} โˆˆ โ—ก(๐น โˆ– (V ร— { 0 })))
137136, 125eleqtrdi 2844 . . . . . 6 ((๐œ‘ โˆง ๐‘ง โˆˆ (๐น โˆ– (V ร— { 0 }))) โ†’ โˆช โ—ก{๐‘ง} โˆˆ (โ—ก๐น โˆ– ({ 0 } ร— V)))
138 eqeq2 2745 . . . . . . . . 9 (๐‘ข = โˆช โ—ก{๐‘ง} โ†’ (๐‘ก = ๐‘ข โ†” ๐‘ก = โˆช โ—ก{๐‘ง}))
139138bibi2d 343 . . . . . . . 8 (๐‘ข = โˆช โ—ก{๐‘ง} โ†’ ((๐‘ง = โŸจ(2nd โ€˜๐‘ก), (1st โ€˜๐‘ก)โŸฉ โ†” ๐‘ก = ๐‘ข) โ†” (๐‘ง = โŸจ(2nd โ€˜๐‘ก), (1st โ€˜๐‘ก)โŸฉ โ†” ๐‘ก = โˆช โ—ก{๐‘ง})))
140139ralbidv 3178 . . . . . . 7 (๐‘ข = โˆช โ—ก{๐‘ง} โ†’ (โˆ€๐‘ก โˆˆ (โ—ก๐น โˆ– ({ 0 } ร— V))(๐‘ง = โŸจ(2nd โ€˜๐‘ก), (1st โ€˜๐‘ก)โŸฉ โ†” ๐‘ก = ๐‘ข) โ†” โˆ€๐‘ก โˆˆ (โ—ก๐น โˆ– ({ 0 } ร— V))(๐‘ง = โŸจ(2nd โ€˜๐‘ก), (1st โ€˜๐‘ก)โŸฉ โ†” ๐‘ก = โˆช โ—ก{๐‘ง})))
141140adantl 483 . . . . . 6 (((๐œ‘ โˆง ๐‘ง โˆˆ (๐น โˆ– (V ร— { 0 }))) โˆง ๐‘ข = โˆช โ—ก{๐‘ง}) โ†’ (โˆ€๐‘ก โˆˆ (โ—ก๐น โˆ– ({ 0 } ร— V))(๐‘ง = โŸจ(2nd โ€˜๐‘ก), (1st โ€˜๐‘ก)โŸฉ โ†” ๐‘ก = ๐‘ข) โ†” โˆ€๐‘ก โˆˆ (โ—ก๐น โˆ– ({ 0 } ร— V))(๐‘ง = โŸจ(2nd โ€˜๐‘ก), (1st โ€˜๐‘ก)โŸฉ โ†” ๐‘ก = โˆช โ—ก{๐‘ง})))
142117, 118mp1i 13 . . . . . . . . 9 ((((๐œ‘ โˆง ๐‘ง โˆˆ (๐น โˆ– (V ร— { 0 }))) โˆง ๐‘ก โˆˆ (โ—ก๐น โˆ– ({ 0 } ร— V))) โˆง ๐‘ง = โŸจ(2nd โ€˜๐‘ก), (1st โ€˜๐‘ก)โŸฉ) โ†’ Rel (โ—ก๐น โˆ– ({ 0 } ร— V)))
143 simplr 768 . . . . . . . . 9 ((((๐œ‘ โˆง ๐‘ง โˆˆ (๐น โˆ– (V ร— { 0 }))) โˆง ๐‘ก โˆˆ (โ—ก๐น โˆ– ({ 0 } ร— V))) โˆง ๐‘ง = โŸจ(2nd โ€˜๐‘ก), (1st โ€˜๐‘ก)โŸฉ) โ†’ ๐‘ก โˆˆ (โ—ก๐น โˆ– ({ 0 } ร— V)))
144 simpr 486 . . . . . . . . . 10 ((((๐œ‘ โˆง ๐‘ง โˆˆ (๐น โˆ– (V ร— { 0 }))) โˆง ๐‘ก โˆˆ (โ—ก๐น โˆ– ({ 0 } ร— V))) โˆง ๐‘ง = โŸจ(2nd โ€˜๐‘ก), (1st โ€˜๐‘ก)โŸฉ) โ†’ ๐‘ง = โŸจ(2nd โ€˜๐‘ก), (1st โ€˜๐‘ก)โŸฉ)
145 df-rel 5684 . . . . . . . . . . . . . 14 (Rel (โ—ก๐น โˆ– ({ 0 } ร— V)) โ†” (โ—ก๐น โˆ– ({ 0 } ร— V)) โŠ† (V ร— V))
146119, 145sylib 217 . . . . . . . . . . . . 13 (๐œ‘ โ†’ (โ—ก๐น โˆ– ({ 0 } ร— V)) โŠ† (V ร— V))
147146ad3antrrr 729 . . . . . . . . . . . 12 ((((๐œ‘ โˆง ๐‘ง โˆˆ (๐น โˆ– (V ร— { 0 }))) โˆง ๐‘ก โˆˆ (โ—ก๐น โˆ– ({ 0 } ร— V))) โˆง ๐‘ง = โŸจ(2nd โ€˜๐‘ก), (1st โ€˜๐‘ก)โŸฉ) โ†’ (โ—ก๐น โˆ– ({ 0 } ร— V)) โŠ† (V ร— V))
148147, 143sseldd 3984 . . . . . . . . . . 11 ((((๐œ‘ โˆง ๐‘ง โˆˆ (๐น โˆ– (V ร— { 0 }))) โˆง ๐‘ก โˆˆ (โ—ก๐น โˆ– ({ 0 } ร— V))) โˆง ๐‘ง = โŸจ(2nd โ€˜๐‘ก), (1st โ€˜๐‘ก)โŸฉ) โ†’ ๐‘ก โˆˆ (V ร— V))
149 2nd1st 8024 . . . . . . . . . . 11 (๐‘ก โˆˆ (V ร— V) โ†’ โˆช โ—ก{๐‘ก} = โŸจ(2nd โ€˜๐‘ก), (1st โ€˜๐‘ก)โŸฉ)
150148, 149syl 17 . . . . . . . . . 10 ((((๐œ‘ โˆง ๐‘ง โˆˆ (๐น โˆ– (V ร— { 0 }))) โˆง ๐‘ก โˆˆ (โ—ก๐น โˆ– ({ 0 } ร— V))) โˆง ๐‘ง = โŸจ(2nd โ€˜๐‘ก), (1st โ€˜๐‘ก)โŸฉ) โ†’ โˆช โ—ก{๐‘ก} = โŸจ(2nd โ€˜๐‘ก), (1st โ€˜๐‘ก)โŸฉ)
151144, 150eqtr4d 2776 . . . . . . . . 9 ((((๐œ‘ โˆง ๐‘ง โˆˆ (๐น โˆ– (V ร— { 0 }))) โˆง ๐‘ก โˆˆ (โ—ก๐น โˆ– ({ 0 } ร— V))) โˆง ๐‘ง = โŸจ(2nd โ€˜๐‘ก), (1st โ€˜๐‘ก)โŸฉ) โ†’ ๐‘ง = โˆช โ—ก{๐‘ก})
152 cnvf1olem 8096 . . . . . . . . . 10 ((Rel (โ—ก๐น โˆ– ({ 0 } ร— V)) โˆง (๐‘ก โˆˆ (โ—ก๐น โˆ– ({ 0 } ร— V)) โˆง ๐‘ง = โˆช โ—ก{๐‘ก})) โ†’ (๐‘ง โˆˆ โ—ก(โ—ก๐น โˆ– ({ 0 } ร— V)) โˆง ๐‘ก = โˆช โ—ก{๐‘ง}))
153152simprd 497 . . . . . . . . 9 ((Rel (โ—ก๐น โˆ– ({ 0 } ร— V)) โˆง (๐‘ก โˆˆ (โ—ก๐น โˆ– ({ 0 } ร— V)) โˆง ๐‘ง = โˆช โ—ก{๐‘ก})) โ†’ ๐‘ก = โˆช โ—ก{๐‘ง})
154142, 143, 151, 153syl12anc 836 . . . . . . . 8 ((((๐œ‘ โˆง ๐‘ง โˆˆ (๐น โˆ– (V ร— { 0 }))) โˆง ๐‘ก โˆˆ (โ—ก๐น โˆ– ({ 0 } ร— V))) โˆง ๐‘ง = โŸจ(2nd โ€˜๐‘ก), (1st โ€˜๐‘ก)โŸฉ) โ†’ ๐‘ก = โˆช โ—ก{๐‘ง})
15527ad3antrrr 729 . . . . . . . . . 10 ((((๐œ‘ โˆง ๐‘ง โˆˆ (๐น โˆ– (V ร— { 0 }))) โˆง ๐‘ก โˆˆ (โ—ก๐น โˆ– ({ 0 } ร— V))) โˆง ๐‘ก = โˆช โ—ก{๐‘ง}) โ†’ Rel (๐น โˆ– (V ร— { 0 })))
15696ad2antrr 725 . . . . . . . . . 10 ((((๐œ‘ โˆง ๐‘ง โˆˆ (๐น โˆ– (V ร— { 0 }))) โˆง ๐‘ก โˆˆ (โ—ก๐น โˆ– ({ 0 } ร— V))) โˆง ๐‘ก = โˆช โ—ก{๐‘ง}) โ†’ ๐‘ง โˆˆ (๐น โˆ– (V ร— { 0 })))
157 simpr 486 . . . . . . . . . 10 ((((๐œ‘ โˆง ๐‘ง โˆˆ (๐น โˆ– (V ร— { 0 }))) โˆง ๐‘ก โˆˆ (โ—ก๐น โˆ– ({ 0 } ร— V))) โˆง ๐‘ก = โˆช โ—ก{๐‘ง}) โ†’ ๐‘ก = โˆช โ—ก{๐‘ง})
158 cnvf1olem 8096 . . . . . . . . . . 11 ((Rel (๐น โˆ– (V ร— { 0 })) โˆง (๐‘ง โˆˆ (๐น โˆ– (V ร— { 0 })) โˆง ๐‘ก = โˆช โ—ก{๐‘ง})) โ†’ (๐‘ก โˆˆ โ—ก(๐น โˆ– (V ร— { 0 })) โˆง ๐‘ง = โˆช โ—ก{๐‘ก}))
159158simprd 497 . . . . . . . . . 10 ((Rel (๐น โˆ– (V ร— { 0 })) โˆง (๐‘ง โˆˆ (๐น โˆ– (V ร— { 0 })) โˆง ๐‘ก = โˆช โ—ก{๐‘ง})) โ†’ ๐‘ง = โˆช โ—ก{๐‘ก})
160155, 156, 157, 159syl12anc 836 . . . . . . . . 9 ((((๐œ‘ โˆง ๐‘ง โˆˆ (๐น โˆ– (V ร— { 0 }))) โˆง ๐‘ก โˆˆ (โ—ก๐น โˆ– ({ 0 } ร— V))) โˆง ๐‘ก = โˆช โ—ก{๐‘ง}) โ†’ ๐‘ง = โˆช โ—ก{๐‘ก})
161146ad3antrrr 729 . . . . . . . . . . 11 ((((๐œ‘ โˆง ๐‘ง โˆˆ (๐น โˆ– (V ร— { 0 }))) โˆง ๐‘ก โˆˆ (โ—ก๐น โˆ– ({ 0 } ร— V))) โˆง ๐‘ก = โˆช โ—ก{๐‘ง}) โ†’ (โ—ก๐น โˆ– ({ 0 } ร— V)) โŠ† (V ร— V))
162 simplr 768 . . . . . . . . . . 11 ((((๐œ‘ โˆง ๐‘ง โˆˆ (๐น โˆ– (V ร— { 0 }))) โˆง ๐‘ก โˆˆ (โ—ก๐น โˆ– ({ 0 } ร— V))) โˆง ๐‘ก = โˆช โ—ก{๐‘ง}) โ†’ ๐‘ก โˆˆ (โ—ก๐น โˆ– ({ 0 } ร— V)))
163161, 162sseldd 3984 . . . . . . . . . 10 ((((๐œ‘ โˆง ๐‘ง โˆˆ (๐น โˆ– (V ร— { 0 }))) โˆง ๐‘ก โˆˆ (โ—ก๐น โˆ– ({ 0 } ร— V))) โˆง ๐‘ก = โˆช โ—ก{๐‘ง}) โ†’ ๐‘ก โˆˆ (V ร— V))
164163, 149syl 17 . . . . . . . . 9 ((((๐œ‘ โˆง ๐‘ง โˆˆ (๐น โˆ– (V ร— { 0 }))) โˆง ๐‘ก โˆˆ (โ—ก๐น โˆ– ({ 0 } ร— V))) โˆง ๐‘ก = โˆช โ—ก{๐‘ง}) โ†’ โˆช โ—ก{๐‘ก} = โŸจ(2nd โ€˜๐‘ก), (1st โ€˜๐‘ก)โŸฉ)
165160, 164eqtrd 2773 . . . . . . . 8 ((((๐œ‘ โˆง ๐‘ง โˆˆ (๐น โˆ– (V ร— { 0 }))) โˆง ๐‘ก โˆˆ (โ—ก๐น โˆ– ({ 0 } ร— V))) โˆง ๐‘ก = โˆช โ—ก{๐‘ง}) โ†’ ๐‘ง = โŸจ(2nd โ€˜๐‘ก), (1st โ€˜๐‘ก)โŸฉ)
166154, 165impbida 800 . . . . . . 7 (((๐œ‘ โˆง ๐‘ง โˆˆ (๐น โˆ– (V ร— { 0 }))) โˆง ๐‘ก โˆˆ (โ—ก๐น โˆ– ({ 0 } ร— V))) โ†’ (๐‘ง = โŸจ(2nd โ€˜๐‘ก), (1st โ€˜๐‘ก)โŸฉ โ†” ๐‘ก = โˆช โ—ก{๐‘ง}))
167166ralrimiva 3147 . . . . . 6 ((๐œ‘ โˆง ๐‘ง โˆˆ (๐น โˆ– (V ร— { 0 }))) โ†’ โˆ€๐‘ก โˆˆ (โ—ก๐น โˆ– ({ 0 } ร— V))(๐‘ง = โŸจ(2nd โ€˜๐‘ก), (1st โ€˜๐‘ก)โŸฉ โ†” ๐‘ก = โˆช โ—ก{๐‘ง}))
168137, 141, 167rspcedvd 3615 . . . . 5 ((๐œ‘ โˆง ๐‘ง โˆˆ (๐น โˆ– (V ร— { 0 }))) โ†’ โˆƒ๐‘ข โˆˆ (โ—ก๐น โˆ– ({ 0 } ร— V))โˆ€๐‘ก โˆˆ (โ—ก๐น โˆ– ({ 0 } ร— V))(๐‘ง = โŸจ(2nd โ€˜๐‘ก), (1st โ€˜๐‘ก)โŸฉ โ†” ๐‘ก = ๐‘ข))
169 reu6 3723 . . . . 5 (โˆƒ!๐‘ก โˆˆ (โ—ก๐น โˆ– ({ 0 } ร— V))๐‘ง = โŸจ(2nd โ€˜๐‘ก), (1st โ€˜๐‘ก)โŸฉ โ†” โˆƒ๐‘ข โˆˆ (โ—ก๐น โˆ– ({ 0 } ร— V))โˆ€๐‘ก โˆˆ (โ—ก๐น โˆ– ({ 0 } ร— V))(๐‘ง = โŸจ(2nd โ€˜๐‘ก), (1st โ€˜๐‘ก)โŸฉ โ†” ๐‘ก = ๐‘ข))
170168, 169sylibr 233 . . . 4 ((๐œ‘ โˆง ๐‘ง โˆˆ (๐น โˆ– (V ร— { 0 }))) โ†’ โˆƒ!๐‘ก โˆˆ (โ—ก๐น โˆ– ({ 0 } ร— V))๐‘ง = โŸจ(2nd โ€˜๐‘ก), (1st โ€˜๐‘ก)โŸฉ)
171103, 6, 7, 106, 8, 109, 114, 116, 131, 170gsummptf1o 19831 . . 3 (๐œ‘ โ†’ (๐บ ฮฃg (๐‘ง โˆˆ (๐น โˆ– (V ร— { 0 })) โ†ฆ (2nd โ€˜๐‘ง))) = (๐บ ฮฃg (๐‘ก โˆˆ (โ—ก๐น โˆ– ({ 0 } ร— V)) โ†ฆ (1st โ€˜๐‘ก))))
172 fveq2 6892 . . . . . 6 (๐‘ก = ๐‘ง โ†’ (1st โ€˜๐‘ก) = (1st โ€˜๐‘ง))
173172cbvmptv 5262 . . . . 5 (๐‘ก โˆˆ (โ—ก๐น โˆ– ({ 0 } ร— V)) โ†ฆ (1st โ€˜๐‘ก)) = (๐‘ง โˆˆ (โ—ก๐น โˆ– ({ 0 } ร— V)) โ†ฆ (1st โ€˜๐‘ง))
17433cnveqd 5876 . . . . . . 7 (๐œ‘ โ†’ โ—ก(๐น โ†พ (๐น supp 0 )) = โ—ก(๐น โˆ– (V ร— { 0 })))
175174, 125eqtr2di 2790 . . . . . 6 (๐œ‘ โ†’ (โ—ก๐น โˆ– ({ 0 } ร— V)) = โ—ก(๐น โ†พ (๐น supp 0 )))
176175mpteq1d 5244 . . . . 5 (๐œ‘ โ†’ (๐‘ง โˆˆ (โ—ก๐น โˆ– ({ 0 } ร— V)) โ†ฆ (1st โ€˜๐‘ง)) = (๐‘ง โˆˆ โ—ก(๐น โ†พ (๐น supp 0 )) โ†ฆ (1st โ€˜๐‘ง)))
177173, 176eqtrid 2785 . . . 4 (๐œ‘ โ†’ (๐‘ก โˆˆ (โ—ก๐น โˆ– ({ 0 } ร— V)) โ†ฆ (1st โ€˜๐‘ก)) = (๐‘ง โˆˆ โ—ก(๐น โ†พ (๐น supp 0 )) โ†ฆ (1st โ€˜๐‘ง)))
178177oveq2d 7425 . . 3 (๐œ‘ โ†’ (๐บ ฮฃg (๐‘ก โˆˆ (โ—ก๐น โˆ– ({ 0 } ร— V)) โ†ฆ (1st โ€˜๐‘ก))) = (๐บ ฮฃg (๐‘ง โˆˆ โ—ก(๐น โ†พ (๐น supp 0 )) โ†ฆ (1st โ€˜๐‘ง))))
179102, 171, 1783eqtrd 2777 . 2 (๐œ‘ โ†’ (๐บ ฮฃg ๐น) = (๐บ ฮฃg (๐‘ง โˆˆ โ—ก(๐น โ†พ (๐น supp 0 )) โ†ฆ (1st โ€˜๐‘ง))))
180 nfcv 2904 . . 3 โ„ฒ๐‘ฆ(1st โ€˜๐‘ง)
181 nfv 1918 . . 3 โ„ฒ๐‘ฅ๐œ‘
182 vex 3479 . . . 4 ๐‘ฆ โˆˆ V
18374, 182op1std 7985 . . 3 (๐‘ง = โŸจ๐‘ฅ, ๐‘ฆโŸฉ โ†’ (1st โ€˜๐‘ง) = ๐‘ฅ)
184 relcnv 6104 . . . 4 Rel โ—ก(๐น โ†พ (๐น supp 0 ))
185184a1i 11 . . 3 (๐œ‘ โ†’ Rel โ—ก(๐น โ†พ (๐น supp 0 )))
186 cnvfi 9180 . . . 4 ((๐น โ†พ (๐น supp 0 )) โˆˆ Fin โ†’ โ—ก(๐น โ†พ (๐น supp 0 )) โˆˆ Fin)
187108, 186syl 17 . . 3 (๐œ‘ โ†’ โ—ก(๐น โ†พ (๐น supp 0 )) โˆˆ Fin)
188112adantr 482 . . . 4 ((๐œ‘ โˆง ๐‘ง โˆˆ โ—ก(๐น โ†พ (๐น supp 0 ))) โ†’ ran ๐น โŠ† ๐ต)
189184a1i 11 . . . . . . 7 ((๐œ‘ โˆง ๐‘ง โˆˆ โ—ก(๐น โ†พ (๐น supp 0 ))) โ†’ Rel โ—ก(๐น โ†พ (๐น supp 0 )))
190 simpr 486 . . . . . . 7 ((๐œ‘ โˆง ๐‘ง โˆˆ โ—ก(๐น โ†พ (๐น supp 0 ))) โ†’ ๐‘ง โˆˆ โ—ก(๐น โ†พ (๐น supp 0 )))
191 1stdm 8026 . . . . . . 7 ((Rel โ—ก(๐น โ†พ (๐น supp 0 )) โˆง ๐‘ง โˆˆ โ—ก(๐น โ†พ (๐น supp 0 ))) โ†’ (1st โ€˜๐‘ง) โˆˆ dom โ—ก(๐น โ†พ (๐น supp 0 )))
192189, 190, 191syl2anc 585 . . . . . 6 ((๐œ‘ โˆง ๐‘ง โˆˆ โ—ก(๐น โ†พ (๐น supp 0 ))) โ†’ (1st โ€˜๐‘ง) โˆˆ dom โ—ก(๐น โ†พ (๐น supp 0 )))
193 df-rn 5688 . . . . . 6 ran (๐น โ†พ (๐น supp 0 )) = dom โ—ก(๐น โ†พ (๐น supp 0 ))
194192, 193eleqtrrdi 2845 . . . . 5 ((๐œ‘ โˆง ๐‘ง โˆˆ โ—ก(๐น โ†พ (๐น supp 0 ))) โ†’ (1st โ€˜๐‘ง) โˆˆ ran (๐น โ†พ (๐น supp 0 )))
195111, 194sselid 3981 . . . 4 ((๐œ‘ โˆง ๐‘ง โˆˆ โ—ก(๐น โ†พ (๐น supp 0 ))) โ†’ (1st โ€˜๐‘ง) โˆˆ ran ๐น)
196188, 195sseldd 3984 . . 3 ((๐œ‘ โˆง ๐‘ง โˆˆ โ—ก(๐น โ†พ (๐น supp 0 ))) โ†’ (1st โ€˜๐‘ง) โˆˆ ๐ต)
197180, 181, 6, 183, 185, 187, 8, 196gsummpt2d 32201 . 2 (๐œ‘ โ†’ (๐บ ฮฃg (๐‘ง โˆˆ โ—ก(๐น โ†พ (๐น supp 0 )) โ†ฆ (1st โ€˜๐‘ง))) = (๐บ ฮฃg (๐‘ฅ โˆˆ dom โ—ก(๐น โ†พ (๐น supp 0 )) โ†ฆ (๐บ ฮฃg (๐‘ฆ โˆˆ (โ—ก(๐น โ†พ (๐น supp 0 )) โ€œ {๐‘ฅ}) โ†ฆ ๐‘ฅ)))))
198 df-ima 5690 . . . . . . 7 (๐น โ€œ (๐น supp 0 )) = ran (๐น โ†พ (๐น supp 0 ))
199 supppreima 31913 . . . . . . . . 9 ((Fun ๐น โˆง ๐น โˆˆ V โˆง 0 โˆˆ V) โ†’ (๐น supp 0 ) = (โ—ก๐น โ€œ (ran ๐น โˆ– { 0 })))
20024, 12, 31, 199syl3anc 1372 . . . . . . . 8 (๐œ‘ โ†’ (๐น supp 0 ) = (โ—ก๐น โ€œ (ran ๐น โˆ– { 0 })))
201200imaeq2d 6060 . . . . . . 7 (๐œ‘ โ†’ (๐น โ€œ (๐น supp 0 )) = (๐น โ€œ (โ—ก๐น โ€œ (ran ๐น โˆ– { 0 }))))
202198, 201eqtr3id 2787 . . . . . 6 (๐œ‘ โ†’ ran (๐น โ†พ (๐น supp 0 )) = (๐น โ€œ (โ—ก๐น โ€œ (ran ๐น โˆ– { 0 }))))
203 funimacnv 6630 . . . . . . 7 (Fun ๐น โ†’ (๐น โ€œ (โ—ก๐น โ€œ (ran ๐น โˆ– { 0 }))) = ((ran ๐น โˆ– { 0 }) โˆฉ ran ๐น))
20424, 203syl 17 . . . . . 6 (๐œ‘ โ†’ (๐น โ€œ (โ—ก๐น โ€œ (ran ๐น โˆ– { 0 }))) = ((ran ๐น โˆ– { 0 }) โˆฉ ran ๐น))
205 difssd 4133 . . . . . . 7 (๐œ‘ โ†’ (ran ๐น โˆ– { 0 }) โŠ† ran ๐น)
206 df-ss 3966 . . . . . . 7 ((ran ๐น โˆ– { 0 }) โŠ† ran ๐น โ†” ((ran ๐น โˆ– { 0 }) โˆฉ ran ๐น) = (ran ๐น โˆ– { 0 }))
207205, 206sylib 217 . . . . . 6 (๐œ‘ โ†’ ((ran ๐น โˆ– { 0 }) โˆฉ ran ๐น) = (ran ๐น โˆ– { 0 }))
208202, 204, 2073eqtrd 2777 . . . . 5 (๐œ‘ โ†’ ran (๐น โ†พ (๐น supp 0 )) = (ran ๐น โˆ– { 0 }))
209193, 208eqtr3id 2787 . . . 4 (๐œ‘ โ†’ dom โ—ก(๐น โ†พ (๐น supp 0 )) = (ran ๐น โˆ– { 0 }))
2108cmnmndd 19672 . . . . . . 7 (๐œ‘ โ†’ ๐บ โˆˆ Mnd)
211210adantr 482 . . . . . 6 ((๐œ‘ โˆง ๐‘ฅ โˆˆ dom โ—ก(๐น โ†พ (๐น supp 0 ))) โ†’ ๐บ โˆˆ Mnd)
212108adantr 482 . . . . . . 7 ((๐œ‘ โˆง ๐‘ฅ โˆˆ dom โ—ก(๐น โ†พ (๐น supp 0 ))) โ†’ (๐น โ†พ (๐น supp 0 )) โˆˆ Fin)
213 imafi2 31936 . . . . . . 7 (โ—ก(๐น โ†พ (๐น supp 0 )) โˆˆ Fin โ†’ (โ—ก(๐น โ†พ (๐น supp 0 )) โ€œ {๐‘ฅ}) โˆˆ Fin)
214212, 186, 2133syl 18 . . . . . 6 ((๐œ‘ โˆง ๐‘ฅ โˆˆ dom โ—ก(๐น โ†พ (๐น supp 0 ))) โ†’ (โ—ก(๐น โ†พ (๐น supp 0 )) โ€œ {๐‘ฅ}) โˆˆ Fin)
215193, 113eqsstrrid 4032 . . . . . . 7 (๐œ‘ โ†’ dom โ—ก(๐น โ†พ (๐น supp 0 )) โŠ† ๐ต)
216215sselda 3983 . . . . . 6 ((๐œ‘ โˆง ๐‘ฅ โˆˆ dom โ—ก(๐น โ†พ (๐น supp 0 ))) โ†’ ๐‘ฅ โˆˆ ๐ต)
217 gsumhashmul.x . . . . . . 7 ยท = (.gโ€˜๐บ)
2186, 217gsumconst 19802 . . . . . 6 ((๐บ โˆˆ Mnd โˆง (โ—ก(๐น โ†พ (๐น supp 0 )) โ€œ {๐‘ฅ}) โˆˆ Fin โˆง ๐‘ฅ โˆˆ ๐ต) โ†’ (๐บ ฮฃg (๐‘ฆ โˆˆ (โ—ก(๐น โ†พ (๐น supp 0 )) โ€œ {๐‘ฅ}) โ†ฆ ๐‘ฅ)) = ((โ™ฏโ€˜(โ—ก(๐น โ†พ (๐น supp 0 )) โ€œ {๐‘ฅ})) ยท ๐‘ฅ))
219211, 214, 216, 218syl3anc 1372 . . . . 5 ((๐œ‘ โˆง ๐‘ฅ โˆˆ dom โ—ก(๐น โ†พ (๐น supp 0 ))) โ†’ (๐บ ฮฃg (๐‘ฆ โˆˆ (โ—ก(๐น โ†พ (๐น supp 0 )) โ€œ {๐‘ฅ}) โ†ฆ ๐‘ฅ)) = ((โ™ฏโ€˜(โ—ก(๐น โ†พ (๐น supp 0 )) โ€œ {๐‘ฅ})) ยท ๐‘ฅ))
220 cnvresima 6230 . . . . . . . 8 (โ—ก(๐น โ†พ (๐น supp 0 )) โ€œ {๐‘ฅ}) = ((โ—ก๐น โ€œ {๐‘ฅ}) โˆฉ (๐น supp 0 ))
221209eleq2d 2820 . . . . . . . . . . . . 13 (๐œ‘ โ†’ (๐‘ฅ โˆˆ dom โ—ก(๐น โ†พ (๐น supp 0 )) โ†” ๐‘ฅ โˆˆ (ran ๐น โˆ– { 0 })))
222221biimpa 478 . . . . . . . . . . . 12 ((๐œ‘ โˆง ๐‘ฅ โˆˆ dom โ—ก(๐น โ†พ (๐น supp 0 ))) โ†’ ๐‘ฅ โˆˆ (ran ๐น โˆ– { 0 }))
223222snssd 4813 . . . . . . . . . . 11 ((๐œ‘ โˆง ๐‘ฅ โˆˆ dom โ—ก(๐น โ†พ (๐น supp 0 ))) โ†’ {๐‘ฅ} โŠ† (ran ๐น โˆ– { 0 }))
224 sspreima 7070 . . . . . . . . . . 11 ((Fun ๐น โˆง {๐‘ฅ} โŠ† (ran ๐น โˆ– { 0 })) โ†’ (โ—ก๐น โ€œ {๐‘ฅ}) โŠ† (โ—ก๐น โ€œ (ran ๐น โˆ– { 0 })))
22524, 223, 224syl2an2r 684 . . . . . . . . . 10 ((๐œ‘ โˆง ๐‘ฅ โˆˆ dom โ—ก(๐น โ†พ (๐น supp 0 ))) โ†’ (โ—ก๐น โ€œ {๐‘ฅ}) โŠ† (โ—ก๐น โ€œ (ran ๐น โˆ– { 0 })))
226200adantr 482 . . . . . . . . . 10 ((๐œ‘ โˆง ๐‘ฅ โˆˆ dom โ—ก(๐น โ†พ (๐น supp 0 ))) โ†’ (๐น supp 0 ) = (โ—ก๐น โ€œ (ran ๐น โˆ– { 0 })))
227225, 226sseqtrrd 4024 . . . . . . . . 9 ((๐œ‘ โˆง ๐‘ฅ โˆˆ dom โ—ก(๐น โ†พ (๐น supp 0 ))) โ†’ (โ—ก๐น โ€œ {๐‘ฅ}) โŠ† (๐น supp 0 ))
228 df-ss 3966 . . . . . . . . 9 ((โ—ก๐น โ€œ {๐‘ฅ}) โŠ† (๐น supp 0 ) โ†” ((โ—ก๐น โ€œ {๐‘ฅ}) โˆฉ (๐น supp 0 )) = (โ—ก๐น โ€œ {๐‘ฅ}))
229227, 228sylib 217 . . . . . . . 8 ((๐œ‘ โˆง ๐‘ฅ โˆˆ dom โ—ก(๐น โ†พ (๐น supp 0 ))) โ†’ ((โ—ก๐น โ€œ {๐‘ฅ}) โˆฉ (๐น supp 0 )) = (โ—ก๐น โ€œ {๐‘ฅ}))
230220, 229eqtr2id 2786 . . . . . . 7 ((๐œ‘ โˆง ๐‘ฅ โˆˆ dom โ—ก(๐น โ†พ (๐น supp 0 ))) โ†’ (โ—ก๐น โ€œ {๐‘ฅ}) = (โ—ก(๐น โ†พ (๐น supp 0 )) โ€œ {๐‘ฅ}))
231230fveq2d 6896 . . . . . 6 ((๐œ‘ โˆง ๐‘ฅ โˆˆ dom โ—ก(๐น โ†พ (๐น supp 0 ))) โ†’ (โ™ฏโ€˜(โ—ก๐น โ€œ {๐‘ฅ})) = (โ™ฏโ€˜(โ—ก(๐น โ†พ (๐น supp 0 )) โ€œ {๐‘ฅ})))
232231oveq1d 7424 . . . . 5 ((๐œ‘ โˆง ๐‘ฅ โˆˆ dom โ—ก(๐น โ†พ (๐น supp 0 ))) โ†’ ((โ™ฏโ€˜(โ—ก๐น โ€œ {๐‘ฅ})) ยท ๐‘ฅ) = ((โ™ฏโ€˜(โ—ก(๐น โ†พ (๐น supp 0 )) โ€œ {๐‘ฅ})) ยท ๐‘ฅ))
233219, 232eqtr4d 2776 . . . 4 ((๐œ‘ โˆง ๐‘ฅ โˆˆ dom โ—ก(๐น โ†พ (๐น supp 0 ))) โ†’ (๐บ ฮฃg (๐‘ฆ โˆˆ (โ—ก(๐น โ†พ (๐น supp 0 )) โ€œ {๐‘ฅ}) โ†ฆ ๐‘ฅ)) = ((โ™ฏโ€˜(โ—ก๐น โ€œ {๐‘ฅ})) ยท ๐‘ฅ))
234209, 233mpteq12dva 5238 . . 3 (๐œ‘ โ†’ (๐‘ฅ โˆˆ dom โ—ก(๐น โ†พ (๐น supp 0 )) โ†ฆ (๐บ ฮฃg (๐‘ฆ โˆˆ (โ—ก(๐น โ†พ (๐น supp 0 )) โ€œ {๐‘ฅ}) โ†ฆ ๐‘ฅ))) = (๐‘ฅ โˆˆ (ran ๐น โˆ– { 0 }) โ†ฆ ((โ™ฏโ€˜(โ—ก๐น โ€œ {๐‘ฅ})) ยท ๐‘ฅ)))
235234oveq2d 7425 . 2 (๐œ‘ โ†’ (๐บ ฮฃg (๐‘ฅ โˆˆ dom โ—ก(๐น โ†พ (๐น supp 0 )) โ†ฆ (๐บ ฮฃg (๐‘ฆ โˆˆ (โ—ก(๐น โ†พ (๐น supp 0 )) โ€œ {๐‘ฅ}) โ†ฆ ๐‘ฅ)))) = (๐บ ฮฃg (๐‘ฅ โˆˆ (ran ๐น โˆ– { 0 }) โ†ฆ ((โ™ฏโ€˜(โ—ก๐น โ€œ {๐‘ฅ})) ยท ๐‘ฅ))))
236179, 197, 2353eqtrd 2777 1 (๐œ‘ โ†’ (๐บ ฮฃg ๐น) = (๐บ ฮฃg (๐‘ฅ โˆˆ (ran ๐น โˆ– { 0 }) โ†ฆ ((โ™ฏโ€˜(โ—ก๐น โ€œ {๐‘ฅ})) ยท ๐‘ฅ))))
Colors of variables: wff setvar class
Syntax hints:   โ†’ wi 4   โ†” wb 205   โˆง wa 397   = wceq 1542  โˆƒwex 1782   โˆˆ wcel 2107  โˆ€wral 3062  โˆƒwrex 3071  โˆƒ!wreu 3375  Vcvv 3475   โˆ– cdif 3946   โˆฉ cin 3948   โŠ† wss 3949  {csn 4629  โŸจcop 4635  โˆช cuni 4909   class class class wbr 5149   โ†ฆ cmpt 5232   ร— cxp 5675  โ—กccnv 5676  dom cdm 5677  ran crn 5678   โ†พ cres 5679   โ€œ cima 5680  Rel wrel 5682  Fun wfun 6538   Fn wfn 6539  โŸถwf 6540  โ€˜cfv 6544  (class class class)co 7409  1st c1st 7973  2nd c2nd 7974   supp csupp 8146  Fincfn 8939   finSupp cfsupp 9361  โ™ฏchash 14290  Basecbs 17144  0gc0g 17385   ฮฃg cgsu 17386  Mndcmnd 18625  .gcmg 18950  CMndccmn 19648
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 2704  ax-rep 5286  ax-sep 5300  ax-nul 5307  ax-pow 5364  ax-pr 5428  ax-un 7725  ax-cnex 11166  ax-resscn 11167  ax-1cn 11168  ax-icn 11169  ax-addcl 11170  ax-addrcl 11171  ax-mulcl 11172  ax-mulrcl 11173  ax-mulcom 11174  ax-addass 11175  ax-mulass 11176  ax-distr 11177  ax-i2m1 11178  ax-1ne0 11179  ax-1rid 11180  ax-rnegex 11181  ax-rrecex 11182  ax-cnre 11183  ax-pre-lttri 11184  ax-pre-lttrn 11185  ax-pre-ltadd 11186  ax-pre-mulgt0 11187
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 2535  df-eu 2564  df-clab 2711  df-cleq 2725  df-clel 2811  df-nfc 2886  df-ne 2942  df-nel 3048  df-ral 3063  df-rex 3072  df-rmo 3377  df-reu 3378  df-rab 3434  df-v 3477  df-sbc 3779  df-csb 3895  df-dif 3952  df-un 3954  df-in 3956  df-ss 3966  df-pss 3968  df-nul 4324  df-if 4530  df-pw 4605  df-sn 4630  df-pr 4632  df-op 4636  df-uni 4910  df-int 4952  df-iun 5000  df-iin 5001  df-br 5150  df-opab 5212  df-mpt 5233  df-tr 5267  df-id 5575  df-eprel 5581  df-po 5589  df-so 5590  df-fr 5632  df-se 5633  df-we 5634  df-xp 5683  df-rel 5684  df-cnv 5685  df-co 5686  df-dm 5687  df-rn 5688  df-res 5689  df-ima 5690  df-pred 6301  df-ord 6368  df-on 6369  df-lim 6370  df-suc 6371  df-iota 6496  df-fun 6546  df-fn 6547  df-f 6548  df-f1 6549  df-fo 6550  df-f1o 6551  df-fv 6552  df-isom 6553  df-riota 7365  df-ov 7412  df-oprab 7413  df-mpo 7414  df-of 7670  df-om 7856  df-1st 7975  df-2nd 7976  df-supp 8147  df-frecs 8266  df-wrecs 8297  df-recs 8371  df-rdg 8410  df-1o 8466  df-er 8703  df-en 8940  df-dom 8941  df-sdom 8942  df-fin 8943  df-fsupp 9362  df-oi 9505  df-card 9934  df-pnf 11250  df-mnf 11251  df-xr 11252  df-ltxr 11253  df-le 11254  df-sub 11446  df-neg 11447  df-nn 12213  df-2 12275  df-n0 12473  df-z 12559  df-uz 12823  df-fz 13485  df-fzo 13628  df-seq 13967  df-hash 14291  df-sets 17097  df-slot 17115  df-ndx 17127  df-base 17145  df-ress 17174  df-plusg 17210  df-0g 17387  df-gsum 17388  df-mre 17530  df-mrc 17531  df-acs 17533  df-mgm 18561  df-sgrp 18610  df-mnd 18626  df-submnd 18672  df-mulg 18951  df-cntz 19181  df-cmn 19650
This theorem is referenced by:  elrspunidl  32546
  Copyright terms: Public domain W3C validator