MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  mdetmul Structured version   Unicode version
Theorem mdetmul 18441
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.)
Hypotheses
Ref Expression
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
Ref Expression
mdetmul |- ( ( R e. CRing /\ F e. B /\ G e. B ) -> ( D ` ( F .xb G ) ) = ( ( D ` F ) .x. ( D ` G ) ) )
Proof of Theorem mdetmul
Dummy variables a b c d e are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 mdetmul.a . . 3 |- A = ( N Mat R )
2 mdetmul.b . . 3 |- B = ( Base ` A )
3 eqid 2443 . . 3 |- ( Base ` R ) = ( Base ` R )
4 eqid 2443 . . 3 |- ( 0g ` R ) = ( 0g ` R )
5 eqid 2443 . . 3 |- ( 1r ` R ) = ( 1r ` R )
6 eqid 2443 . . 3 |- ( +g ` R ) = ( +g ` R )
7 mdetmul.t1 . . 3 |- .x. = ( .r ` R )
81, 2matrcl 18324 . . . . 5 |- ( F e. B -> ( N e. Fin /\ R e. _V ) )
98simpld 459 . . . 4 |- ( F e. B -> N e. Fin )
1093ad2ant2 1010 . . 3 |- ( ( R e. CRing /\ F e. B /\ G e. B ) -> N e. Fin )
11 crngrng 16667 . . . 4 |- ( R e. CRing -> R e. Ring )
12113ad2ant1 1009 . . 3 |- ( ( R e. CRing /\ F e. B /\ G e. B ) -> R e. Ring )
13 mdetmul.d . . . . . . . 8 |- D = ( N maDet R )
1413, 1, 2, 3mdetf 18418 . . . . . . 7 |- ( R e. CRing -> D : B --> ( Base ` R ) )
15143ad2ant1 1009 . . . . . 6 |- ( ( R e. CRing /\ F e. B /\ G e. B ) -> D : B --> ( Base ` R ) )
1615adantr 465 . . . . 5 |- ( ( ( R e. CRing /\ F e. B /\ G e. B ) /\ a e. B ) -> D : B --> ( Base ` R ) )
171matrng 18342 . . . . . . . 8 |- ( ( N e. Fin /\ R e. Ring ) -> A e. Ring )
1810, 12, 17syl2anc 661 . . . . . . 7 |- ( ( R e. CRing /\ F e. B /\ G e. B ) -> A e. Ring )
1918adantr 465 . . . . . 6 |- ( ( ( R e. CRing /\ F e. B /\ G e. B ) /\ a e. B ) -> A e. Ring )
20 simpr 461 . . . . . 6 |- ( ( ( R e. CRing /\ F e. B /\ G e. B ) /\ a e. B ) -> a e. B )
21 simpl3 993 . . . . . 6 |- ( ( ( R e. CRing /\ F e. B /\ G e. B ) /\ a e. B ) -> G e. B )
22 mdetmul.t2 . . . . . . 7 |- .xb = ( .r ` A )
232, 22rngcl 16670 . . . . . 6 |- ( ( A e. Ring /\ a e. B /\ G e. B ) -> ( a .xb G ) e. B )
2419, 20, 21, 23syl3anc 1218 . . . . 5 |- ( ( ( R e. CRing /\ F e. B /\ G e. B ) /\ a e. B ) -> ( a .xb G ) e. B )
2516, 24ffvelrnd 5856 . . . 4 |- ( ( ( R e. CRing /\ F e. B /\ G e. B ) /\ a e. B ) -> ( D ` ( a .xb G ) ) e. ( Base ` R ) )
26 eqid 2443 . . . 4 |- ( a e. B |-> ( D ` ( a .xb G ) ) ) = ( a e. B |-> ( D ` ( a .xb G ) ) )
2725, 26fmptd 5879 . . 3 |- ( ( R e. CRing /\ F e. B /\ G e. B ) -> ( a e. B |-> ( D ` ( a .xb G ) ) ) : B --> ( Base ` R ) )
28 simp21 1021 . . . . . . 7 |- ( ( ( 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 )
29 oveq1 6110 . . . . . . . . 9 |- ( a = b -> ( a .xb G ) = ( b .xb G ) )
3029fveq2d 5707 . . . . . . . 8 |- ( a = b -> ( D ` ( a .xb G ) ) = ( D ` ( b .xb G ) ) )
31 fvex 5713 . . . . . . . 8 |- ( D ` ( b .xb G ) ) e. _V
3230, 26, 31fvmpt 5786 . . . . . . 7 |- ( b e. B -> ( ( a e. B |-> ( D ` ( a .xb G ) ) ) ` b ) = ( D ` ( b .xb G ) ) )
3328, 32syl 16 . . . . . 6 |- ( ( ( 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 ) ) )
34 simp11 1018 . . . . . . 7 |- ( ( ( 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 )
3518adantr 465 . . . . . . . . 9 |- ( ( ( R e. CRing /\ F e. B /\ G e. B ) /\ ( b e. B /\ c e. N /\ d e. N ) ) -> A e. Ring )
36 simpr1 994 . . . . . . . . 9 |- ( ( ( R e. CRing /\ F e. B /\ G e. B ) /\ ( b e. B /\ c e. N /\ d e. N ) ) -> b e. B )
37 simpl3 993 . . . . . . . . 9 |- ( ( ( R e. CRing /\ F e. B /\ G e. B ) /\ ( b e. B /\ c e. N /\ d e. N ) ) -> G e. B )
382, 22rngcl 16670 . . . . . . . . 9 |- ( ( A e. Ring /\ b e. B /\ G e. B ) -> ( b .xb G ) e. B )
3935, 36, 37, 38syl3anc 1218 . . . . . . . 8 |- ( ( ( R e. CRing /\ F e. B /\ G e. B ) /\ ( b e. B /\ c e. N /\ d e. N ) ) -> ( b .xb G ) e. B )
40393adant3 1008 . . . . . . 7 |- ( ( ( 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 )
41 simp22 1022 . . . . . . 7 |- ( ( ( 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 )
42 simp23 1023 . . . . . . 7 |- ( ( ( 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 )
43 simp3l 1016 . . . . . . 7 |- ( ( ( 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 )
44 simpl3r 1044 . . . . . . . . . 10 |- ( ( ( ( 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 ) )
45 eqid 2443 . . . . . . . . . . . 12 |- N = N
46 oveq1 6110 . . . . . . . . . . . . 13 |- ( ( c b e ) = ( d b e ) -> ( ( c b e ) .x. ( e G a ) ) = ( ( d b e ) .x. ( e G a ) ) )
4746ralimi 2803 . . . . . . . . . . . 12 |- ( 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 ) ) )
48 mpteq12 4383 . . . . . . . . . . . 12 |- ( ( 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 ) ) ) )
4945, 47, 48sylancr 663 . . . . . . . . . . 11 |- ( 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 ) ) ) )
5049oveq2d 6119 . . . . . . . . . 10 |- ( A. e e. N ( c b e ) = ( d b e ) -> ( R gsumg ( e e. N |-> ( ( c b e ) .x. ( e G a ) ) ) ) = ( R gsumg ( e e. N |-> ( ( d b e ) .x. ( e G a ) ) ) ) )
5144, 50syl 16 . . . . . . . . 9 |- ( ( ( ( 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 gsumg ( e e. N |-> ( ( c b e ) .x. ( e G a ) ) ) ) = ( R gsumg ( e e. N |-> ( ( d b e ) .x. ( e G a ) ) ) ) )
52 simp1 988 . . . . . . . . . . . . . . 15 |- ( ( R e. CRing /\ F e. B /\ G e. B ) -> R e. CRing )
53 eqid 2443 . . . . . . . . . . . . . . . . 17 |- ( R maMul <. N , N , N >. ) = ( R maMul <. N , N , N >. )
541, 53matmulr 18325 . . . . . . . . . . . . . . . 16 |- ( ( N e. Fin /\ R e. CRing ) -> ( R maMul <. N , N , N >. ) = ( .r ` A ) )
5554, 22syl6eqr 2493 . . . . . . . . . . . . . . 15 |- ( ( N e. Fin /\ R e. CRing ) -> ( R maMul <. N , N , N >. ) = .xb )
5610, 52, 55syl2anc 661 . . . . . . . . . . . . . 14 |- ( ( R e. CRing /\ F e. B /\ G e. B ) -> ( R maMul <. N , N , N >. ) = .xb )
5756ad2antrr 725 . . . . . . . . . . . . 13 |- ( ( ( ( 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 )
5857oveqd 6120 . . . . . . . . . . . 12 |- ( ( ( ( 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 ) )
5958oveqd 6120 . . . . . . . . . . 11 |- ( ( ( ( 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 ) )
60 simpll1 1027 . . . . . . . . . . . 12 |- ( ( ( ( R e. CRing /\ F e. B /\ G e. B ) /\ ( b e. B /\ c e. N /\ d e. N ) ) /\ a e. N ) -> R e. CRing )
6110ad2antrr 725 . . . . . . . . . . . 12 |- ( ( ( ( R e. CRing /\ F e. B /\ G e. B ) /\ ( b e. B /\ c e. N /\ d e. N ) ) /\ a e. N ) -> N e. Fin )
62 simplr1 1030 . . . . . . . . . . . . 13 |- ( ( ( ( R e. CRing /\ F e. B /\ G e. B ) /\ ( b e. B /\ c e. N /\ d e. N ) ) /\ a e. N ) -> b e. B )
631, 3, 2matbas2i 18335 . . . . . . . . . . . . 13 |- ( b e. B -> b e. ( ( Base ` R ) ^m ( N X. N ) ) )
6462, 63syl 16 . . . . . . . . . . . 12 |- ( ( ( ( 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 ) ) )
651, 3, 2matbas2i 18335 . . . . . . . . . . . . . 14 |- ( G e. B -> G e. ( ( Base ` R ) ^m ( N X. N ) ) )
66653ad2ant3 1011 . . . . . . . . . . . . 13 |- ( ( R e. CRing /\ F e. B /\ G e. B ) -> G e. ( ( Base ` R ) ^m ( N X. N ) ) )
6766ad2antrr 725 . . . . . . . . . . . 12 |- ( ( ( ( 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 ) ) )
68 simplr2 1031 . . . . . . . . . . . 12 |- ( ( ( ( R e. CRing /\ F e. B /\ G e. B ) /\ ( b e. B /\ c e. N /\ d e. N ) ) /\ a e. N ) -> c e. N )
69 simpr 461 . . . . . . . . . . . 12 |- ( ( ( ( R e. CRing /\ F e. B /\ G e. B ) /\ ( b e. B /\ c e. N /\ d e. N ) ) /\ a e. N ) -> a e. N )
7053, 3, 7, 60, 61, 61, 61, 64, 67, 68, 69mamufv 18297 . . . . . . . . . . 11 |- ( ( ( ( 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 gsumg ( e e. N |-> ( ( c b e ) .x. ( e G a ) ) ) ) )
7159, 70eqtr3d 2477 . . . . . . . . . 10 |- ( ( ( ( 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 gsumg ( e e. N |-> ( ( c b e ) .x. ( e G a ) ) ) ) )
72713adantl3 1146 . . . . . . . . 9 |- ( ( ( ( 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 gsumg ( e e. N |-> ( ( c b e ) .x. ( e G a ) ) ) ) )
7358oveqd 6120 . . . . . . . . . . 11 |- ( ( ( ( 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 ) )
74 simplr3 1032 . . . . . . . . . . . 12 |- ( ( ( ( R e. CRing /\ F e. B /\ G e. B ) /\ ( b e. B /\ c e. N /\ d e. N ) ) /\ a e. N ) -> d e. N )
7553, 3, 7, 60, 61, 61, 61, 64, 67, 74, 69mamufv 18297 . . . . . . . . . . 11 |- ( ( ( ( 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 gsumg ( e e. N |-> ( ( d b e ) .x. ( e G a ) ) ) ) )
7673, 75eqtr3d 2477 . . . . . . . . . 10 |- ( ( ( ( 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 gsumg ( e e. N |-> ( ( d b e ) .x. ( e G a ) ) ) ) )
77763adantl3 1146 . . . . . . . . 9 |- ( ( ( ( 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 gsumg ( e e. N |-> ( ( d b e ) .x. ( e G a ) ) ) ) )
7851, 72, 773eqtr4d 2485 . . . . . . . 8 |- ( ( ( ( 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 ) )
7978ralrimiva 2811 . . . . . . 7 |- ( ( ( 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 ) )
8013, 1, 2, 4, 34, 40, 41, 42, 43, 79mdetralt 18426 . . . . . 6 |- ( ( ( 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 ) )
8133, 80eqtrd 2475 . . . . 5 |- ( ( ( 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 ) )
82813expia 1189 . . . 4 |- ( ( ( 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 ) ) )
8382ralrimivvva 2821 . . 3 |- ( ( 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 ) ) )
84 simp11 1018 . . . . . . . . 9 |- ( ( ( 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 )
8518adantr 465 . . . . . . . . . . 11 |- ( ( ( R e. CRing /\ F e. B /\ G e. B ) /\ ( ( b e. B /\ c e. B ) /\ ( d e. B /\ e e. N ) ) ) -> A e. Ring )
86 simprll 761 . . . . . . . . . . 11 |- ( ( ( R e. CRing /\ F e. B /\ G e. B ) /\ ( ( b e. B /\ c e. B ) /\ ( d e. B /\ e e. N ) ) ) -> b e. B )
87 simpl3 993 . . . . . . . . . . 11 |- ( ( ( R e. CRing /\ F e. B /\ G e. B ) /\ ( ( b e. B /\ c e. B ) /\ ( d e. B /\ e e. N ) ) ) -> G e. B )
8885, 86, 87, 38syl3anc 1218 . . . . . . . . . 10 |- ( ( ( 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 )
89883adant3 1008 . . . . . . . . 9 |- ( ( ( 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 )
90 simprlr 762 . . . . . . . . . . 11 |- ( ( ( R e. CRing /\ F e. B /\ G e. B ) /\ ( ( b e. B /\ c e. B ) /\ ( d e. B /\ e e. N ) ) ) -> c e. B )
912, 22rngcl 16670 . . . . . . . . . . 11 |- ( ( A e. Ring /\ c e. B /\ G e. B ) -> ( c .xb G ) e. B )
9285, 90, 87, 91syl3anc 1218 . . . . . . . . . 10 |- ( ( ( 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 )
93923adant3 1008 . . . . . . . . 9 |- ( ( ( 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 )
94 simprrl 763 . . . . . . . . . . 11 |- ( ( ( R e. CRing /\ F e. B /\ G e. B ) /\ ( ( b e. B /\ c e. B ) /\ ( d e. B /\ e e. N ) ) ) -> d e. B )
952, 22rngcl 16670 . . . . . . . . . . 11 |- ( ( A e. Ring /\ d e. B /\ G e. B ) -> ( d .xb G ) e. B )
9685, 94, 87, 95syl3anc 1218 . . . . . . . . . 10 |- ( ( ( 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 )
97963adant3 1008 . . . . . . . . 9 |- ( ( ( 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 )
98 simp2rr 1058 . . . . . . . . 9 |- ( ( ( 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 )
99 simp31 1024 . . . . . . . . . . . 12 |- ( ( ( 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 ) ) ) )
10099oveq1d 6118 . . . . . . . . . . 11 |- ( ( ( 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 ) )
10112adantr 465 . . . . . . . . . . . . 13 |- ( ( ( R e. CRing /\ F e. B /\ G e. B ) /\ ( ( b e. B /\ c e. B ) /\ ( d e. B /\ e e. N ) ) ) -> R e. Ring )
102 eqid 2443 . . . . . . . . . . . . 13 |- ( R maMul <. { e } , N , N >. ) = ( R maMul <. { e } , N , N >. )
103 snfi 7402 . . . . . . . . . . . . . 14 |- { e } e. Fin
104103a1i 11 . . . . . . . . . . . . 13 |- ( ( ( R e. CRing /\ F e. B /\ G e. B ) /\ ( ( b e. B /\ c e. B ) /\ ( d e. B /\ e e. N ) ) ) -> { e } e. Fin )
10510adantr 465 . . . . . . . . . . . . 13 |- ( ( ( R e. CRing /\ F e. B /\ G e. B ) /\ ( ( b e. B /\ c e. B ) /\ ( d e. B /\ e e. N ) ) ) -> N e. Fin )
1061, 3, 2matbas2i 18335 . . . . . . . . . . . . . . 15 |- ( c e. B -> c e. ( ( Base ` R ) ^m ( N X. N ) ) )
10790, 106syl 16 . . . . . . . . . . . . . 14 |- ( ( ( 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 ) ) )
108 simprrr 764 . . . . . . . . . . . . . . . 16 |- ( ( ( R e. CRing /\ F e. B /\ G e. B ) /\ ( ( b e. B /\ c e. B ) /\ ( d e. B /\ e e. N ) ) ) -> e e. N )
109108snssd 4030 . . . . . . . . . . . . . . 15 |- ( ( ( R e. CRing /\ F e. B /\ G e. B ) /\ ( ( b e. B /\ c e. B ) /\ ( d e. B /\ e e. N ) ) ) -> { e } C_ N )
110 xpss1 4960 . . . . . . . . . . . . . . 15 |- ( { e } C_ N -> ( { e } X. N ) C_ ( N X. N ) )
111109, 110syl 16 . . . . . . . . . . . . . 14 |- ( ( ( 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 ) )
112 elmapssres 7249 . . . . . . . . . . . . . 14 |- ( ( 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 ) ) )
113107, 111, 112syl2anc 661 . . . . . . . . . . . . 13 |- ( ( ( 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 ) ) )
1141, 3, 2matbas2i 18335 . . . . . . . . . . . . . . 15 |- ( d e. B -> d e. ( ( Base ` R ) ^m ( N X. N ) ) )
11594, 114syl 16 . . . . . . . . . . . . . 14 |- ( ( ( 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 ) ) )
116 elmapssres 7249 . . . . . . . . . . . . . 14 |- ( ( 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 ) ) )
117115, 111, 116syl2anc 661 . . . . . . . . . . . . 13 |- ( ( ( 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 ) ) )
11866adantr 465 . . . . . . . . . . . . 13 |- ( ( ( 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 ) ) )
1193, 101, 102, 104, 105, 105, 6, 113, 117, 118mamudi 18319 . . . . . . . . . . . 12 |- ( ( ( 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 ) ) )
1201193adant3 1008 . . . . . . . . . . 11 |- ( ( ( 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 ) ) )
121100, 120eqtrd 2475 . . . . . . . . . 10 |- ( ( ( 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 ) ) )
12256adantr 465 . . . . . . . . . . . . . 14 |- ( ( ( 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 )
123122oveqd 6120 . . . . . . . . . . . . 13 |- ( ( ( 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 ) )
124123reseq1d 5121 . . . . . . . . . . . 12 |- ( ( ( 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 ) ) )
125 simpl1 991 . . . . . . . . . . . . 13 |- ( ( ( R e. CRing /\ F e. B /\ G e. B ) /\ ( ( b e. B /\ c e. B ) /\ ( d e. B /\ e e. N ) ) ) -> R e. CRing )
12686, 63syl 16 . . . . . . . . . . . . 13 |- ( ( ( 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 ) ) )
12753, 102, 3, 125, 105, 105, 105, 109, 126, 118mamures 18302 . . . . . . . . . . . 12 |- ( ( ( 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 ) )
128124, 127eqtr3d 2477 . . . . . . . . . . 11 |- ( ( ( 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 ) )
1291283adant3 1008 . . . . . . . . . 10 |- ( ( ( 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 ) )
130122oveqd 6120 . . . . . . . . . . . . . 14 |- ( ( ( 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 ) )
131130reseq1d 5121 . . . . . . . . . . . . 13 |- ( ( ( 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 ) ) )
13253, 102, 3, 125, 105, 105, 105, 109, 107, 118mamures 18302 . . . . . . . . . . . . 13 |- ( ( ( 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 ) )
133131, 132eqtr3d 2477 . . . . . . . . . . . 12 |- ( ( ( 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 ) )
134122oveqd 6120 . . . . . . . . . . . . . 14 |- ( ( ( 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 ) )
135134reseq1d 5121 . . . . . . . . . . . . 13 |- ( ( ( 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 ) ) )
13653, 102, 3, 125, 105, 105, 105, 109, 115, 118mamures 18302 . . . . . . . . . . . . 13 |- ( ( ( 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 ) )
137135, 136eqtr3d 2477 . . . . . . . . . . . 12 |- ( ( ( 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 ) )
138133, 137oveq12d 6121 . . . . . . . . . . 11 |- ( ( ( 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 ) ) )
1391383adant3 1008 . . . . . . . . . 10 |- ( ( ( 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 ) ) )
140121, 129, 1393eqtr4d 2485 . . . . . . . . 9 |- ( ( ( 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 ) ) ) )
141 simp32 1025 . . . . . . . . . . 11 |- ( ( ( 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 ) ) )
142141oveq1d 6118 . . . . . . . . . 10 |- ( ( ( 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 ) )
143123reseq1d 5121 . . . . . . . . . . . 12 |- ( ( ( 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 ) ) )
144 eqid 2443 . . . . . . . . . . . . 13 |- ( R maMul <. ( N \ { e } ) , N , N >. ) = ( R maMul <. ( N \ { e } ) , N , N >. )
145 difssd 3496 . . . . . . . . . . . . 13 |- ( ( ( 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 )
14653, 144, 3, 125, 105, 105, 105, 145, 126, 118mamures 18302 . . . . . . . . . . . 12 |- ( ( ( 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 ) )
147143, 146eqtr3d 2477 . . . . . . . . . . 11 |- ( ( ( 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 ) )
1481473adant3 1008 . . . . . . . . . 10 |- ( ( ( 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 ) )
149130reseq1d 5121 . . . . . . . . . . . 12 |- ( ( ( 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 ) ) )
15053, 144, 3, 125, 105, 105, 105, 145, 107, 118mamures 18302 . . . . . . . . . . . 12 |- ( ( ( 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 ) )
151149, 150eqtr3d 2477 . . . . . . . . . . 11 |- ( ( ( 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 ) )
1521513adant3 1008 . . . . . . . . . 10 |- ( ( ( 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 ) )
153142, 148, 1523eqtr4d 2485 . . . . . . . . 9 |- ( ( ( 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 ) ) )
154 simp33 1026 . . . . . . . . . . 11 |- ( ( ( 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 ) ) )
155154oveq1d 6118 . . . . . . . . . 10 |- ( ( ( 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 ) )
156134reseq1d 5121 . . . . . . . . . . . 12 |- ( ( ( 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 ) ) )
15753, 144, 3, 125, 105, 105, 105, 145, 115, 118mamures 18302 . . . . . . . . . . . 12 |- ( ( ( 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 ) )
158156, 157eqtr3d 2477 . . . . . . . . . . 11 |- ( ( ( 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 ) )
1591583adant3 1008 . . . . . . . . . 10 |- ( ( ( 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 ) )
160155, 148, 1593eqtr4d 2485 . . . . . . . . 9 |- ( ( ( 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 ) ) )
16113, 1, 2, 6, 84, 89, 93, 97, 98, 140, 153, 160mdetrlin 18421 . . . . . . . 8 |- ( ( ( 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 ) ) ) )
16286, 32syl 16 . . . . . . . . 9 |- ( ( ( 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 ) ) )
1631623adant3 1008 . . . . . . . 8 |- ( ( ( 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 ) ) )
164 oveq1 6110 . . . . . . . . . . . . 13 |- ( a = c -> ( a .xb G ) = ( c .xb G ) )
165164fveq2d 5707 . . . . . . . . . . . 12 |- ( a = c -> ( D ` ( a .xb G ) ) = ( D ` ( c .xb G ) ) )
166 fvex 5713 . . . . . . . . . . . 12 |- ( D ` ( c .xb G ) ) e. _V
167165, 26, 166fvmpt 5786 . . . . . . . . . . 11 |- ( c e. B -> ( ( a e. B |-> ( D ` ( a .xb G ) ) ) ` c ) = ( D ` ( c .xb G ) ) )
16890, 167syl 16 . . . . . . . . . 10 |- ( ( ( 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 ) ) )
169 oveq1 6110 . . . . . . . . . . . . 13 |- ( a = d -> ( a .xb G ) = ( d .xb G ) )
170169fveq2d 5707 . . . . . . . . . . . 12 |- ( a = d -> ( D ` ( a .xb G ) ) = ( D ` ( d .xb G ) ) )
171 fvex 5713 . . . . . . . . . . . 12 |- ( D ` ( d .xb G ) ) e. _V
172170, 26, 171fvmpt 5786 . . . . . . . . . . 11 |- ( d e. B -> ( ( a e. B |-> ( D ` ( a .xb G ) ) ) ` d ) = ( D ` ( d .xb G ) ) )
17394, 172syl 16 . . . . . . . . . 10 |- ( ( ( 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 ) ) )
174168, 173oveq12d 6121 . . . . . . . . 9 |- ( ( ( 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 ) ) ) )
1751743adant3 1008 . . . . . . . 8 |- ( ( ( 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 ) ) ) )
176161, 163, 1753eqtr4d 2485 . . . . . . 7 |- ( ( ( 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 ) ) )
1771763expia 1189 . . . . . 6 |- ( ( ( 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 ) ) ) )
178177anassrs 648 . . . . 5 |- ( ( ( ( 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 ) ) ) )
179178ralrimivva 2820 . . . 4 |- ( ( ( 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 ) ) ) )
180179ralrimivva 2820 . . 3 |- ( ( 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 ) ) ) )
181 simp11 1018 . . . . . . . . 9 |- ( ( ( 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 )
18218adantr 465 . . . . . . . . . . 11 |- ( ( ( 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 )
183 simprll 761 . . . . . . . . . . 11 |- ( ( ( 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 )
184 simpl3 993 . . . . . . . . . . 11 |- ( ( ( 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 )
185182, 183, 184, 38syl3anc 1218 . . . . . . . . . 10 |- ( ( ( 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 )
1861853adant3 1008 . . . . . . . . 9 |- ( ( ( 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 )
187 simp2lr 1056 . . . . . . . . 9 |- ( ( ( 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 ) )
188 simprrl 763 . . . . . . . . . . 11 |- ( ( ( 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 )
189182, 188, 184, 95syl3anc 1218 . . . . . . . . . 10 |- ( ( ( 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 )
1901893adant3 1008 . . . . . . . . 9 |- ( ( ( 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 )
191 simp2rr 1058 . . . . . . . . 9 |- ( ( ( 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 )
192 simp3l 1016 . . . . . . . . . . 11 |- ( ( ( 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 ) ) ) )
193192oveq1d 6118 . . . . . . . . . 10 |- ( ( ( 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 ) )
19456adantr 465 . . . . . . . . . . . . . 14 |- ( ( ( 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 )
195194oveqd 6120 . . . . . . . . . . . . 13 |- ( ( ( 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 ) )
196195reseq1d 5121 . . . . . . . . . . . 12 |- ( ( ( 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 ) ) )
197 simpl1 991 . . . . . . . . . . . . 13 |- ( ( ( 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 )
19810adantr 465 . . . . . . . . . . . . 13 |- ( ( ( 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 )
199 simprrr 764 . . . . . . . . . . . . . 14 |- ( ( ( 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 )
200199snssd 4030 . . . . . . . . . . . . 13 |- ( ( ( 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 )
201183, 63syl 16 . . . . . . . . . . . . 13 |- ( ( ( 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 ) ) )
20266adantr 465 . . . . . . . . . . . . 13 |- ( ( ( 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 ) ) )
20353, 102, 3, 197, 198, 198, 198, 200, 201, 202mamures 18302 . . . . . . . . . . . 12 |- ( ( ( 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 ) )
204196, 203eqtr3d 2477 . . . . . . . . . . 11 |- ( ( ( 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 ) )
2052043adant3 1008 . . . . . . . . . 10 |- ( ( ( 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 ) )
206194oveqd 6120 . . . . . . . . . . . . . . 15 |- ( ( ( 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 ) )
207206reseq1d 5121 . . . . . . . . . . . . . 14 |- ( ( ( 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 ) ) )
208188, 114syl 16 . . . . . . . . . . . . . . 15 |- ( ( ( 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 ) ) )
20953, 102, 3, 197, 198, 198, 198, 200, 208, 202mamures 18302 . . . . . . . . . . . . . 14 |- ( ( ( 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 ) )
210207, 209eqtr3d 2477 . . . . . . . . . . . . 13 |- ( ( ( 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 ) )
211210oveq2d 6119 . . . . . . . . . . . 12 |- ( ( ( 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 ) ) )
21212adantr 465 . . . . . . . . . . . . 13 |- ( ( ( 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 )
213103a1i 11 . . . . . . . . . . . . 13 |- ( ( ( 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 )
214 simprlr 762 . . . . . . . . . . . . 13 |- ( ( ( 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 ) )
215200, 110syl 16 . . . . . . . . . . . . . 14 |- ( ( ( 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 ) )
216208, 215, 116syl2anc 661 . . . . . . . . . . . . 13 |- ( ( ( 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 ) ) )
2173, 212, 102, 213, 198, 198, 7, 214, 216, 202mamuvs1 18321 . . . . . . . . . . . 12 |- ( ( ( 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 ) ) )
218211, 217eqtr4d 2478 . . . . . . . . . . 11 |- ( ( ( 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 ) )
2192183adant3 1008 . . . . . . . . . 10 |- ( ( ( 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 ) )