Metamath Proof Explorer

Theorem dmatmul

Description: The product of two diagonal matrices. (Contributed by AV, 19-Aug-2019) (Revised by AV, 18-Dec-2019)

Ref Expression
Hypotheses dmatid.a 
|- A = ( N Mat R )
dmatid.b 
|- B = ( Base ` A )
dmatid.0 
|- .0. = ( 0g ` R )
dmatid.d 
|- D = ( N DMat R )
Assertion dmatmul 
|- ( ( ( N e. Fin /\ R e. Ring ) /\ ( X e. D /\ Y e. D ) ) -> ( X ( .r ` A ) Y ) = ( x e. N , y e. N |-> if ( x = y , ( ( x X y ) ( .r ` R ) ( x Y y ) ) , .0. ) ) )

Proof

Step Hyp Ref Expression
1 dmatid.a 
 |-  A = ( N Mat R )
2 dmatid.b 
 |-  B = ( Base ` A )
3 dmatid.0 
 |-  .0. = ( 0g ` R )
4 dmatid.d 
 |-  D = ( N DMat R )
5 eqid 
 |-  ( R maMul <. N , N , N >. ) = ( R maMul <. N , N , N >. )
6 1 5 matmulr 
 |-  ( ( N e. Fin /\ R e. Ring ) -> ( R maMul <. N , N , N >. ) = ( .r ` A ) )
7 6 adantr 
 |-  ( ( ( N e. Fin /\ R e. Ring ) /\ ( X e. D /\ Y e. D ) ) -> ( R maMul <. N , N , N >. ) = ( .r ` A ) )
8 7 eqcomd 
 |-  ( ( ( N e. Fin /\ R e. Ring ) /\ ( X e. D /\ Y e. D ) ) -> ( .r ` A ) = ( R maMul <. N , N , N >. ) )
9 8 oveqd 
 |-  ( ( ( N e. Fin /\ R e. Ring ) /\ ( X e. D /\ Y e. D ) ) -> ( X ( .r ` A ) Y ) = ( X ( R maMul <. N , N , N >. ) Y ) )
10 eqid 
 |-  ( Base ` R ) = ( Base ` R )
11 eqid 
 |-  ( .r ` R ) = ( .r ` R )
12 simplr 
 |-  ( ( ( N e. Fin /\ R e. Ring ) /\ ( X e. D /\ Y e. D ) ) -> R e. Ring )
13 simpll 
 |-  ( ( ( N e. Fin /\ R e. Ring ) /\ ( X e. D /\ Y e. D ) ) -> N e. Fin )
14 1 2 3 4 dmatmat 
 |-  ( ( N e. Fin /\ R e. Ring ) -> ( X e. D -> X e. B ) )
15 14 imp 
 |-  ( ( ( N e. Fin /\ R e. Ring ) /\ X e. D ) -> X e. B )
16 1 10 2 matbas2i 
 |-  ( X e. B -> X e. ( ( Base ` R ) ^m ( N X. N ) ) )
17 15 16 syl 
 |-  ( ( ( N e. Fin /\ R e. Ring ) /\ X e. D ) -> X e. ( ( Base ` R ) ^m ( N X. N ) ) )
18 17 adantrr 
 |-  ( ( ( N e. Fin /\ R e. Ring ) /\ ( X e. D /\ Y e. D ) ) -> X e. ( ( Base ` R ) ^m ( N X. N ) ) )
19 1 2 3 4 dmatmat 
 |-  ( ( N e. Fin /\ R e. Ring ) -> ( Y e. D -> Y e. B ) )
20 19 imp 
 |-  ( ( ( N e. Fin /\ R e. Ring ) /\ Y e. D ) -> Y e. B )
21 1 10 2 matbas2i 
 |-  ( Y e. B -> Y e. ( ( Base ` R ) ^m ( N X. N ) ) )
22 20 21 syl 
 |-  ( ( ( N e. Fin /\ R e. Ring ) /\ Y e. D ) -> Y e. ( ( Base ` R ) ^m ( N X. N ) ) )
23 22 adantrl 
 |-  ( ( ( N e. Fin /\ R e. Ring ) /\ ( X e. D /\ Y e. D ) ) -> Y e. ( ( Base ` R ) ^m ( N X. N ) ) )
