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

Theorem gsumdixp 20208
Description: Distribute a binary product of sums to a sum of binary products in a ring. (Contributed by Mario Carneiro, 8-Mar-2015.) (Revised by AV, 10-Jul-2019.)
Hypotheses
Ref Expression
gsumdixp.b ๐ต = (Baseโ€˜๐‘…)
gsumdixp.t ยท = (.rโ€˜๐‘…)
gsumdixp.z 0 = (0gโ€˜๐‘…)
gsumdixp.i (๐œ‘ โ†’ ๐ผ โˆˆ ๐‘‰)
gsumdixp.j (๐œ‘ โ†’ ๐ฝ โˆˆ ๐‘Š)
gsumdixp.r (๐œ‘ โ†’ ๐‘… โˆˆ Ring)
gsumdixp.x ((๐œ‘ โˆง ๐‘ฅ โˆˆ ๐ผ) โ†’ ๐‘‹ โˆˆ ๐ต)
gsumdixp.y ((๐œ‘ โˆง ๐‘ฆ โˆˆ ๐ฝ) โ†’ ๐‘Œ โˆˆ ๐ต)
gsumdixp.xf (๐œ‘ โ†’ (๐‘ฅ โˆˆ ๐ผ โ†ฆ ๐‘‹) finSupp 0 )
gsumdixp.yf (๐œ‘ โ†’ (๐‘ฆ โˆˆ ๐ฝ โ†ฆ ๐‘Œ) finSupp 0 )
Assertion
Ref Expression
gsumdixp (๐œ‘ โ†’ ((๐‘… ฮฃg (๐‘ฅ โˆˆ ๐ผ โ†ฆ ๐‘‹)) ยท (๐‘… ฮฃg (๐‘ฆ โˆˆ ๐ฝ โ†ฆ ๐‘Œ))) = (๐‘… ฮฃg (๐‘ฅ โˆˆ ๐ผ, ๐‘ฆ โˆˆ ๐ฝ โ†ฆ (๐‘‹ ยท ๐‘Œ))))
Distinct variable groups:   ๐œ‘,๐‘ฅ,๐‘ฆ   ๐‘ฅ,๐ต,๐‘ฆ   ๐‘ฅ,๐ผ,๐‘ฆ   ๐‘ฅ,๐ฝ,๐‘ฆ   ๐‘ฅ,๐‘…   ๐‘ฅ, ยท ,๐‘ฆ   ๐‘ฆ,๐‘‹   ๐‘ฅ,๐‘Œ
Allowed substitution hints:   ๐‘…(๐‘ฆ)   ๐‘‰(๐‘ฅ,๐‘ฆ)   ๐‘Š(๐‘ฅ,๐‘ฆ)   ๐‘‹(๐‘ฅ)   ๐‘Œ(๐‘ฆ)   0 (๐‘ฅ,๐‘ฆ)

