Metamath Proof Explorer

Theorem madugsum

Description: The determinant of a matrix with a row L consisting of the same element X is the sum of the elements of the L -th column of the adjunct of the matrix multiplied with X . (Contributed by Stefan O'Rear, 16-Jul-2018)

Ref Expression
Hypotheses maduf.a 
|- A = ( N Mat R )
maduf.j 
|- J = ( N maAdju R )
maduf.b 
|- B = ( Base ` A )
madugsum.d 
|- D = ( N maDet R )
madugsum.t 
|- .x. = ( .r ` R )
madugsum.k 
|- K = ( Base ` R )
madugsum.m 
|- ( ph -> M e. B )
madugsum.r 
|- ( ph -> R e. CRing )
madugsum.x 
|- ( ( ph /\ i e. N ) -> X e. K )
madugsum.l 
|- ( ph -> L e. N )
Assertion madugsum 
|- ( ph -> ( R gsum ( i e. N |-> ( X .x. ( i ( J ` M ) L ) ) ) ) = ( D ` ( j e. N , i e. N |-> if ( j = L , X , ( j M i ) ) ) ) )

Proof

Step Hyp Ref Expression
1 maduf.a 
 |-  A = ( N Mat R )
2 maduf.j 
 |-  J = ( N maAdju R )
3 maduf.b 
 |-  B = ( Base ` A )
4 madugsum.d 
 |-  D = ( N maDet R )
5 madugsum.t 
 |-  .x. = ( .r ` R )
6 madugsum.k 
 |-  K = ( Base ` R )
7 madugsum.m 
 |-  ( ph -> M e. B )
8 madugsum.r 
 |-  ( ph -> R e. CRing )
9 madugsum.x 
 |-  ( ( ph /\ i e. N ) -> X e. K )
10 madugsum.l 
 |-  ( ph -> L e. N )
11 mpteq1 
 |-  ( c = (/) -> ( b e. c |-> ( [_ b / i ]_ X .x. ( b ( J ` M ) L ) ) ) = ( b e. (/) |-> ( [_ b / i ]_ X .x. ( b ( J ` M ) L ) ) ) )
12 11 oveq2d 
 |-  ( c = (/) -> ( R gsum ( b e. c |-> ( [_ b / i ]_ X .x. ( b ( J ` M ) L ) ) ) ) = ( R gsum ( b e. (/) |-> ( [_ b / i ]_ X .x. ( b ( J ` M ) L ) ) ) ) )
13 eleq2 
 |-  ( c = (/) -> ( b e. c <-> b e. (/) ) )
14 13 ifbid 
 |-  ( c = (/) -> if ( b e. c , [_ b / i ]_ X , ( 0g ` R ) ) = if ( b e. (/) , [_ b / i ]_ X , ( 0g ` R ) ) )
15 14 ifeq1d 
 |-  ( c = (/) -> if ( a = L , if ( b e. c , [_ b / i ]_ X , ( 0g ` R ) ) , ( a M b ) ) = if ( a = L , if ( b e. (/) , [_ b / i ]_ X , ( 0g ` R ) ) , ( a M b ) ) )
16 15 mpoeq3dv 
 |-  ( c = (/) -> ( a e. N , b e. N |-> if ( a = L , if ( b e. c , [_ b / i ]_ X , ( 0g ` R ) ) , ( a M b ) ) ) = ( a e. N , b e. N |-> if ( a = L , if ( b e. (/) , [_ b / i ]_ X , ( 0g ` R ) ) , ( a M b ) ) ) )
17 16 fveq2d 
 |-  ( c = (/) -> ( D ` ( a e. N , b e. N |-> if ( a = L , if ( b e. c , [_ b / i ]_ X , ( 0g ` R ) ) , ( a M b ) ) ) ) = ( D ` ( a e. N , b e. N |-> if ( a = L , if ( b e. (/) , [_ b / i ]_ X , ( 0g ` R ) ) , ( a M b ) ) ) ) )
18 12 17 eqeq12d 
 |-  ( c = (/) -> ( ( R gsum ( b e. c |-> ( [_ b / i ]_ X .x. ( b ( J ` M ) L ) ) ) ) = ( D ` ( a e. N , b e. N |-> if ( a = L , if ( b e. c , [_ b / i ]_ X , ( 0g ` R ) ) , ( a M b ) ) ) ) <-> ( R gsum ( b e. (/) |-> ( [_ b / i ]_ X .x. ( b ( J ` M ) L ) ) ) ) = ( D ` ( a e. N , b e. N |-> if ( a = L , if ( b e. (/) , [_ b / i ]_ X , ( 0g ` R ) ) , ( a M b ) ) ) ) ) )
19 mpteq1 
 |-  ( c = d -> ( b e. c |-> ( [_ b / i ]_ X .x. ( b ( J ` M ) L ) ) ) = ( b e. d |-> ( [_ b / i ]_ X .x. ( b ( J ` M ) L ) ) ) )
20 19 oveq2d 
 |-  ( c = d -> ( R gsum ( b e. c |-> ( [_ b / i ]_ X .x. ( b ( J ` M ) L ) ) ) ) = ( R gsum ( b e. d |-> ( [_ b / i ]_ X .x. ( b ( J ` M ) L ) ) ) ) )
21 eleq2 
 |-  ( c = d -> ( b e. c <-> b e. d ) )
22 21 ifbid 
 |-  ( c = d -> if ( b e. c , [_ b / i ]_ X , ( 0g ` R ) ) = if ( b e. d , [_ b / i ]_ X , ( 0g ` R ) ) )
23 22 ifeq1d 
 |-  ( c = d -> if ( a = L , if ( b e. c , [_ b / i ]_ X , ( 0g ` R ) ) , ( a M b ) ) = if ( a = L , if ( b e. d , [_ b / i ]_ X , ( 0g ` R ) ) , ( a M b ) ) )
24 23 mpoeq3dv 
 |-  ( c = d -> ( a e. N , b e. N |-> if ( a = L , if ( b e. c , [_ b / i ]_ X , ( 0g ` R ) ) , ( a M b ) ) ) = ( a e. N , b e. N |-> if ( a = L , if ( b e. d , [_ b / i ]_ X , ( 0g ` R ) ) , ( a M b ) ) ) )
25 24 fveq2d 
 |-  ( c = d -> ( D ` ( a e. N , b e. N |-> if ( a = L , if ( b e. c , [_ b / i ]_ X , ( 0g ` R ) ) , ( a M b ) ) ) ) = ( D ` ( a e. N , b e. N |-> if ( a = L , if ( b e. d , [_ b / i ]_ X , ( 0g ` R ) ) , ( a M b ) ) ) ) )
