Metamath Proof Explorer

Theorem mdetmul

Description: Multiplicativity of the determinant function: the determinant of a matrix product of square matrices equals the product of their determinants. Proposition 4.15 in Lang p. 517. (Contributed by Stefan O'Rear, 16-Jul-2018)

Ref Expression
Hypotheses mdetmul.a 
|- A = ( N Mat R )
mdetmul.b 
|- B = ( Base ` A )
mdetmul.d 
|- D = ( N maDet R )
mdetmul.t1 
|- .x. = ( .r ` R )
mdetmul.t2 
|- .xb = ( .r ` A )
Assertion mdetmul 
|- ( ( R e. CRing /\ F e. B /\ G e. B ) -> ( D ` ( F .xb G ) ) = ( ( D ` F ) .x. ( D ` G ) ) )

Proof

Step Hyp Ref Expression
1 mdetmul.a 
 |-  A = ( N Mat R )
2 mdetmul.b 
 |-  B = ( Base ` A )
3 mdetmul.d 
 |-  D = ( N maDet R )
4 mdetmul.t1 
 |-  .x. = ( .r ` R )
5 mdetmul.t2 
 |-  .xb = ( .r ` A )
6 eqid 
 |-  ( Base ` R ) = ( Base ` R )
7 eqid 
 |-  ( 0g ` R ) = ( 0g ` R )
8 eqid 
 |-  ( 1r ` R ) = ( 1r ` R )
9 eqid 
 |-  ( +g ` R ) = ( +g ` R )
10 1 2 matrcl 
 |-  ( F e. B -> ( N e. Fin /\ R e. _V ) )
11 10 simpld 
 |-  ( F e. B -> N e. Fin )
12 11 3ad2ant2 
 |-  ( ( R e. CRing /\ F e. B /\ G e. B ) -> N e. Fin )
13 crngring 
 |-  ( R e. CRing -> R e. Ring )
14 13 3ad2ant1 
 |-  ( ( R e. CRing /\ F e. B /\ G e. B ) -> R e. Ring )
15 3 1 2 6 mdetf 
 |-  ( R e. CRing -> D : B --> ( Base ` R ) )
16 15 3ad2ant1 
 |-  ( ( R e. CRing /\ F e. B /\ G e. B ) -> D : B --> ( Base ` R ) )
17 16 adantr 
 |-  ( ( ( R e. CRing /\ F e. B /\ G e. B ) /\ a e. B ) -> D : B --> ( Base ` R ) )
18 1 matring 
 |-  ( ( N e. Fin /\ R e. Ring ) -> A e. Ring )
19 12 14 18 syl2anc 
 |-  ( ( R e. CRing /\ F e. B /\ G e. B ) -> A e. Ring )
20 19 adantr 
 |-  ( ( ( R e. CRing /\ F e. B /\ G e. B ) /\ a e. B ) -> A e. Ring )
21 simpr 
 |-  ( ( ( R e. CRing /\ F e. B /\ G e. B ) /\ a e. B ) -> a e. B )
22 simpl3 
 |-  ( ( ( R e. CRing /\ F e. B /\ G e. B ) /\ a e. B ) -> G e. B )
23 2 5 ringcl 
 |-  ( ( A e. Ring /\ a e. B /\ G e. B ) -> ( a .xb G ) e. B )
24 20 21 22 23 syl3anc 
 |-  ( ( ( R e. CRing /\ F e. B /\ G e. B ) /\ a e. B ) -> ( a .xb G ) e. B )
25 17 24 ffvelrnd 
 |-  ( ( ( R e. CRing /\ F e. B /\ G e. B ) /\ a e. B ) -> ( D ` ( a .xb G ) ) e. ( Base ` R ) )
26 25 fmpttd 
 |-  ( ( R e. CRing /\ F e. B /\ G e. B ) -> ( a e. B |-> ( D ` ( a .xb G ) ) ) : B --> ( Base ` R ) )
27 simp21 
 |-  ( ( ( R e. CRing /\ F e. B /\ G e. B ) /\ ( b e. B /\ c e. N /\ d e. N ) /\ ( c =/= d /\ A. e e. N ( c b e ) = ( d b e ) ) ) -> b e. B )
28 fvoveq1 
 |-  ( a = b -> ( D ` ( a .xb G ) ) = ( D ` ( b .xb G ) ) )
29 eqid 
 |-  ( a e. B |-> ( D ` ( a .xb G ) ) ) = ( a e. B |-> ( D ` ( a .xb G ) ) )
30 fvex 
 |-  ( D ` ( b .xb G ) ) e. _V
31 28 29 30 fvmpt 
 |-  ( b e. B -> ( ( a e. B |-> ( D ` ( a .xb G ) ) ) ` b ) = ( D ` ( b .xb G ) ) )
32 27 31 syl 
 |-  ( ( ( R e. CRing /\ F e. B /\ G e. B ) /\ ( b e. B /\ c e. N /\ d e. N ) /\ ( c =/= d /\ A. e e. N ( c b e ) = ( d b e ) ) ) -> ( ( a e. B |-> ( D ` ( a .xb G ) ) ) ` b ) = ( D ` ( b .xb G ) ) )
33 simp11 
 |-  ( ( ( R e. CRing /\ F e. B /\ G e. B ) /\ ( b e. B /\ c e. N /\ d e. N ) /\ ( c =/= d /\ A. e e. N ( c b e ) = ( d b e ) ) ) -> R e. CRing )
34 19 adantr 
 |-  ( ( ( R e. CRing /\ F e. B /\ G e. B ) /\ ( b e. B /\ c e. N /\ d e. N ) ) -> A e. Ring )
35 simpr1 
 |-  ( ( ( R e. CRing /\ F e. B /\ G e. B ) /\ ( b e. B /\ c e. N /\ d e. N ) ) -> b e. B )
36 simpl3 
 |-  ( ( ( R e. CRing /\ F e. B /\ G e. B ) /\ ( b e. B /\ c e. N /\ d e. N ) ) -> G e. B )
37 2 5 ringcl 
 |-  ( ( A e. Ring /\ b e. B /\ G e. B ) -> ( b .xb G ) e. B )
38 34 35 36 37 syl3anc 
 |-  ( ( ( R e. CRing /\ F e. B /\ G e. B ) /\ ( b e. B /\ c e. N /\ d e. N ) ) -> ( b .xb G ) e. B )
39 38 3adant3 
 |-  ( ( ( R e. CRing /\ F e. B /\ G e. B ) /\ ( b e. B /\ c e. N /\ d e. N ) /\ ( c =/= d /\ A. e e. N ( c b e ) = ( d b e ) ) ) -> ( b .xb G ) e. B )
40 simp22 
 |-  ( ( ( R e. CRing /\ F e. B /\ G e. B ) /\ ( b e. B /\ c e. N /\ d e. N ) /\ ( c =/= d /\ A. e e. N ( c b e ) = ( d b e ) ) ) -> c e. N )
41 simp23 
 |-  ( ( ( R e. CRing /\ F e. B /\ G e. B ) /\ ( b e. B /\ c e. N /\ d e. N ) /\ ( c =/= d /\ A. e e. N ( c b e ) = ( d b e ) ) ) -> d e. N )
42 simp3l 
 |-  ( ( ( R e. CRing /\ F e. B /\ G e. B ) /\ ( b e. B /\ c e. N /\ d e. N ) /\ ( c =/= d /\ A. e e. N ( c b e ) = ( d b e ) ) ) -> c =/= d )
43 simpl3r 
 |-  ( ( ( ( R e. CRing /\ F e. B /\ G e. B ) /\ ( b e. B /\ c e. N /\ d e. N ) /\ ( c =/= d /\ A. e e. N ( c b e ) = ( d b e ) ) ) /\ a e. N ) -> A. e e. N ( c b e ) = ( d b e ) )
44 eqid 
 |-  N = N
45 oveq1 
 |-  ( ( c b e ) = ( d b e ) -> ( ( c b e ) .x. ( e G a ) ) = ( ( d b e ) .x. ( e G a ) ) )
46 45 ralimi 
 |-  ( A. e e. N ( c b e ) = ( d b e ) -> A. e e. N ( ( c b e ) .x. ( e G a ) ) = ( ( d b e ) .x. ( e G a ) ) )
47 mpteq12 
 |-  ( ( N = N /\ A. e e. N ( ( c b e ) .x. ( e G a ) ) = ( ( d b e ) .x. ( e G a ) ) ) -> ( e e. N |-> ( ( c b e ) .x. ( e G a ) ) ) = ( e e. N |-> ( ( d b e ) .x. ( e G a ) ) ) )
48 44 46 47 sylancr 
 |-  ( A. e e. N ( c b e ) = ( d b e ) -> ( e e. N |-> ( ( c b e ) .x. ( e G a ) ) ) = ( e e. N |-> ( ( d b e ) .x. ( e G a ) ) ) )
49 48 oveq2d 
 |-  ( A. e e. N ( c b e ) = ( d b e ) -> ( R gsum ( e e. N |-> ( ( c b e ) .x. ( e G a ) ) ) ) = ( R gsum ( e e. N |-> ( ( d b e ) .x. ( e G a ) ) ) ) )
50 43 49 syl 
 |-  ( ( ( ( R e. CRing /\ F e. B /\ G e. B ) /\ ( b e. B /\ c e. N /\ d e. N ) /\ ( c =/= d /\ A. e e. N ( c b e ) = ( d b e ) ) ) /\ a e. N ) -> ( R gsum ( e e. N |-> ( ( c b e ) .x. ( e G a ) ) ) ) = ( R gsum ( e e. N |-> ( ( d b e ) .x. ( e G a ) ) ) ) )
51 simp1 
 |-  ( ( R e. CRing /\ F e. B /\ G e. B ) -> R e. CRing )
52 eqid 
 |-  ( R maMul <. N , N , N >. ) = ( R maMul <. N , N , N >. )
53 1 52 matmulr 
 |-  ( ( N e. Fin /\ R e. CRing ) -> ( R maMul <. N , N , N >. ) = ( .r ` A ) )
54 53 5 eqtr4di 
 |-  ( ( N e. Fin /\ R e. CRing ) -> ( R maMul <. N , N , N >. ) = .xb )
55 12 51 54 syl2anc 
 |-  ( ( R e. CRing /\ F e. B /\ G e. B ) -> ( R maMul <. N , N , N >. ) = .xb )
56 55 ad2antrr 
 |-  ( ( ( ( R e. CRing /\ F e. B /\ G e. B ) /\ ( b e. B /\ c e. N /\ d e. N ) ) /\ a e. N ) -> ( R maMul <. N , N , N >. ) = .xb )
57 56 oveqd 
 |-  ( ( ( ( R e. CRing /\ F e. B /\ G e. B ) /\ ( b e. B /\ c e. N /\ d e. N ) ) /\ a e. N ) -> ( b ( R maMul <. N , N , N >. ) G ) = ( b .xb G ) )
58 57 oveqd 
 |-  ( ( ( ( R e. CRing /\ F e. B /\ G e. B ) /\ ( b e. B /\ c e. N /\ d e. N ) ) /\ a e. N ) -> ( c ( b ( R maMul <. N , N , N >. ) G ) a ) = ( c ( b .xb G ) a ) )
59 simpll1 
 |-  ( ( ( ( R e. CRing /\ F e. B /\ G e. B ) /\ ( b e. B /\ c e. N /\ d e. N ) ) /\ a e. N ) -> R e. CRing )
60 12 ad2antrr 
 |-  ( ( ( ( R e. CRing /\ F e. B /\ G e. B ) /\ ( b e. B /\ c e. N /\ d e. N ) ) /\ a e. N ) -> N e. Fin )
61 simplr1 
 |-  ( ( ( ( R e. CRing /\ F e. B /\ G e. B ) /\ ( b e. B /\ c e. N /\ d e. N ) ) /\ a e. N ) -> b e. B )
62 1 6 2 matbas2i 
 |-  ( b e. B -> b e. ( ( Base ` R ) ^m ( N X. N ) ) )
63 61 62 syl 
 |-  ( ( ( ( R e. CRing /\ F e. B /\ G e. B ) /\ ( b e. B /\ c e. N /\ d e. N ) ) /\ a e. N ) -> b e. ( ( Base ` R ) ^m ( N X. N ) ) )
64 1 6 2 matbas2i 
 |-  ( G e. B -> G e. ( ( Base ` R ) ^m ( N X. N ) ) )
65 64 3ad2ant3 
 |-  ( ( R e. CRing /\ F e. B /\ G e. B ) -> G e. ( ( Base ` R ) ^m ( N X. N ) ) )
66 65 ad2antrr 
 |-  ( ( ( ( R e. CRing /\ F e. B /\ G e. B ) /\ ( b e. B /\ c e. N /\ d e. N ) ) /\ a e. N ) -> G e. ( ( Base ` R ) ^m ( N X. N ) ) )
67 simplr2 
 |-  ( ( ( ( R e. CRing /\ F e. B /\ G e. B ) /\ ( b e. B /\ c e. N /\ d e. N ) ) /\ a e. N ) -> c e. N )
68 simpr 
 |-  ( ( ( ( R e. CRing /\ F e. B /\ G e. B ) /\ ( b e. B /\ c e. N /\ d e. N ) ) /\ a e. N ) -> a e. N )
69 52 6 4 59 60 60 60 63 66 67 68 mamufv 
 |-  ( ( ( ( R e. CRing /\ F e. B /\ G e. B ) /\ ( b e. B /\ c e. N /\ d e. N ) ) /\ a e. N ) -> ( c ( b ( R maMul <. N , N , N >. ) G ) a ) = ( R gsum ( e e. N |-> ( ( c b e ) .x. ( e G a ) ) ) ) )
70 58 69 eqtr3d 
 |-  ( ( ( ( R e. CRing /\ F e. B /\ G e. B ) /\ ( b e. B /\ c e. N /\ d e. N ) ) /\ a e. N ) -> ( c ( b .xb G ) a ) = ( R gsum ( e e. N |-> ( ( c b e ) .x. ( e G a ) ) ) ) )
71 70 3adantl3 
 |-  ( ( ( ( R e. CRing /\ F e. B /\ G e. B ) /\ ( b e. B /\ c e. N /\ d e. N ) /\ ( c =/= d /\ A. e e. N ( c b e ) = ( d b e ) ) ) /\ a e. N ) -> ( c ( b .xb G ) a ) = ( R gsum ( e e. N |-> ( ( c b e ) .x. ( e G a ) ) ) ) )
72 57 oveqd 
 |-  ( ( ( ( R e. CRing /\ F e. B /\ G e. B ) /\ ( b e. B /\ c e. N /\ d e. N ) ) /\ a e. N ) -> ( d ( b ( R maMul <. N , N , N >. ) G ) a ) = ( d ( b .xb G ) a ) )
73 simplr3 
 |-  ( ( ( ( R e. CRing /\ F e. B /\ G e. B ) /\ ( b e. B /\ c e. N /\ d e. N ) ) /\ a e. N ) -> d e. N )
74 52 6 4 59 60 60 60 63 66 73 68 mamufv 
 |-  ( ( ( ( R e. CRing /\ F e. B /\ G e. B ) /\ ( b e. B /\ c e. N /\ d e. N ) ) /\ a e. N ) -> ( d ( b ( R maMul <. N , N , N >. ) G ) a ) = ( R gsum ( e e. N |-> ( ( d b e ) .x. ( e G a ) ) ) ) )
75 72 74 eqtr3d 
 |-  ( ( ( ( R e. CRing /\ F e. B /\ G e. B ) /\ ( b e. B /\ c e. N /\ d e. N ) ) /\ a e. N ) -> ( d ( b .xb G ) a ) = ( R gsum ( e e. N |-> ( ( d b e ) .x. ( e G a ) ) ) ) )
76 75 3adantl3 
 |-  ( ( ( ( R e. CRing /\ F e. B /\ G e. B ) /\ ( b e. B /\ c e. N /\ d e. N ) /\ ( c =/= d /\ A. e e. N ( c b e ) = ( d b e ) ) ) /\ a e. N ) -> ( d ( b .xb G ) a ) = ( R gsum ( e e. N |-> ( ( d b e ) .x. ( e G a ) ) ) ) )
77 50 71 76 3eqtr4d 
 |-  ( ( ( ( R e. CRing /\ F e. B /\ G e. B ) /\ ( b e. B /\ c e. N /\ d e. N ) /\ ( c =/= d /\ A. e e. N ( c b e ) = ( d b e ) ) ) /\ a e. N ) -> ( c ( b .xb G ) a ) = ( d ( b .xb G ) a ) )
78 77 ralrimiva 
 |-  ( ( ( R e. CRing /\ F e. B /\ G e. B ) /\ ( b e. B /\ c e. N /\ d e. N ) /\ ( c =/= d /\ A. e e. N ( c b e ) = ( d b e ) ) ) -> A. a e. N ( c ( b .xb G ) a ) = ( d ( b .xb G ) a ) )
79 3 1 2 7 33 39 40 41 42 78 mdetralt 
 |-  ( ( ( R e. CRing /\ F e. B /\ G e. B ) /\ ( b e. B /\ c e. N /\ d e. N ) /\ ( c =/= d /\ A. e e. N ( c b e ) = ( d b e ) ) ) -> ( D ` ( b .xb G ) ) = ( 0g ` R ) )
80 32 79 eqtrd 
 |-  ( ( ( R e. CRing /\ F e. B /\ G e. B ) /\ ( b e. B /\ c e. N /\ d e. N ) /\ ( c =/= d /\ A. e e. N ( c b e ) = ( d b e ) ) ) -> ( ( a e. B |-> ( D ` ( a .xb G ) ) ) ` b ) = ( 0g ` R ) )
81 80 3expia 
 |-  ( ( ( R e. CRing /\ F e. B /\ G e. B ) /\ ( b e. B /\ c e. N /\ d e. N ) ) -> ( ( c =/= d /\ A. e e. N ( c b e ) = ( d b e ) ) -> ( ( a e. B |-> ( D ` ( a .xb G ) ) ) ` b ) = ( 0g ` R ) ) )
82 81 ralrimivvva 
 |-  ( ( R e. CRing /\ F e. B /\ G e. B ) -> A. b e. B A. c e. N A. d e. N ( ( c =/= d /\ A. e e. N ( c b e ) = ( d b e ) ) -> ( ( a e. B |-> ( D ` ( a .xb G ) ) ) ` b ) = ( 0g ` R ) ) )
83 simp11 
 |-  ( ( ( R e. CRing /\ F e. B /\ G e. B ) /\ ( ( b e. B /\ c e. B ) /\ ( d e. B /\ e e. N ) ) /\ ( ( b |` ( { e } X. N ) ) = ( ( c |` ( { e } X. N ) ) oF ( +g ` R ) ( d |` ( { e } X. N ) ) ) /\ ( b |` ( ( N \ { e } ) X. N ) ) = ( c |` ( ( N \ { e } ) X. N ) ) /\ ( b |` ( ( N \ { e } ) X. N ) ) = ( d |` ( ( N \ { e } ) X. N ) ) ) ) -> R e. CRing )