24 5 10 11 12 13 13 13 18 23 mamuval 
 |-  ( ( ( N e. Fin /\ R e. Ring ) /\ ( X e. D /\ Y e. D ) ) -> ( X ( R maMul <. N , N , N >. ) Y ) = ( x e. N , y e. N |-> ( R gsum ( k e. N |-> ( ( x X k ) ( .r ` R ) ( k Y y ) ) ) ) ) )
25 eqid 
 |-  ( +g ` R ) = ( +g ` R )
26 ringcmn 
 |-  ( R e. Ring -> R e. CMnd )
27 26 ad2antlr 
 |-  ( ( ( N e. Fin /\ R e. Ring ) /\ ( X e. D /\ Y e. D ) ) -> R e. CMnd )
28 27 3ad2ant1 
 |-  ( ( ( ( N e. Fin /\ R e. Ring ) /\ ( X e. D /\ Y e. D ) ) /\ x e. N /\ y e. N ) -> R e. CMnd )
29 28 adantl 
 |-  ( ( x = y /\ ( ( ( N e. Fin /\ R e. Ring ) /\ ( X e. D /\ Y e. D ) ) /\ x e. N /\ y e. N ) ) -> R e. CMnd )
30 13 3ad2ant1 
 |-  ( ( ( ( N e. Fin /\ R e. Ring ) /\ ( X e. D /\ Y e. D ) ) /\ x e. N /\ y e. N ) -> N e. Fin )
31 30 adantl 
 |-  ( ( x = y /\ ( ( ( N e. Fin /\ R e. Ring ) /\ ( X e. D /\ Y e. D ) ) /\ x e. N /\ y e. N ) ) -> N e. Fin )
32 eqid 
 |-  ( k e. N |-> ( ( x X k ) ( .r ` R ) ( k Y y ) ) ) = ( k e. N |-> ( ( x X k ) ( .r ` R ) ( k Y y ) ) )
33 ovexd 
 |-  ( ( ( x = y /\ ( ( ( N e. Fin /\ R e. Ring ) /\ ( X e. D /\ Y e. D ) ) /\ x e. N /\ y e. N ) ) /\ k e. N ) -> ( ( x X k ) ( .r ` R ) ( k Y y ) ) e. _V )
34 fvexd 
 |-  ( ( x = y /\ ( ( ( N e. Fin /\ R e. Ring ) /\ ( X e. D /\ Y e. D ) ) /\ x e. N /\ y e. N ) ) -> ( 0g ` R ) e. _V )
35 32 31 33 34 fsuppmptdm 
 |-  ( ( x = y /\ ( ( ( N e. Fin /\ R e. Ring ) /\ ( X e. D /\ Y e. D ) ) /\ x e. N /\ y e. N ) ) -> ( k e. N |-> ( ( x X k ) ( .r ` R ) ( k Y y ) ) ) finSupp ( 0g ` R ) )
36 12 3ad2ant1 
 |-  ( ( ( ( N e. Fin /\ R e. Ring ) /\ ( X e. D /\ Y e. D ) ) /\ x e. N /\ y e. N ) -> R e. Ring )
37 36 ad2antlr 
 |-  ( ( ( x = y /\ ( ( ( N e. Fin /\ R e. Ring ) /\ ( X e. D /\ Y e. D ) ) /\ x e. N /\ y e. N ) ) /\ k e. N ) -> R e. Ring )
38 simp2 
 |-  ( ( ( ( N e. Fin /\ R e. Ring ) /\ ( X e. D /\ Y e. D ) ) /\ x e. N /\ y e. N ) -> x e. N )
39 38 ad2antlr 
 |-  ( ( ( x = y /\ ( ( ( N e. Fin /\ R e. Ring ) /\ ( X e. D /\ Y e. D ) ) /\ x e. N /\ y e. N ) ) /\ k e. N ) -> x e. N )
40 simpr 
 |-  ( ( ( x = y /\ ( ( ( N e. Fin /\ R e. Ring ) /\ ( X e. D /\ Y e. D ) ) /\ x e. N /\ y e. N ) ) /\ k e. N ) -> k e. N )
41 eqid 
 |-  ( Base ` A ) = ( Base ` A )
42 1 41 3 4 dmatmat 
 |-  ( ( N e. Fin /\ R e. Ring ) -> ( X e. D -> X e. ( Base ` A ) ) )
43 42 imp 
 |-  ( ( ( N e. Fin /\ R e. Ring ) /\ X e. D ) -> X e. ( Base ` A ) )
44 43 adantrr 
 |-  ( ( ( N e. Fin /\ R e. Ring ) /\ ( X e. D /\ Y e. D ) ) -> X e. ( Base ` A ) )
45 44 3ad2ant1 
 |-  ( ( ( ( N e. Fin /\ R e. Ring ) /\ ( X e. D /\ Y e. D ) ) /\ x e. N /\ y e. N ) -> X e. ( Base ` A ) )
46 45 ad2antlr 
 |-  ( ( ( x = y /\ ( ( ( N e. Fin /\ R e. Ring ) /\ ( X e. D /\ Y e. D ) ) /\ x e. N /\ y e. N ) ) /\ k e. N ) -> X e. ( Base ` A ) )
47 1 10 matecl 
 |-  ( ( x e. N /\ k e. N /\ X e. ( Base ` A ) ) -> ( x X k ) e. ( Base ` R ) )
48 39 40 46 47 syl3anc 
 |-  ( ( ( x = y /\ ( ( ( N e. Fin /\ R e. Ring ) /\ ( X e. D /\ Y e. D ) ) /\ x e. N /\ y e. N ) ) /\ k e. N ) -> ( x X k ) e. ( Base ` R ) )
49 simplr3 
 |-  ( ( ( x = y /\ ( ( ( N e. Fin /\ R e. Ring ) /\ ( X e. D /\ Y e. D ) ) /\ x e. N /\ y e. N ) ) /\ k e. N ) -> y e. N )
50 1 41 3 4 dmatmat 
 |-  ( ( N e. Fin /\ R e. Ring ) -> ( Y e. D -> Y e. ( Base ` A ) ) )
51 50 imp 
 |-  ( ( ( N e. Fin /\ R e. Ring ) /\ Y e. D ) -> Y e. ( Base ` A ) )
52 51 adantrl 
 |-  ( ( ( N e. Fin /\ R e. Ring ) /\ ( X e. D /\ Y e. D ) ) -> Y e. ( Base ` A ) )
53 52 3ad2ant1 
 |-  ( ( ( ( N e. Fin /\ R e. Ring ) /\ ( X e. D /\ Y e. D ) ) /\ x e. N /\ y e. N ) -> Y e. ( Base ` A ) )
54 53 ad2antlr 
 |-  ( ( ( x = y /\ ( ( ( N e. Fin /\ R e. Ring ) /\ ( X e. D /\ Y e. D ) ) /\ x e. N /\ y e. N ) ) /\ k e. N ) -> Y e. ( Base ` A ) )