26 20 25 eqeq12d 
 |-  ( c = d -> ( ( R gsum ( b e. c |-> ( [_ b / i ]_ X .x. ( b ( J ` M ) L ) ) ) ) = ( D ` ( a e. N , b e. N |-> if ( a = L , if ( b e. c , [_ b / i ]_ X , ( 0g ` R ) ) , ( a M b ) ) ) ) <-> ( R gsum ( b e. d |-> ( [_ b / i ]_ X .x. ( b ( J ` M ) L ) ) ) ) = ( D ` ( a e. N , b e. N |-> if ( a = L , if ( b e. d , [_ b / i ]_ X , ( 0g ` R ) ) , ( a M b ) ) ) ) ) )
27 mpteq1 
 |-  ( c = ( d u. { e } ) -> ( b e. c |-> ( [_ b / i ]_ X .x. ( b ( J ` M ) L ) ) ) = ( b e. ( d u. { e } ) |-> ( [_ b / i ]_ X .x. ( b ( J ` M ) L ) ) ) )
28 27 oveq2d 
 |-  ( c = ( d u. { e } ) -> ( R gsum ( b e. c |-> ( [_ b / i ]_ X .x. ( b ( J ` M ) L ) ) ) ) = ( R gsum ( b e. ( d u. { e } ) |-> ( [_ b / i ]_ X .x. ( b ( J ` M ) L ) ) ) ) )
29 eleq2 
 |-  ( c = ( d u. { e } ) -> ( b e. c <-> b e. ( d u. { e } ) ) )
30 29 ifbid 
 |-  ( c = ( d u. { e } ) -> if ( b e. c , [_ b / i ]_ X , ( 0g ` R ) ) = if ( b e. ( d u. { e } ) , [_ b / i ]_ X , ( 0g ` R ) ) )
31 30 ifeq1d 
 |-  ( c = ( d u. { e } ) -> if ( a = L , if ( b e. c , [_ b / i ]_ X , ( 0g ` R ) ) , ( a M b ) ) = if ( a = L , if ( b e. ( d u. { e } ) , [_ b / i ]_ X , ( 0g ` R ) ) , ( a M b ) ) )
32 31 mpoeq3dv 
 |-  ( c = ( d u. { e } ) -> ( a e. N , b e. N |-> if ( a = L , if ( b e. c , [_ b / i ]_ X , ( 0g ` R ) ) , ( a M b ) ) ) = ( a e. N , b e. N |-> if ( a = L , if ( b e. ( d u. { e } ) , [_ b / i ]_ X , ( 0g ` R ) ) , ( a M b ) ) ) )
33 32 fveq2d 
 |-  ( c = ( d u. { e } ) -> ( D ` ( a e. N , b e. N |-> if ( a = L , if ( b e. c , [_ b / i ]_ X , ( 0g ` R ) ) , ( a M b ) ) ) ) = ( D ` ( a e. N , b e. N |-> if ( a = L , if ( b e. ( d u. { e } ) , [_ b / i ]_ X , ( 0g ` R ) ) , ( a M b ) ) ) ) )
34 28 33 eqeq12d 
 |-  ( c = ( d u. { e } ) -> ( ( R gsum ( b e. c |-> ( [_ b / i ]_ X .x. ( b ( J ` M ) L ) ) ) ) = ( D ` ( a e. N , b e. N |-> if ( a = L , if ( b e. c , [_ b / i ]_ X , ( 0g ` R ) ) , ( a M b ) ) ) ) <-> ( R gsum ( b e. ( d u. { e } ) |-> ( [_ b / i ]_ X .x. ( b ( J ` M ) L ) ) ) ) = ( D ` ( a e. N , b e. N |-> if ( a = L , if ( b e. ( d u. { e } ) , [_ b / i ]_ X , ( 0g ` R ) ) , ( a M b ) ) ) ) ) )
35 mpteq1 
 |-  ( c = N -> ( b e. c |-> ( [_ b / i ]_ X .x. ( b ( J ` M ) L ) ) ) = ( b e. N |-> ( [_ b / i ]_ X .x. ( b ( J ` M ) L ) ) ) )
36 35 oveq2d 
 |-  ( c = N -> ( R gsum ( b e. c |-> ( [_ b / i ]_ X .x. ( b ( J ` M ) L ) ) ) ) = ( R gsum ( b e. N |-> ( [_ b / i ]_ X .x. ( b ( J ` M ) L ) ) ) ) )
37 eleq2 
 |-  ( c = N -> ( b e. c <-> b e. N ) )
38 37 ifbid 
 |-  ( c = N -> if ( b e. c , [_ b / i ]_ X , ( 0g ` R ) ) = if ( b e. N , [_ b / i ]_ X , ( 0g ` R ) ) )
39 38 ifeq1d 
 |-  ( c = N -> if ( a = L , if ( b e. c , [_ b / i ]_ X , ( 0g ` R ) ) , ( a M b ) ) = if ( a = L , if ( b e. N , [_ b / i ]_ X , ( 0g ` R ) ) , ( a M b ) ) )
40 39 mpoeq3dv 
 |-  ( c = N -> ( a e. N , b e. N |-> if ( a = L , if ( b e. c , [_ b / i ]_ X , ( 0g ` R ) ) , ( a M b ) ) ) = ( a e. N , b e. N |-> if ( a = L , if ( b e. N , [_ b / i ]_ X , ( 0g ` R ) ) , ( a M b ) ) ) )
41 40 fveq2d 
 |-  ( c = N -> ( D ` ( a e. N , b e. N |-> if ( a = L , if ( b e. c , [_ b / i ]_ X , ( 0g ` R ) ) , ( a M b ) ) ) ) = ( D ` ( a e. N , b e. N |-> if ( a = L , if ( b e. N , [_ b / i ]_ X , ( 0g ` R ) ) , ( a M b ) ) ) ) )
42 36 41 eqeq12d 
 |-  ( c = N -> ( ( R gsum ( b e. c |-> ( [_ b / i ]_ X .x. ( b ( J ` M ) L ) ) ) ) = ( D ` ( a e. N , b e. N |-> if ( a = L , if ( b e. c , [_ b / i ]_ X , ( 0g ` R ) ) , ( a M b ) ) ) ) <-> ( R gsum ( b e. N |-> ( [_ b / i ]_ X .x. ( b ( J ` M ) L ) ) ) ) = ( D ` ( a e. N , b e. N |-> if ( a = L , if ( b e. N , [_ b / i ]_ X , ( 0g ` R ) ) , ( a M b ) ) ) ) ) )