84 19 adantr 
 |-  ( ( ( R e. CRing /\ F e. B /\ G e. B ) /\ ( ( b e. B /\ c e. B ) /\ ( d e. B /\ e e. N ) ) ) -> A e. Ring )
85 simprll 
 |-  ( ( ( R e. CRing /\ F e. B /\ G e. B ) /\ ( ( b e. B /\ c e. B ) /\ ( d e. B /\ e e. N ) ) ) -> b e. B )
86 simpl3 
 |-  ( ( ( R e. CRing /\ F e. B /\ G e. B ) /\ ( ( b e. B /\ c e. B ) /\ ( d e. B /\ e e. N ) ) ) -> G e. B )
87 84 85 86 37 syl3anc 
 |-  ( ( ( R e. CRing /\ F e. B /\ G e. B ) /\ ( ( b e. B /\ c e. B ) /\ ( d e. B /\ e e. N ) ) ) -> ( b .xb G ) e. B )
88 87 3adant3 
 |-  ( ( ( R e. CRing /\ F e. B /\ G e. B ) /\ ( ( b e. B /\ c e. B ) /\ ( d e. B /\ e e. N ) ) /\ ( ( b |` ( { e } X. N ) ) = ( ( c |` ( { e } X. N ) ) oF ( +g ` R ) ( d |` ( { e } X. N ) ) ) /\ ( b |` ( ( N \ { e } ) X. N ) ) = ( c |` ( ( N \ { e } ) X. N ) ) /\ ( b |` ( ( N \ { e } ) X. N ) ) = ( d |` ( ( N \ { e } ) X. N ) ) ) ) -> ( b .xb G ) e. B )
89 simprlr 
 |-  ( ( ( R e. CRing /\ F e. B /\ G e. B ) /\ ( ( b e. B /\ c e. B ) /\ ( d e. B /\ e e. N ) ) ) -> c e. B )
90 2 5 ringcl 
 |-  ( ( A e. Ring /\ c e. B /\ G e. B ) -> ( c .xb G ) e. B )
91 84 89 86 90 syl3anc 
 |-  ( ( ( R e. CRing /\ F e. B /\ G e. B ) /\ ( ( b e. B /\ c e. B ) /\ ( d e. B /\ e e. N ) ) ) -> ( c .xb G ) e. B )
92 91 3adant3 
 |-  ( ( ( R e. CRing /\ F e. B /\ G e. B ) /\ ( ( b e. B /\ c e. B ) /\ ( d e. B /\ e e. N ) ) /\ ( ( b |` ( { e } X. N ) ) = ( ( c |` ( { e } X. N ) ) oF ( +g ` R ) ( d |` ( { e } X. N ) ) ) /\ ( b |` ( ( N \ { e } ) X. N ) ) = ( c |` ( ( N \ { e } ) X. N ) ) /\ ( b |` ( ( N \ { e } ) X. N ) ) = ( d |` ( ( N \ { e } ) X. N ) ) ) ) -> ( c .xb G ) e. B )
93 simprrl 
 |-  ( ( ( R e. CRing /\ F e. B /\ G e. B ) /\ ( ( b e. B /\ c e. B ) /\ ( d e. B /\ e e. N ) ) ) -> d e. B )
94 2 5 ringcl 
 |-  ( ( A e. Ring /\ d e. B /\ G e. B ) -> ( d .xb G ) e. B )
95 84 93 86 94 syl3anc 
 |-  ( ( ( R e. CRing /\ F e. B /\ G e. B ) /\ ( ( b e. B /\ c e. B ) /\ ( d e. B /\ e e. N ) ) ) -> ( d .xb G ) e. B )
96 95 3adant3 
 |-  ( ( ( R e. CRing /\ F e. B /\ G e. B ) /\ ( ( b e. B /\ c e. B ) /\ ( d e. B /\ e e. N ) ) /\ ( ( b |` ( { e } X. N ) ) = ( ( c |` ( { e } X. N ) ) oF ( +g ` R ) ( d |` ( { e } X. N ) ) ) /\ ( b |` ( ( N \ { e } ) X. N ) ) = ( c |` ( ( N \ { e } ) X. N ) ) /\ ( b |` ( ( N \ { e } ) X. N ) ) = ( d |` ( ( N \ { e } ) X. N ) ) ) ) -> ( d .xb G ) e. B )
97 simp2rr 
 |-  ( ( ( R e. CRing /\ F e. B /\ G e. B ) /\ ( ( b e. B /\ c e. B ) /\ ( d e. B /\ e e. N ) ) /\ ( ( b |` ( { e } X. N ) ) = ( ( c |` ( { e } X. N ) ) oF ( +g ` R ) ( d |` ( { e } X. N ) ) ) /\ ( b |` ( ( N \ { e } ) X. N ) ) = ( c |` ( ( N \ { e } ) X. N ) ) /\ ( b |` ( ( N \ { e } ) X. N ) ) = ( d |` ( ( N \ { e } ) X. N ) ) ) ) -> e e. N )
98 simp31 
 |-  ( ( ( R e. CRing /\ F e. B /\ G e. B ) /\ ( ( b e. B /\ c e. B ) /\ ( d e. B /\ e e. N ) ) /\ ( ( b |` ( { e } X. N ) ) = ( ( c |` ( { e } X. N ) ) oF ( +g ` R ) ( d |` ( { e } X. N ) ) ) /\ ( b |` ( ( N \ { e } ) X. N ) ) = ( c |` ( ( N \ { e } ) X. N ) ) /\ ( b |` ( ( N \ { e } ) X. N ) ) = ( d |` ( ( N \ { e } ) X. N ) ) ) ) -> ( b |` ( { e } X. N ) ) = ( ( c |` ( { e } X. N ) ) oF ( +g ` R ) ( d |` ( { e } X. N ) ) ) )