55 1 10 matecl 
 |-  ( ( k e. N /\ y e. N /\ Y e. ( Base ` A ) ) -> ( k Y y ) e. ( Base ` R ) )
56 40 49 54 55 syl3anc 
 |-  ( ( ( x = y /\ ( ( ( N e. Fin /\ R e. Ring ) /\ ( X e. D /\ Y e. D ) ) /\ x e. N /\ y e. N ) ) /\ k e. N ) -> ( k Y y ) e. ( Base ` R ) )
57 10 11 ringcl 
 |-  ( ( R e. Ring /\ ( x X k ) e. ( Base ` R ) /\ ( k Y y ) e. ( Base ` R ) ) -> ( ( x X k ) ( .r ` R ) ( k Y y ) ) e. ( Base ` R ) )
58 37 48 56 57 syl3anc 
 |-  ( ( ( x = y /\ ( ( ( N e. Fin /\ R e. Ring ) /\ ( X e. D /\ Y e. D ) ) /\ x e. N /\ y e. N ) ) /\ k e. N ) -> ( ( x X k ) ( .r ` R ) ( k Y y ) ) e. ( Base ` R ) )
59 38 adantl 
 |-  ( ( x = y /\ ( ( ( N e. Fin /\ R e. Ring ) /\ ( X e. D /\ Y e. D ) ) /\ x e. N /\ y e. N ) ) -> x e. N )
60 simp3 
 |-  ( ( ( ( N e. Fin /\ R e. Ring ) /\ ( X e. D /\ Y e. D ) ) /\ x e. N /\ y e. N ) -> y e. N )
61 15 adantrr 
 |-  ( ( ( N e. Fin /\ R e. Ring ) /\ ( X e. D /\ Y e. D ) ) -> X e. B )
62 61 2 eleqtrdi 
 |-  ( ( ( N e. Fin /\ R e. Ring ) /\ ( X e. D /\ Y e. D ) ) -> X e. ( Base ` A ) )
63 62 3ad2ant1 
 |-  ( ( ( ( N e. Fin /\ R e. Ring ) /\ ( X e. D /\ Y e. D ) ) /\ x e. N /\ y e. N ) -> X e. ( Base ` A ) )
64 1 10 matecl 
 |-  ( ( x e. N /\ y e. N /\ X e. ( Base ` A ) ) -> ( x X y ) e. ( Base ` R ) )
65 38 60 63 64 syl3anc 
 |-  ( ( ( ( N e. Fin /\ R e. Ring ) /\ ( X e. D /\ Y e. D ) ) /\ x e. N /\ y e. N ) -> ( x X y ) e. ( Base ` R ) )