43 mpt0 
 |-  ( b e. (/) |-> ( [_ b / i ]_ X .x. ( b ( J ` M ) L ) ) ) = (/)
44 43 oveq2i 
 |-  ( R gsum ( b e. (/) |-> ( [_ b / i ]_ X .x. ( b ( J ` M ) L ) ) ) ) = ( R gsum (/) )
45 eqid 
 |-  ( 0g ` R ) = ( 0g ` R )
46 45 gsum0 
 |-  ( R gsum (/) ) = ( 0g ` R )
47 44 46 eqtri 
 |-  ( R gsum ( b e. (/) |-> ( [_ b / i ]_ X .x. ( b ( J ` M ) L ) ) ) ) = ( 0g ` R )
48 noel 
 |-  -. b e. (/)
49 iffalse 
 |-  ( -. b e. (/) -> if ( b e. (/) , [_ b / i ]_ X , ( 0g ` R ) ) = ( 0g ` R ) )
50 48 49 mp1i 
 |-  ( ( a e. N /\ b e. N ) -> if ( b e. (/) , [_ b / i ]_ X , ( 0g ` R ) ) = ( 0g ` R ) )
51 50 ifeq1d 
 |-  ( ( a e. N /\ b e. N ) -> if ( a = L , if ( b e. (/) , [_ b / i ]_ X , ( 0g ` R ) ) , ( a M b ) ) = if ( a = L , ( 0g ` R ) , ( a M b ) ) )
52 51 mpoeq3ia 
 |-  ( a e. N , b e. N |-> if ( a = L , if ( b e. (/) , [_ b / i ]_ X , ( 0g ` R ) ) , ( a M b ) ) ) = ( a e. N , b e. N |-> if ( a = L , ( 0g ` R ) , ( a M b ) ) )
53 52 fveq2i 
 |-  ( D ` ( a e. N , b e. N |-> if ( a = L , if ( b e. (/) , [_ b / i ]_ X , ( 0g ` R ) ) , ( a M b ) ) ) ) = ( D ` ( a e. N , b e. N |-> if ( a = L , ( 0g ` R ) , ( a M b ) ) ) )
54 1 3 matrcl 
 |-  ( M e. B -> ( N e. Fin /\ R e. _V ) )
55 7 54 syl 
 |-  ( ph -> ( N e. Fin /\ R e. _V ) )
56 55 simpld 
 |-  ( ph -> N e. Fin )
57 1 6 3 matbas2i 
 |-  ( M e. B -> M e. ( K ^m ( N X. N ) ) )
58 elmapi 
 |-  ( M e. ( K ^m ( N X. N ) ) -> M : ( N X. N ) --> K )
59 7 57 58 3syl 
 |-  ( ph -> M : ( N X. N ) --> K )
60 59 fovrnda 
 |-  ( ( ph /\ ( a e. N /\ b e. N ) ) -> ( a M b ) e. K )
61 60 3impb 
 |-  ( ( ph /\ a e. N /\ b e. N ) -> ( a M b ) e. K )
62 4 6 45 8 56 61 10 mdetr0 
 |-  ( ph -> ( D ` ( a e. N , b e. N |-> if ( a = L , ( 0g ` R ) , ( a M b ) ) ) ) = ( 0g ` R ) )
63 53 62 syl5eq 
 |-  ( ph -> ( D ` ( a e. N , b e. N |-> if ( a = L , if ( b e. (/) , [_ b / i ]_ X , ( 0g ` R ) ) , ( a M b ) ) ) ) = ( 0g ` R ) )
64 47 63 eqtr4id 
 |-  ( ph -> ( R gsum ( b e. (/) |-> ( [_ b / i ]_ X .x. ( b ( J ` M ) L ) ) ) ) = ( D ` ( a e. N , b e. N |-> if ( a = L , if ( b e. (/) , [_ b / i ]_ X , ( 0g ` R ) ) , ( a M b ) ) ) ) )
65 eqid 
 |-  ( +g ` R ) = ( +g ` R )
66 8 adantr 
 |-  ( ( ph /\ ( d C_ N /\ e e. ( N \ d ) ) ) -> R e. CRing )
67 crngring 
 |-  ( R e. CRing -> R e. Ring )
68 66 67 syl 
 |-  ( ( ph /\ ( d C_ N /\ e e. ( N \ d ) ) ) -> R e. Ring )
69 ringcmn 
 |-  ( R e. Ring -> R e. CMnd )
70 68 69 syl 
 |-  ( ( ph /\ ( d C_ N /\ e e. ( N \ d ) ) ) -> R e. CMnd )
71 56 adantr 
 |-  ( ( ph /\ ( d C_ N /\ e e. ( N \ d ) ) ) -> N e. Fin )
72 simprl 
 |-  ( ( ph /\ ( d C_ N /\ e e. ( N \ d ) ) ) -> d C_ N )
73 71 72 ssfid 
 |-  ( ( ph /\ ( d C_ N /\ e e. ( N \ d ) ) ) -> d e. Fin )
74 68 adantr 
 |-  ( ( ( ph /\ ( d C_ N /\ e e. ( N \ d ) ) ) /\ b e. d ) -> R e. Ring )
75 72 sselda 
 |-  ( ( ( ph /\ ( d C_ N /\ e e. ( N \ d ) ) ) /\ b e. d ) -> b e. N )
76 9 ralrimiva 
 |-  ( ph -> A. i e. N X e. K )
77 76 ad2antrr 
 |-  ( ( ( ph /\ ( d C_ N /\ e e. ( N \ d ) ) ) /\ b e. d ) -> A. i e. N X e. K )
78 rspcsbela 
 |-  ( ( b e. N /\ A. i e. N X e. K ) -> [_ b / i ]_ X e. K )
79 75 77 78 syl2anc 
 |-  ( ( ( ph /\ ( d C_ N /\ e e. ( N \ d ) ) ) /\ b e. d ) -> [_ b / i ]_ X e. K )
80 1 2 3 maduf 
 |-  ( R e. CRing -> J : B --> B )
81 8 80 syl 
 |-  ( ph -> J : B --> B )
82 81 7 ffvelrnd 
 |-  ( ph -> ( J ` M ) e. B )
83 1 6 3 matbas2i 
 |-  ( ( J ` M ) e. B -> ( J ` M ) e. ( K ^m ( N X. N ) ) )
84 elmapi 
 |-  ( ( J ` M ) e. ( K ^m ( N X. N ) ) -> ( J ` M ) : ( N X. N ) --> K )
85 82 83 84 3syl 
 |-  ( ph -> ( J ` M ) : ( N X. N ) --> K )