Proof of Theorem gsumdixp
Dummy variables ๐‘– ๐‘— are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 gsumdixp.b . . . 4 ๐ต = (Baseโ€˜๐‘…)
2 gsumdixp.z . . . 4 0 = (0gโ€˜๐‘…)
3 gsumdixp.r . . . . 5 (๐œ‘ โ†’ ๐‘… โˆˆ Ring)
43ringcmnd 20173 . . . 4 (๐œ‘ โ†’ ๐‘… โˆˆ CMnd)
5 gsumdixp.i . . . 4 (๐œ‘ โ†’ ๐ผ โˆˆ ๐‘‰)
6 gsumdixp.j . . . . 5 (๐œ‘ โ†’ ๐ฝ โˆˆ ๐‘Š)
76adantr 480 . . . 4 ((๐œ‘ โˆง ๐‘– โˆˆ ๐ผ) โ†’ ๐ฝ โˆˆ ๐‘Š)
8 gsumdixp.t . . . . 5 ยท = (.rโ€˜๐‘…)
93adantr 480 . . . . 5 ((๐œ‘ โˆง (๐‘– โˆˆ ๐ผ โˆง ๐‘— โˆˆ ๐ฝ)) โ†’ ๐‘… โˆˆ Ring)
10 gsumdixp.x . . . . . . 7 ((๐œ‘ โˆง ๐‘ฅ โˆˆ ๐ผ) โ†’ ๐‘‹ โˆˆ ๐ต)
1110fmpttd 7117 . . . . . 6 (๐œ‘ โ†’ (๐‘ฅ โˆˆ ๐ผ โ†ฆ ๐‘‹):๐ผโŸถ๐ต)
12 simpl 482 . . . . . 6 ((๐‘– โˆˆ ๐ผ โˆง ๐‘— โˆˆ ๐ฝ) โ†’ ๐‘– โˆˆ ๐ผ)
13 ffvelcdm 7084 . . . . . 6 (((๐‘ฅ โˆˆ ๐ผ โ†ฆ ๐‘‹):๐ผโŸถ๐ต โˆง ๐‘– โˆˆ ๐ผ) โ†’ ((๐‘ฅ โˆˆ ๐ผ โ†ฆ ๐‘‹)โ€˜๐‘–) โˆˆ ๐ต)
1411, 12, 13syl2an 595 . . . . 5 ((๐œ‘ โˆง (๐‘– โˆˆ ๐ผ โˆง ๐‘— โˆˆ ๐ฝ)) โ†’ ((๐‘ฅ โˆˆ ๐ผ โ†ฆ ๐‘‹)โ€˜๐‘–) โˆˆ ๐ต)
15 gsumdixp.y . . . . . . 7 ((๐œ‘ โˆง ๐‘ฆ โˆˆ ๐ฝ) โ†’ ๐‘Œ โˆˆ ๐ต)
1615fmpttd 7117 . . . . . 6 (๐œ‘ โ†’ (๐‘ฆ โˆˆ ๐ฝ โ†ฆ ๐‘Œ):๐ฝโŸถ๐ต)
17 simpr 484 . . . . . 6 ((๐‘– โˆˆ ๐ผ โˆง ๐‘— โˆˆ ๐ฝ) โ†’ ๐‘— โˆˆ ๐ฝ)
18 ffvelcdm 7084 . . . . . 6 (((๐‘ฆ โˆˆ ๐ฝ โ†ฆ ๐‘Œ):๐ฝโŸถ๐ต โˆง ๐‘— โˆˆ ๐ฝ) โ†’ ((๐‘ฆ โˆˆ ๐ฝ โ†ฆ ๐‘Œ)โ€˜๐‘—) โˆˆ ๐ต)
1916, 17, 18syl2an 595 . . . . 5 ((๐œ‘ โˆง (๐‘– โˆˆ ๐ผ โˆง ๐‘— โˆˆ ๐ฝ)) โ†’ ((๐‘ฆ โˆˆ ๐ฝ โ†ฆ ๐‘Œ)โ€˜๐‘—) โˆˆ ๐ต)
201, 8, 9, 14, 19ringcld 20152 . . . 4 ((๐œ‘ โˆง (๐‘– โˆˆ ๐ผ โˆง ๐‘— โˆˆ ๐ฝ)) โ†’ (((๐‘ฅ โˆˆ ๐ผ โ†ฆ ๐‘‹)โ€˜๐‘–) ยท ((๐‘ฆ โˆˆ ๐ฝ โ†ฆ ๐‘Œ)โ€˜๐‘—)) โˆˆ ๐ต)
21 gsumdixp.xf . . . . . 6 (๐œ‘ โ†’ (๐‘ฅ โˆˆ ๐ผ โ†ฆ ๐‘‹) finSupp 0 )
2221fsuppimpd 9372 . . . . 5 (๐œ‘ โ†’ ((๐‘ฅ โˆˆ ๐ผ โ†ฆ ๐‘‹) supp 0 ) โˆˆ Fin)
23 gsumdixp.yf . . . . . 6 (๐œ‘ โ†’ (๐‘ฆ โˆˆ ๐ฝ โ†ฆ ๐‘Œ) finSupp 0 )
2423fsuppimpd 9372 . . . . 5 (๐œ‘ โ†’ ((๐‘ฆ โˆˆ ๐ฝ โ†ฆ ๐‘Œ) supp 0 ) โˆˆ Fin)
25 xpfi 9320 . . . . 5 ((((๐‘ฅ โˆˆ ๐ผ โ†ฆ ๐‘‹) supp 0 ) โˆˆ Fin โˆง ((๐‘ฆ โˆˆ ๐ฝ โ†ฆ ๐‘Œ) supp 0 ) โˆˆ Fin) โ†’ (((๐‘ฅ โˆˆ ๐ผ โ†ฆ ๐‘‹) supp 0 ) ร— ((๐‘ฆ โˆˆ ๐ฝ โ†ฆ ๐‘Œ) supp 0 )) โˆˆ Fin)
2622, 24, 25syl2anc 583 . . . 4 (๐œ‘ โ†’ (((๐‘ฅ โˆˆ ๐ผ โ†ฆ ๐‘‹) supp 0 ) ร— ((๐‘ฆ โˆˆ ๐ฝ โ†ฆ ๐‘Œ) supp 0 )) โˆˆ Fin)
27 ianor 979 . . . . . . 7 (ยฌ (๐‘– โˆˆ ((๐‘ฅ โˆˆ ๐ผ โ†ฆ ๐‘‹) supp 0 ) โˆง ๐‘— โˆˆ ((๐‘ฆ โˆˆ ๐ฝ โ†ฆ ๐‘Œ) supp 0 )) โ†” (ยฌ ๐‘– โˆˆ ((๐‘ฅ โˆˆ ๐ผ โ†ฆ ๐‘‹) supp 0 ) โˆจ ยฌ ๐‘— โˆˆ ((๐‘ฆ โˆˆ ๐ฝ โ†ฆ ๐‘Œ) supp 0 )))
28 brxp 5726 . . . . . . 7 (๐‘–(((๐‘ฅ โˆˆ ๐ผ โ†ฆ ๐‘‹) supp 0 ) ร— ((๐‘ฆ โˆˆ ๐ฝ โ†ฆ ๐‘Œ) supp 0 ))๐‘— โ†” (๐‘– โˆˆ ((๐‘ฅ โˆˆ ๐ผ โ†ฆ ๐‘‹) supp 0 ) โˆง ๐‘— โˆˆ ((๐‘ฆ โˆˆ ๐ฝ โ†ฆ ๐‘Œ) supp 0 )))
2927, 28xchnxbir 332 . . . . . 6 (ยฌ ๐‘–(((๐‘ฅ โˆˆ ๐ผ โ†ฆ ๐‘‹) supp 0 ) ร— ((๐‘ฆ โˆˆ ๐ฝ โ†ฆ ๐‘Œ) supp 0 ))๐‘— โ†” (ยฌ ๐‘– โˆˆ ((๐‘ฅ โˆˆ ๐ผ โ†ฆ ๐‘‹) supp 0 ) โˆจ ยฌ ๐‘— โˆˆ ((๐‘ฆ โˆˆ ๐ฝ โ†ฆ ๐‘Œ) supp 0 )))
30 simprl 768 . . . . . . . . . . 11 ((๐œ‘ โˆง (๐‘– โˆˆ ๐ผ โˆง ๐‘— โˆˆ ๐ฝ)) โ†’ ๐‘– โˆˆ ๐ผ)
31 eldif 3959 . . . . . . . . . . . 12 (๐‘– โˆˆ (๐ผ โˆ– ((๐‘ฅ โˆˆ ๐ผ โ†ฆ ๐‘‹) supp 0 )) โ†” (๐‘– โˆˆ ๐ผ โˆง ยฌ ๐‘– โˆˆ ((๐‘ฅ โˆˆ ๐ผ โ†ฆ ๐‘‹) supp 0 )))
3231biimpri 227 . . . . . . . . . . 11 ((๐‘– โˆˆ ๐ผ โˆง ยฌ ๐‘– โˆˆ ((๐‘ฅ โˆˆ ๐ผ โ†ฆ ๐‘‹) supp 0 )) โ†’ ๐‘– โˆˆ (๐ผ โˆ– ((๐‘ฅ โˆˆ ๐ผ โ†ฆ ๐‘‹) supp 0 )))
3330, 32sylan 579 . . . . . . . . . 10 (((๐œ‘ โˆง (๐‘– โˆˆ ๐ผ โˆง ๐‘— โˆˆ ๐ฝ)) โˆง ยฌ ๐‘– โˆˆ ((๐‘ฅ โˆˆ ๐ผ โ†ฆ ๐‘‹) supp 0 )) โ†’ ๐‘– โˆˆ (๐ผ โˆ– ((๐‘ฅ โˆˆ ๐ผ โ†ฆ ๐‘‹) supp 0 )))
3411adantr 480 . . . . . . . . . . 11 ((๐œ‘ โˆง (๐‘– โˆˆ ๐ผ โˆง ๐‘— โˆˆ ๐ฝ)) โ†’ (๐‘ฅ โˆˆ ๐ผ โ†ฆ ๐‘‹):๐ผโŸถ๐ต)
35 ssidd 4006 . . . . . . . . . . 11 ((๐œ‘ โˆง (๐‘– โˆˆ ๐ผ โˆง ๐‘— โˆˆ ๐ฝ)) โ†’ ((๐‘ฅ โˆˆ ๐ผ โ†ฆ ๐‘‹) supp 0 ) โŠ† ((๐‘ฅ โˆˆ ๐ผ โ†ฆ ๐‘‹) supp 0 ))
365adantr 480 . . . . . . . . . . 11 ((๐œ‘ โˆง (๐‘– โˆˆ ๐ผ โˆง ๐‘— โˆˆ ๐ฝ)) โ†’ ๐ผ โˆˆ ๐‘‰)
372fvexi 6906 . . . . . . . . . . . 12 0 โˆˆ V
3837a1i 11 . . . . . . . . . . 11 ((๐œ‘ โˆง (๐‘– โˆˆ ๐ผ โˆง ๐‘— โˆˆ ๐ฝ)) โ†’ 0 โˆˆ V)
3934, 35, 36, 38suppssr 8184 . . . . . . . . . 10 (((๐œ‘ โˆง (๐‘– โˆˆ ๐ผ โˆง ๐‘— โˆˆ ๐ฝ)) โˆง ๐‘– โˆˆ (๐ผ โˆ– ((๐‘ฅ โˆˆ ๐ผ โ†ฆ ๐‘‹) supp 0 ))) โ†’ ((๐‘ฅ โˆˆ ๐ผ โ†ฆ ๐‘‹)โ€˜๐‘–) = 0 )
4033, 39syldan 590 . . . . . . . . 9 (((๐œ‘ โˆง (๐‘– โˆˆ ๐ผ โˆง ๐‘— โˆˆ ๐ฝ)) โˆง ยฌ ๐‘– โˆˆ ((๐‘ฅ โˆˆ ๐ผ โ†ฆ ๐‘‹) supp 0 )) โ†’ ((๐‘ฅ โˆˆ ๐ผ โ†ฆ ๐‘‹)โ€˜๐‘–) = 0 )
4140oveq1d 7427 . . . . . . . 8 (((๐œ‘ โˆง (๐‘– โˆˆ ๐ผ โˆง ๐‘— โˆˆ ๐ฝ)) โˆง ยฌ ๐‘– โˆˆ ((๐‘ฅ โˆˆ ๐ผ โ†ฆ ๐‘‹) supp 0 )) โ†’ (((๐‘ฅ โˆˆ ๐ผ โ†ฆ ๐‘‹)โ€˜๐‘–) ยท ((๐‘ฆ โˆˆ ๐ฝ โ†ฆ ๐‘Œ)โ€˜๐‘—)) = ( 0 ยท ((๐‘ฆ โˆˆ ๐ฝ โ†ฆ ๐‘Œ)โ€˜๐‘—)))
421, 8, 2ringlz 20182 . . . . . . . . . 10 ((๐‘… โˆˆ Ring โˆง ((๐‘ฆ โˆˆ ๐ฝ โ†ฆ ๐‘Œ)โ€˜๐‘—) โˆˆ ๐ต) โ†’ ( 0 ยท ((๐‘ฆ โˆˆ ๐ฝ โ†ฆ ๐‘Œ)โ€˜๐‘—)) = 0 )
439, 19, 42syl2anc 583 . . . . . . . . 9 ((๐œ‘ โˆง (๐‘– โˆˆ ๐ผ โˆง ๐‘— โˆˆ ๐ฝ)) โ†’ ( 0 ยท ((๐‘ฆ โˆˆ ๐ฝ โ†ฆ ๐‘Œ)โ€˜๐‘—)) = 0 )
4443adantr 480 . . . . . . . 8 (((๐œ‘ โˆง (๐‘– โˆˆ ๐ผ โˆง ๐‘— โˆˆ ๐ฝ)) โˆง ยฌ ๐‘– โˆˆ ((๐‘ฅ โˆˆ ๐ผ โ†ฆ ๐‘‹) supp 0 )) โ†’ ( 0 ยท ((๐‘ฆ โˆˆ ๐ฝ โ†ฆ ๐‘Œ)โ€˜๐‘—)) = 0 )
4541, 44eqtrd 2771 . . . . . . 7 (((๐œ‘ โˆง (๐‘– โˆˆ ๐ผ โˆง ๐‘— โˆˆ ๐ฝ)) โˆง ยฌ ๐‘– โˆˆ ((๐‘ฅ โˆˆ ๐ผ โ†ฆ ๐‘‹) supp 0 )) โ†’ (((๐‘ฅ โˆˆ ๐ผ โ†ฆ ๐‘‹)โ€˜๐‘–) ยท ((๐‘ฆ โˆˆ ๐ฝ โ†ฆ ๐‘Œ)โ€˜๐‘—)) = 0 )
46 simprr 770 . . . . . . . . . . 11 ((๐œ‘ โˆง (๐‘– โˆˆ ๐ผ โˆง ๐‘— โˆˆ ๐ฝ)) โ†’ ๐‘— โˆˆ ๐ฝ)
47 eldif 3959 . . . . . . . . . . . 12 (๐‘— โˆˆ (๐ฝ โˆ– ((๐‘ฆ โˆˆ ๐ฝ โ†ฆ ๐‘Œ) supp 0 )) โ†” (๐‘— โˆˆ ๐ฝ โˆง ยฌ ๐‘— โˆˆ ((๐‘ฆ โˆˆ ๐ฝ โ†ฆ ๐‘Œ) supp 0 )))
4847biimpri 227 . . . . . . . . . . 11 ((๐‘— โˆˆ ๐ฝ โˆง ยฌ ๐‘— โˆˆ ((๐‘ฆ โˆˆ ๐ฝ โ†ฆ ๐‘Œ) supp 0 )) โ†’ ๐‘— โˆˆ (๐ฝ โˆ– ((๐‘ฆ โˆˆ ๐ฝ โ†ฆ ๐‘Œ) supp 0 )))
4946, 48sylan 579 . . . . . . . . . 10 (((๐œ‘ โˆง (๐‘– โˆˆ ๐ผ โˆง ๐‘— โˆˆ ๐ฝ)) โˆง ยฌ ๐‘— โˆˆ ((๐‘ฆ โˆˆ ๐ฝ โ†ฆ ๐‘Œ) supp 0 )) โ†’ ๐‘— โˆˆ (๐ฝ โˆ– ((๐‘ฆ โˆˆ ๐ฝ โ†ฆ ๐‘Œ) supp 0 )))
5016adantr 480 . . . . . . . . . . 11 ((๐œ‘ โˆง (๐‘– โˆˆ ๐ผ โˆง ๐‘— โˆˆ ๐ฝ)) โ†’ (๐‘ฆ โˆˆ ๐ฝ โ†ฆ ๐‘Œ):๐ฝโŸถ๐ต)
51 ssidd 4006 . . . . . . . . . . 11 ((๐œ‘ โˆง (๐‘– โˆˆ ๐ผ โˆง ๐‘— โˆˆ ๐ฝ)) โ†’ ((๐‘ฆ โˆˆ ๐ฝ โ†ฆ ๐‘Œ) supp 0 ) โŠ† ((๐‘ฆ โˆˆ ๐ฝ โ†ฆ ๐‘Œ) supp 0 ))
526adantr 480 . . . . . . . . . . 11 ((๐œ‘ โˆง (๐‘– โˆˆ ๐ผ โˆง ๐‘— โˆˆ ๐ฝ)) โ†’ ๐ฝ โˆˆ ๐‘Š)
5350, 51, 52, 38suppssr 8184 . . . . . . . . . 10 (((๐œ‘ โˆง (๐‘– โˆˆ ๐ผ โˆง ๐‘— โˆˆ ๐ฝ)) โˆง ๐‘— โˆˆ (๐ฝ โˆ– ((๐‘ฆ โˆˆ ๐ฝ โ†ฆ ๐‘Œ) supp 0 ))) โ†’ ((๐‘ฆ โˆˆ ๐ฝ โ†ฆ ๐‘Œ)โ€˜๐‘—) = 0 )
5449, 53syldan 590 . . . . . . . . 9 (((๐œ‘ โˆง (๐‘– โˆˆ ๐ผ โˆง ๐‘— โˆˆ ๐ฝ)) โˆง ยฌ ๐‘— โˆˆ ((๐‘ฆ โˆˆ ๐ฝ โ†ฆ ๐‘Œ) supp 0 )) โ†’ ((๐‘ฆ โˆˆ ๐ฝ โ†ฆ ๐‘Œ)โ€˜๐‘—) = 0 )
5554oveq2d 7428 . . . . . . . 8 (((๐œ‘ โˆง (๐‘– โˆˆ ๐ผ โˆง ๐‘— โˆˆ ๐ฝ)) โˆง ยฌ ๐‘— โˆˆ ((๐‘ฆ โˆˆ ๐ฝ โ†ฆ ๐‘Œ) supp 0 )) โ†’ (((๐‘ฅ โˆˆ ๐ผ โ†ฆ ๐‘‹)โ€˜๐‘–) ยท ((๐‘ฆ โˆˆ ๐ฝ โ†ฆ ๐‘Œ)โ€˜๐‘—)) = (((๐‘ฅ โˆˆ ๐ผ โ†ฆ ๐‘‹)โ€˜๐‘–) ยท 0 ))
561, 8, 2ringrz 20183 . . . . . . . . . 10 ((๐‘… โˆˆ Ring โˆง ((๐‘ฅ โˆˆ ๐ผ โ†ฆ ๐‘‹)โ€˜๐‘–) โˆˆ ๐ต) โ†’ (((๐‘ฅ โˆˆ ๐ผ โ†ฆ ๐‘‹)โ€˜๐‘–) ยท 0 ) = 0 )
579, 14, 56syl2anc 583 . . . . . . . . 9 ((๐œ‘ โˆง (๐‘– โˆˆ ๐ผ โˆง ๐‘— โˆˆ ๐ฝ)) โ†’ (((๐‘ฅ โˆˆ ๐ผ โ†ฆ ๐‘‹)โ€˜๐‘–) ยท 0 ) = 0 )
5857adantr 480 . . . . . . . 8 (((๐œ‘ โˆง (๐‘– โˆˆ ๐ผ โˆง ๐‘— โˆˆ ๐ฝ)) โˆง ยฌ ๐‘— โˆˆ ((๐‘ฆ โˆˆ ๐ฝ โ†ฆ ๐‘Œ) supp 0 )) โ†’ (((๐‘ฅ โˆˆ ๐ผ โ†ฆ ๐‘‹)โ€˜๐‘–) ยท 0 ) = 0 )
5955, 58eqtrd 2771 . . . . . . 7 (((๐œ‘ โˆง (๐‘– โˆˆ ๐ผ โˆง ๐‘— โˆˆ ๐ฝ)) โˆง ยฌ ๐‘— โˆˆ ((๐‘ฆ โˆˆ ๐ฝ โ†ฆ ๐‘Œ) supp 0 )) โ†’ (((๐‘ฅ โˆˆ ๐ผ โ†ฆ ๐‘‹)โ€˜๐‘–) ยท ((๐‘ฆ โˆˆ ๐ฝ โ†ฆ ๐‘Œ)โ€˜๐‘—)) = 0 )
6045, 59jaodan 955 . . . . . 6 (((๐œ‘ โˆง (๐‘– โˆˆ ๐ผ โˆง ๐‘— โˆˆ ๐ฝ)) โˆง (ยฌ ๐‘– โˆˆ ((๐‘ฅ โˆˆ ๐ผ โ†ฆ ๐‘‹) supp 0 ) โˆจ ยฌ ๐‘— โˆˆ ((๐‘ฆ โˆˆ ๐ฝ โ†ฆ ๐‘Œ) supp 0 ))) โ†’ (((๐‘ฅ โˆˆ ๐ผ โ†ฆ ๐‘‹)โ€˜๐‘–) ยท ((๐‘ฆ โˆˆ ๐ฝ โ†ฆ ๐‘Œ)โ€˜๐‘—)) = 0 )
6129, 60sylan2b 593 . . . . 5 (((๐œ‘ โˆง (๐‘– โˆˆ ๐ผ โˆง ๐‘— โˆˆ ๐ฝ)) โˆง ยฌ ๐‘–(((๐‘ฅ โˆˆ ๐ผ โ†ฆ ๐‘‹) supp 0 ) ร— ((๐‘ฆ โˆˆ ๐ฝ โ†ฆ ๐‘Œ) supp 0 ))๐‘—) โ†’ (((๐‘ฅ โˆˆ ๐ผ โ†ฆ ๐‘‹)โ€˜๐‘–) ยท ((๐‘ฆ โˆˆ ๐ฝ โ†ฆ ๐‘Œ)โ€˜๐‘—)) = 0 )
6261anasss 466 . . . 4 ((๐œ‘ โˆง ((๐‘– โˆˆ ๐ผ โˆง ๐‘— โˆˆ ๐ฝ) โˆง ยฌ ๐‘–(((๐‘ฅ โˆˆ ๐ผ โ†ฆ ๐‘‹) supp 0 ) ร— ((๐‘ฆ โˆˆ ๐ฝ โ†ฆ ๐‘Œ) supp 0 ))๐‘—)) โ†’ (((๐‘ฅ โˆˆ ๐ผ โ†ฆ ๐‘‹)โ€˜๐‘–) ยท ((๐‘ฆ โˆˆ ๐ฝ โ†ฆ ๐‘Œ)โ€˜๐‘—)) = 0 )
631, 2, 4, 5, 7, 20, 26, 62gsum2d2 19884 . . 3 (๐œ‘ โ†’ (๐‘… ฮฃg (๐‘– โˆˆ ๐ผ, ๐‘— โˆˆ ๐ฝ โ†ฆ (((๐‘ฅ โˆˆ ๐ผ โ†ฆ ๐‘‹)โ€˜๐‘–) ยท ((๐‘ฆ โˆˆ ๐ฝ โ†ฆ ๐‘Œ)โ€˜๐‘—)))) = (๐‘… ฮฃg (๐‘– โˆˆ ๐ผ โ†ฆ (๐‘… ฮฃg (๐‘— โˆˆ ๐ฝ โ†ฆ (((๐‘ฅ โˆˆ ๐ผ โ†ฆ ๐‘‹)โ€˜๐‘–) ยท ((๐‘ฆ โˆˆ ๐ฝ โ†ฆ ๐‘Œ)โ€˜๐‘—)))))))
64 nffvmpt1 6903 . . . . . . 7 โ„ฒ๐‘ฅ((๐‘ฅ โˆˆ ๐ผ โ†ฆ ๐‘‹)โ€˜๐‘–)
65 nfcv 2902 . . . . . . 7 โ„ฒ๐‘ฅ ยท
66 nfcv 2902 . . . . . . 7 โ„ฒ๐‘ฅ((๐‘ฆ โˆˆ ๐ฝ โ†ฆ ๐‘Œ)โ€˜๐‘—)
6764, 65, 66nfov 7442 . . . . . 6 โ„ฒ๐‘ฅ(((๐‘ฅ โˆˆ ๐ผ โ†ฆ ๐‘‹)โ€˜๐‘–) ยท ((๐‘ฆ โˆˆ ๐ฝ โ†ฆ ๐‘Œ)โ€˜๐‘—))
68 nfcv 2902 . . . . . . 7 โ„ฒ๐‘ฆ((๐‘ฅ โˆˆ ๐ผ โ†ฆ ๐‘‹)โ€˜๐‘–)
69 nfcv 2902 . . . . . . 7 โ„ฒ๐‘ฆ ยท
70 nffvmpt1 6903 . . . . . . 7 โ„ฒ๐‘ฆ((๐‘ฆ โˆˆ ๐ฝ โ†ฆ ๐‘Œ)โ€˜๐‘—)
7168, 69, 70nfov 7442 . . . . . 6 โ„ฒ๐‘ฆ(((๐‘ฅ โˆˆ ๐ผ โ†ฆ ๐‘‹)โ€˜๐‘–) ยท ((๐‘ฆ โˆˆ ๐ฝ โ†ฆ ๐‘Œ)โ€˜๐‘—))
72 nfcv 2902 . . . . . 6 โ„ฒ๐‘–(((๐‘ฅ โˆˆ ๐ผ โ†ฆ ๐‘‹)โ€˜๐‘ฅ) ยท ((๐‘ฆ โˆˆ ๐ฝ โ†ฆ ๐‘Œ)โ€˜๐‘ฆ))
73 nfcv 2902 . . . . . 6 โ„ฒ๐‘—(((๐‘ฅ โˆˆ ๐ผ โ†ฆ ๐‘‹)โ€˜๐‘ฅ) ยท ((๐‘ฆ โˆˆ ๐ฝ โ†ฆ ๐‘Œ)โ€˜๐‘ฆ))
74 fveq2 6892 . . . . . . 7 (๐‘– = ๐‘ฅ โ†’ ((๐‘ฅ โˆˆ ๐ผ โ†ฆ ๐‘‹)โ€˜๐‘–) = ((๐‘ฅ โˆˆ ๐ผ โ†ฆ ๐‘‹)โ€˜๐‘ฅ))
75 fveq2 6892 . . . . . . 7 (๐‘— = ๐‘ฆ โ†’ ((๐‘ฆ โˆˆ ๐ฝ โ†ฆ ๐‘Œ)โ€˜๐‘—) = ((๐‘ฆ โˆˆ ๐ฝ โ†ฆ ๐‘Œ)โ€˜๐‘ฆ))
7674, 75oveqan12d 7431 . . . . . 6 ((๐‘– = ๐‘ฅ โˆง ๐‘— = ๐‘ฆ) โ†’ (((๐‘ฅ โˆˆ ๐ผ โ†ฆ ๐‘‹)โ€˜๐‘–) ยท ((๐‘ฆ โˆˆ ๐ฝ โ†ฆ ๐‘Œ)โ€˜๐‘—)) = (((๐‘ฅ โˆˆ ๐ผ โ†ฆ ๐‘‹)โ€˜๐‘ฅ) ยท ((๐‘ฆ โˆˆ ๐ฝ โ†ฆ ๐‘Œ)โ€˜๐‘ฆ)))
7767, 71, 72, 73, 76cbvmpo 7506 . . . . 5 (๐‘– โˆˆ ๐ผ, ๐‘— โˆˆ ๐ฝ โ†ฆ (((๐‘ฅ โˆˆ ๐ผ โ†ฆ ๐‘‹)โ€˜๐‘–) ยท ((๐‘ฆ โˆˆ ๐ฝ โ†ฆ ๐‘Œ)โ€˜๐‘—))) = (๐‘ฅ โˆˆ ๐ผ, ๐‘ฆ โˆˆ ๐ฝ โ†ฆ (((๐‘ฅ โˆˆ ๐ผ โ†ฆ ๐‘‹)โ€˜๐‘ฅ) ยท ((๐‘ฆ โˆˆ ๐ฝ โ†ฆ ๐‘Œ)โ€˜๐‘ฆ)))
78 simp2 1136 . . . . . . . 8 ((๐œ‘ โˆง ๐‘ฅ โˆˆ ๐ผ โˆง ๐‘ฆ โˆˆ ๐ฝ) โ†’ ๐‘ฅ โˆˆ ๐ผ)
79103adant3 1131 . . . . . . . 8 ((๐œ‘ โˆง ๐‘ฅ โˆˆ ๐ผ โˆง ๐‘ฆ โˆˆ ๐ฝ) โ†’ ๐‘‹ โˆˆ ๐ต)
80 eqid 2731 . . . . . . . . 9 (๐‘ฅ โˆˆ ๐ผ โ†ฆ ๐‘‹) = (๐‘ฅ โˆˆ ๐ผ โ†ฆ ๐‘‹)
8180fvmpt2 7010 . . . . . . . 8 ((๐‘ฅ โˆˆ ๐ผ โˆง ๐‘‹ โˆˆ ๐ต) โ†’ ((๐‘ฅ โˆˆ ๐ผ โ†ฆ ๐‘‹)โ€˜๐‘ฅ) = ๐‘‹)
8278, 79, 81syl2anc 583 . . . . . . 7 ((๐œ‘ โˆง ๐‘ฅ โˆˆ ๐ผ โˆง ๐‘ฆ โˆˆ ๐ฝ) โ†’ ((๐‘ฅ โˆˆ ๐ผ โ†ฆ ๐‘‹)โ€˜๐‘ฅ) = ๐‘‹)
83 simp3 1137 . . . . . . . 8 ((๐œ‘ โˆง ๐‘ฅ โˆˆ ๐ผ โˆง ๐‘ฆ โˆˆ ๐ฝ) โ†’ ๐‘ฆ โˆˆ ๐ฝ)
84 eqid 2731 . . . . . . . . 9 (๐‘ฆ โˆˆ ๐ฝ โ†ฆ ๐‘Œ) = (๐‘ฆ โˆˆ ๐ฝ โ†ฆ ๐‘Œ)
8584fvmpt2 7010 . . . . . . . 8 ((๐‘ฆ โˆˆ ๐ฝ โˆง ๐‘Œ โˆˆ ๐ต) โ†’ ((๐‘ฆ โˆˆ ๐ฝ โ†ฆ ๐‘Œ)โ€˜๐‘ฆ) = ๐‘Œ)
8683, 15, 853imp3i2an 1344 . . . . . . 7 ((๐œ‘ โˆง ๐‘ฅ โˆˆ ๐ผ โˆง ๐‘ฆ โˆˆ ๐ฝ) โ†’ ((๐‘ฆ โˆˆ ๐ฝ โ†ฆ ๐‘Œ)โ€˜๐‘ฆ) = ๐‘Œ)
8782, 86oveq12d 7430 . . . . . 6 ((๐œ‘ โˆง ๐‘ฅ โˆˆ ๐ผ โˆง ๐‘ฆ โˆˆ ๐ฝ) โ†’ (((๐‘ฅ โˆˆ ๐ผ โ†ฆ ๐‘‹)โ€˜๐‘ฅ) ยท ((๐‘ฆ โˆˆ ๐ฝ โ†ฆ ๐‘Œ)โ€˜๐‘ฆ)) = (๐‘‹ ยท ๐‘Œ))
8887mpoeq3dva 7489 . . . . 5 (๐œ‘ โ†’ (๐‘ฅ โˆˆ ๐ผ, ๐‘ฆ โˆˆ ๐ฝ โ†ฆ (((๐‘ฅ โˆˆ ๐ผ โ†ฆ ๐‘‹)โ€˜๐‘ฅ) ยท ((๐‘ฆ โˆˆ ๐ฝ โ†ฆ ๐‘Œ)โ€˜๐‘ฆ))) = (๐‘ฅ โˆˆ ๐ผ, ๐‘ฆ โˆˆ ๐ฝ โ†ฆ (๐‘‹ ยท ๐‘Œ)))
8977, 88eqtrid 2783 . . . 4 (๐œ‘ โ†’ (๐‘– โˆˆ ๐ผ, ๐‘— โˆˆ ๐ฝ โ†ฆ (((๐‘ฅ โˆˆ ๐ผ โ†ฆ ๐‘‹)โ€˜๐‘–) ยท ((๐‘ฆ โˆˆ ๐ฝ โ†ฆ ๐‘Œ)โ€˜๐‘—))) = (๐‘ฅ โˆˆ ๐ผ, ๐‘ฆ โˆˆ ๐ฝ โ†ฆ (๐‘‹ ยท ๐‘Œ)))
9089oveq2d 7428 . . 3 (๐œ‘ โ†’ (๐‘… ฮฃg (๐‘– โˆˆ ๐ผ, ๐‘— โˆˆ ๐ฝ โ†ฆ (((๐‘ฅ โˆˆ ๐ผ โ†ฆ ๐‘‹)โ€˜๐‘–) ยท ((๐‘ฆ โˆˆ ๐ฝ โ†ฆ ๐‘Œ)โ€˜๐‘—)))) = (๐‘… ฮฃg (๐‘ฅ โˆˆ ๐ผ, ๐‘ฆ โˆˆ ๐ฝ โ†ฆ (๐‘‹ ยท ๐‘Œ))))
91 nfcv 2902 . . . . . . 7 โ„ฒ๐‘ฅ๐‘…
92 nfcv 2902 . . . . . . 7 โ„ฒ๐‘ฅ ฮฃg
93 nfcv 2902 . . . . . . . 8 โ„ฒ๐‘ฅ๐ฝ
9493, 67nfmpt 5256 . . . . . . 7 โ„ฒ๐‘ฅ(๐‘— โˆˆ ๐ฝ โ†ฆ (((๐‘ฅ โˆˆ ๐ผ โ†ฆ ๐‘‹)โ€˜๐‘–) ยท ((๐‘ฆ โˆˆ ๐ฝ โ†ฆ ๐‘Œ)โ€˜๐‘—)))
9591, 92, 94nfov 7442 . . . . . 6 โ„ฒ๐‘ฅ(๐‘… ฮฃg (๐‘— โˆˆ ๐ฝ โ†ฆ (((๐‘ฅ โˆˆ ๐ผ โ†ฆ ๐‘‹)โ€˜๐‘–) ยท ((๐‘ฆ โˆˆ ๐ฝ โ†ฆ ๐‘Œ)โ€˜๐‘—))))
96 nfcv 2902 . . . . . 6 โ„ฒ๐‘–(๐‘… ฮฃg (๐‘ฆ โˆˆ ๐ฝ โ†ฆ (((๐‘ฅ โˆˆ ๐ผ โ†ฆ ๐‘‹)โ€˜๐‘ฅ) ยท ((๐‘ฆ โˆˆ ๐ฝ โ†ฆ ๐‘Œ)โ€˜๐‘ฆ))))
9774oveq1d 7427 . . . . . . . . 9 (๐‘– = ๐‘ฅ โ†’ (((๐‘ฅ โˆˆ ๐ผ โ†ฆ ๐‘‹)โ€˜๐‘–) ยท ((๐‘ฆ โˆˆ ๐ฝ โ†ฆ ๐‘Œ)โ€˜๐‘—)) = (((๐‘ฅ โˆˆ ๐ผ โ†ฆ ๐‘‹)โ€˜๐‘ฅ) ยท ((๐‘ฆ โˆˆ ๐ฝ โ†ฆ ๐‘Œ)โ€˜๐‘—)))
9897mpteq2dv 5251 . . . . . . . 8 (๐‘– = ๐‘ฅ โ†’ (๐‘— โˆˆ ๐ฝ โ†ฆ (((๐‘ฅ โˆˆ ๐ผ โ†ฆ ๐‘‹)โ€˜๐‘–) ยท ((๐‘ฆ โˆˆ ๐ฝ โ†ฆ ๐‘Œ)โ€˜๐‘—))) = (๐‘— โˆˆ ๐ฝ โ†ฆ (((๐‘ฅ โˆˆ ๐ผ โ†ฆ ๐‘‹)โ€˜๐‘ฅ) ยท ((๐‘ฆ โˆˆ ๐ฝ โ†ฆ ๐‘Œ)โ€˜๐‘—))))
99 nfcv 2902 . . . . . . . . . 10 โ„ฒ๐‘ฆ((๐‘ฅ โˆˆ ๐ผ โ†ฆ ๐‘‹)โ€˜๐‘ฅ)
10099, 69, 70nfov 7442 . . . . . . . . 9 โ„ฒ๐‘ฆ(((๐‘ฅ โˆˆ ๐ผ โ†ฆ ๐‘‹)โ€˜๐‘ฅ) ยท ((๐‘ฆ โˆˆ ๐ฝ โ†ฆ ๐‘Œ)โ€˜๐‘—))
10175oveq2d 7428 . . . . . . . . 9 (๐‘— = ๐‘ฆ โ†’ (((๐‘ฅ โˆˆ ๐ผ โ†ฆ ๐‘‹)โ€˜๐‘ฅ) ยท ((๐‘ฆ โˆˆ ๐ฝ โ†ฆ ๐‘Œ)โ€˜๐‘—)) = (((๐‘ฅ โˆˆ ๐ผ โ†ฆ ๐‘‹)โ€˜๐‘ฅ) ยท ((๐‘ฆ โˆˆ ๐ฝ โ†ฆ ๐‘Œ)โ€˜๐‘ฆ)))
102100, 73, 101cbvmpt 5260 . . . . . . . 8 (๐‘— โˆˆ ๐ฝ โ†ฆ (((๐‘ฅ โˆˆ ๐ผ โ†ฆ ๐‘‹)โ€˜๐‘ฅ) ยท ((๐‘ฆ โˆˆ ๐ฝ โ†ฆ ๐‘Œ)โ€˜๐‘—))) = (๐‘ฆ โˆˆ ๐ฝ โ†ฆ (((๐‘ฅ โˆˆ ๐ผ โ†ฆ ๐‘‹)โ€˜๐‘ฅ) ยท ((๐‘ฆ โˆˆ ๐ฝ โ†ฆ ๐‘Œ)โ€˜๐‘ฆ)))
10398, 102eqtrdi 2787 . . . . . . 7 (๐‘– = ๐‘ฅ โ†’ (๐‘— โˆˆ ๐ฝ โ†ฆ (((๐‘ฅ โˆˆ ๐ผ โ†ฆ ๐‘‹)โ€˜๐‘–) ยท ((๐‘ฆ โˆˆ ๐ฝ โ†ฆ ๐‘Œ)โ€˜๐‘—))) = (๐‘ฆ โˆˆ ๐ฝ โ†ฆ (((๐‘ฅ โˆˆ ๐ผ โ†ฆ ๐‘‹)โ€˜๐‘ฅ) ยท ((๐‘ฆ โˆˆ ๐ฝ โ†ฆ ๐‘Œ)โ€˜๐‘ฆ))))
104103oveq2d 7428 . . . . . 6 (๐‘– = ๐‘ฅ โ†’ (๐‘… ฮฃg (๐‘— โˆˆ ๐ฝ โ†ฆ (((๐‘ฅ โˆˆ ๐ผ โ†ฆ ๐‘‹)โ€˜๐‘–) ยท ((๐‘ฆ โˆˆ ๐ฝ โ†ฆ ๐‘Œ)โ€˜๐‘—)))) = (๐‘… ฮฃg (๐‘ฆ โˆˆ ๐ฝ โ†ฆ (((๐‘ฅ โˆˆ ๐ผ โ†ฆ ๐‘‹)โ€˜๐‘ฅ) ยท ((๐‘ฆ โˆˆ ๐ฝ โ†ฆ ๐‘Œ)โ€˜๐‘ฆ)))))
10595, 96, 104cbvmpt 5260 . . . . 5 (๐‘– โˆˆ ๐ผ โ†ฆ (๐‘… ฮฃg (๐‘— โˆˆ ๐ฝ โ†ฆ (((๐‘ฅ โˆˆ ๐ผ โ†ฆ ๐‘‹)โ€˜๐‘–) ยท ((๐‘ฆ โˆˆ ๐ฝ โ†ฆ ๐‘Œ)โ€˜๐‘—))))) = (๐‘ฅ โˆˆ ๐ผ โ†ฆ (๐‘… ฮฃg (๐‘ฆ โˆˆ ๐ฝ โ†ฆ (((๐‘ฅ โˆˆ ๐ผ โ†ฆ ๐‘‹)โ€˜๐‘ฅ) ยท ((๐‘ฆ โˆˆ ๐ฝ โ†ฆ ๐‘Œ)โ€˜๐‘ฆ)))))
106873expa 1117 . . . . . . . 8 (((๐œ‘ โˆง ๐‘ฅ โˆˆ ๐ผ) โˆง ๐‘ฆ โˆˆ ๐ฝ) โ†’ (((๐‘ฅ โˆˆ ๐ผ โ†ฆ ๐‘‹)โ€˜๐‘ฅ) ยท ((๐‘ฆ โˆˆ ๐ฝ โ†ฆ ๐‘Œ)โ€˜๐‘ฆ)) = (๐‘‹ ยท ๐‘Œ))
107106mpteq2dva 5249 . . . . . . 7 ((๐œ‘ โˆง ๐‘ฅ โˆˆ ๐ผ) โ†’ (๐‘ฆ โˆˆ ๐ฝ โ†ฆ (((๐‘ฅ โˆˆ ๐ผ โ†ฆ ๐‘‹)โ€˜๐‘ฅ) ยท ((๐‘ฆ โˆˆ ๐ฝ โ†ฆ ๐‘Œ)โ€˜๐‘ฆ))) = (๐‘ฆ โˆˆ ๐ฝ โ†ฆ (๐‘‹ ยท ๐‘Œ)))
108107oveq2d 7428 . . . . . 6 ((๐œ‘ โˆง ๐‘ฅ โˆˆ ๐ผ) โ†’ (๐‘… ฮฃg (๐‘ฆ โˆˆ ๐ฝ โ†ฆ (((๐‘ฅ โˆˆ ๐ผ โ†ฆ ๐‘‹)โ€˜๐‘ฅ) ยท ((๐‘ฆ โˆˆ ๐ฝ โ†ฆ ๐‘Œ)โ€˜๐‘ฆ)))) = (๐‘… ฮฃg (๐‘ฆ โˆˆ ๐ฝ โ†ฆ (๐‘‹ ยท ๐‘Œ))))
109108mpteq2dva 5249 . . . . 5 (๐œ‘ โ†’ (๐‘ฅ โˆˆ ๐ผ โ†ฆ (๐‘… ฮฃg (๐‘ฆ โˆˆ ๐ฝ โ†ฆ (((๐‘ฅ โˆˆ ๐ผ โ†ฆ ๐‘‹)โ€˜๐‘ฅ) ยท ((๐‘ฆ โˆˆ ๐ฝ โ†ฆ ๐‘Œ)โ€˜๐‘ฆ))))) = (๐‘ฅ โˆˆ ๐ผ โ†ฆ (๐‘… ฮฃg (๐‘ฆ โˆˆ ๐ฝ โ†ฆ (๐‘‹ ยท ๐‘Œ)))))
110105, 109eqtrid 2783 . . . 4 (๐œ‘ โ†’ (๐‘– โˆˆ ๐ผ โ†ฆ (๐‘… ฮฃg (๐‘— โˆˆ ๐ฝ โ†ฆ (((๐‘ฅ โˆˆ ๐ผ โ†ฆ ๐‘‹)โ€˜๐‘–) ยท ((๐‘ฆ โˆˆ ๐ฝ โ†ฆ ๐‘Œ)โ€˜๐‘—))))) = (๐‘ฅ โˆˆ ๐ผ โ†ฆ (๐‘… ฮฃg (๐‘ฆ โˆˆ ๐ฝ โ†ฆ (๐‘‹ ยท ๐‘Œ)))))
111110oveq2d 7428 . . 3 (๐œ‘ โ†’ (๐‘… ฮฃg (๐‘– โˆˆ ๐ผ โ†ฆ (๐‘… ฮฃg (๐‘— โˆˆ ๐ฝ โ†ฆ (((๐‘ฅ โˆˆ ๐ผ โ†ฆ ๐‘‹)โ€˜๐‘–) ยท ((๐‘ฆ โˆˆ ๐ฝ โ†ฆ ๐‘Œ)โ€˜๐‘—)))))) = (๐‘… ฮฃg (๐‘ฅ โˆˆ ๐ผ โ†ฆ (๐‘… ฮฃg (๐‘ฆ โˆˆ ๐ฝ โ†ฆ (๐‘‹ ยท ๐‘Œ))))))
11263, 90, 1113eqtr3d 2779 . 2 (๐œ‘ โ†’ (๐‘… ฮฃg (๐‘ฅ โˆˆ ๐ผ, ๐‘ฆ โˆˆ ๐ฝ โ†ฆ (๐‘‹ ยท ๐‘Œ))) = (๐‘… ฮฃg (๐‘ฅ โˆˆ ๐ผ โ†ฆ (๐‘… ฮฃg (๐‘ฆ โˆˆ ๐ฝ โ†ฆ (๐‘‹ ยท ๐‘Œ))))))
1133adantr 480 . . . . 5 ((๐œ‘ โˆง ๐‘ฅ โˆˆ ๐ผ) โ†’ ๐‘… โˆˆ Ring)
1146adantr 480 . . . . 5 ((๐œ‘ โˆง ๐‘ฅ โˆˆ ๐ผ) โ†’ ๐ฝ โˆˆ ๐‘Š)
11515adantlr 712 . . . . 5 (((๐œ‘ โˆง ๐‘ฅ โˆˆ ๐ผ) โˆง ๐‘ฆ โˆˆ ๐ฝ) โ†’ ๐‘Œ โˆˆ ๐ต)
11623adantr 480 . . . . 5 ((๐œ‘ โˆง ๐‘ฅ โˆˆ ๐ผ) โ†’ (๐‘ฆ โˆˆ ๐ฝ โ†ฆ ๐‘Œ) finSupp 0 )
1171, 2, 8, 113, 114, 10, 115, 116gsummulc2 20206 . . . 4 ((๐œ‘ โˆง ๐‘ฅ โˆˆ ๐ผ) โ†’ (๐‘… ฮฃg (๐‘ฆ โˆˆ ๐ฝ โ†ฆ (๐‘‹ ยท ๐‘Œ))) = (๐‘‹ ยท (๐‘… ฮฃg (๐‘ฆ โˆˆ ๐ฝ โ†ฆ ๐‘Œ))))
118117mpteq2dva 5249 . . 3 (๐œ‘ โ†’ (๐‘ฅ โˆˆ ๐ผ โ†ฆ (๐‘… ฮฃg (๐‘ฆ โˆˆ ๐ฝ โ†ฆ (๐‘‹ ยท ๐‘Œ)))) = (๐‘ฅ โˆˆ ๐ผ โ†ฆ (๐‘‹ ยท (๐‘… ฮฃg (๐‘ฆ โˆˆ ๐ฝ โ†ฆ ๐‘Œ)))))
119118oveq2d 7428 . 2 (๐œ‘ โ†’ (๐‘… ฮฃg (๐‘ฅ โˆˆ ๐ผ โ†ฆ (๐‘… ฮฃg (๐‘ฆ โˆˆ ๐ฝ โ†ฆ (๐‘‹ ยท ๐‘Œ))))) = (๐‘… ฮฃg (๐‘ฅ โˆˆ ๐ผ โ†ฆ (๐‘‹ ยท (๐‘… ฮฃg (๐‘ฆ โˆˆ ๐ฝ โ†ฆ ๐‘Œ))))))
1201, 2, 4, 6, 16, 23gsumcl 19825 . . 3 (๐œ‘ โ†’ (๐‘… ฮฃg (๐‘ฆ โˆˆ ๐ฝ โ†ฆ ๐‘Œ)) โˆˆ ๐ต)
1211, 2, 8, 3, 5, 120, 10, 21gsummulc1 20205 . 2 (๐œ‘ โ†’ (๐‘… ฮฃg (๐‘ฅ โˆˆ ๐ผ โ†ฆ (๐‘‹ ยท (๐‘… ฮฃg (๐‘ฆ โˆˆ ๐ฝ โ†ฆ ๐‘Œ))))) = ((๐‘… ฮฃg (๐‘ฅ โˆˆ ๐ผ โ†ฆ ๐‘‹)) ยท (๐‘… ฮฃg (๐‘ฆ โˆˆ ๐ฝ โ†ฆ ๐‘Œ))))
122112, 119, 1213eqtrrd 2776 1 (๐œ‘ โ†’ ((๐‘… ฮฃg (๐‘ฅ โˆˆ ๐ผ โ†ฆ ๐‘‹)) ยท (๐‘… ฮฃg (๐‘ฆ โˆˆ ๐ฝ โ†ฆ ๐‘Œ))) = (๐‘… ฮฃg (๐‘ฅ โˆˆ ๐ผ, ๐‘ฆ โˆˆ ๐ฝ โ†ฆ (๐‘‹ ยท ๐‘Œ))))
Colors of variables: wff setvar class
Syntax hints:  ยฌ wn 3   โ†’ wi 4   โˆง wa 395   โˆจ wo 844   โˆง w3a 1086   = wceq 1540   โˆˆ wcel 2105  Vcvv 3473   โˆ– cdif 3946   class class class wbr 5149   โ†ฆ cmpt 5232   ร— cxp 5675  โŸถwf 6540  โ€˜cfv 6544  (class class class)co 7412   โˆˆ cmpo 7414   supp csupp 8149  Fincfn 8942   finSupp cfsupp 9364  Basecbs 17149  .rcmulr 17203  0gc0g 17390   ฮฃg cgsu 17391  Ringcrg 20128
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1912  ax-6 1970  ax-7 2010  ax-8 2107  ax-9 2115  ax-10 2136  ax-11 2153  ax-12 2170  ax-ext 2702  ax-rep 5286  ax-sep 5300  ax-nul 5307  ax-pow 5364  ax-pr 5428  ax-un 7728  ax-cnex 11169  ax-resscn 11170  ax-1cn 11171  ax-icn 11172  ax-addcl 11173  ax-addrcl 11174  ax-mulcl 11175  ax-mulrcl 11176  ax-mulcom 11177  ax-addass 11178  ax-mulass 11179  ax-distr 11180  ax-i2m1 11181  ax-1ne0 11182  ax-1rid 11183  ax-rnegex 11184  ax-rrecex 11185  ax-cnre 11186  ax-pre-lttri 11187  ax-pre-lttrn 11188  ax-pre-ltadd 11189  ax-pre-mulgt0 11190
This theorem depends on definitions:  df-bi 206  df-an 396  df-or 845  df-3or 1087  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1781  df-nf 1785  df-sb 2067  df-mo 2533  df-eu 2562  df-clab 2709  df-cleq 2723  df-clel 2809  df-nfc 2884  df-ne 2940  df-nel 3046  df-ral 3061  df-rex 3070  df-rmo 3375  df-reu 3376  df-rab 3432  df-v 3475  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 7368  df-ov 7415  df-oprab 7416  df-mpo 7417  df-of 7673  df-om 7859  df-1st 7978  df-2nd 7979  df-supp 8150  df-frecs 8269  df-wrecs 8300  df-recs 8374  df-rdg 8413  df-1o 8469  df-er 8706  df-map 8825  df-en 8943  df-dom 8944  df-sdom 8945  df-fin 8946  df-fsupp 9365  df-oi 9508  df-card 9937  df-pnf 11255  df-mnf 11256  df-xr 11257  df-ltxr 11258  df-le 11259  df-sub 11451  df-neg 11452  df-nn 12218  df-2 12280  df-n0 12478  df-z 12564  df-uz 12828  df-fz 13490  df-fzo 13633  df-seq 13972  df-hash 14296  df-sets 17102  df-slot 17120  df-ndx 17132  df-base 17150  df-ress 17179  df-plusg 17215  df-0g 17392  df-gsum 17393  df-mre 17535  df-mrc 17536  df-acs 17538  df-mgm 18566  df-sgrp 18645  df-mnd 18661  df-mhm 18706  df-submnd 18707  df-grp 18859  df-minusg 18860  df-mulg 18988  df-ghm 19129  df-cntz 19223  df-cmn 19692  df-abl 19693  df-mgp 20030  df-rng 20048  df-ur 20077  df-ring 20130
This theorem is referenced by:  evlslem2  21862
  Copyright terms: Public domain W3C validator