Metamath Proof Explorer


Theorem prdsgsum

Description: Finite commutative sums in a product structure are taken componentwise. (Contributed by Stefan O'Rear, 1-Feb-2015) (Revised by Mario Carneiro, 3-Jul-2015) (Revised by AV, 9-Jun-2019)

Ref Expression
Hypotheses prdsgsum.y Y=S𝑠xIR
prdsgsum.b B=BaseR
prdsgsum.z 0˙=0Y
prdsgsum.i φIV
prdsgsum.j φJW
prdsgsum.s φSX
prdsgsum.r φxIRCMnd
prdsgsum.f φxIyJUB
prdsgsum.w φfinSupp0˙yJxIU
Assertion prdsgsum φYyJxIU=xIRyJU

Proof

Step Hyp Ref Expression
1 prdsgsum.y Y=S𝑠xIR
2 prdsgsum.b B=BaseR
3 prdsgsum.z 0˙=0Y
4 prdsgsum.i φIV
5 prdsgsum.j φJW
6 prdsgsum.s φSX
7 prdsgsum.r φxIRCMnd
8 prdsgsum.f φxIyJUB
9 prdsgsum.w φfinSupp0˙yJxIU
10 eqid BaseY=BaseY
11 7 fmpttd φxIR:ICMnd
12 11 ffnd φxIRFnI
13 1 4 6 11 prdscmnd φYCMnd
14 8 anassrs φxIyJUB
15 14 an32s φyJxIUB
16 15 ralrimiva φyJxIUB
17 7 ralrimiva φxIRCMnd
18 1 10 6 4 17 2 prdsbasmpt2 φxIUBaseYxIUB
19 18 adantr φyJxIUBaseYxIUB
20 16 19 mpbird φyJxIUBaseY
21 20 fmpttd φyJxIU:JBaseY
22 10 3 13 5 21 9 gsumcl φYyJxIUBaseY
23 1 10 6 4 12 22 prdsbasfn φYyJxIUFnI
24 nfcv _xY
25 nfcv _xΣ𝑔
26 nfcv _xJ
27 nfmpt1 _xxIU
28 26 27 nfmpt _xyJxIU
29 24 25 28 nfov _xYyJxIU
30 29 dffn5f YyJxIUFnIYyJxIU=xIYyJxIUx
31 23 30 sylib φYyJxIU=xIYyJxIUx
32 simpr φxIxI
33 eqid xIU=xIU
34 33 fvmpt2 xIUBxIUx=U
35 32 14 34 syl2an2r φxIyJxIUx=U
36 35 mpteq2dva φxIyJxIUx=yJU
37 36 oveq2d φxIRyJxIUx=RyJU
38 13 adantr φxIYCMnd
39 cmnmnd RCMndRMnd
40 7 39 syl φxIRMnd
41 5 adantr φxIJW
42 4 adantr φxIIV
43 6 adantr φxISX
44 40 fmpttd φxIR:IMnd
45 44 adantr φxIxIR:IMnd
46 1 10 42 43 45 32 prdspjmhm φxIaBaseYaxYMndHomxIRx
47 eqid xIR=xIR
48 47 fvmpt2 xIRCMndxIRx=R
49 32 7 48 syl2anc φxIxIRx=R
50 49 oveq2d φxIYMndHomxIRx=YMndHomR
51 46 50 eleqtrd φxIaBaseYaxYMndHomR
52 20 adantlr φxIyJxIUBaseY
53 9 adantr φxIfinSupp0˙yJxIU
54 fveq1 a=xIUax=xIUx
55 fveq1 a=YyJxIUax=YyJxIUx
56 10 3 38 40 41 51 52 53 54 55 gsummhm2 φxIRyJxIUx=YyJxIUx
57 37 56 eqtr3d φxIRyJU=YyJxIUx
58 57 mpteq2dva φxIRyJU=xIYyJxIUx
59 31 58 eqtr4d φYyJxIU=xIRyJU