66 50 a1d 
 |-  ( ( N e. Fin /\ R e. Ring ) -> ( X e. D -> ( Y e. D -> Y e. ( Base ` A ) ) ) )
67 66 imp32 
 |-  ( ( ( N e. Fin /\ R e. Ring ) /\ ( X e. D /\ Y e. D ) ) -> Y e. ( Base ` A ) )
68 67 3ad2ant1 
 |-  ( ( ( ( N e. Fin /\ R e. Ring ) /\ ( X e. D /\ Y e. D ) ) /\ x e. N /\ y e. N ) -> Y e. ( Base ` A ) )
69 1 10 matecl 
 |-  ( ( x e. N /\ y e. N /\ Y e. ( Base ` A ) ) -> ( x Y y ) e. ( Base ` R ) )
70 38 60 68 69 syl3anc 
 |-  ( ( ( ( N e. Fin /\ R e. Ring ) /\ ( X e. D /\ Y e. D ) ) /\ x e. N /\ y e. N ) -> ( x Y y ) e. ( Base ` R ) )
71 10 11 ringcl 
 |-  ( ( R e. Ring /\ ( x X y ) e. ( Base ` R ) /\ ( x Y y ) e. ( Base ` R ) ) -> ( ( x X y ) ( .r ` R ) ( x Y y ) ) e. ( Base ` R ) )
72 36 65 70 71 syl3anc 
 |-  ( ( ( ( N e. Fin /\ R e. Ring ) /\ ( X e. D /\ Y e. D ) ) /\ x e. N /\ y e. N ) -> ( ( x X y ) ( .r ` R ) ( x Y y ) ) e. ( Base ` R ) )
73 72 adantl 
 |-  ( ( x = y /\ ( ( ( N e. Fin /\ R e. Ring ) /\ ( X e. D /\ Y e. D ) ) /\ x e. N /\ y e. N ) ) -> ( ( x X y ) ( .r ` R ) ( x Y y ) ) e. ( Base ` R ) )
74 eqtr 
 |-  ( ( k = x /\ x = y ) -> k = y )
75 74 ancoms 
 |-  ( ( x = y /\ k = x ) -> k = y )
76 75 oveq2d 
 |-  ( ( x = y /\ k = x ) -> ( x X k ) = ( x X y ) )
77 76 adantlr 
 |-  ( ( ( x = y /\ ( ( ( N e. Fin /\ R e. Ring ) /\ ( X e. D /\ Y e. D ) ) /\ x e. N /\ y e. N ) ) /\ k = x ) -> ( x X k ) = ( x X y ) )
78 oveq1 
 |-  ( k = x -> ( k Y y ) = ( x Y y ) )
79 78 adantl 
 |-  ( ( ( x = y /\ ( ( ( N e. Fin /\ R e. Ring ) /\ ( X e. D /\ Y e. D ) ) /\ x e. N /\ y e. N ) ) /\ k = x ) -> ( k Y y ) = ( x Y y ) )
80 77 79 oveq12d 
 |-  ( ( ( x = y /\ ( ( ( N e. Fin /\ R e. Ring ) /\ ( X e. D /\ Y e. D ) ) /\ x e. N /\ y e. N ) ) /\ k = x ) -> ( ( x X k ) ( .r ` R ) ( k Y y ) ) = ( ( x X y ) ( .r ` R ) ( x Y y ) ) )
81 10 25 29 31 35 58 59 73 80 gsumdifsnd 
 |-  ( ( x = y /\ ( ( ( N e. Fin /\ R e. Ring ) /\ ( X e. D /\ Y e. D ) ) /\ x e. N /\ y e. N ) ) -> ( R gsum ( k e. N |-> ( ( x X k ) ( .r ` R ) ( k Y y ) ) ) ) = ( ( R gsum ( k e. ( N \ { x } ) |-> ( ( x X k ) ( .r ` R ) ( k Y y ) ) ) ) ( +g ` R ) ( ( x X y ) ( .r ` R ) ( x Y y ) ) ) )
82 simprl 
 |-  ( ( ( N e. Fin /\ R e. Ring ) /\ ( X e. D /\ Y e. D ) ) -> X e. D )
83 13 12 82 3jca 
 |-  ( ( ( N e. Fin /\ R e. Ring ) /\ ( X e. D /\ Y e. D ) ) -> ( N e. Fin /\ R e. Ring /\ X e. D ) )
84 83 3ad2ant1 
 |-  ( ( ( ( N e. Fin /\ R e. Ring ) /\ ( X e. D /\ Y e. D ) ) /\ x e. N /\ y e. N ) -> ( N e. Fin /\ R e. Ring /\ X e. D ) )
85 84 ad2antlr 
 |-  ( ( ( x = y /\ ( ( ( N e. Fin /\ R e. Ring ) /\ ( X e. D /\ Y e. D ) ) /\ x e. N /\ y e. N ) ) /\ k e. ( N \ { x } ) ) -> ( N e. Fin /\ R e. Ring /\ X e. D ) )
86 38 ad2antlr 
 |-  ( ( ( x = y /\ ( ( ( N e. Fin /\ R e. Ring ) /\ ( X e. D /\ Y e. D ) ) /\ x e. N /\ y e. N ) ) /\ k e. ( N \ { x } ) ) -> x e. N )
87 eldifi 
 |-  ( k e. ( N \ { x } ) -> k e. N )
88 87 adantl 
 |-  ( ( ( x = y /\ ( ( ( N e. Fin /\ R e. Ring ) /\ ( X e. D /\ Y e. D ) ) /\ x e. N /\ y e. N ) ) /\ k e. ( N \ { x } ) ) -> k e. N )
89 eldifsni 
 |-  ( k e. ( N \ { x } ) -> k =/= x )
90 89 necomd 
 |-  ( k e. ( N \ { x } ) -> x =/= k )
91 90 adantl 
 |-  ( ( ( x = y /\ ( ( ( N e. Fin /\ R e. Ring ) /\ ( X e. D /\ Y e. D ) ) /\ x e. N /\ y e. N ) ) /\ k e. ( N \ { x } ) ) -> x =/= k )
92 1 2 3 4 dmatelnd 
 |-  ( ( ( N e. Fin /\ R e. Ring /\ X e. D ) /\ ( x e. N /\ k e. N /\ x =/= k ) ) -> ( x X k ) = .0. )
93 85 86 88 91 92 syl13anc 
 |-  ( ( ( x = y /\ ( ( ( N e. Fin /\ R e. Ring ) /\ ( X e. D /\ Y e. D ) ) /\ x e. N /\ y e. N ) ) /\ k e. ( N \ { x } ) ) -> ( x X k ) = .0. )
94 93 oveq1d 
 |-  ( ( ( x = y /\ ( ( ( N e. Fin /\ R e. Ring ) /\ ( X e. D /\ Y e. D ) ) /\ x e. N /\ y e. N ) ) /\ k e. ( N \ { x } ) ) -> ( ( x X k ) ( .r ` R ) ( k Y y ) ) = ( .0. ( .r ` R ) ( k Y y ) ) )
95 36 ad2antlr 
 |-  ( ( ( x = y /\ ( ( ( N e. Fin /\ R e. Ring ) /\ ( X e. D /\ Y e. D ) ) /\ x e. N /\ y e. N ) ) /\ k e. ( N \ { x } ) ) -> R e. Ring )
96 simplr3 
 |-  ( ( ( x = y /\ ( ( ( N e. Fin /\ R e. Ring ) /\ ( X e. D /\ Y e. D ) ) /\ x e. N /\ y e. N ) ) /\ k e. ( N \ { x } ) ) -> y e. N )
97 53 ad2antlr 
 |-  ( ( ( x = y /\ ( ( ( N e. Fin /\ R e. Ring ) /\ ( X e. D /\ Y e. D ) ) /\ x e. N /\ y e. N ) ) /\ k e. ( N \ { x } ) ) -> Y e. ( Base ` A ) )
98 88 96 97 55 syl3anc 
 |-  ( ( ( x = y /\ ( ( ( N e. Fin /\ R e. Ring ) /\ ( X e. D /\ Y e. D ) ) /\ x e. N /\ y e. N ) ) /\ k e. ( N \ { x } ) ) -> ( k Y y ) e. ( Base ` R ) )
99 10 11 3 ringlz 
 |-  ( ( R e. Ring /\ ( k Y y ) e. ( Base ` R ) ) -> ( .0. ( .r ` R ) ( k Y y ) ) = .0. )
100 95 98 99 syl2anc 
 |-  ( ( ( x = y /\ ( ( ( N e. Fin /\ R e. Ring ) /\ ( X e. D /\ Y e. D ) ) /\ x e. N /\ y e. N ) ) /\ k e. ( N \ { x } ) ) -> ( .0. ( .r ` R ) ( k Y y ) ) = .0. )
101 94 100 eqtrd 
 |-  ( ( ( x = y /\ ( ( ( N e. Fin /\ R e. Ring ) /\ ( X e. D /\ Y e. D ) ) /\ x e. N /\ y e. N ) ) /\ k e. ( N \ { x } ) ) -> ( ( x X k ) ( .r ` R ) ( k Y y ) ) = .0. )
102 101 mpteq2dva 
 |-  ( ( x = y /\ ( ( ( N e. Fin /\ R e. Ring ) /\ ( X e. D /\ Y e. D ) ) /\ x e. N /\ y e. N ) ) -> ( k e. ( N \ { x } ) |-> ( ( x X k ) ( .r ` R ) ( k Y y ) ) ) = ( k e. ( N \ { x } ) |-> .0. ) )
103 102 oveq2d 
 |-  ( ( x = y /\ ( ( ( N e. Fin /\ R e. Ring ) /\ ( X e. D /\ Y e. D ) ) /\ x e. N /\ y e. N ) ) -> ( R gsum ( k e. ( N \ { x } ) |-> ( ( x X k ) ( .r ` R ) ( k Y y ) ) ) ) = ( R gsum ( k e. ( N \ { x } ) |-> .0. ) ) )
104 diffi 
 |-  ( N e. Fin -> ( N \ { x } ) e. Fin )
105 ringmnd 
 |-  ( R e. Ring -> R e. Mnd )
106 104 105 anim12ci 
 |-  ( ( N e. Fin /\ R e. Ring ) -> ( R e. Mnd /\ ( N \ { x } ) e. Fin ) )
107 106 adantr 
 |-  ( ( ( N e. Fin /\ R e. Ring ) /\ ( X e. D /\ Y e. D ) ) -> ( R e. Mnd /\ ( N \ { x } ) e. Fin ) )
108 107 3ad2ant1 
 |-  ( ( ( ( N e. Fin /\ R e. Ring ) /\ ( X e. D /\ Y e. D ) ) /\ x e. N /\ y e. N ) -> ( R e. Mnd /\ ( N \ { x } ) e. Fin ) )
109 108 adantl 
 |-  ( ( x = y /\ ( ( ( N e. Fin /\ R e. Ring ) /\ ( X e. D /\ Y e. D ) ) /\ x e. N /\ y e. N ) ) -> ( R e. Mnd /\ ( N \ { x } ) e. Fin ) )
110 3 gsumz 
 |-  ( ( R e. Mnd /\ ( N \ { x } ) e. Fin ) -> ( R gsum ( k e. ( N \ { x } ) |-> .0. ) ) = .0. )
111 109 110 syl 
 |-  ( ( x = y /\ ( ( ( N e. Fin /\ R e. Ring ) /\ ( X e. D /\ Y e. D ) ) /\ x e. N /\ y e. N ) ) -> ( R gsum ( k e. ( N \ { x } ) |-> .0. ) ) = .0. )
112 103 111 eqtrd 
 |-  ( ( x = y /\ ( ( ( N e. Fin /\ R e. Ring ) /\ ( X e. D /\ Y e. D ) ) /\ x e. N /\ y e. N ) ) -> ( R gsum ( k e. ( N \ { x } ) |-> ( ( x X k ) ( .r ` R ) ( k Y y ) ) ) ) = .0. )
113 112 oveq1d 
 |-  ( ( x = y /\ ( ( ( N e. Fin /\ R e. Ring ) /\ ( X e. D /\ Y e. D ) ) /\ x e. N /\ y e. N ) ) -> ( ( R gsum ( k e. ( N \ { x } ) |-> ( ( x X k ) ( .r ` R ) ( k Y y ) ) ) ) ( +g ` R ) ( ( x X y ) ( .r ` R ) ( x Y y ) ) ) = ( .0. ( +g ` R ) ( ( x X y ) ( .r ` R ) ( x Y y ) ) ) )
