Metamath Proof Explorer


Theorem gsumdixp

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)

Ref Expression
Hypotheses gsumdixp.b B = Base R
gsumdixp.t · ˙ = R
gsumdixp.z 0 ˙ = 0 R
gsumdixp.i φ I V
gsumdixp.j φ J W
gsumdixp.r φ R Ring
gsumdixp.x φ x I X B
gsumdixp.y φ y J Y B
gsumdixp.xf φ finSupp 0 ˙ x I X
gsumdixp.yf φ finSupp 0 ˙ y J Y
Assertion gsumdixp φ R x I X · ˙ R y J Y = R x I , y J X · ˙ Y

Proof

Step Hyp Ref Expression
1 gsumdixp.b B = Base R
2 gsumdixp.t · ˙ = R
3 gsumdixp.z 0 ˙ = 0 R
4 gsumdixp.i φ I V
5 gsumdixp.j φ J W
6 gsumdixp.r φ R Ring
7 gsumdixp.x φ x I X B
8 gsumdixp.y φ y J Y B
9 gsumdixp.xf φ finSupp 0 ˙ x I X
10 gsumdixp.yf φ finSupp 0 ˙ y J Y
11 6 ringcmnd φ R CMnd
12 5 adantr φ i I J W
13 6 adantr φ i I j J R Ring
14 7 fmpttd φ x I X : I B
15 simpl i I j J i I
16 ffvelcdm x I X : I B i I x I X i B
17 14 15 16 syl2an φ i I j J x I X i B
18 8 fmpttd φ y J Y : J B
19 simpr i I j J j J
20 ffvelcdm y J Y : J B j J y J Y j B
21 18 19 20 syl2an φ i I j J y J Y j B
22 1 2 13 17 21 ringcld φ i I j J x I X i · ˙ y J Y j B
23 9 fsuppimpd φ x I X supp 0 ˙ Fin
24 10 fsuppimpd φ y J Y supp 0 ˙ Fin
25 xpfi x I X supp 0 ˙ Fin y J Y supp 0 ˙ Fin supp 0 ˙ x I X × supp 0 ˙ y J Y Fin
26 23 24 25 syl2anc φ supp 0 ˙ x I X × supp 0 ˙ y J Y Fin
27 ianor ¬ i supp 0 ˙ x I X j supp 0 ˙ y J Y ¬ i supp 0 ˙ x I X ¬ j supp 0 ˙ y J Y
28 brxp i supp 0 ˙ x I X × supp 0 ˙ y J Y j i supp 0 ˙ x I X j supp 0 ˙ y J Y
29 27 28 xchnxbir ¬ i supp 0 ˙ x I X × supp 0 ˙ y J Y j ¬ i supp 0 ˙ x I X ¬ j supp 0 ˙ y J Y
30 simprl φ i I j J i I
31 eldif i I supp 0 ˙ x I X i I ¬ i supp 0 ˙ x I X
32 31 biimpri i I ¬ i supp 0 ˙ x I X i I supp 0 ˙ x I X
33 30 32 sylan φ i I j J ¬ i supp 0 ˙ x I X i I supp 0 ˙ x I X
34 14 adantr φ i I j J x I X : I B
35 ssidd φ i I j J x I X supp 0 ˙ x I X supp 0 ˙
36 4 adantr φ i I j J I V
37 3 fvexi 0 ˙ V
38 37 a1i φ i I j J 0 ˙ V
39 34 35 36 38 suppssr φ i I j J i I supp 0 ˙ x I X x I X i = 0 ˙
40 33 39 syldan φ i I j J ¬ i supp 0 ˙ x I X x I X i = 0 ˙
41 40 oveq1d φ i I j J ¬ i supp 0 ˙ x I X x I X i · ˙ y J Y j = 0 ˙ · ˙ y J Y j
42 1 2 3 ringlz R Ring y J Y j B 0 ˙ · ˙ y J Y j = 0 ˙
43 13 21 42 syl2anc φ i I j J 0 ˙ · ˙ y J Y j = 0 ˙
44 43 adantr φ i I j J ¬ i supp 0 ˙ x I X 0 ˙ · ˙ y J Y j = 0 ˙
45 41 44 eqtrd φ i I j J ¬ i supp 0 ˙ x I X x I X i · ˙ y J Y j = 0 ˙
46 simprr φ i I j J j J
47 eldif j J supp 0 ˙ y J Y j J ¬ j supp 0 ˙ y J Y
48 47 biimpri j J ¬ j supp 0 ˙ y J Y j J supp 0 ˙ y J Y
49 46 48 sylan φ i I j J ¬ j supp 0 ˙ y J Y j J supp 0 ˙ y J Y
50 18 adantr φ i I j J y J Y : J B
51 ssidd φ i I j J y J Y supp 0 ˙ y J Y supp 0 ˙
52 5 adantr φ i I j J J W
53 50 51 52 38 suppssr φ i I j J j J supp 0 ˙ y J Y y J Y j = 0 ˙
54 49 53 syldan φ i I j J ¬ j supp 0 ˙ y J Y y J Y j = 0 ˙
55 54 oveq2d φ i I j J ¬ j supp 0 ˙ y J Y x I X i · ˙ y J Y j = x I X i · ˙ 0 ˙
56 1 2 3 ringrz R Ring x I X i B x I X i · ˙ 0 ˙ = 0 ˙
57 13 17 56 syl2anc φ i I j J x I X i · ˙ 0 ˙ = 0 ˙
58 57 adantr φ i I j J ¬ j supp 0 ˙ y J Y x I X i · ˙ 0 ˙ = 0 ˙
59 55 58 eqtrd φ i I j J ¬ j supp 0 ˙ y J Y x I X i · ˙ y J Y j = 0 ˙
60 45 59 jaodan φ i I j J ¬ i supp 0 ˙ x I X ¬ j supp 0 ˙ y J Y x I X i · ˙ y J Y j = 0 ˙
61 29 60 sylan2b φ i I j J ¬ i supp 0 ˙ x I X × supp 0 ˙ y J Y j x I X i · ˙ y J Y j = 0 ˙
62 61 anasss φ i I j J ¬ i supp 0 ˙ x I X × supp 0 ˙ y J Y j x I X i · ˙ y J Y j = 0 ˙
63 1 3 11 4 12 22 26 62 gsum2d2 φ R i I , j J x I X i · ˙ y J Y j = R i I R j J x I X i · ˙ y J Y j
64 nffvmpt1 _ x x I X i
65 nfcv _ x · ˙
66 nfcv _ x y J Y j
67 64 65 66 nfov _ x x I X i · ˙ y J Y j
68 nfcv _ y x I X i
69 nfcv _ y · ˙
70 nffvmpt1 _ y y J Y j
71 68 69 70 nfov _ y x I X i · ˙ y J Y j
72 nfcv _ i x I X x · ˙ y J Y y
73 nfcv _ j x I X x · ˙ y J Y y
74 fveq2 i = x x I X i = x I X x
75 fveq2 j = y y J Y j = y J Y y
76 74 75 oveqan12d i = x j = y x I X i · ˙ y J Y j = x I X x · ˙ y J Y y
77 67 71 72 73 76 cbvmpo i I , j J x I X i · ˙ y J Y j = x I , y J x I X x · ˙ y J Y y
78 simp2 φ x I y J x I
79 7 3adant3 φ x I y J X B
80 eqid x I X = x I X
81 80 fvmpt2 x I X B x I X x = X
82 78 79 81 syl2anc φ x I y J x I X x = X
83 simp3 φ x I y J y J
84 eqid y J Y = y J Y
85 84 fvmpt2 y J Y B y J Y y = Y
86 83 8 85 3imp3i2an φ x I y J y J Y y = Y
87 82 86 oveq12d φ x I y J x I X x · ˙ y J Y y = X · ˙ Y
88 87 mpoeq3dva φ x I , y J x I X x · ˙ y J Y y = x I , y J X · ˙ Y
89 77 88 eqtrid φ i I , j J x I X i · ˙ y J Y j = x I , y J X · ˙ Y
90 89 oveq2d φ R i I , j J x I X i · ˙ y J Y j = R x I , y J X · ˙ Y
91 nfcv _ x R
92 nfcv _ x Σ𝑔
93 nfcv _ x J
94 93 67 nfmpt _ x j J x I X i · ˙ y J Y j
95 91 92 94 nfov _ x R j J x I X i · ˙ y J Y j
96 nfcv _ i R y J x I X x · ˙ y J Y y
97 74 oveq1d i = x x I X i · ˙ y J Y j = x I X x · ˙ y J Y j
98 97 mpteq2dv i = x j J x I X i · ˙ y J Y j = j J x I X x · ˙ y J Y j
99 nfcv _ y x I X x
100 99 69 70 nfov _ y x I X x · ˙ y J Y j
101 75 oveq2d j = y x I X x · ˙ y J Y j = x I X x · ˙ y J Y y
102 100 73 101 cbvmpt j J x I X x · ˙ y J Y j = y J x I X x · ˙ y J Y y
103 98 102 eqtrdi i = x j J x I X i · ˙ y J Y j = y J x I X x · ˙ y J Y y
104 103 oveq2d i = x R j J x I X i · ˙ y J Y j = R y J x I X x · ˙ y J Y y
105 95 96 104 cbvmpt i I R j J x I X i · ˙ y J Y j = x I R y J x I X x · ˙ y J Y y
106 87 3expa φ x I y J x I X x · ˙ y J Y y = X · ˙ Y
107 106 mpteq2dva φ x I y J x I X x · ˙ y J Y y = y J X · ˙ Y
108 107 oveq2d φ x I R y J x I X x · ˙ y J Y y = R y J X · ˙ Y
109 108 mpteq2dva φ x I R y J x I X x · ˙ y J Y y = x I R y J X · ˙ Y
110 105 109 eqtrid φ i I R j J x I X i · ˙ y J Y j = x I R y J X · ˙ Y
111 110 oveq2d φ R i I R j J x I X i · ˙ y J Y j = R x I R y J X · ˙ Y
112 63 90 111 3eqtr3d φ R x I , y J X · ˙ Y = R x I R y J X · ˙ Y
113 6 adantr φ x I R Ring
114 5 adantr φ x I J W
115 8 adantlr φ x I y J Y B
116 10 adantr φ x I finSupp 0 ˙ y J Y
117 1 3 2 113 114 7 115 116 gsummulc2 φ x I R y J X · ˙ Y = X · ˙ R y J Y
118 117 mpteq2dva φ x I R y J X · ˙ Y = x I X · ˙ R y J Y
119 118 oveq2d φ R x I R y J X · ˙ Y = R x I X · ˙ R y J Y
120 1 3 11 5 18 10 gsumcl φ R y J Y B
121 1 3 2 6 4 120 7 9 gsummulc1 φ R x I X · ˙ R y J Y = R x I X · ˙ R y J Y
122 112 119 121 3eqtrrd φ R x I X · ˙ R y J Y = R x I , y J X · ˙ Y