99 98 oveq1d 
 |-  ( ( ( R e. CRing /\ F e. B /\ G e. B ) /\ ( ( b e. B /\ c e. B ) /\ ( d e. B /\ e e. N ) ) /\ ( ( b |` ( { e } X. N ) ) = ( ( c |` ( { e } X. N ) ) oF ( +g ` R ) ( d |` ( { e } X. N ) ) ) /\ ( b |` ( ( N \ { e } ) X. N ) ) = ( c |` ( ( N \ { e } ) X. N ) ) /\ ( b |` ( ( N \ { e } ) X. N ) ) = ( d |` ( ( N \ { e } ) X. N ) ) ) ) -> ( ( b |` ( { e } X. N ) ) ( R maMul <. { e } , N , N >. ) G ) = ( ( ( c |` ( { e } X. N ) ) oF ( +g ` R ) ( d |` ( { e } X. N ) ) ) ( R maMul <. { e } , N , N >. ) G ) )
100 14 adantr 
 |-  ( ( ( R e. CRing /\ F e. B /\ G e. B ) /\ ( ( b e. B /\ c e. B ) /\ ( d e. B /\ e e. N ) ) ) -> R e. Ring )
101 eqid 
 |-  ( R maMul <. { e } , N , N >. ) = ( R maMul <. { e } , N , N >. )
102 snfi 
 |-  { e } e. Fin
103 102 a1i 
 |-  ( ( ( R e. CRing /\ F e. B /\ G e. B ) /\ ( ( b e. B /\ c e. B ) /\ ( d e. B /\ e e. N ) ) ) -> { e } e. Fin )
104 12 adantr 
 |-  ( ( ( R e. CRing /\ F e. B /\ G e. B ) /\ ( ( b e. B /\ c e. B ) /\ ( d e. B /\ e e. N ) ) ) -> N e. Fin )
105 1 6 2 matbas2i 
 |-  ( c e. B -> c e. ( ( Base ` R ) ^m ( N X. N ) ) )
106 89 105 syl 
 |-  ( ( ( R e. CRing /\ F e. B /\ G e. B ) /\ ( ( b e. B /\ c e. B ) /\ ( d e. B /\ e e. N ) ) ) -> c e. ( ( Base ` R ) ^m ( N X. N ) ) )
107 simprrr 
 |-  ( ( ( R e. CRing /\ F e. B /\ G e. B ) /\ ( ( b e. B /\ c e. B ) /\ ( d e. B /\ e e. N ) ) ) -> e e. N )
108 107 snssd 
 |-  ( ( ( R e. CRing /\ F e. B /\ G e. B ) /\ ( ( b e. B /\ c e. B ) /\ ( d e. B /\ e e. N ) ) ) -> { e } C_ N )
109 xpss1 
 |-  ( { e } C_ N -> ( { e } X. N ) C_ ( N X. N ) )
110 108 109 syl 
 |-  ( ( ( R e. CRing /\ F e. B /\ G e. B ) /\ ( ( b e. B /\ c e. B ) /\ ( d e. B /\ e e. N ) ) ) -> ( { e } X. N ) C_ ( N X. N ) )
111 elmapssres 
 |-  ( ( c e. ( ( Base ` R ) ^m ( N X. N ) ) /\ ( { e } X. N ) C_ ( N X. N ) ) -> ( c |` ( { e } X. N ) ) e. ( ( Base ` R ) ^m ( { e } X. N ) ) )
112 106 110 111 syl2anc 
 |-  ( ( ( R e. CRing /\ F e. B /\ G e. B ) /\ ( ( b e. B /\ c e. B ) /\ ( d e. B /\ e e. N ) ) ) -> ( c |` ( { e } X. N ) ) e. ( ( Base ` R ) ^m ( { e } X. N ) ) )
113 1 6 2 matbas2i 
 |-  ( d e. B -> d e. ( ( Base ` R ) ^m ( N X. N ) ) )
114 93 113 syl 
 |-  ( ( ( R e. CRing /\ F e. B /\ G e. B ) /\ ( ( b e. B /\ c e. B ) /\ ( d e. B /\ e e. N ) ) ) -> d e. ( ( Base ` R ) ^m ( N X. N ) ) )
115 elmapssres 
 |-  ( ( d e. ( ( Base ` R ) ^m ( N X. N ) ) /\ ( { e } X. N ) C_ ( N X. N ) ) -> ( d |` ( { e } X. N ) ) e. ( ( Base ` R ) ^m ( { e } X. N ) ) )
116 114 110 115 syl2anc 
 |-  ( ( ( R e. CRing /\ F e. B /\ G e. B ) /\ ( ( b e. B /\ c e. B ) /\ ( d e. B /\ e e. N ) ) ) -> ( d |` ( { e } X. N ) ) e. ( ( Base ` R ) ^m ( { e } X. N ) ) )
117 65 adantr 
 |-  ( ( ( R e. CRing /\ F e. B /\ G e. B ) /\ ( ( b e. B /\ c e. B ) /\ ( d e. B /\ e e. N ) ) ) -> G e. ( ( Base ` R ) ^m ( N X. N ) ) )
118 6 100 101 103 104 104 9 112 116 117 mamudi 
 |-  ( ( ( R e. CRing /\ F e. B /\ G e. B ) /\ ( ( b e. B /\ c e. B ) /\ ( d e. B /\ e e. N ) ) ) -> ( ( ( c |` ( { e } X. N ) ) oF ( +g ` R ) ( d |` ( { e } X. N ) ) ) ( R maMul <. { e } , N , N >. ) G ) = ( ( ( c |` ( { e } X. N ) ) ( R maMul <. { e } , N , N >. ) G ) oF ( +g ` R ) ( ( d |` ( { e } X. N ) ) ( R maMul <. { e } , N , N >. ) G ) ) )
119 118 3adant3 
 |-  ( ( ( R e. CRing /\ F e. B /\ G e. B ) /\ ( ( b e. B /\ c e. B ) /\ ( d e. B /\ e e. N ) ) /\ ( ( b |` ( { e } X. N ) ) = ( ( c |` ( { e } X. N ) ) oF ( +g ` R ) ( d |` ( { e } X. N ) ) ) /\ ( b |` ( ( N \ { e } ) X. N ) ) = ( c |` ( ( N \ { e } ) X. N ) ) /\ ( b |` ( ( N \ { e } ) X. N ) ) = ( d |` ( ( N \ { e } ) X. N ) ) ) ) -> ( ( ( c |` ( { e } X. N ) ) oF ( +g ` R ) ( d |` ( { e } X. N ) ) ) ( R maMul <. { e } , N , N >. ) G ) = ( ( ( c |` ( { e } X. N ) ) ( R maMul <. { e } , N , N >. ) G ) oF ( +g ` R ) ( ( d |` ( { e } X. N ) ) ( R maMul <. { e } , N , N >. ) G ) ) )
120 99 119 eqtrd 
 |-  ( ( ( R e. CRing /\ F e. B /\ G e. B ) /\ ( ( b e. B /\ c e. B ) /\ ( d e. B /\ e e. N ) ) /\ ( ( b |` ( { e } X. N ) ) = ( ( c |` ( { e } X. N ) ) oF ( +g ` R ) ( d |` ( { e } X. N ) ) ) /\ ( b |` ( ( N \ { e } ) X. N ) ) = ( c |` ( ( N \ { e } ) X. N ) ) /\ ( b |` ( ( N \ { e } ) X. N ) ) = ( d |` ( ( N \ { e } ) X. N ) ) ) ) -> ( ( b |` ( { e } X. N ) ) ( R maMul <. { e } , N , N >. ) G ) = ( ( ( c |` ( { e } X. N ) ) ( R maMul <. { e } , N , N >. ) G ) oF ( +g ` R ) ( ( d |` ( { e } X. N ) ) ( R maMul <. { e } , N , N >. ) G ) ) )
121 55 adantr 
 |-  ( ( ( R e. CRing /\ F e. B /\ G e. B ) /\ ( ( b e. B /\ c e. B ) /\ ( d e. B /\ e e. N ) ) ) -> ( R maMul <. N , N , N >. ) = .xb )
122 121 oveqd 
 |-  ( ( ( R e. CRing /\ F e. B /\ G e. B ) /\ ( ( b e. B /\ c e. B ) /\ ( d e. B /\ e e. N ) ) ) -> ( b ( R maMul <. N , N , N >. ) G ) = ( b .xb G ) )
123 122 reseq1d 
 |-  ( ( ( R e. CRing /\ F e. B /\ G e. B ) /\ ( ( b e. B /\ c e. B ) /\ ( d e. B /\ e e. N ) ) ) -> ( ( b ( R maMul <. N , N , N >. ) G ) |` ( { e } X. N ) ) = ( ( b .xb G ) |` ( { e } X. N ) ) )
124 simpl1 
 |-  ( ( ( R e. CRing /\ F e. B /\ G e. B ) /\ ( ( b e. B /\ c e. B ) /\ ( d e. B /\ e e. N ) ) ) -> R e. CRing )
125 85 62 syl 
 |-  ( ( ( R e. CRing /\ F e. B /\ G e. B ) /\ ( ( b e. B /\ c e. B ) /\ ( d e. B /\ e e. N ) ) ) -> b e. ( ( Base ` R ) ^m ( N X. N ) ) )
126 52 101 6 124 104 104 104 108 125 117 mamures 
 |-  ( ( ( R e. CRing /\ F e. B /\ G e. B ) /\ ( ( b e. B /\ c e. B ) /\ ( d e. B /\ e e. N ) ) ) -> ( ( b ( R maMul <. N , N , N >. ) G ) |` ( { e } X. N ) ) = ( ( b |` ( { e } X. N ) ) ( R maMul <. { e } , N , N >. ) G ) )
127 123 126 eqtr3d 
 |-  ( ( ( R e. CRing /\ F e. B /\ G e. B ) /\ ( ( b e. B /\ c e. B ) /\ ( d e. B /\ e e. N ) ) ) -> ( ( b .xb G ) |` ( { e } X. N ) ) = ( ( b |` ( { e } X. N ) ) ( R maMul <. { e } , N , N >. ) G ) )
128 127 3adant3 
 |-  ( ( ( R e. CRing /\ F e. B /\ G e. B ) /\ ( ( b e. B /\ c e. B ) /\ ( d e. B /\ e e. N ) ) /\ ( ( b |` ( { e } X. N ) ) = ( ( c |` ( { e } X. N ) ) oF ( +g ` R ) ( d |` ( { e } X. N ) ) ) /\ ( b |` ( ( N \ { e } ) X. N ) ) = ( c |` ( ( N \ { e } ) X. N ) ) /\ ( b |` ( ( N \ { e } ) X. N ) ) = ( d |` ( ( N \ { e } ) X. N ) ) ) ) -> ( ( b .xb G ) |` ( { e } X. N ) ) = ( ( b |` ( { e } X. N ) ) ( R maMul <. { e } , N , N >. ) G ) )
129 121 oveqd 
 |-  ( ( ( R e. CRing /\ F e. B /\ G e. B ) /\ ( ( b e. B /\ c e. B ) /\ ( d e. B /\ e e. N ) ) ) -> ( c ( R maMul <. N , N , N >. ) G ) = ( c .xb G ) )
130 129 reseq1d 
 |-  ( ( ( R e. CRing /\ F e. B /\ G e. B ) /\ ( ( b e. B /\ c e. B ) /\ ( d e. B /\ e e. N ) ) ) -> ( ( c ( R maMul <. N , N , N >. ) G ) |` ( { e } X. N ) ) = ( ( c .xb G ) |` ( { e } X. N ) ) )
131 52 101 6 124 104 104 104 108 106 117 mamures 
 |-  ( ( ( R e. CRing /\ F e. B /\ G e. B ) /\ ( ( b e. B /\ c e. B ) /\ ( d e. B /\ e e. N ) ) ) -> ( ( c ( R maMul <. N , N , N >. ) G ) |` ( { e } X. N ) ) = ( ( c |` ( { e } X. N ) ) ( R maMul <. { e } , N , N >. ) G ) )
132 130 131 eqtr3d 
 |-  ( ( ( R e. CRing /\ F e. B /\ G e. B ) /\ ( ( b e. B /\ c e. B ) /\ ( d e. B /\ e e. N ) ) ) -> ( ( c .xb G ) |` ( { e } X. N ) ) = ( ( c |` ( { e } X. N ) ) ( R maMul <. { e } , N , N >. ) G ) )