114 105 ad2antlr 
 |-  ( ( ( N e. Fin /\ R e. Ring ) /\ ( X e. D /\ Y e. D ) ) -> R e. Mnd )
115 114 3ad2ant1 
 |-  ( ( ( ( N e. Fin /\ R e. Ring ) /\ ( X e. D /\ Y e. D ) ) /\ x e. N /\ y e. N ) -> R e. Mnd )
116 38 60 53 69 syl3anc 
 |-  ( ( ( ( N e. Fin /\ R e. Ring ) /\ ( X e. D /\ Y e. D ) ) /\ x e. N /\ y e. N ) -> ( x Y y ) e. ( Base ` R ) )
117 36 65 116 71 syl3anc 
 |-  ( ( ( ( N e. Fin /\ R e. Ring ) /\ ( X e. D /\ Y e. D ) ) /\ x e. N /\ y e. N ) -> ( ( x X y ) ( .r ` R ) ( x Y y ) ) e. ( Base ` R ) )
118 115 117 jca 
 |-  ( ( ( ( N e. Fin /\ R e. Ring ) /\ ( X e. D /\ Y e. D ) ) /\ x e. N /\ y e. N ) -> ( R e. Mnd /\ ( ( x X y ) ( .r ` R ) ( x Y y ) ) e. ( Base ` R ) ) )
119 118 adantl 
 |-  ( ( x = y /\ ( ( ( N e. Fin /\ R e. Ring ) /\ ( X e. D /\ Y e. D ) ) /\ x e. N /\ y e. N ) ) -> ( R e. Mnd /\ ( ( x X y ) ( .r ` R ) ( x Y y ) ) e. ( Base ` R ) ) )
120 10 25 3 mndlid 
 |-  ( ( R e. Mnd /\ ( ( x X y ) ( .r ` R ) ( x Y y ) ) e. ( Base ` R ) ) -> ( .0. ( +g ` R ) ( ( x X y ) ( .r ` R ) ( x Y y ) ) ) = ( ( x X y ) ( .r ` R ) ( x Y y ) ) )