86 85 ad2antrr 
 |-  ( ( ( ph /\ ( d C_ N /\ e e. ( N \ d ) ) ) /\ b e. d ) -> ( J ` M ) : ( N X. N ) --> K )
87 10 ad2antrr 
 |-  ( ( ( ph /\ ( d C_ N /\ e e. ( N \ d ) ) ) /\ b e. d ) -> L e. N )
88 86 75 87 fovrnd 
 |-  ( ( ( ph /\ ( d C_ N /\ e e. ( N \ d ) ) ) /\ b e. d ) -> ( b ( J ` M ) L ) e. K )
89 6 5 ringcl 
 |-  ( ( R e. Ring /\ [_ b / i ]_ X e. K /\ ( b ( J ` M ) L ) e. K ) -> ( [_ b / i ]_ X .x. ( b ( J ` M ) L ) ) e. K )
90 74 79 88 89 syl3anc 
 |-  ( ( ( ph /\ ( d C_ N /\ e e. ( N \ d ) ) ) /\ b e. d ) -> ( [_ b / i ]_ X .x. ( b ( J ` M ) L ) ) e. K )
91 vex 
 |-  e e. _V
92 91 a1i 
 |-  ( ( ph /\ ( d C_ N /\ e e. ( N \ d ) ) ) -> e e. _V )
93 eldifn 
 |-  ( e e. ( N \ d ) -> -. e e. d )
94 93 ad2antll 
 |-  ( ( ph /\ ( d C_ N /\ e e. ( N \ d ) ) ) -> -. e e. d )
95 eldifi 
 |-  ( e e. ( N \ d ) -> e e. N )
96 95 ad2antll 
 |-  ( ( ph /\ ( d C_ N /\ e e. ( N \ d ) ) ) -> e e. N )
97 76 adantr 
 |-  ( ( ph /\ ( d C_ N /\ e e. ( N \ d ) ) ) -> A. i e. N X e. K )
98 rspcsbela 
 |-  ( ( e e. N /\ A. i e. N X e. K ) -> [_ e / i ]_ X e. K )
99 96 97 98 syl2anc 
 |-  ( ( ph /\ ( d C_ N /\ e e. ( N \ d ) ) ) -> [_ e / i ]_ X e. K )
100 85 adantr 
 |-  ( ( ph /\ ( d C_ N /\ e e. ( N \ d ) ) ) -> ( J ` M ) : ( N X. N ) --> K )
101 10 adantr 
 |-  ( ( ph /\ ( d C_ N /\ e e. ( N \ d ) ) ) -> L e. N )
102 100 96 101 fovrnd 
 |-  ( ( ph /\ ( d C_ N /\ e e. ( N \ d ) ) ) -> ( e ( J ` M ) L ) e. K )
103 6 5 ringcl 
 |-  ( ( R e. Ring /\ [_ e / i ]_ X e. K /\ ( e ( J ` M ) L ) e. K ) -> ( [_ e / i ]_ X .x. ( e ( J ` M ) L ) ) e. K )
104 68 99 102 103 syl3anc 
 |-  ( ( ph /\ ( d C_ N /\ e e. ( N \ d ) ) ) -> ( [_ e / i ]_ X .x. ( e ( J ` M ) L ) ) e. K )
105 csbeq1 
 |-  ( b = e -> [_ b / i ]_ X = [_ e / i ]_ X )
106 oveq1 
 |-  ( b = e -> ( b ( J ` M ) L ) = ( e ( J ` M ) L ) )
107 105 106 oveq12d 
 |-  ( b = e -> ( [_ b / i ]_ X .x. ( b ( J ` M ) L ) ) = ( [_ e / i ]_ X .x. ( e ( J ` M ) L ) ) )
108 6 65 70 73 90 92 94 104 107 gsumunsn 
 |-  ( ( ph /\ ( d C_ N /\ e e. ( N \ d ) ) ) -> ( R gsum ( b e. ( d u. { e } ) |-> ( [_ b / i ]_ X .x. ( b ( J ` M ) L ) ) ) ) = ( ( R gsum ( b e. d |-> ( [_ b / i ]_ X .x. ( b ( J ` M ) L ) ) ) ) ( +g ` R ) ( [_ e / i ]_ X .x. ( e ( J ` M ) L ) ) ) )