133 121 oveqd 
 |-  ( ( ( R e. CRing /\ F e. B /\ G e. B ) /\ ( ( b e. B /\ c e. B ) /\ ( d e. B /\ e e. N ) ) ) -> ( d ( R maMul <. N , N , N >. ) G ) = ( d .xb G ) )
134 133 reseq1d 
 |-  ( ( ( R e. CRing /\ F e. B /\ G e. B ) /\ ( ( b e. B /\ c e. B ) /\ ( d e. B /\ e e. N ) ) ) -> ( ( d ( R maMul <. N , N , N >. ) G ) |` ( { e } X. N ) ) = ( ( d .xb G ) |` ( { e } X. N ) ) )
135 52 101 6 124 104 104 104 108 114 117 mamures 
 |-  ( ( ( R e. CRing /\ F e. B /\ G e. B ) /\ ( ( b e. B /\ c e. B ) /\ ( d e. B /\ e e. N ) ) ) -> ( ( d ( R maMul <. N , N , N >. ) G ) |` ( { e } X. N ) ) = ( ( d |` ( { e } X. N ) ) ( R maMul <. { e } , N , N >. ) G ) )
136 134 135 eqtr3d 
 |-  ( ( ( R e. CRing /\ F e. B /\ G e. B ) /\ ( ( b e. B /\ c e. B ) /\ ( d e. B /\ e e. N ) ) ) -> ( ( d .xb G ) |` ( { e } X. N ) ) = ( ( d |` ( { e } X. N ) ) ( R maMul <. { e } , N , N >. ) G ) )
137 132 136 oveq12d 
 |-  ( ( ( R e. CRing /\ F e. B /\ G e. B ) /\ ( ( b e. B /\ c e. B ) /\ ( d e. B /\ e e. N ) ) ) -> ( ( ( c .xb G ) |` ( { e } X. N ) ) oF ( +g ` R ) ( ( d .xb G ) |` ( { e } X. N ) ) ) = ( ( ( c |` ( { e } X. N ) ) ( R maMul <. { e } , N , N >. ) G ) oF ( +g ` R ) ( ( d |` ( { e } X. N ) ) ( R maMul <. { e } , N , N >. ) G ) ) )
138 137 3adant3 
 |-  ( ( ( R e. CRing /\ F e. B /\ G e. B ) /\ ( ( b e. B /\ c e. B ) /\ ( d e. B /\ e e. N ) ) /\ ( ( b |` ( { e } X. N ) ) = ( ( c |` ( { e } X. N ) ) oF ( +g ` R ) ( d |` ( { e } X. N ) ) ) /\ ( b |` ( ( N \ { e } ) X. N ) ) = ( c |` ( ( N \ { e } ) X. N ) ) /\ ( b |` ( ( N \ { e } ) X. N ) ) = ( d |` ( ( N \ { e } ) X. N ) ) ) ) -> ( ( ( c .xb G ) |` ( { e } X. N ) ) oF ( +g ` R ) ( ( d .xb G ) |` ( { e } X. N ) ) ) = ( ( ( c |` ( { e } X. N ) ) ( R maMul <. { e } , N , N >. ) G ) oF ( +g ` R ) ( ( d |` ( { e } X. N ) ) ( R maMul <. { e } , N , N >. ) G ) ) )
139 120 128 138 3eqtr4d 
 |-  ( ( ( R e. CRing /\ F e. B /\ G e. B ) /\ ( ( b e. B /\ c e. B ) /\ ( d e. B /\ e e. N ) ) /\ ( ( b |` ( { e } X. N ) ) = ( ( c |` ( { e } X. N ) ) oF ( +g ` R ) ( d |` ( { e } X. N ) ) ) /\ ( b |` ( ( N \ { e } ) X. N ) ) = ( c |` ( ( N \ { e } ) X. N ) ) /\ ( b |` ( ( N \ { e } ) X. N ) ) = ( d |` ( ( N \ { e } ) X. N ) ) ) ) -> ( ( b .xb G ) |` ( { e } X. N ) ) = ( ( ( c .xb G ) |` ( { e } X. N ) ) oF ( +g ` R ) ( ( d .xb G ) |` ( { e } X. N ) ) ) )
140 simp32 
 |-  ( ( ( R e. CRing /\ F e. B /\ G e. B ) /\ ( ( b e. B /\ c e. B ) /\ ( d e. B /\ e e. N ) ) /\ ( ( b |` ( { e } X. N ) ) = ( ( c |` ( { e } X. N ) ) oF ( +g ` R ) ( d |` ( { e } X. N ) ) ) /\ ( b |` ( ( N \ { e } ) X. N ) ) = ( c |` ( ( N \ { e } ) X. N ) ) /\ ( b |` ( ( N \ { e } ) X. N ) ) = ( d |` ( ( N \ { e } ) X. N ) ) ) ) -> ( b |` ( ( N \ { e } ) X. N ) ) = ( c |` ( ( N \ { e } ) X. N ) ) )
141 140 oveq1d 
 |-  ( ( ( R e. CRing /\ F e. B /\ G e. B ) /\ ( ( b e. B /\ c e. B ) /\ ( d e. B /\ e e. N ) ) /\ ( ( b |` ( { e } X. N ) ) = ( ( c |` ( { e } X. N ) ) oF ( +g ` R ) ( d |` ( { e } X. N ) ) ) /\ ( b |` ( ( N \ { e } ) X. N ) ) = ( c |` ( ( N \ { e } ) X. N ) ) /\ ( b |` ( ( N \ { e } ) X. N ) ) = ( d |` ( ( N \ { e } ) X. N ) ) ) ) -> ( ( b |` ( ( N \ { e } ) X. N ) ) ( R maMul <. ( N \ { e } ) , N , N >. ) G ) = ( ( c |` ( ( N \ { e } ) X. N ) ) ( R maMul <. ( N \ { e } ) , N , N >. ) G ) )
142 122 reseq1d 
 |-  ( ( ( R e. CRing /\ F e. B /\ G e. B ) /\ ( ( b e. B /\ c e. B ) /\ ( d e. B /\ e e. N ) ) ) -> ( ( b ( R maMul <. N , N , N >. ) G ) |` ( ( N \ { e } ) X. N ) ) = ( ( b .xb G ) |` ( ( N \ { e } ) X. N ) ) )
143 eqid 
 |-  ( R maMul <. ( N \ { e } ) , N , N >. ) = ( R maMul <. ( N \ { e } ) , N , N >. )
144 difssd 
 |-  ( ( ( R e. CRing /\ F e. B /\ G e. B ) /\ ( ( b e. B /\ c e. B ) /\ ( d e. B /\ e e. N ) ) ) -> ( N \ { e } ) C_ N )
145 52 143 6 124 104 104 104 144 125 117 mamures 
 |-  ( ( ( R e. CRing /\ F e. B /\ G e. B ) /\ ( ( b e. B /\ c e. B ) /\ ( d e. B /\ e e. N ) ) ) -> ( ( b ( R maMul <. N , N , N >. ) G ) |` ( ( N \ { e } ) X. N ) ) = ( ( b |` ( ( N \ { e } ) X. N ) ) ( R maMul <. ( N \ { e } ) , N , N >. ) G ) )
146 142 145 eqtr3d 
 |-  ( ( ( R e. CRing /\ F e. B /\ G e. B ) /\ ( ( b e. B /\ c e. B ) /\ ( d e. B /\ e e. N ) ) ) -> ( ( b .xb G ) |` ( ( N \ { e } ) X. N ) ) = ( ( b |` ( ( N \ { e } ) X. N ) ) ( R maMul <. ( N \ { e } ) , N , N >. ) G ) )
147 146 3adant3 
 |-  ( ( ( R e. CRing /\ F e. B /\ G e. B ) /\ ( ( b e. B /\ c e. B ) /\ ( d e. B /\ e e. N ) ) /\ ( ( b |` ( { e } X. N ) ) = ( ( c |` ( { e } X. N ) ) oF ( +g ` R ) ( d |` ( { e } X. N ) ) ) /\ ( b |` ( ( N \ { e } ) X. N ) ) = ( c |` ( ( N \ { e } ) X. N ) ) /\ ( b |` ( ( N \ { e } ) X. N ) ) = ( d |` ( ( N \ { e } ) X. N ) ) ) ) -> ( ( b .xb G ) |` ( ( N \ { e } ) X. N ) ) = ( ( b |` ( ( N \ { e } ) X. N ) ) ( R maMul <. ( N \ { e } ) , N , N >. ) G ) )
148 129 reseq1d 
 |-  ( ( ( R e. CRing /\ F e. B /\ G e. B ) /\ ( ( b e. B /\ c e. B ) /\ ( d e. B /\ e e. N ) ) ) -> ( ( c ( R maMul <. N , N , N >. ) G ) |` ( ( N \ { e } ) X. N ) ) = ( ( c .xb G ) |` ( ( N \ { e } ) X. N ) ) )
149 52 143 6 124 104 104 104 144 106 117 mamures 
 |-  ( ( ( R e. CRing /\ F e. B /\ G e. B ) /\ ( ( b e. B /\ c e. B ) /\ ( d e. B /\ e e. N ) ) ) -> ( ( c ( R maMul <. N , N , N >. ) G ) |` ( ( N \ { e } ) X. N ) ) = ( ( c |` ( ( N \ { e } ) X. N ) ) ( R maMul <. ( N \ { e } ) , N , N >. ) G ) )
150 148 149 eqtr3d 
 |-  ( ( ( R e. CRing /\ F e. B /\ G e. B ) /\ ( ( b e. B /\ c e. B ) /\ ( d e. B /\ e e. N ) ) ) -> ( ( c .xb G ) |` ( ( N \ { e } ) X. N ) ) = ( ( c |` ( ( N \ { e } ) X. N ) ) ( R maMul <. ( N \ { e } ) , N , N >. ) G ) )
151 150 3adant3 
 |-  ( ( ( R e. CRing /\ F e. B /\ G e. B ) /\ ( ( b e. B /\ c e. B ) /\ ( d e. B /\ e e. N ) ) /\ ( ( b |` ( { e } X. N ) ) = ( ( c |` ( { e } X. N ) ) oF ( +g ` R ) ( d |` ( { e } X. N ) ) ) /\ ( b |` ( ( N \ { e } ) X. N ) ) = ( c |` ( ( N \ { e } ) X. N ) ) /\ ( b |` ( ( N \ { e } ) X. N ) ) = ( d |` ( ( N \ { e } ) X. N ) ) ) ) -> ( ( c .xb G ) |` ( ( N \ { e } ) X. N ) ) = ( ( c |` ( ( N \ { e } ) X. N ) ) ( R maMul <. ( N \ { e } ) , N , N >. ) G ) )
152 141 147 151 3eqtr4d 
 |-  ( ( ( R e. CRing /\ F e. B /\ G e. B ) /\ ( ( b e. B /\ c e. B ) /\ ( d e. B /\ e e. N ) ) /\ ( ( b |` ( { e } X. N ) ) = ( ( c |` ( { e } X. N ) ) oF ( +g ` R ) ( d |` ( { e } X. N ) ) ) /\ ( b |` ( ( N \ { e } ) X. N ) ) = ( c |` ( ( N \ { e } ) X. N ) ) /\ ( b |` ( ( N \ { e } ) X. N ) ) = ( d |` ( ( N \ { e } ) X. N ) ) ) ) -> ( ( b .xb G ) |` ( ( N \ { e } ) X. N ) ) = ( ( c .xb G ) |` ( ( N \ { e } ) X. N ) ) )
153 simp33 
 |-  ( ( ( R e. CRing /\ F e. B /\ G e. B ) /\ ( ( b e. B /\ c e. B ) /\ ( d e. B /\ e e. N ) ) /\ ( ( b |` ( { e } X. N ) ) = ( ( c |` ( { e } X. N ) ) oF ( +g ` R ) ( d |` ( { e } X. N ) ) ) /\ ( b |` ( ( N \ { e } ) X. N ) ) = ( c |` ( ( N \ { e } ) X. N ) ) /\ ( b |` ( ( N \ { e } ) X. N ) ) = ( d |` ( ( N \ { e } ) X. N ) ) ) ) -> ( b |` ( ( N \ { e } ) X. N ) ) = ( d |` ( ( N \ { e } ) X. N ) ) )