121 119 120 syl 
 |-  ( ( x = y /\ ( ( ( N e. Fin /\ R e. Ring ) /\ ( X e. D /\ Y e. D ) ) /\ x e. N /\ y e. N ) ) -> ( .0. ( +g ` R ) ( ( x X y ) ( .r ` R ) ( x Y y ) ) ) = ( ( x X y ) ( .r ` R ) ( x Y y ) ) )
122 81 113 121 3eqtrd 
 |-  ( ( x = y /\ ( ( ( N e. Fin /\ R e. Ring ) /\ ( X e. D /\ Y e. D ) ) /\ x e. N /\ y e. N ) ) -> ( R gsum ( k e. N |-> ( ( x X k ) ( .r ` R ) ( k Y y ) ) ) ) = ( ( x X y ) ( .r ` R ) ( x Y y ) ) )
123 iftrue 
 |-  ( x = y -> if ( x = y , ( ( x X y ) ( .r ` R ) ( x Y y ) ) , .0. ) = ( ( x X y ) ( .r ` R ) ( x Y y ) ) )
124 123 adantr 
 |-  ( ( x = y /\ ( ( ( N e. Fin /\ R e. Ring ) /\ ( X e. D /\ Y e. D ) ) /\ x e. N /\ y e. N ) ) -> if ( x = y , ( ( x X y ) ( .r ` R ) ( x Y y ) ) , .0. ) = ( ( x X y ) ( .r ` R ) ( x Y y ) ) )
125 122 124 eqtr4d 
 |-  ( ( x = y /\ ( ( ( N e. Fin /\ R e. Ring ) /\ ( X e. D /\ Y e. D ) ) /\ x e. N /\ y e. N ) ) -> ( R gsum ( k e. N |-> ( ( x X k ) ( .r ` R ) ( k Y y ) ) ) ) = if ( x = y , ( ( x X y ) ( .r ` R ) ( x Y y ) ) , .0. ) )
126 simprr 
 |-  ( ( ( N e. Fin /\ R e. Ring ) /\ ( X e. D /\ Y e. D ) ) -> Y e. D )
127 13 12 126 3jca 
 |-  ( ( ( N e. Fin /\ R e. Ring ) /\ ( X e. D /\ Y e. D ) ) -> ( N e. Fin /\ R e. Ring /\ Y e. D ) )
128 127 3ad2ant1 
 |-  ( ( ( ( N e. Fin /\ R e. Ring ) /\ ( X e. D /\ Y e. D ) ) /\ x e. N /\ y e. N ) -> ( N e. Fin /\ R e. Ring /\ Y e. D ) )
129 128 ad2antlr 
 |-  ( ( ( -. x = y /\ ( ( ( N e. Fin /\ R e. Ring ) /\ ( X e. D /\ Y e. D ) ) /\ x e. N /\ y e. N ) ) /\ k e. N ) -> ( N e. Fin /\ R e. Ring /\ Y e. D ) )
130 129 adantl 
 |-  ( ( x = k /\ ( ( -. x = y /\ ( ( ( N e. Fin /\ R e. Ring ) /\ ( X e. D /\ Y e. D ) ) /\ x e. N /\ y e. N ) ) /\ k e. N ) ) -> ( N e. Fin /\ R e. Ring /\ Y e. D ) )
131 simprr 
 |-  ( ( x = k /\ ( ( -. x = y /\ ( ( ( N e. Fin /\ R e. Ring ) /\ ( X e. D /\ Y e. D ) ) /\ x e. N /\ y e. N ) ) /\ k e. N ) ) -> k e. N )
132 simplr3 
 |-  ( ( ( -. x = y /\ ( ( ( N e. Fin /\ R e. Ring ) /\ ( X e. D /\ Y e. D ) ) /\ x e. N /\ y e. N ) ) /\ k e. N ) -> y e. N )
133 132 adantl 
 |-  ( ( x = k /\ ( ( -. x = y /\ ( ( ( N e. Fin /\ R e. Ring ) /\ ( X e. D /\ Y e. D ) ) /\ x e. N /\ y e. N ) ) /\ k e. N ) ) -> y e. N )
134 df-ne 
 |-  ( x =/= y <-> -. x = y )
135 neeq1 
 |-  ( x = k -> ( x =/= y <-> k =/= y ) )
136 135 biimpcd 
 |-  ( x =/= y -> ( x = k -> k =/= y ) )
137 134 136 sylbir 
 |-  ( -. x = y -> ( x = k -> k =/= y ) )
138 137 adantr 
 |-  ( ( -. x = y /\ ( ( ( N e. Fin /\ R e. Ring ) /\ ( X e. D /\ Y e. D ) ) /\ x e. N /\ y e. N ) ) -> ( x = k -> k =/= y ) )
139 138 adantr 
 |-  ( ( ( -. x = y /\ ( ( ( N e. Fin /\ R e. Ring ) /\ ( X e. D /\ Y e. D ) ) /\ x e. N /\ y e. N ) ) /\ k e. N ) -> ( x = k -> k =/= y ) )
140 139 impcom 
 |-  ( ( x = k /\ ( ( -. x = y /\ ( ( ( N e. Fin /\ R e. Ring ) /\ ( X e. D /\ Y e. D ) ) /\ x e. N /\ y e. N ) ) /\ k e. N ) ) -> k =/= y )
141 1 2 3 4 dmatelnd 
 |-  ( ( ( N e. Fin /\ R e. Ring /\ Y e. D ) /\ ( k e. N /\ y e. N /\ k =/= y ) ) -> ( k Y y ) = .0. )
142 130 131 133 140 141 syl13anc 
 |-  ( ( x = k /\ ( ( -. x = y /\ ( ( ( N e. Fin /\ R e. Ring ) /\ ( X e. D /\ Y e. D ) ) /\ x e. N /\ y e. N ) ) /\ k e. N ) ) -> ( k Y y ) = .0. )
143 142 oveq2d 
 |-  ( ( x = k /\ ( ( -. x = y /\ ( ( ( N e. Fin /\ R e. Ring ) /\ ( X e. D /\ Y e. D ) ) /\ x e. N /\ y e. N ) ) /\ k e. N ) ) -> ( ( x X k ) ( .r ` R ) ( k Y y ) ) = ( ( x X k ) ( .r ` R ) .0. ) )
144 36 ad2antlr 
 |-  ( ( ( -. x = y /\ ( ( ( N e. Fin /\ R e. Ring ) /\ ( X e. D /\ Y e. D ) ) /\ x e. N /\ y e. N ) ) /\ k e. N ) -> R e. Ring )
145 38 ad2antlr 
 |-  ( ( ( -. x = y /\ ( ( ( N e. Fin /\ R e. Ring ) /\ ( X e. D /\ Y e. D ) ) /\ x e. N /\ y e. N ) ) /\ k e. N ) -> x e. N )
146 simpr 
 |-  ( ( ( -. x = y /\ ( ( ( N e. Fin /\ R e. Ring ) /\ ( X e. D /\ Y e. D ) ) /\ x e. N /\ y e. N ) ) /\ k e. N ) -> k e. N )
147 63 ad2antlr 
 |-  ( ( ( -. x = y /\ ( ( ( N e. Fin /\ R e. Ring ) /\ ( X e. D /\ Y e. D ) ) /\ x e. N /\ y e. N ) ) /\ k e. N ) -> X e. ( Base ` A ) )
148 145 146 147 47 syl3anc 
 |-  ( ( ( -. x = y /\ ( ( ( N e. Fin /\ R e. Ring ) /\ ( X e. D /\ Y e. D ) ) /\ x e. N /\ y e. N ) ) /\ k e. N ) -> ( x X k ) e. ( Base ` R ) )
149 10 11 3 ringrz 
 |-  ( ( R e. Ring /\ ( x X k ) e. ( Base ` R ) ) -> ( ( x X k ) ( .r ` R ) .0. ) = .0. )
150 144 148 149 syl2anc 
 |-  ( ( ( -. x = y /\ ( ( ( N e. Fin /\ R e. Ring ) /\ ( X e. D /\ Y e. D ) ) /\ x e. N /\ y e. N ) ) /\ k e. N ) -> ( ( x X k ) ( .r ` R ) .0. ) = .0. )