109 108 adantr 
 |-  ( ( ( ph /\ ( d C_ N /\ e e. ( N \ d ) ) ) /\ ( R gsum ( b e. d |-> ( [_ b / i ]_ X .x. ( b ( J ` M ) L ) ) ) ) = ( D ` ( a e. N , b e. N |-> if ( a = L , if ( b e. d , [_ b / i ]_ X , ( 0g ` R ) ) , ( a M b ) ) ) ) ) -> ( R gsum ( b e. ( d u. { e } ) |-> ( [_ b / i ]_ X .x. ( b ( J ` M ) L ) ) ) ) = ( ( R gsum ( b e. d |-> ( [_ b / i ]_ X .x. ( b ( J ` M ) L ) ) ) ) ( +g ` R ) ( [_ e / i ]_ X .x. ( e ( J ` M ) L ) ) ) )
110 oveq1 
 |-  ( ( R gsum ( b e. d |-> ( [_ b / i ]_ X .x. ( b ( J ` M ) L ) ) ) ) = ( D ` ( a e. N , b e. N |-> if ( a = L , if ( b e. d , [_ b / i ]_ X , ( 0g ` R ) ) , ( a M b ) ) ) ) -> ( ( R gsum ( b e. d |-> ( [_ b / i ]_ X .x. ( b ( J ` M ) L ) ) ) ) ( +g ` R ) ( [_ e / i ]_ X .x. ( e ( J ` M ) L ) ) ) = ( ( D ` ( a e. N , b e. N |-> if ( a = L , if ( b e. d , [_ b / i ]_ X , ( 0g ` R ) ) , ( a M b ) ) ) ) ( +g ` R ) ( [_ e / i ]_ X .x. ( e ( J ` M ) L ) ) ) )
111 110 adantl 
 |-  ( ( ( ph /\ ( d C_ N /\ e e. ( N \ d ) ) ) /\ ( R gsum ( b e. d |-> ( [_ b / i ]_ X .x. ( b ( J ` M ) L ) ) ) ) = ( D ` ( a e. N , b e. N |-> if ( a = L , if ( b e. d , [_ b / i ]_ X , ( 0g ` R ) ) , ( a M b ) ) ) ) ) -> ( ( R gsum ( b e. d |-> ( [_ b / i ]_ X .x. ( b ( J ` M ) L ) ) ) ) ( +g ` R ) ( [_ e / i ]_ X .x. ( e ( J ` M ) L ) ) ) = ( ( D ` ( a e. N , b e. N |-> if ( a = L , if ( b e. d , [_ b / i ]_ X , ( 0g ` R ) ) , ( a M b ) ) ) ) ( +g ` R ) ( [_ e / i ]_ X .x. ( e ( J ` M ) L ) ) ) )
112 elun 
 |-  ( b e. ( d u. { e } ) <-> ( b e. d \/ b e. { e } ) )
113 velsn 
 |-  ( b e. { e } <-> b = e )
114 113 orbi2i 
 |-  ( ( b e. d \/ b e. { e } ) <-> ( b e. d \/ b = e ) )
115 112 114 bitri 
 |-  ( b e. ( d u. { e } ) <-> ( b e. d \/ b = e ) )
116 ifbi 
 |-  ( ( b e. ( d u. { e } ) <-> ( b e. d \/ b = e ) ) -> if ( b e. ( d u. { e } ) , [_ b / i ]_ X , ( 0g ` R ) ) = if ( ( b e. d \/ b = e ) , [_ b / i ]_ X , ( 0g ` R ) ) )
117 115 116 ax-mp 
 |-  if ( b e. ( d u. { e } ) , [_ b / i ]_ X , ( 0g ` R ) ) = if ( ( b e. d \/ b = e ) , [_ b / i ]_ X , ( 0g ` R ) )
118 ringmnd 
 |-  ( R e. Ring -> R e. Mnd )
119 68 118 syl 
 |-  ( ( ph /\ ( d C_ N /\ e e. ( N \ d ) ) ) -> R e. Mnd )
120 119 3ad2ant1 
 |-  ( ( ( ph /\ ( d C_ N /\ e e. ( N \ d ) ) ) /\ a e. N /\ b e. N ) -> R e. Mnd )
121 simp3 
 |-  ( ( ( ph /\ ( d C_ N /\ e e. ( N \ d ) ) ) /\ a e. N /\ b e. N ) -> b e. N )
122 97 3ad2ant1 
 |-  ( ( ( ph /\ ( d C_ N /\ e e. ( N \ d ) ) ) /\ a e. N /\ b e. N ) -> A. i e. N X e. K )
123 121 122 78 syl2anc 
 |-  ( ( ( ph /\ ( d C_ N /\ e e. ( N \ d ) ) ) /\ a e. N /\ b e. N ) -> [_ b / i ]_ X e. K )
124 elequ1 
 |-  ( b = e -> ( b e. d <-> e e. d ) )
125 124 biimpac 
 |-  ( ( b e. d /\ b = e ) -> e e. d )
126 94 125 nsyl 
 |-  ( ( ph /\ ( d C_ N /\ e e. ( N \ d ) ) ) -> -. ( b e. d /\ b = e ) )
127 126 3ad2ant1 
 |-  ( ( ( ph /\ ( d C_ N /\ e e. ( N \ d ) ) ) /\ a e. N /\ b e. N ) -> -. ( b e. d /\ b = e ) )
128 6 45 65 mndifsplit 
 |-  ( ( R e. Mnd /\ [_ b / i ]_ X e. K /\ -. ( b e. d /\ b = e ) ) -> if ( ( b e. d \/ b = e ) , [_ b / i ]_ X , ( 0g ` R ) ) = ( if ( b e. d , [_ b / i ]_ X , ( 0g ` R ) ) ( +g ` R ) if ( b = e , [_ b / i ]_ X , ( 0g ` R ) ) ) )
129 120 123 127 128 syl3anc 
 |-  ( ( ( ph /\ ( d C_ N /\ e e. ( N \ d ) ) ) /\ a e. N /\ b e. N ) -> if ( ( b e. d \/ b = e ) , [_ b / i ]_ X , ( 0g ` R ) ) = ( if ( b e. d , [_ b / i ]_ X , ( 0g ` R ) ) ( +g ` R ) if ( b = e , [_ b / i ]_ X , ( 0g ` R ) ) ) )
130 117 129 syl5eq 
 |-  ( ( ( ph /\ ( d C_ N /\ e e. ( N \ d ) ) ) /\ a e. N /\ b e. N ) -> if ( b e. ( d u. { e } ) , [_ b / i ]_ X , ( 0g ` R ) ) = ( if ( b e. d , [_ b / i ]_ X , ( 0g ` R ) ) ( +g ` R ) if ( b = e , [_ b / i ]_ X , ( 0g ` R ) ) ) )
131 105 adantl 
 |-  ( ( ( ph /\ ( d C_ N /\ e e. ( N \ d ) ) ) /\ b = e ) -> [_ b / i ]_ X = [_ e / i ]_ X )
132 131 ifeq1da 
 |-  ( ( ph /\ ( d C_ N /\ e e. ( N \ d ) ) ) -> if ( b = e , [_ b / i ]_ X , ( 0g ` R ) ) = if ( b = e , [_ e / i ]_ X , ( 0g ` R ) ) )
133 ovif2 
 |-  ( [_ e / i ]_ X .x. if ( b = e , ( 1r ` R ) , ( 0g ` R ) ) ) = if ( b = e , ( [_ e / i ]_ X .x. ( 1r ` R ) ) , ( [_ e / i ]_ X .x. ( 0g ` R ) ) )
134 eqid 
 |-  ( 1r ` R ) = ( 1r ` R )
135 6 5 134 ringridm 
 |-  ( ( R e. Ring /\ [_ e / i ]_ X e. K ) -> ( [_ e / i ]_ X .x. ( 1r ` R ) ) = [_ e / i ]_ X )
136 68 99 135 syl2anc 
 |-  ( ( ph /\ ( d C_ N /\ e e. ( N \ d ) ) ) -> ( [_ e / i ]_ X .x. ( 1r ` R ) ) = [_ e / i ]_ X )
137 6 5 45 ringrz 
 |-  ( ( R e. Ring /\ [_ e / i ]_ X e. K ) -> ( [_ e / i ]_ X .x. ( 0g ` R ) ) = ( 0g ` R ) )
138 68 99 137 syl2anc 
 |-  ( ( ph /\ ( d C_ N /\ e e. ( N \ d ) ) ) -> ( [_ e / i ]_ X .x. ( 0g ` R ) ) = ( 0g ` R ) )
139 136 138 ifeq12d 
 |-  ( ( ph /\ ( d C_ N /\ e e. ( N \ d ) ) ) -> if ( b = e , ( [_ e / i ]_ X .x. ( 1r ` R ) ) , ( [_ e / i ]_ X .x. ( 0g ` R ) ) ) = if ( b = e , [_ e / i ]_ X , ( 0g ` R ) ) )
140 133 139 syl5eq 
 |-  ( ( ph /\ ( d C_ N /\ e e. ( N \ d ) ) ) -> ( [_ e / i ]_ X .x. if ( b = e , ( 1r ` R ) , ( 0g ` R ) ) ) = if ( b = e , [_ e / i ]_ X , ( 0g ` R ) ) )
141 132 140 eqtr4d 
 |-  ( ( ph /\ ( d C_ N /\ e e. ( N \ d ) ) ) -> if ( b = e , [_ b / i ]_ X , ( 0g ` R ) ) = ( [_ e / i ]_ X .x. if ( b = e , ( 1r ` R ) , ( 0g ` R ) ) ) )
142 141 oveq2d 
 |-  ( ( ph /\ ( d C_ N /\ e e. ( N \ d ) ) ) -> ( if ( b e. d , [_ b / i ]_ X , ( 0g ` R ) ) ( +g ` R ) if ( b = e , [_ b / i ]_ X , ( 0g ` R ) ) ) = ( if ( b e. d , [_ b / i ]_ X , ( 0g ` R ) ) ( +g ` R ) ( [_ e / i ]_ X .x. if ( b = e , ( 1r ` R ) , ( 0g ` R ) ) ) ) )
143 142 3ad2ant1 
 |-  ( ( ( ph /\ ( d C_ N /\ e e. ( N \ d ) ) ) /\ a e. N /\ b e. N ) -> ( if ( b e. d , [_ b / i ]_ X , ( 0g ` R ) ) ( +g ` R ) if ( b = e , [_ b / i ]_ X , ( 0g ` R ) ) ) = ( if ( b e. d , [_ b / i ]_ X , ( 0g ` R ) ) ( +g ` R ) ( [_ e / i ]_ X .x. if ( b = e , ( 1r ` R ) , ( 0g ` R ) ) ) ) )
144 130 143 eqtrd 
 |-  ( ( ( ph /\ ( d C_ N /\ e e. ( N \ d ) ) ) /\ a e. N /\ b e. N ) -> if ( b e. ( d u. { e } ) , [_ b / i ]_ X , ( 0g ` R ) ) = ( if ( b e. d , [_ b / i ]_ X , ( 0g ` R ) ) ( +g ` R ) ( [_ e / i ]_ X .x. if ( b = e , ( 1r ` R ) , ( 0g ` R ) ) ) ) )
145 144 ifeq1d 
 |-  ( ( ( ph /\ ( d C_ N /\ e e. ( N \ d ) ) ) /\ a e. N /\ b e. N ) -> if ( a = L , if ( b e. ( d u. { e } ) , [_ b / i ]_ X , ( 0g ` R ) ) , ( a M b ) ) = if ( a = L , ( if ( b e. d , [_ b / i ]_ X , ( 0g ` R ) ) ( +g ` R ) ( [_ e / i ]_ X .x. if ( b = e , ( 1r ` R ) , ( 0g ` R ) ) ) ) , ( a M b ) ) )
146 145 mpoeq3dva 
 |-  ( ( ph /\ ( d C_ N /\ e e. ( N \ d ) ) ) -> ( a e. N , b e. N |-> if ( a = L , if ( b e. ( d u. { e } ) , [_ b / i ]_ X , ( 0g ` R ) ) , ( a M b ) ) ) = ( a e. N , b e. N |-> if ( a = L , ( if ( b e. d , [_ b / i ]_ X , ( 0g ` R ) ) ( +g ` R ) ( [_ e / i ]_ X .x. if ( b = e , ( 1r ` R ) , ( 0g ` R ) ) ) ) , ( a M b ) ) ) )
147 146 fveq2d 
 |-  ( ( ph /\ ( d C_ N /\ e e. ( N \ d ) ) ) -> ( D ` ( a e. N , b e. N |-> if ( a = L , if ( b e. ( d u. { e } ) , [_ b / i ]_ X , ( 0g ` R ) ) , ( a M b ) ) ) ) = ( D ` ( a e. N , b e. N |-> if ( a = L , ( if ( b e. d , [_ b / i ]_ X , ( 0g ` R ) ) ( +g ` R ) ( [_ e / i ]_ X .x. if ( b = e , ( 1r ` R ) , ( 0g ` R ) ) ) ) , ( a M b ) ) ) ) )
148 6 45 ring0cl 
 |-  ( R e. Ring -> ( 0g ` R ) e. K )
149 68 148 syl 
 |-  ( ( ph /\ ( d C_ N /\ e e. ( N \ d ) ) ) -> ( 0g ` R ) e. K )
150 149 3ad2ant1 
 |-  ( ( ( ph /\ ( d C_ N /\ e e. ( N \ d ) ) ) /\ a e. N /\ b e. N ) -> ( 0g ` R ) e. K )
151 123 150 ifcld 
 |-  ( ( ( ph /\ ( d C_ N /\ e e. ( N \ d ) ) ) /\ a e. N /\ b e. N ) -> if ( b e. d , [_ b / i ]_ X , ( 0g ` R ) ) e. K )
152 6 134 ringidcl 
 |-  ( R e. Ring -> ( 1r ` R ) e. K )
153 68 152 syl 
 |-  ( ( ph /\ ( d C_ N /\ e e. ( N \ d ) ) ) -> ( 1r ` R ) e. K )
154 153 149 ifcld 
 |-  ( ( ph /\ ( d C_ N /\ e e. ( N \ d ) ) ) -> if ( b = e , ( 1r ` R ) , ( 0g ` R ) ) e. K )
155 6 5 ringcl 
 |-  ( ( R e. Ring /\ [_ e / i ]_ X e. K /\ if ( b = e , ( 1r ` R ) , ( 0g ` R ) ) e. K ) -> ( [_ e / i ]_ X .x. if ( b = e , ( 1r ` R ) , ( 0g ` R ) ) ) e. K )
156 68 99 154 155 syl3anc 
 |-  ( ( ph /\ ( d C_ N /\ e e. ( N \ d ) ) ) -> ( [_ e / i ]_ X .x. if ( b = e , ( 1r ` R ) , ( 0g ` R ) ) ) e. K )
157 156 3ad2ant1 
 |-  ( ( ( ph /\ ( d C_ N /\ e e. ( N \ d ) ) ) /\ a e. N /\ b e. N ) -> ( [_ e / i ]_ X .x. if ( b = e , ( 1r ` R ) , ( 0g ` R ) ) ) e. K )
158 59 adantr 
 |-  ( ( ph /\ ( d C_ N /\ e e. ( N \ d ) ) ) -> M : ( N X. N ) --> K )
159 158 fovrnda 
 |-  ( ( ( ph /\ ( d C_ N /\ e e. ( N \ d ) ) ) /\ ( a e. N /\ b e. N ) ) -> ( a M b ) e. K )
160 159 3impb 
 |-  ( ( ( ph /\ ( d C_ N /\ e e. ( N \ d ) ) ) /\ a e. N /\ b e. N ) -> ( a M b ) e. K )
161 4 6 65 66 71 151 157 160 101 mdetrlin2 
 |-  ( ( ph /\ ( d C_ N /\ e e. ( N \ d ) ) ) -> ( D ` ( a e. N , b e. N |-> if ( a = L , ( if ( b e. d , [_ b / i ]_ X , ( 0g ` R ) ) ( +g ` R ) ( [_ e / i ]_ X .x. if ( b = e , ( 1r ` R ) , ( 0g ` R ) ) ) ) , ( a M b ) ) ) ) = ( ( D ` ( a e. N , b e. N |-> if ( a = L , if ( b e. d , [_ b / i ]_ X , ( 0g ` R ) ) , ( a M b ) ) ) ) ( +g ` R ) ( D ` ( a e. N , b e. N |-> if ( a = L , ( [_ e / i ]_ X .x. if ( b = e , ( 1r ` R ) , ( 0g ` R ) ) ) , ( a M b ) ) ) ) ) )
162 154 3ad2ant1 
 |-  ( ( ( ph /\ ( d C_ N /\ e e. ( N \ d ) ) ) /\ a e. N /\ b e. N ) -> if ( b = e , ( 1r ` R ) , ( 0g ` R ) ) e. K )
163 4 6 5 66 71 162 160 99 101 mdetrsca2 
 |-  ( ( ph /\ ( d C_ N /\ e e. ( N \ d ) ) ) -> ( D ` ( a e. N , b e. N |-> if ( a = L , ( [_ e / i ]_ X .x. if ( b = e , ( 1r ` R ) , ( 0g ` R ) ) ) , ( a M b ) ) ) ) = ( [_ e / i ]_ X .x. ( D ` ( a e. N , b e. N |-> if ( a = L , if ( b = e , ( 1r ` R ) , ( 0g ` R ) ) , ( a M b ) ) ) ) ) )
164 7 adantr 
 |-  ( ( ph /\ ( d C_ N /\ e e. ( N \ d ) ) ) -> M e. B )
165 1 4 2 3 134 45 maducoeval 
 |-  ( ( M e. B /\ e e. N /\ L e. N ) -> ( e ( J ` M ) L ) = ( D ` ( a e. N , b e. N |-> if ( a = L , if ( b = e , ( 1r ` R ) , ( 0g ` R ) ) , ( a M b ) ) ) ) )
166 164 96 101 165 syl3anc 
 |-  ( ( ph /\ ( d C_ N /\ e e. ( N \ d ) ) ) -> ( e ( J ` M ) L ) = ( D ` ( a e. N , b e. N |-> if ( a = L , if ( b = e , ( 1r ` R ) , ( 0g ` R ) ) , ( a M b ) ) ) ) )
167 166 oveq2d 
 |-  ( ( ph /\ ( d C_ N /\ e e. ( N \ d ) ) ) -> ( [_ e / i ]_ X .x. ( e ( J ` M ) L ) ) = ( [_ e / i ]_ X .x. ( D ` ( a e. N , b e. N |-> if ( a = L , if ( b = e , ( 1r ` R ) , ( 0g ` R ) ) , ( a M b ) ) ) ) ) )
168 163 167 eqtr4d 
 |-  ( ( ph /\ ( d C_ N /\ e e. ( N \ d ) ) ) -> ( D ` ( a e. N , b e. N |-> if ( a = L , ( [_ e / i ]_ X .x. if ( b = e , ( 1r ` R ) , ( 0g ` R ) ) ) , ( a M b ) ) ) ) = ( [_ e / i ]_ X .x. ( e ( J ` M ) L ) ) )
169 168 oveq2d 
 |-  ( ( ph /\ ( d C_ N /\ e e. ( N \ d ) ) ) -> ( ( D ` ( a e. N , b e. N |-> if ( a = L , if ( b e. d , [_ b / i ]_ X , ( 0g ` R ) ) , ( a M b ) ) ) ) ( +g ` R ) ( D ` ( a e. N , b e. N |-> if ( a = L , ( [_ e / i ]_ X .x. if ( b = e , ( 1r ` R ) , ( 0g ` R ) ) ) , ( a M b ) ) ) ) ) = ( ( D ` ( a e. N , b e. N |-> if ( a = L , if ( b e. d , [_ b / i ]_ X , ( 0g ` R ) ) , ( a M b ) ) ) ) ( +g ` R ) ( [_ e / i ]_ X .x. ( e ( J ` M ) L ) ) ) )
170 147 161 169 3eqtrrd 
 |-  ( ( ph /\ ( d C_ N /\ e e. ( N \ d ) ) ) -> ( ( D ` ( a e. N , b e. N |-> if ( a = L , if ( b e. d , [_ b / i ]_ X , ( 0g ` R ) ) , ( a M b ) ) ) ) ( +g ` R ) ( [_ e / i ]_ X .x. ( e ( J ` M ) L ) ) ) = ( D ` ( a e. N , b e. N |-> if ( a = L , if ( b e. ( d u. { e } ) , [_ b / i ]_ X , ( 0g ` R ) ) , ( a M b ) ) ) ) )
171 170 adantr 
 |-  ( ( ( ph /\ ( d C_ N /\ e e. ( N \ d ) ) ) /\ ( R gsum ( b e. d |-> ( [_ b / i ]_ X .x. ( b ( J ` M ) L ) ) ) ) = ( D ` ( a e. N , b e. N |-> if ( a = L , if ( b e. d , [_ b / i ]_ X , ( 0g ` R ) ) , ( a M b ) ) ) ) ) -> ( ( D ` ( a e. N , b e. N |-> if ( a = L , if ( b e. d , [_ b / i ]_ X , ( 0g ` R ) ) , ( a M b ) ) ) ) ( +g ` R ) ( [_ e / i ]_ X .x. ( e ( J ` M ) L ) ) ) = ( D ` ( a e. N , b e. N |-> if ( a = L , if ( b e. ( d u. { e } ) , [_ b / i ]_ X , ( 0g ` R ) ) , ( a M b ) ) ) ) )
172 109 111 171 3eqtrd 
 |-  ( ( ( ph /\ ( d C_ N /\ e e. ( N \ d ) ) ) /\ ( R gsum ( b e. d |-> ( [_ b / i ]_ X .x. ( b ( J ` M ) L ) ) ) ) = ( D ` ( a e. N , b e. N |-> if ( a = L , if ( b e. d , [_ b / i ]_ X , ( 0g ` R ) ) , ( a M b ) ) ) ) ) -> ( R gsum ( b e. ( d u. { e } ) |-> ( [_ b / i ]_ X .x. ( b ( J ` M ) L ) ) ) ) = ( D ` ( a e. N , b e. N |-> if ( a = L , if ( b e. ( d u. { e } ) , [_ b / i ]_ X , ( 0g ` R ) ) , ( a M b ) ) ) ) )
173 172 ex 
 |-  ( ( ph /\ ( d C_ N /\ e e. ( N \ d ) ) ) -> ( ( R gsum ( b e. d |-> ( [_ b / i ]_ X .x. ( b ( J ` M ) L ) ) ) ) = ( D ` ( a e. N , b e. N |-> if ( a = L , if ( b e. d , [_ b / i ]_ X , ( 0g ` R ) ) , ( a M b ) ) ) ) -> ( R gsum ( b e. ( d u. { e } ) |-> ( [_ b / i ]_ X .x. ( b ( J ` M ) L ) ) ) ) = ( D ` ( a e. N , b e. N |-> if ( a = L , if ( b e. ( d u. { e } ) , [_ b / i ]_ X , ( 0g ` R ) ) , ( a M b ) ) ) ) ) )
174 18 26 34 42 64 173 56 findcard2d 
 |-  ( ph -> ( R gsum ( b e. N |-> ( [_ b / i ]_ X .x. ( b ( J ` M ) L ) ) ) ) = ( D ` ( a e. N , b e. N |-> if ( a = L , if ( b e. N , [_ b / i ]_ X , ( 0g ` R ) ) , ( a M b ) ) ) ) )
175 nfcv 
 |-  F/_ b ( X .x. ( i ( J ` M ) L ) )
176 nfcsb1v 
 |-  F/_ i [_ b / i ]_ X
177 nfcv 
 |-  F/_ i .x.
178 nfcv 
 |-  F/_ i ( b ( J ` M ) L )
179 176 177 178 nfov 
 |-  F/_ i ( [_ b / i ]_ X .x. ( b ( J ` M ) L ) )
180 csbeq1a 
 |-  ( i = b -> X = [_ b / i ]_ X )
181 oveq1 
 |-  ( i = b -> ( i ( J ` M ) L ) = ( b ( J ` M ) L ) )
182 180 181 oveq12d 
 |-  ( i = b -> ( X .x. ( i ( J ` M ) L ) ) = ( [_ b / i ]_ X .x. ( b ( J ` M ) L ) ) )
183 175 179 182 cbvmpt 
 |-  ( i e. N |-> ( X .x. ( i ( J ` M ) L ) ) ) = ( b e. N |-> ( [_ b / i ]_ X .x. ( b ( J ` M ) L ) ) )
184 183 oveq2i 
 |-  ( R gsum ( i e. N |-> ( X .x. ( i ( J ` M ) L ) ) ) ) = ( R gsum ( b e. N |-> ( [_ b / i ]_ X .x. ( b ( J ` M ) L ) ) ) )
185 nfcv 
 |-  F/_ a if ( j = L , X , ( j M i ) )
186 nfcv 
 |-  F/_ b if ( j = L , X , ( j M i ) )
187 nfcv 
 |-  F/_ j if ( a = L , [_ b / i ]_ X , ( a M b ) )
188 nfv 
 |-  F/ i a = L
189 nfcv 
 |-  F/_ i ( a M b )
190 188 176 189 nfif 
 |-  F/_ i if ( a = L , [_ b / i ]_ X , ( a M b ) )
191 eqeq1 
 |-  ( j = a -> ( j = L <-> a = L ) )
192 191 adantr 
 |-  ( ( j = a /\ i = b ) -> ( j = L <-> a = L ) )
193 180 adantl 
 |-  ( ( j = a /\ i = b ) -> X = [_ b / i ]_ X )
194 oveq12 
 |-  ( ( j = a /\ i = b ) -> ( j M i ) = ( a M b ) )
195 192 193 194 ifbieq12d 
 |-  ( ( j = a /\ i = b ) -> if ( j = L , X , ( j M i ) ) = if ( a = L , [_ b / i ]_ X , ( a M b ) ) )
196 185 186 187 190 195 cbvmpo 
 |-  ( j e. N , i e. N |-> if ( j = L , X , ( j M i ) ) ) = ( a e. N , b e. N |-> if ( a = L , [_ b / i ]_ X , ( a M b ) ) )
197 iftrue 
 |-  ( b e. N -> if ( b e. N , [_ b / i ]_ X , ( 0g ` R ) ) = [_ b / i ]_ X )
198 197 eqcomd 
 |-  ( b e. N -> [_ b / i ]_ X = if ( b e. N , [_ b / i ]_ X , ( 0g ` R ) ) )
199 198 adantl 
 |-  ( ( a e. N /\ b e. N ) -> [_ b / i ]_ X = if ( b e. N , [_ b / i ]_ X , ( 0g ` R ) ) )
200 199 ifeq1d 
 |-  ( ( a e. N /\ b e. N ) -> if ( a = L , [_ b / i ]_ X , ( a M b ) ) = if ( a = L , if ( b e. N , [_ b / i ]_ X , ( 0g ` R ) ) , ( a M b ) ) )
201 200 mpoeq3ia 
 |-  ( a e. N , b e. N |-> if ( a = L , [_ b / i ]_ X , ( a M b ) ) ) = ( a e. N , b e. N |-> if ( a = L , if ( b e. N , [_ b / i ]_ X , ( 0g ` R ) ) , ( a M b ) ) )
202 196 201 eqtri 
 |-  ( j e. N , i e. N |-> if ( j = L , X , ( j M i ) ) ) = ( a e. N , b e. N |-> if ( a = L , if ( b e. N , [_ b / i ]_ X , ( 0g ` R ) ) , ( a M b ) ) )
203 202 fveq2i 
 |-  ( D ` ( j e. N , i e. N |-> if ( j = L , X , ( j M i ) ) ) ) = ( D ` ( a e. N , b e. N |-> if ( a = L , if ( b e. N , [_ b / i ]_ X , ( 0g ` R ) ) , ( a M b ) ) ) )
204 174 184 203 3eqtr4g 
 |-  ( ph -> ( R gsum ( i e. N |-> ( X .x. ( i ( J ` M ) L ) ) ) ) = ( D ` ( j e. N , i e. N |-> if ( j = L , X , ( j M i ) ) ) ) )