154 153 oveq1d 
 |-  ( ( ( R e. CRing /\ F e. B /\ G e. B ) /\ ( ( b e. B /\ c e. B ) /\ ( d e. B /\ e e. N ) ) /\ ( ( b |` ( { e } X. N ) ) = ( ( c |` ( { e } X. N ) ) oF ( +g ` R ) ( d |` ( { e } X. N ) ) ) /\ ( b |` ( ( N \ { e } ) X. N ) ) = ( c |` ( ( N \ { e } ) X. N ) ) /\ ( b |` ( ( N \ { e } ) X. N ) ) = ( d |` ( ( N \ { e } ) X. N ) ) ) ) -> ( ( b |` ( ( N \ { e } ) X. N ) ) ( R maMul <. ( N \ { e } ) , N , N >. ) G ) = ( ( d |` ( ( N \ { e } ) X. N ) ) ( R maMul <. ( N \ { e } ) , N , N >. ) G ) )
155 133 reseq1d 
 |-  ( ( ( R e. CRing /\ F e. B /\ G e. B ) /\ ( ( b e. B /\ c e. B ) /\ ( d e. B /\ e e. N ) ) ) -> ( ( d ( R maMul <. N , N , N >. ) G ) |` ( ( N \ { e } ) X. N ) ) = ( ( d .xb G ) |` ( ( N \ { e } ) X. N ) ) )
156 52 143 6 124 104 104 104 144 114 117 mamures 
 |-  ( ( ( R e. CRing /\ F e. B /\ G e. B ) /\ ( ( b e. B /\ c e. B ) /\ ( d e. B /\ e e. N ) ) ) -> ( ( d ( R maMul <. N , N , N >. ) G ) |` ( ( N \ { e } ) X. N ) ) = ( ( d |` ( ( N \ { e } ) X. N ) ) ( R maMul <. ( N \ { e } ) , N , N >. ) G ) )
157 155 156 eqtr3d 
 |-  ( ( ( R e. CRing /\ F e. B /\ G e. B ) /\ ( ( b e. B /\ c e. B ) /\ ( d e. B /\ e e. N ) ) ) -> ( ( d .xb G ) |` ( ( N \ { e } ) X. N ) ) = ( ( d |` ( ( N \ { e } ) X. N ) ) ( R maMul <. ( N \ { e } ) , N , N >. ) G ) )
158 157 3adant3 
 |-  ( ( ( R e. CRing /\ F e. B /\ G e. B ) /\ ( ( b e. B /\ c e. B ) /\ ( d e. B /\ e e. N ) ) /\ ( ( b |` ( { e } X. N ) ) = ( ( c |` ( { e } X. N ) ) oF ( +g ` R ) ( d |` ( { e } X. N ) ) ) /\ ( b |` ( ( N \ { e } ) X. N ) ) = ( c |` ( ( N \ { e } ) X. N ) ) /\ ( b |` ( ( N \ { e } ) X. N ) ) = ( d |` ( ( N \ { e } ) X. N ) ) ) ) -> ( ( d .xb G ) |` ( ( N \ { e } ) X. N ) ) = ( ( d |` ( ( N \ { e } ) X. N ) ) ( R maMul <. ( N \ { e } ) , N , N >. ) G ) )
159 154 147 158 3eqtr4d 
 |-  ( ( ( R e. CRing /\ F e. B /\ G e. B ) /\ ( ( b e. B /\ c e. B ) /\ ( d e. B /\ e e. N ) ) /\ ( ( b |` ( { e } X. N ) ) = ( ( c |` ( { e } X. N ) ) oF ( +g ` R ) ( d |` ( { e } X. N ) ) ) /\ ( b |` ( ( N \ { e } ) X. N ) ) = ( c |` ( ( N \ { e } ) X. N ) ) /\ ( b |` ( ( N \ { e } ) X. N ) ) = ( d |` ( ( N \ { e } ) X. N ) ) ) ) -> ( ( b .xb G ) |` ( ( N \ { e } ) X. N ) ) = ( ( d .xb G ) |` ( ( N \ { e } ) X. N ) ) )
160 3 1 2 9 83 88 92 96 97 139 152 159 mdetrlin 
 |-  ( ( ( R e. CRing /\ F e. B /\ G e. B ) /\ ( ( b e. B /\ c e. B ) /\ ( d e. B /\ e e. N ) ) /\ ( ( b |` ( { e } X. N ) ) = ( ( c |` ( { e } X. N ) ) oF ( +g ` R ) ( d |` ( { e } X. N ) ) ) /\ ( b |` ( ( N \ { e } ) X. N ) ) = ( c |` ( ( N \ { e } ) X. N ) ) /\ ( b |` ( ( N \ { e } ) X. N ) ) = ( d |` ( ( N \ { e } ) X. N ) ) ) ) -> ( D ` ( b .xb G ) ) = ( ( D ` ( c .xb G ) ) ( +g ` R ) ( D ` ( d .xb G ) ) ) )
161 85 31 syl 
 |-  ( ( ( R e. CRing /\ F e. B /\ G e. B ) /\ ( ( b e. B /\ c e. B ) /\ ( d e. B /\ e e. N ) ) ) -> ( ( a e. B |-> ( D ` ( a .xb G ) ) ) ` b ) = ( D ` ( b .xb G ) ) )
162 161 3adant3 
 |-  ( ( ( R e. CRing /\ F e. B /\ G e. B ) /\ ( ( b e. B /\ c e. B ) /\ ( d e. B /\ e e. N ) ) /\ ( ( b |` ( { e } X. N ) ) = ( ( c |` ( { e } X. N ) ) oF ( +g ` R ) ( d |` ( { e } X. N ) ) ) /\ ( b |` ( ( N \ { e } ) X. N ) ) = ( c |` ( ( N \ { e } ) X. N ) ) /\ ( b |` ( ( N \ { e } ) X. N ) ) = ( d |` ( ( N \ { e } ) X. N ) ) ) ) -> ( ( a e. B |-> ( D ` ( a .xb G ) ) ) ` b ) = ( D ` ( b .xb G ) ) )
163 fvoveq1 
 |-  ( a = c -> ( D ` ( a .xb G ) ) = ( D ` ( c .xb G ) ) )
164 fvex 
 |-  ( D ` ( c .xb G ) ) e. _V
165 163 29 164 fvmpt 
 |-  ( c e. B -> ( ( a e. B |-> ( D ` ( a .xb G ) ) ) ` c ) = ( D ` ( c .xb G ) ) )
166 89 165 syl 
 |-  ( ( ( R e. CRing /\ F e. B /\ G e. B ) /\ ( ( b e. B /\ c e. B ) /\ ( d e. B /\ e e. N ) ) ) -> ( ( a e. B |-> ( D ` ( a .xb G ) ) ) ` c ) = ( D ` ( c .xb G ) ) )
167 fvoveq1 
 |-  ( a = d -> ( D ` ( a .xb G ) ) = ( D ` ( d .xb G ) ) )
168 fvex 
 |-  ( D ` ( d .xb G ) ) e. _V
169 167 29 168 fvmpt 
 |-  ( d e. B -> ( ( a e. B |-> ( D ` ( a .xb G ) ) ) ` d ) = ( D ` ( d .xb G ) ) )
170 93 169 syl 
 |-  ( ( ( R e. CRing /\ F e. B /\ G e. B ) /\ ( ( b e. B /\ c e. B ) /\ ( d e. B /\ e e. N ) ) ) -> ( ( a e. B |-> ( D ` ( a .xb G ) ) ) ` d ) = ( D ` ( d .xb G ) ) )
171 166 170 oveq12d 
 |-  ( ( ( R e. CRing /\ F e. B /\ G e. B ) /\ ( ( b e. B /\ c e. B ) /\ ( d e. B /\ e e. N ) ) ) -> ( ( ( a e. B |-> ( D ` ( a .xb G ) ) ) ` c ) ( +g ` R ) ( ( a e. B |-> ( D ` ( a .xb G ) ) ) ` d ) ) = ( ( D ` ( c .xb G ) ) ( +g ` R ) ( D ` ( d .xb G ) ) ) )
172 171 3adant3 
 |-  ( ( ( R e. CRing /\ F e. B /\ G e. B ) /\ ( ( b e. B /\ c e. B ) /\ ( d e. B /\ e e. N ) ) /\ ( ( b |` ( { e } X. N ) ) = ( ( c |` ( { e } X. N ) ) oF ( +g ` R ) ( d |` ( { e } X. N ) ) ) /\ ( b |` ( ( N \ { e } ) X. N ) ) = ( c |` ( ( N \ { e } ) X. N ) ) /\ ( b |` ( ( N \ { e } ) X. N ) ) = ( d |` ( ( N \ { e } ) X. N ) ) ) ) -> ( ( ( a e. B |-> ( D ` ( a .xb G ) ) ) ` c ) ( +g ` R ) ( ( a e. B |-> ( D ` ( a .xb G ) ) ) ` d ) ) = ( ( D ` ( c .xb G ) ) ( +g ` R ) ( D ` ( d .xb G ) ) ) )
173 160 162 172 3eqtr4d 
 |-  ( ( ( R e. CRing /\ F e. B /\ G e. B ) /\ ( ( b e. B /\ c e. B ) /\ ( d e. B /\ e e. N ) ) /\ ( ( b |` ( { e } X. N ) ) = ( ( c |` ( { e } X. N ) ) oF ( +g ` R ) ( d |` ( { e } X. N ) ) ) /\ ( b |` ( ( N \ { e } ) X. N ) ) = ( c |` ( ( N \ { e } ) X. N ) ) /\ ( b |` ( ( N \ { e } ) X. N ) ) = ( d |` ( ( N \ { e } ) X. N ) ) ) ) -> ( ( a e. B |-> ( D ` ( a .xb G ) ) ) ` b ) = ( ( ( a e. B |-> ( D ` ( a .xb G ) ) ) ` c ) ( +g ` R ) ( ( a e. B |-> ( D ` ( a .xb G ) ) ) ` d ) ) )
174 173 3expia 
 |-  ( ( ( R e. CRing /\ F e. B /\ G e. B ) /\ ( ( b e. B /\ c e. B ) /\ ( d e. B /\ e e. N ) ) ) -> ( ( ( b |` ( { e } X. N ) ) = ( ( c |` ( { e } X. N ) ) oF ( +g ` R ) ( d |` ( { e } X. N ) ) ) /\ ( b |` ( ( N \ { e } ) X. N ) ) = ( c |` ( ( N \ { e } ) X. N ) ) /\ ( b |` ( ( N \ { e } ) X. N ) ) = ( d |` ( ( N \ { e } ) X. N ) ) ) -> ( ( a e. B |-> ( D ` ( a .xb G ) ) ) ` b ) = ( ( ( a e. B |-> ( D ` ( a .xb G ) ) ) ` c ) ( +g ` R ) ( ( a e. B |-> ( D ` ( a .xb G ) ) ) ` d ) ) ) )
175 174 anassrs 
 |-  ( ( ( ( R e. CRing /\ F e. B /\ G e. B ) /\ ( b e. B /\ c e. B ) ) /\ ( d e. B /\ e e. N ) ) -> ( ( ( b |` ( { e } X. N ) ) = ( ( c |` ( { e } X. N ) ) oF ( +g ` R ) ( d |` ( { e } X. N ) ) ) /\ ( b |` ( ( N \ { e } ) X. N ) ) = ( c |` ( ( N \ { e } ) X. N ) ) /\ ( b |` ( ( N \ { e } ) X. N ) ) = ( d |` ( ( N \ { e } ) X. N ) ) ) -> ( ( a e. B |-> ( D ` ( a .xb G ) ) ) ` b ) = ( ( ( a e. B |-> ( D ` ( a .xb G ) ) ) ` c ) ( +g ` R ) ( ( a e. B |-> ( D ` ( a .xb G ) ) ) ` d ) ) ) )
176 175 ralrimivva 
 |-  ( ( ( R e. CRing /\ F e. B /\ G e. B ) /\ ( b e. B /\ c e. B ) ) -> A. d e. B A. e e. N ( ( ( b |` ( { e } X. N ) ) = ( ( c |` ( { e } X. N ) ) oF ( +g ` R ) ( d |` ( { e } X. N ) ) ) /\ ( b |` ( ( N \ { e } ) X. N ) ) = ( c |` ( ( N \ { e } ) X. N ) ) /\ ( b |` ( ( N \ { e } ) X. N ) ) = ( d |` ( ( N \ { e } ) X. N ) ) ) -> ( ( a e. B |-> ( D ` ( a .xb G ) ) ) ` b ) = ( ( ( a e. B |-> ( D ` ( a .xb G ) ) ) ` c ) ( +g ` R ) ( ( a e. B |-> ( D ` ( a .xb G ) ) ) ` d ) ) ) )
177 176 ralrimivva 
 |-  ( ( R e. CRing /\ F e. B /\ G e. B ) -> A. b e. B A. c e. B A. d e. B A. e e. N ( ( ( b |` ( { e } X. N ) ) = ( ( c |` ( { e } X. N ) ) oF ( +g ` R ) ( d |` ( { e } X. N ) ) ) /\ ( b |` ( ( N \ { e } ) X. N ) ) = ( c |` ( ( N \ { e } ) X. N ) ) /\ ( b |` ( ( N \ { e } ) X. N ) ) = ( d |` ( ( N \ { e } ) X. N ) ) ) -> ( ( a e. B |-> ( D ` ( a .xb G ) ) ) ` b ) = ( ( ( a e. B |-> ( D ` ( a .xb G ) ) ) ` c ) ( +g ` R ) ( ( a e. B |-> ( D ` ( a .xb G ) ) ) ` d ) ) ) )
178 simp11 
 |-  ( ( ( R e. CRing /\ F e. B /\ G e. B ) /\ ( ( b e. B /\ c e. ( Base ` R ) ) /\ ( d e. B /\ e e. N ) ) /\ ( ( b |` ( { e } X. N ) ) = ( ( ( { e } X. N ) X. { c } ) oF .x. ( d |` ( { e } X. N ) ) ) /\ ( b |` ( ( N \ { e } ) X. N ) ) = ( d |` ( ( N \ { e } ) X. N ) ) ) ) -> R e. CRing )