151 150 adantl 
 |-  ( ( x = k /\ ( ( -. x = y /\ ( ( ( N e. Fin /\ R e. Ring ) /\ ( X e. D /\ Y e. D ) ) /\ x e. N /\ y e. N ) ) /\ k e. N ) ) -> ( ( x X k ) ( .r ` R ) .0. ) = .0. )
152 143 151 eqtrd 
 |-  ( ( x = k /\ ( ( -. x = y /\ ( ( ( N e. Fin /\ R e. Ring ) /\ ( X e. D /\ Y e. D ) ) /\ x e. N /\ y e. N ) ) /\ k e. N ) ) -> ( ( x X k ) ( .r ` R ) ( k Y y ) ) = .0. )
153 84 ad2antlr 
 |-  ( ( ( -. x = y /\ ( ( ( N e. Fin /\ R e. Ring ) /\ ( X e. D /\ Y e. D ) ) /\ x e. N /\ y e. N ) ) /\ k e. N ) -> ( N e. Fin /\ R e. Ring /\ X e. D ) )
154 153 adantl 
 |-  ( ( -. x = k /\ ( ( -. x = y /\ ( ( ( N e. Fin /\ R e. Ring ) /\ ( X e. D /\ Y e. D ) ) /\ x e. N /\ y e. N ) ) /\ k e. N ) ) -> ( N e. Fin /\ R e. Ring /\ X e. D ) )
155 145 adantl 
 |-  ( ( -. x = k /\ ( ( -. x = y /\ ( ( ( N e. Fin /\ R e. Ring ) /\ ( X e. D /\ Y e. D ) ) /\ x e. N /\ y e. N ) ) /\ k e. N ) ) -> x e. N )
156 simprr 
 |-  ( ( -. x = k /\ ( ( -. x = y /\ ( ( ( N e. Fin /\ R e. Ring ) /\ ( X e. D /\ Y e. D ) ) /\ x e. N /\ y e. N ) ) /\ k e. N ) ) -> k e. N )
157 neqne 
 |-  ( -. x = k -> x =/= k )
158 157 adantr 
 |-  ( ( -. x = k /\ ( ( -. x = y /\ ( ( ( N e. Fin /\ R e. Ring ) /\ ( X e. D /\ Y e. D ) ) /\ x e. N /\ y e. N ) ) /\ k e. N ) ) -> x =/= k )
159 154 155 156 158 92 syl13anc 
 |-  ( ( -. x = k /\ ( ( -. x = y /\ ( ( ( N e. Fin /\ R e. Ring ) /\ ( X e. D /\ Y e. D ) ) /\ x e. N /\ y e. N ) ) /\ k e. N ) ) -> ( x X k ) = .0. )
160 159 oveq1d 
 |-  ( ( -. x = k /\ ( ( -. x = y /\ ( ( ( N e. Fin /\ R e. Ring ) /\ ( X e. D /\ Y e. D ) ) /\ x e. N /\ y e. N ) ) /\ k e. N ) ) -> ( ( x X k ) ( .r ` R ) ( k Y y ) ) = ( .0. ( .r ` R ) ( k Y y ) ) )
161 68 ad2antlr 
 |-  ( ( ( -. x = y /\ ( ( ( N e. Fin /\ R e. Ring ) /\ ( X e. D /\ Y e. D ) ) /\ x e. N /\ y e. N ) ) /\ k e. N ) -> Y e. ( Base ` A ) )
162 146 132 161 55 syl3anc 
 |-  ( ( ( -. x = y /\ ( ( ( N e. Fin /\ R e. Ring ) /\ ( X e. D /\ Y e. D ) ) /\ x e. N /\ y e. N ) ) /\ k e. N ) -> ( k Y y ) e. ( Base ` R ) )
