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	fovcdmda	\|- ( ( 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	eqtrid	\|- ( 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	ffvelcdmd	\|- ( 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	fovcdmd	\|- ( ( ( 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	fovcdmd	\|- ( ( 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	eqtrid	\|- ( ( ( 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	eqtrid	\|- ( ( 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	fovcdmda	\|- ( ( ( 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 ) ) ) ) )

Metamath Proof Explorer

Theorem madugsum

Proof