179 19 adantr 
 |-  ( ( ( R e. CRing /\ F e. B /\ G e. B ) /\ ( ( b e. B /\ c e. ( Base ` R ) ) /\ ( d e. B /\ e e. N ) ) ) -> A e. Ring )
180 simprll 
 |-  ( ( ( R e. CRing /\ F e. B /\ G e. B ) /\ ( ( b e. B /\ c e. ( Base ` R ) ) /\ ( d e. B /\ e e. N ) ) ) -> b e. B )
181 simpl3 
 |-  ( ( ( R e. CRing /\ F e. B /\ G e. B ) /\ ( ( b e. B /\ c e. ( Base ` R ) ) /\ ( d e. B /\ e e. N ) ) ) -> G e. B )
182 179 180 181 37 syl3anc 
 |-  ( ( ( R e. CRing /\ F e. B /\ G e. B ) /\ ( ( b e. B /\ c e. ( Base ` R ) ) /\ ( d e. B /\ e e. N ) ) ) -> ( b .xb G ) e. B )
183 182 3adant3 
 |-  ( ( ( R e. CRing /\ F e. B /\ G e. B ) /\ ( ( b e. B /\ c e. ( Base ` R ) ) /\ ( d e. B /\ e e. N ) ) /\ ( ( b |` ( { e } X. N ) ) = ( ( ( { e } X. N ) X. { c } ) oF .x. ( d |` ( { e } X. N ) ) ) /\ ( b |` ( ( N \ { e } ) X. N ) ) = ( d |` ( ( N \ { e } ) X. N ) ) ) ) -> ( b .xb G ) e. B )
184 simp2lr 
 |-  ( ( ( R e. CRing /\ F e. B /\ G e. B ) /\ ( ( b e. B /\ c e. ( Base ` R ) ) /\ ( d e. B /\ e e. N ) ) /\ ( ( b |` ( { e } X. N ) ) = ( ( ( { e } X. N ) X. { c } ) oF .x. ( d |` ( { e } X. N ) ) ) /\ ( b |` ( ( N \ { e } ) X. N ) ) = ( d |` ( ( N \ { e } ) X. N ) ) ) ) -> c e. ( Base ` R ) )
185 simprrl 
 |-  ( ( ( R e. CRing /\ F e. B /\ G e. B ) /\ ( ( b e. B /\ c e. ( Base ` R ) ) /\ ( d e. B /\ e e. N ) ) ) -> d e. B )
186 179 185 181 94 syl3anc 
 |-  ( ( ( R e. CRing /\ F e. B /\ G e. B ) /\ ( ( b e. B /\ c e. ( Base ` R ) ) /\ ( d e. B /\ e e. N ) ) ) -> ( d .xb G ) e. B )
187 186 3adant3 
 |-  ( ( ( R e. CRing /\ F e. B /\ G e. B ) /\ ( ( b e. B /\ c e. ( Base ` R ) ) /\ ( d e. B /\ e e. N ) ) /\ ( ( b |` ( { e } X. N ) ) = ( ( ( { e } X. N ) X. { c } ) oF .x. ( d |` ( { e } X. N ) ) ) /\ ( b |` ( ( N \ { e } ) X. N ) ) = ( d |` ( ( N \ { e } ) X. N ) ) ) ) -> ( d .xb G ) e. B )
188 simp2rr 
 |-  ( ( ( R e. CRing /\ F e. B /\ G e. B ) /\ ( ( b e. B /\ c e. ( Base ` R ) ) /\ ( d e. B /\ e e. N ) ) /\ ( ( b |` ( { e } X. N ) ) = ( ( ( { e } X. N ) X. { c } ) oF .x. ( d |` ( { e } X. N ) ) ) /\ ( b |` ( ( N \ { e } ) X. N ) ) = ( d |` ( ( N \ { e } ) X. N ) ) ) ) -> e e. N )
189 simp3l 
 |-  ( ( ( R e. CRing /\ F e. B /\ G e. B ) /\ ( ( b e. B /\ c e. ( Base ` R ) ) /\ ( d e. B /\ e e. N ) ) /\ ( ( b |` ( { e } X. N ) ) = ( ( ( { e } X. N ) X. { c } ) oF .x. ( d |` ( { e } X. N ) ) ) /\ ( b |` ( ( N \ { e } ) X. N ) ) = ( d |` ( ( N \ { e } ) X. N ) ) ) ) -> ( b |` ( { e } X. N ) ) = ( ( ( { e } X. N ) X. { c } ) oF .x. ( d |` ( { e } X. N ) ) ) )