163 144 162 99 syl2anc 
 |-  ( ( ( -. x = y /\ ( ( ( N e. Fin /\ R e. Ring ) /\ ( X e. D /\ Y e. D ) ) /\ x e. N /\ y e. N ) ) /\ k e. N ) -> ( .0. ( .r ` R ) ( k Y y ) ) = .0. )
164 163 adantl 
 |-  ( ( -. x = k /\ ( ( -. x = y /\ ( ( ( N e. Fin /\ R e. Ring ) /\ ( X e. D /\ Y e. D ) ) /\ x e. N /\ y e. N ) ) /\ k e. N ) ) -> ( .0. ( .r ` R ) ( k Y y ) ) = .0. )
165 160 164 eqtrd 
 |-  ( ( -. x = k /\ ( ( -. x = y /\ ( ( ( N e. Fin /\ R e. Ring ) /\ ( X e. D /\ Y e. D ) ) /\ x e. N /\ y e. N ) ) /\ k e. N ) ) -> ( ( x X k ) ( .r ` R ) ( k Y y ) ) = .0. )
166 152 165 pm2.61ian 
 |-  ( ( ( -. x = y /\ ( ( ( N e. Fin /\ R e. Ring ) /\ ( X e. D /\ Y e. D ) ) /\ x e. N /\ y e. N ) ) /\ k e. N ) -> ( ( x X k ) ( .r ` R ) ( k Y y ) ) = .0. )
167 166 mpteq2dva 
 |-  ( ( -. x = y /\ ( ( ( N e. Fin /\ R e. Ring ) /\ ( X e. D /\ Y e. D ) ) /\ x e. N /\ y e. N ) ) -> ( k e. N |-> ( ( x X k ) ( .r ` R ) ( k Y y ) ) ) = ( k e. N |-> .0. ) )
168 167 oveq2d 
 |-  ( ( -. x = y /\ ( ( ( N e. Fin /\ R e. Ring ) /\ ( X e. D /\ Y e. D ) ) /\ x e. N /\ y e. N ) ) -> ( R gsum ( k e. N |-> ( ( x X k ) ( .r ` R ) ( k Y y ) ) ) ) = ( R gsum ( k e. N |-> .0. ) ) )
169 105 anim2i 
 |-  ( ( N e. Fin /\ R e. Ring ) -> ( N e. Fin /\ R e. Mnd ) )
170 169 ancomd 
 |-  ( ( N e. Fin /\ R e. Ring ) -> ( R e. Mnd /\ N e. Fin ) )
171 3 gsumz 
 |-  ( ( R e. Mnd /\ N e. Fin ) -> ( R gsum ( k e. N |-> .0. ) ) = .0. )
172 170 171 syl 
 |-  ( ( N e. Fin /\ R e. Ring ) -> ( R gsum ( k e. N |-> .0. ) ) = .0. )
173 172 adantr 
 |-  ( ( ( N e. Fin /\ R e. Ring ) /\ ( X e. D /\ Y e. D ) ) -> ( R gsum ( k e. N |-> .0. ) ) = .0. )
174 173 3ad2ant1 
 |-  ( ( ( ( N e. Fin /\ R e. Ring ) /\ ( X e. D /\ Y e. D ) ) /\ x e. N /\ y e. N ) -> ( R gsum ( k e. N |-> .0. ) ) = .0. )
175 174 adantl 
 |-  ( ( -. x = y /\ ( ( ( N e. Fin /\ R e. Ring ) /\ ( X e. D /\ Y e. D ) ) /\ x e. N /\ y e. N ) ) -> ( R gsum ( k e. N |-> .0. ) ) = .0. )
176 iffalse 
 |-  ( -. x = y -> if ( x = y , ( ( x X y ) ( .r ` R ) ( x Y y ) ) , .0. ) = .0. )
177 176 eqcomd 
 |-  ( -. x = y -> .0. = if ( x = y , ( ( x X y ) ( .r ` R ) ( x Y y ) ) , .0. ) )
178 177 adantr 
 |-  ( ( -. x = y /\ ( ( ( N e. Fin /\ R e. Ring ) /\ ( X e. D /\ Y e. D ) ) /\ x e. N /\ y e. N ) ) -> .0. = if ( x = y , ( ( x X y ) ( .r ` R ) ( x Y y ) ) , .0. ) )
179 168 175 178 3eqtrd 
 |-  ( ( -. x = y /\ ( ( ( N e. Fin /\ R e. Ring ) /\ ( X e. D /\ Y e. D ) ) /\ x e. N /\ y e. N ) ) -> ( R gsum ( k e. N |-> ( ( x X k ) ( .r ` R ) ( k Y y ) ) ) ) = if ( x = y , ( ( x X y ) ( .r ` R ) ( x Y y ) ) , .0. ) )
180 125 179 pm2.61ian 
 |-  ( ( ( ( N e. Fin /\ R e. Ring ) /\ ( X e. D /\ Y e. D ) ) /\ x e. N /\ y e. N ) -> ( R gsum ( k e. N |-> ( ( x X k ) ( .r ` R ) ( k Y y ) ) ) ) = if ( x = y , ( ( x X y ) ( .r ` R ) ( x Y y ) ) , .0. ) )
181 180 mpoeq3dva 
 |-  ( ( ( N e. Fin /\ R e. Ring ) /\ ( X e. D /\ Y e. D ) ) -> ( x e. N , y e. N |-> ( R gsum ( k e. N |-> ( ( x X k ) ( .r ` R ) ( k Y y ) ) ) ) ) = ( x e. N , y e. N |-> if ( x = y , ( ( x X y ) ( .r ` R ) ( x Y y ) ) , .0. ) ) )
182 9 24 181 3eqtrd 
 |-  ( ( ( N e. Fin /\ R e. Ring ) /\ ( X e. D /\ Y e. D ) ) -> ( X ( .r ` A ) Y ) = ( x e. N , y e. N |-> if ( x = y , ( ( x X y ) ( .r ` R ) ( x Y y ) ) , .0. ) ) )