190 189 oveq1d 
 |-  ( ( ( R e. CRing /\ F e. B /\ G e. B ) /\ ( ( b e. B /\ c e. ( Base ` R ) ) /\ ( d e. B /\ e e. N ) ) /\ ( ( b |` ( { e } X. N ) ) = ( ( ( { e } X. N ) X. { c } ) oF .x. ( d |` ( { e } X. N ) ) ) /\ ( b |` ( ( N \ { e } ) X. N ) ) = ( d |` ( ( N \ { e } ) X. N ) ) ) ) -> ( ( b |` ( { e } X. N ) ) ( R maMul <. { e } , N , N >. ) G ) = ( ( ( ( { e } X. N ) X. { c } ) oF .x. ( d |` ( { e } X. N ) ) ) ( R maMul <. { e } , N , N >. ) G ) )
191 55 adantr 
 |-  ( ( ( R e. CRing /\ F e. B /\ G e. B ) /\ ( ( b e. B /\ c e. ( Base ` R ) ) /\ ( d e. B /\ e e. N ) ) ) -> ( R maMul <. N , N , N >. ) = .xb )
192 191 oveqd 
 |-  ( ( ( R e. CRing /\ F e. B /\ G e. B ) /\ ( ( b e. B /\ c e. ( Base ` R ) ) /\ ( d e. B /\ e e. N ) ) ) -> ( b ( R maMul <. N , N , N >. ) G ) = ( b .xb G ) )
193 192 reseq1d 
 |-  ( ( ( R e. CRing /\ F e. B /\ G e. B ) /\ ( ( b e. B /\ c e. ( Base ` R ) ) /\ ( d e. B /\ e e. N ) ) ) -> ( ( b ( R maMul <. N , N , N >. ) G ) |` ( { e } X. N ) ) = ( ( b .xb G ) |` ( { e } X. N ) ) )
194 simpl1 
 |-  ( ( ( R e. CRing /\ F e. B /\ G e. B ) /\ ( ( b e. B /\ c e. ( Base ` R ) ) /\ ( d e. B /\ e e. N ) ) ) -> R e. CRing )
195 12 adantr 
 |-  ( ( ( R e. CRing /\ F e. B /\ G e. B ) /\ ( ( b e. B /\ c e. ( Base ` R ) ) /\ ( d e. B /\ e e. N ) ) ) -> N e. Fin )
196 simprrr 
 |-  ( ( ( R e. CRing /\ F e. B /\ G e. B ) /\ ( ( b e. B /\ c e. ( Base ` R ) ) /\ ( d e. B /\ e e. N ) ) ) -> e e. N )
197 196 snssd 
 |-  ( ( ( R e. CRing /\ F e. B /\ G e. B ) /\ ( ( b e. B /\ c e. ( Base ` R ) ) /\ ( d e. B /\ e e. N ) ) ) -> { e } C_ N )
198 180 62 syl 
 |-  ( ( ( R e. CRing /\ F e. B /\ G e. B ) /\ ( ( b e. B /\ c e. ( Base ` R ) ) /\ ( d e. B /\ e e. N ) ) ) -> b e. ( ( Base ` R ) ^m ( N X. N ) ) )
199 65 adantr 
 |-  ( ( ( R e. CRing /\ F e. B /\ G e. B ) /\ ( ( b e. B /\ c e. ( Base ` R ) ) /\ ( d e. B /\ e e. N ) ) ) -> G e. ( ( Base ` R ) ^m ( N X. N ) ) )
200 52 101 6 194 195 195 195 197 198 199 mamures 
 |-  ( ( ( R e. CRing /\ F e. B /\ G e. B ) /\ ( ( b e. B /\ c e. ( Base ` R ) ) /\ ( d e. B /\ e e. N ) ) ) -> ( ( b ( R maMul <. N , N , N >. ) G ) |` ( { e } X. N ) ) = ( ( b |` ( { e } X. N ) ) ( R maMul <. { e } , N , N >. ) G ) )
201 193 200 eqtr3d 
 |-  ( ( ( R e. CRing /\ F e. B /\ G e. B ) /\ ( ( b e. B /\ c e. ( Base ` R ) ) /\ ( d e. B /\ e e. N ) ) ) -> ( ( b .xb G ) |` ( { e } X. N ) ) = ( ( b |` ( { e } X. N ) ) ( R maMul <. { e } , N , N >. ) G ) )
202 201 3adant3 
 |-  ( ( ( R e. CRing /\ F e. B /\ G e. B ) /\ ( ( b e. B /\ c e. ( Base ` R ) ) /\ ( d e. B /\ e e. N ) ) /\ ( ( b |` ( { e } X. N ) ) = ( ( ( { e } X. N ) X. { c } ) oF .x. ( d |` ( { e } X. N ) ) ) /\ ( b |` ( ( N \ { e } ) X. N ) ) = ( d |` ( ( N \ { e } ) X. N ) ) ) ) -> ( ( b .xb G ) |` ( { e } X. N ) ) = ( ( b |` ( { e } X. N ) ) ( R maMul <. { e } , N , N >. ) G ) )
203 191 oveqd 
 |-  ( ( ( R e. CRing /\ F e. B /\ G e. B ) /\ ( ( b e. B /\ c e. ( Base ` R ) ) /\ ( d e. B /\ e e. N ) ) ) -> ( d ( R maMul <. N , N , N >. ) G ) = ( d .xb G ) )
204 203 reseq1d 
 |-  ( ( ( R e. CRing /\ F e. B /\ G e. B ) /\ ( ( b e. B /\ c e. ( Base ` R ) ) /\ ( d e. B /\ e e. N ) ) ) -> ( ( d ( R maMul <. N , N , N >. ) G ) |` ( { e } X. N ) ) = ( ( d .xb G ) |` ( { e } X. N ) ) )
205 185 113 syl 
 |-  ( ( ( R e. CRing /\ F e. B /\ G e. B ) /\ ( ( b e. B /\ c e. ( Base ` R ) ) /\ ( d e. B /\ e e. N ) ) ) -> d e. ( ( Base ` R ) ^m ( N X. N ) ) )
206 52 101 6 194 195 195 195 197 205 199 mamures 
 |-  ( ( ( R e. CRing /\ F e. B /\ G e. B ) /\ ( ( b e. B /\ c e. ( Base ` R ) ) /\ ( d e. B /\ e e. N ) ) ) -> ( ( d ( R maMul <. N , N , N >. ) G ) |` ( { e } X. N ) ) = ( ( d |` ( { e } X. N ) ) ( R maMul <. { e } , N , N >. ) G ) )
207 204 206 eqtr3d 
 |-  ( ( ( R e. CRing /\ F e. B /\ G e. B ) /\ ( ( b e. B /\ c e. ( Base ` R ) ) /\ ( d e. B /\ e e. N ) ) ) -> ( ( d .xb G ) |` ( { e } X. N ) ) = ( ( d |` ( { e } X. N ) ) ( R maMul <. { e } , N , N >. ) G ) )
208 207 oveq2d 
 |-  ( ( ( R e. CRing /\ F e. B /\ G e. B ) /\ ( ( b e. B /\ c e. ( Base ` R ) ) /\ ( d e. B /\ e e. N ) ) ) -> ( ( ( { e } X. N ) X. { c } ) oF .x. ( ( d .xb G ) |` ( { e } X. N ) ) ) = ( ( ( { e } X. N ) X. { c } ) oF .x. ( ( d |` ( { e } X. N ) ) ( R maMul <. { e } , N , N >. ) G ) ) )
209 14 adantr 
 |-  ( ( ( R e. CRing /\ F e. B /\ G e. B ) /\ ( ( b e. B /\ c e. ( Base ` R ) ) /\ ( d e. B /\ e e. N ) ) ) -> R e. Ring )
210 102 a1i 
 |-  ( ( ( R e. CRing /\ F e. B /\ G e. B ) /\ ( ( b e. B /\ c e. ( Base ` R ) ) /\ ( d e. B /\ e e. N ) ) ) -> { e } e. Fin )
211 simprlr 
 |-  ( ( ( R e. CRing /\ F e. B /\ G e. B ) /\ ( ( b e. B /\ c e. ( Base ` R ) ) /\ ( d e. B /\ e e. N ) ) ) -> c e. ( Base ` R ) )
212 197 109 syl 
 |-  ( ( ( R e. CRing /\ F e. B /\ G e. B ) /\ ( ( b e. B /\ c e. ( Base ` R ) ) /\ ( d e. B /\ e e. N ) ) ) -> ( { e } X. N ) C_ ( N X. N ) )
213 205 212 115 syl2anc 
 |-  ( ( ( R e. CRing /\ F e. B /\ G e. B ) /\ ( ( b e. B /\ c e. ( Base ` R ) ) /\ ( d e. B /\ e e. N ) ) ) -> ( d |` ( { e } X. N ) ) e. ( ( Base ` R ) ^m ( { e } X. N ) ) )
214 6 209 101 210 195 195 4 211 213 199 mamuvs1 
 |-  ( ( ( R e. CRing /\ F e. B /\ G e. B ) /\ ( ( b e. B /\ c e. ( Base ` R ) ) /\ ( d e. B /\ e e. N ) ) ) -> ( ( ( ( { e } X. N ) X. { c } ) oF .x. ( d |` ( { e } X. N ) ) ) ( R maMul <. { e } , N , N >. ) G ) = ( ( ( { e } X. N ) X. { c } ) oF .x. ( ( d |` ( { e } X. N ) ) ( R maMul <. { e } , N , N >. ) G ) ) )
215 208 214 eqtr4d 
 |-  ( ( ( R e. CRing /\ F e. B /\ G e. B ) /\ ( ( b e. B /\ c e. ( Base ` R ) ) /\ ( d e. B /\ e e. N ) ) ) -> ( ( ( { e } X. N ) X. { c } ) oF .x. ( ( d .xb G ) |` ( { e } X. N ) ) ) = ( ( ( ( { e } X. N ) X. { c } ) oF .x. ( d |` ( { e } X. N ) ) ) ( R maMul <. { e } , N , N >. ) G ) )
216 215 3adant3 
 |-  ( ( ( R e. CRing /\ F e. B /\ G e. B ) /\ ( ( b e. B /\ c e. ( Base ` R ) ) /\ ( d e. B /\ e e. N ) ) /\ ( ( b |` ( { e } X. N ) ) = ( ( ( { e } X. N ) X. { c } ) oF .x. ( d |` ( { e } X. N ) ) ) /\ ( b |` ( ( N \ { e } ) X. N ) ) = ( d |` ( ( N \ { e } ) X. N ) ) ) ) -> ( ( ( { e } X. N ) X. { c } ) oF .x. ( ( d .xb G ) |` ( { e } X. N ) ) ) = ( ( ( ( { e } X. N ) X. { c } ) oF .x. ( d |` ( { e } X. N ) ) ) ( R maMul <. { e } , N , N >. ) G ) )
217 190 202 216 3eqtr4d 
 |-  ( ( ( R e. CRing /\ F e. B /\ G e. B ) /\ ( ( b e. B /\ c e. ( Base ` R ) ) /\ ( d e. B /\ e e. N ) ) /\ ( ( b |` ( { e } X. N ) ) = ( ( ( { e } X. N ) X. { c } ) oF .x. ( d |` ( { e } X. N ) ) ) /\ ( b |` ( ( N \ { e } ) X. N ) ) = ( d |` ( ( N \ { e } ) X. N ) ) ) ) -> ( ( b .xb G ) |` ( { e } X. N ) ) = ( ( ( { e } X. N ) X. { c } ) oF .x. ( ( d .xb G ) |` ( { e } X. N ) ) ) )
218 simp3r 
 |-  ( ( ( R e. CRing /\ F e. B /\ G e. B ) /\ ( ( b e. B /\ c e. ( Base ` R ) ) /\ ( d e. B /\ e e. N ) ) /\ ( ( b |` ( { e } X. N ) ) = ( ( ( { e } X. N ) X. { c } ) oF .x. ( d |` ( { e } X. N ) ) ) /\ ( b |` ( ( N \ { e } ) X. N ) ) = ( d |` ( ( N \ { e } ) X. N ) ) ) ) -> ( b |` ( ( N \ { e } ) X. N ) ) = ( d |` ( ( N \ { e } ) X. N ) ) )
219 218 oveq1d 
 |-  ( ( ( R e. CRing /\ F e. B /\ G e. B ) /\ ( ( b e. B /\ c e. ( Base ` R ) ) /\ ( d e. B /\ e e. N ) ) /\ ( ( b |` ( { e } X. N ) ) = ( ( ( { e } X. N ) X. { c } ) oF .x. ( d |` ( { e } X. N ) ) ) /\ ( b |` ( ( N \ { e } ) X. N ) ) = ( d |` ( ( N \ { e } ) X. N ) ) ) ) -> ( ( b |` ( ( N \ { e } ) X. N ) ) ( R maMul <. ( N \ { e } ) , N , N >. ) G ) = ( ( d |` ( ( N \ { e } ) X. N ) ) ( R maMul <. ( N \ { e } ) , N , N >. ) G ) )
220 192 reseq1d 
 |-  ( ( ( R e. CRing /\ F e. B /\ G e. B ) /\ ( ( b e. B /\ c e. ( Base ` R ) ) /\ ( d e. B /\ e e. N ) ) ) -> ( ( b ( R maMul <. N , N , N >. ) G ) |` ( ( N \ { e } ) X. N ) ) = ( ( b .xb G ) |` ( ( N \ { e } ) X. N ) ) )
221 difssd 
 |-  ( ( ( R e. CRing /\ F e. B /\ G e. B ) /\ ( ( b e. B /\ c e. ( Base ` R ) ) /\ ( d e. B /\ e e. N ) ) ) -> ( N \ { e } ) C_ N )
222 52 143 6 194 195 195 195 221 198 199 mamures 
 |-  ( ( ( R e. CRing /\ F e. B /\ G e. B ) /\ ( ( b e. B /\ c e. ( Base ` R ) ) /\ ( d e. B /\ e e. N ) ) ) -> ( ( b ( R maMul <. N , N , N >. ) G ) |` ( ( N \ { e } ) X. N ) ) = ( ( b |` ( ( N \ { e } ) X. N ) ) ( R maMul <. ( N \ { e } ) , N , N >. ) G ) )
223 220 222 eqtr3d 
 |-  ( ( ( R e. CRing /\ F e. B /\ G e. B ) /\ ( ( b e. B /\ c e. ( Base ` R ) ) /\ ( d e. B /\ e e. N ) ) ) -> ( ( b .xb G ) |` ( ( N \ { e } ) X. N ) ) = ( ( b |` ( ( N \ { e } ) X. N ) ) ( R maMul <. ( N \ { e } ) , N , N >. ) G ) )
224 223 3adant3 
 |-  ( ( ( R e. CRing /\ F e. B /\ G e. B ) /\ ( ( b e. B /\ c e. ( Base ` R ) ) /\ ( d e. B /\ e e. N ) ) /\ ( ( b |` ( { e } X. N ) ) = ( ( ( { e } X. N ) X. { c } ) oF .x. ( d |` ( { e } X. N ) ) ) /\ ( b |` ( ( N \ { e } ) X. N ) ) = ( d |` ( ( N \ { e } ) X. N ) ) ) ) -> ( ( b .xb G ) |` ( ( N \ { e } ) X. N ) ) = ( ( b |` ( ( N \ { e } ) X. N ) ) ( R maMul <. ( N \ { e } ) , N , N >. ) G ) )
225 203 reseq1d 
 |-  ( ( ( R e. CRing /\ F e. B /\ G e. B ) /\ ( ( b e. B /\ c e. ( Base ` R ) ) /\ ( d e. B /\ e e. N ) ) ) -> ( ( d ( R maMul <. N , N , N >. ) G ) |` ( ( N \ { e } ) X. N ) ) = ( ( d .xb G ) |` ( ( N \ { e } ) X. N ) ) )
226 52 143 6 194 195 195 195 221 205 199 mamures 
 |-  ( ( ( R e. CRing /\ F e. B /\ G e. B ) /\ ( ( b e. B /\ c e. ( Base ` R ) ) /\ ( d e. B /\ e e. N ) ) ) -> ( ( d ( R maMul <. N , N , N >. ) G ) |` ( ( N \ { e } ) X. N ) ) = ( ( d |` ( ( N \ { e } ) X. N ) ) ( R maMul <. ( N \ { e } ) , N , N >. ) G ) )
227 225 226 eqtr3d 
 |-  ( ( ( R e. CRing /\ F e. B /\ G e. B ) /\ ( ( b e. B /\ c e. ( Base ` R ) ) /\ ( d e. B /\ e e. N ) ) ) -> ( ( d .xb G ) |` ( ( N \ { e } ) X. N ) ) = ( ( d |` ( ( N \ { e } ) X. N ) ) ( R maMul <. ( N \ { e } ) , N , N >. ) G ) )
228 227 3adant3 
 |-  ( ( ( R e. CRing /\ F e. B /\ G e. B ) /\ ( ( b e. B /\ c e. ( Base ` R ) ) /\ ( d e. B /\ e e. N ) ) /\ ( ( b |` ( { e } X. N ) ) = ( ( ( { e } X. N ) X. { c } ) oF .x. ( d |` ( { e } X. N ) ) ) /\ ( b |` ( ( N \ { e } ) X. N ) ) = ( d |` ( ( N \ { e } ) X. N ) ) ) ) -> ( ( d .xb G ) |` ( ( N \ { e } ) X. N ) ) = ( ( d |` ( ( N \ { e } ) X. N ) ) ( R maMul <. ( N \ { e } ) , N , N >. ) G ) )
229 219 224 228 3eqtr4d 
 |-  ( ( ( R e. CRing /\ F e. B /\ G e. B ) /\ ( ( b e. B /\ c e. ( Base ` R ) ) /\ ( d e. B /\ e e. N ) ) /\ ( ( b |` ( { e } X. N ) ) = ( ( ( { e } X. N ) X. { c } ) oF .x. ( d |` ( { e } X. N ) ) ) /\ ( b |` ( ( N \ { e } ) X. N ) ) = ( d |` ( ( N \ { e } ) X. N ) ) ) ) -> ( ( b .xb G ) |` ( ( N \ { e } ) X. N ) ) = ( ( d .xb G ) |` ( ( N \ { e } ) X. N ) ) )
230 3 1 2 6 4 178 183 184 187 188 217 229 mdetrsca 
 |-  ( ( ( R e. CRing /\ F e. B /\ G e. B ) /\ ( ( b e. B /\ c e. ( Base ` R ) ) /\ ( d e. B /\ e e. N ) ) /\ ( ( b |` ( { e } X. N ) ) = ( ( ( { e } X. N ) X. { c } ) oF .x. ( d |` ( { e } X. N ) ) ) /\ ( b |` ( ( N \ { e } ) X. N ) ) = ( d |` ( ( N \ { e } ) X. N ) ) ) ) -> ( D ` ( b .xb G ) ) = ( c .x. ( D ` ( d .xb G ) ) ) )
231 simp2ll 
 |-  ( ( ( R e. CRing /\ F e. B /\ G e. B ) /\ ( ( b e. B /\ c e. ( Base ` R ) ) /\ ( d e. B /\ e e. N ) ) /\ ( ( b |` ( { e } X. N ) ) = ( ( ( { e } X. N ) X. { c } ) oF .x. ( d |` ( { e } X. N ) ) ) /\ ( b |` ( ( N \ { e } ) X. N ) ) = ( d |` ( ( N \ { e } ) X. N ) ) ) ) -> b e. B )
232 231 31 syl 
 |-  ( ( ( R e. CRing /\ F e. B /\ G e. B ) /\ ( ( b e. B /\ c e. ( Base ` R ) ) /\ ( d e. B /\ e e. N ) ) /\ ( ( b |` ( { e } X. N ) ) = ( ( ( { e } X. N ) X. { c } ) oF .x. ( d |` ( { e } X. N ) ) ) /\ ( b |` ( ( N \ { e } ) X. N ) ) = ( d |` ( ( N \ { e } ) X. N ) ) ) ) -> ( ( a e. B |-> ( D ` ( a .xb G ) ) ) ` b ) = ( D ` ( b .xb G ) ) )
233 simp2rl 
 |-  ( ( ( R e. CRing /\ F e. B /\ G e. B ) /\ ( ( b e. B /\ c e. ( Base ` R ) ) /\ ( d e. B /\ e e. N ) ) /\ ( ( b |` ( { e } X. N ) ) = ( ( ( { e } X. N ) X. { c } ) oF .x. ( d |` ( { e } X. N ) ) ) /\ ( b |` ( ( N \ { e } ) X. N ) ) = ( d |` ( ( N \ { e } ) X. N ) ) ) ) -> d e. B )
234 169 oveq2d 
 |-  ( d e. B -> ( c .x. ( ( a e. B |-> ( D ` ( a .xb G ) ) ) ` d ) ) = ( c .x. ( D ` ( d .xb G ) ) ) )
235 233 234 syl 
 |-  ( ( ( R e. CRing /\ F e. B /\ G e. B ) /\ ( ( b e. B /\ c e. ( Base ` R ) ) /\ ( d e. B /\ e e. N ) ) /\ ( ( b |` ( { e } X. N ) ) = ( ( ( { e } X. N ) X. { c } ) oF .x. ( d |` ( { e } X. N ) ) ) /\ ( b |` ( ( N \ { e } ) X. N ) ) = ( d |` ( ( N \ { e } ) X. N ) ) ) ) -> ( c .x. ( ( a e. B |-> ( D ` ( a .xb G ) ) ) ` d ) ) = ( c .x. ( D ` ( d .xb G ) ) ) )
236 230 232 235 3eqtr4d 
 |-  ( ( ( R e. CRing /\ F e. B /\ G e. B ) /\ ( ( b e. B /\ c e. ( Base ` R ) ) /\ ( d e. B /\ e e. N ) ) /\ ( ( b |` ( { e } X. N ) ) = ( ( ( { e } X. N ) X. { c } ) oF .x. ( d |` ( { e } X. N ) ) ) /\ ( b |` ( ( N \ { e } ) X. N ) ) = ( d |` ( ( N \ { e } ) X. N ) ) ) ) -> ( ( a e. B |-> ( D ` ( a .xb G ) ) ) ` b ) = ( c .x. ( ( a e. B |-> ( D ` ( a .xb G ) ) ) ` d ) ) )
237 236 3expia 
 |-  ( ( ( R e. CRing /\ F e. B /\ G e. B ) /\ ( ( b e. B /\ c e. ( Base ` R ) ) /\ ( d e. B /\ e e. N ) ) ) -> ( ( ( b |` ( { e } X. N ) ) = ( ( ( { e } X. N ) X. { c } ) oF .x. ( d |` ( { e } X. N ) ) ) /\ ( b |` ( ( N \ { e } ) X. N ) ) = ( d |` ( ( N \ { e } ) X. N ) ) ) -> ( ( a e. B |-> ( D ` ( a .xb G ) ) ) ` b ) = ( c .x. ( ( a e. B |-> ( D ` ( a .xb G ) ) ) ` d ) ) ) )
238 237 anassrs 
 |-  ( ( ( ( R e. CRing /\ F e. B /\ G e. B ) /\ ( b e. B /\ c e. ( Base ` R ) ) ) /\ ( d e. B /\ e e. N ) ) -> ( ( ( b |` ( { e } X. N ) ) = ( ( ( { e } X. N ) X. { c } ) oF .x. ( d |` ( { e } X. N ) ) ) /\ ( b |` ( ( N \ { e } ) X. N ) ) = ( d |` ( ( N \ { e } ) X. N ) ) ) -> ( ( a e. B |-> ( D ` ( a .xb G ) ) ) ` b ) = ( c .x. ( ( a e. B |-> ( D ` ( a .xb G ) ) ) ` d ) ) ) )
239 238 ralrimivva 
 |-  ( ( ( R e. CRing /\ F e. B /\ G e. B ) /\ ( b e. B /\ c e. ( Base ` R ) ) ) -> A. d e. B A. e e. N ( ( ( b |` ( { e } X. N ) ) = ( ( ( { e } X. N ) X. { c } ) oF .x. ( d |` ( { e } X. N ) ) ) /\ ( b |` ( ( N \ { e } ) X. N ) ) = ( d |` ( ( N \ { e } ) X. N ) ) ) -> ( ( a e. B |-> ( D ` ( a .xb G ) ) ) ` b ) = ( c .x. ( ( a e. B |-> ( D ` ( a .xb G ) ) ) ` d ) ) ) )
240 239 ralrimivva 
 |-  ( ( R e. CRing /\ F e. B /\ G e. B ) -> A. b e. B A. c e. ( Base ` R ) A. d e. B A. e e. N ( ( ( b |` ( { e } X. N ) ) = ( ( ( { e } X. N ) X. { c } ) oF .x. ( d |` ( { e } X. N ) ) ) /\ ( b |` ( ( N \ { e } ) X. N ) ) = ( d |` ( ( N \ { e } ) X. N ) ) ) -> ( ( a e. B |-> ( D ` ( a .xb G ) ) ) ` b ) = ( c .x. ( ( a e. B |-> ( D ` ( a .xb G ) ) ) ` d ) ) ) )
241 simp2 
 |-  ( ( R e. CRing /\ F e. B /\ G e. B ) -> F e. B )
242 1 2 6 7 8 9 4 12 14 26 82 177 240 3 51 241 mdetuni0 
 |-  ( ( R e. CRing /\ F e. B /\ G e. B ) -> ( ( a e. B |-> ( D ` ( a .xb G ) ) ) ` F ) = ( ( ( a e. B |-> ( D ` ( a .xb G ) ) ) ` ( 1r ` A ) ) .x. ( D ` F ) ) )
243 fvoveq1 
 |-  ( a = F -> ( D ` ( a .xb G ) ) = ( D ` ( F .xb G ) ) )
244 fvex 
 |-  ( D ` ( F .xb G ) ) e. _V
245 243 29 244 fvmpt 
 |-  ( F e. B -> ( ( a e. B |-> ( D ` ( a .xb G ) ) ) ` F ) = ( D ` ( F .xb G ) ) )
246 245 3ad2ant2 
 |-  ( ( R e. CRing /\ F e. B /\ G e. B ) -> ( ( a e. B |-> ( D ` ( a .xb G ) ) ) ` F ) = ( D ` ( F .xb G ) ) )
247 eqid 
 |-  ( 1r ` A ) = ( 1r ` A )
248 2 247 ringidcl 
 |-  ( A e. Ring -> ( 1r ` A ) e. B )
249 fvoveq1 
 |-  ( a = ( 1r ` A ) -> ( D ` ( a .xb G ) ) = ( D ` ( ( 1r ` A ) .xb G ) ) )
250 fvex 
 |-  ( D ` ( ( 1r ` A ) .xb G ) ) e. _V
251 249 29 250 fvmpt 
 |-  ( ( 1r ` A ) e. B -> ( ( a e. B |-> ( D ` ( a .xb G ) ) ) ` ( 1r ` A ) ) = ( D ` ( ( 1r ` A ) .xb G ) ) )
252 19 248 251 3syl 
 |-  ( ( R e. CRing /\ F e. B /\ G e. B ) -> ( ( a e. B |-> ( D ` ( a .xb G ) ) ) ` ( 1r ` A ) ) = ( D ` ( ( 1r ` A ) .xb G ) ) )
253 simp3 
 |-  ( ( R e. CRing /\ F e. B /\ G e. B ) -> G e. B )
254 2 5 247 ringlidm 
 |-  ( ( A e. Ring /\ G e. B ) -> ( ( 1r ` A ) .xb G ) = G )
255 19 253 254 syl2anc 
 |-  ( ( R e. CRing /\ F e. B /\ G e. B ) -> ( ( 1r ` A ) .xb G ) = G )
256 255 fveq2d 
 |-  ( ( R e. CRing /\ F e. B /\ G e. B ) -> ( D ` ( ( 1r ` A ) .xb G ) ) = ( D ` G ) )
257 252 256 eqtrd 
 |-  ( ( R e. CRing /\ F e. B /\ G e. B ) -> ( ( a e. B |-> ( D ` ( a .xb G ) ) ) ` ( 1r ` A ) ) = ( D ` G ) )
258 257 oveq1d 
 |-  ( ( R e. CRing /\ F e. B /\ G e. B ) -> ( ( ( a e. B |-> ( D ` ( a .xb G ) ) ) ` ( 1r ` A ) ) .x. ( D ` F ) ) = ( ( D ` G ) .x. ( D ` F ) ) )
259 16 253 ffvelrnd 
 |-  ( ( R e. CRing /\ F e. B /\ G e. B ) -> ( D ` G ) e. ( Base ` R ) )
260 16 241 ffvelrnd 
 |-  ( ( R e. CRing /\ F e. B /\ G e. B ) -> ( D ` F ) e. ( Base ` R ) )
261 6 4 crngcom 
 |-  ( ( R e. CRing /\ ( D ` G ) e. ( Base ` R ) /\ ( D ` F ) e. ( Base ` R ) ) -> ( ( D ` G ) .x. ( D ` F ) ) = ( ( D ` F ) .x. ( D ` G ) ) )
262 51 259 260 261 syl3anc 
 |-  ( ( R e. CRing /\ F e. B /\ G e. B ) -> ( ( D ` G ) .x. ( D ` F ) ) = ( ( D ` F ) .x. ( D ` G ) ) )
263 258 262 eqtrd 
 |-  ( ( R e. CRing /\ F e. B /\ G e. B ) -> ( ( ( a e. B |-> ( D ` ( a .xb G ) ) ) ` ( 1r ` A ) ) .x. ( D ` F ) ) = ( ( D ` F ) .x. ( D ` G ) ) )
264 242 246 263 3eqtr3d 
 |-  ( ( R e. CRing /\ F e. B /\ G e. B ) -> ( D ` ( F .xb G ) ) = ( ( D ` F ) .x. ( D ` G ) ) )