MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  mdetmul Structured version   Unicode version

Theorem mdetmul 18388
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 2441 . . 3  |-  ( Base `  R )  =  (
Base `  R )
4 eqid 2441 . . 3  |-  ( 0g
`  R )  =  ( 0g `  R
)
5 eqid 2441 . . 3  |-  ( 1r
`  R )  =  ( 1r `  R
)
6 eqid 2441 . . 3  |-  ( +g  `  R )  =  ( +g  `  R )
7 mdetmul.t1 . . 3  |-  .x.  =  ( .r `  R )
81, 2matrcl 18271 . . . . 5  |-  ( F  e.  B  ->  ( N  e.  Fin  /\  R  e.  _V ) )
98simpld 456 . . . 4  |-  ( F  e.  B  ->  N  e.  Fin )
1093ad2ant2 1005 . . 3  |-  ( ( R  e.  CRing  /\  F  e.  B  /\  G  e.  B )  ->  N  e.  Fin )
11 crngrng 16645 . . . 4  |-  ( R  e.  CRing  ->  R  e.  Ring )
12113ad2ant1 1004 . . 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 18365 . . . . . . 7  |-  ( R  e.  CRing  ->  D : B
--> ( Base `  R
) )
15143ad2ant1 1004 . . . . . 6  |-  ( ( R  e.  CRing  /\  F  e.  B  /\  G  e.  B )  ->  D : B --> ( Base `  R
) )
1615adantr 462 . . . . 5  |-  ( ( ( R  e.  CRing  /\  F  e.  B  /\  G  e.  B )  /\  a  e.  B
)  ->  D : B
--> ( Base `  R
) )
171matrng 18289 . . . . . . . 8  |-  ( ( N  e.  Fin  /\  R  e.  Ring )  ->  A  e.  Ring )
1810, 12, 17syl2anc 656 . . . . . . 7  |-  ( ( R  e.  CRing  /\  F  e.  B  /\  G  e.  B )  ->  A  e.  Ring )
1918adantr 462 . . . . . 6  |-  ( ( ( R  e.  CRing  /\  F  e.  B  /\  G  e.  B )  /\  a  e.  B
)  ->  A  e.  Ring )
20 simpr 458 . . . . . 6  |-  ( ( ( R  e.  CRing  /\  F  e.  B  /\  G  e.  B )  /\  a  e.  B
)  ->  a  e.  B )
21 simpl3 988 . . . . . 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 16648 . . . . . 6  |-  ( ( A  e.  Ring  /\  a  e.  B  /\  G  e.  B )  ->  (
a  .xb  G )  e.  B )
2419, 20, 21, 23syl3anc 1213 . . . . 5  |-  ( ( ( R  e.  CRing  /\  F  e.  B  /\  G  e.  B )  /\  a  e.  B
)  ->  ( a  .xb  G )  e.  B
)
2516, 24ffvelrnd 5841 . . . 4  |-  ( ( ( R  e.  CRing  /\  F  e.  B  /\  G  e.  B )  /\  a  e.  B
)  ->  ( D `  ( a  .xb  G
) )  e.  (
Base `  R )
)
26 eqid 2441 . . . 4  |-  ( a  e.  B  |->  ( D `
 ( a  .xb  G ) ) )  =  ( a  e.  B  |->  ( D `  ( a  .xb  G
) ) )
2725, 26fmptd 5864 . . 3  |-  ( ( R  e.  CRing  /\  F  e.  B  /\  G  e.  B )  ->  (
a  e.  B  |->  ( D `  ( a 
.xb  G ) ) ) : B --> ( Base `  R ) )
28 simp21 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 ) ) )  -> 
b  e.  B )
29 oveq1 6097 . . . . . . . . 9  |-  ( a  =  b  ->  (
a  .xb  G )  =  ( b  .xb  G ) )
3029fveq2d 5692 . . . . . . . 8  |-  ( a  =  b  ->  ( D `  ( a  .xb  G ) )  =  ( D `  (
b  .xb  G )
) )
31 fvex 5698 . . . . . . . 8  |-  ( D `
 ( b  .xb  G ) )  e. 
_V
3230, 26, 31fvmpt 5771 . . . . . . 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 1013 . . . . . . 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 462 . . . . . . . . 9  |-  ( ( ( R  e.  CRing  /\  F  e.  B  /\  G  e.  B )  /\  ( b  e.  B  /\  c  e.  N  /\  d  e.  N
) )  ->  A  e.  Ring )
36 simpr1 989 . . . . . . . . 9  |-  ( ( ( R  e.  CRing  /\  F  e.  B  /\  G  e.  B )  /\  ( b  e.  B  /\  c  e.  N  /\  d  e.  N
) )  ->  b  e.  B )
37 simpl3 988 . . . . . . . . 9  |-  ( ( ( R  e.  CRing  /\  F  e.  B  /\  G  e.  B )  /\  ( b  e.  B  /\  c  e.  N  /\  d  e.  N
) )  ->  G  e.  B )
382, 22rngcl 16648 . . . . . . . . 9  |-  ( ( A  e.  Ring  /\  b  e.  B  /\  G  e.  B )  ->  (
b  .xb  G )  e.  B )
3935, 36, 37, 38syl3anc 1213 . . . . . . . 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 1003 . . . . . . 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 1017 . . . . . . 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 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 ) ) )  -> 
d  e.  N )
43 simp3l 1011 . . . . . . 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 1039 . . . . . . . . . 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 2441 . . . . . . . . . . . 12  |-  N  =  N
46 oveq1 6097 . . . . . . . . . . . . 13  |-  ( ( c b e )  =  ( d b e )  ->  (
( c b e )  .x.  ( e G a ) )  =  ( ( d b e )  .x.  ( e G a ) ) )
4746ralimi 2789 . . . . . . . . . . . 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 4368 . . . . . . . . . . . 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 658 . . . . . . . . . . 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 6106 . . . . . . . . . 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 983 . . . . . . . . . . . . . . 15  |-  ( ( R  e.  CRing  /\  F  e.  B  /\  G  e.  B )  ->  R  e.  CRing )
53 eqid 2441 . . . . . . . . . . . . . . . . 17  |-  ( R maMul  <. N ,  N ,  N >. )  =  ( R maMul  <. N ,  N ,  N >. )
541, 53matmulr 18272 . . . . . . . . . . . . . . . 16  |-  ( ( N  e.  Fin  /\  R  e.  CRing )  -> 
( R maMul  <. N ,  N ,  N >. )  =  ( .r `  A ) )
5554, 22syl6eqr 2491 . . . . . . . . . . . . . . 15  |-  ( ( N  e.  Fin  /\  R  e.  CRing )  -> 
( R maMul  <. N ,  N ,  N >. )  =  .xb  )
5610, 52, 55syl2anc 656 . . . . . . . . . . . . . 14  |-  ( ( R  e.  CRing  /\  F  e.  B  /\  G  e.  B )  ->  ( R maMul  <. N ,  N ,  N >. )  =  .xb  )
5756ad2antrr 720 . . . . . . . . . . . . 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 6107 . . . . . . . . . . . 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 6107 . . . . . . . . . . 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 1022 . . . . . . . . . . . 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 720 . . . . . . . . . . . 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 1025 . . . . . . . . . . . . 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 18282 . . . . . . . . . . . . 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 18282 . . . . . . . . . . . . . 14  |-  ( G  e.  B  ->  G  e.  ( ( Base `  R
)  ^m  ( N  X.  N ) ) )
66653ad2ant3 1006 . . . . . . . . . . . . 13  |-  ( ( R  e.  CRing  /\  F  e.  B  /\  G  e.  B )  ->  G  e.  ( ( Base `  R
)  ^m  ( N  X.  N ) ) )
6766ad2antrr 720 . . . . . . . . . . . 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 1026 . . . . . . . . . . . 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 458 . . . . . . . . . . . 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 18244 . . . . . . . . . . 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 2475 . . . . . . . . . 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 1141 . . . . . . . . 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 6107 . . . . . . . . . . 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 1027 . . . . . . . . . . . 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 18244 . . . . . . . . . . 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 2475 . . . . . . . . . 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 1141 . . . . . . . . 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 2483 . . . . . . . 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 2797 . . . . . . 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 18373 . . . . . 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 2473 . . . . 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 1184 . . . 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 2807 . . 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 1013 . . . . . . . . 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 462 . . . . . . . . . . 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 756 . . . . . . . . . . 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 988 . . . . . . . . . . 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 1213 . . . . . . . . . 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 1003 . . . . . . . . 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 757 . . . . . . . . . . 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 16648 . . . . . . . . . . 11  |-  ( ( A  e.  Ring  /\  c  e.  B  /\  G  e.  B )  ->  (
c  .xb  G )  e.  B )
9285, 90, 87, 91syl3anc 1213 . . . . . . . . . 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 1003 . . . . . . . . 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 758 . . . . . . . . . . 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 16648 . . . . . . . . . . 11  |-  ( ( A  e.  Ring  /\  d  e.  B  /\  G  e.  B )  ->  (
d  .xb  G )  e.  B )
9685, 94, 87, 95syl3anc 1213 . . . . . . . . . 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 1003 . . . . . . . . 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 1053 . . . . . . . . 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 1019 . . . . . . . . . . . 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 6105 . . . . . . . . . . 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 462 . . . . . . . . . . . . 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 2441 . . . . . . . . . . . . 13  |-  ( R maMul  <. { e } ,  N ,  N >. )  =  ( R maMul  <. { e } ,  N ,  N >. )
103 snfi 7386 . . . . . . . . . . . . . 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 462 . . . . . . . . . . . . 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 18282 . . . . . . . . . . . . . . 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 759 . . . . . . . . . . . . . . . 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 4015 . . . . . . . . . . . . . . 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 4944 . . . . . . . . . . . . . . 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 7233 . . . . . . . . . . . . . 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 656 . . . . . . . . . . . . 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 18282 . . . . . . . . . . . . . . 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 7233 . . . . . . . . . . . . . 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 656 . . . . . . . . . . . . 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 462 . . . . . . . . . . . . 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 18266 . . . . . . . . . . . 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 1003 . . . . . . . . . . 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 2473 . . . . . . . . . 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 462 . . . . . . . . . . . . . 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 6107 . . . . . . . . . . . . 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 5105 . . . . . . . . . . . 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 986 . . . . . . . . . . . . 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 18249 . . . . . . . . . . . 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 2475 . . . . . . . . . . 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 1003 . . . . . . . . . 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 6107 . . . . . . . . . . . . . 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 5105 . . . . . . . . . . . . 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 18249 . . . . . . . . . . . . 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 2475 . . . . . . . . . . . 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 6107 . . . . . . . . . . . . . 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 5105 . . . . . . . . . . . . 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 18249 . . . . . . . . . . . . 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 2475 . . . . . . . . . . . 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 6108 . . . . . . . . . . 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 1003 . . . . . . . . . 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 2483 . . . . . . . . 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 1020 . . . . . . . . . . 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 6105 . . . . . . . . . 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 5105 . . . . . . . . . . . 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 2441 . . . . . . . . . . . . 13  |-  ( R maMul  <. ( N  \  {
e } ) ,  N ,  N >. )  =  ( R maMul  <. ( N  \  { e } ) ,  N ,  N >. )
145 difssd 3481 . . . . . . . . . . . . 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 18249 . . . . . . . . . . . 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 2475 . . . . . . . . . . 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 1003 . . . . . . . . . 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 5105 . . . . . . . . . . . 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 18249 . . . . . . . . . . . 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 2475 . . . . . . . . . . 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 1003 . . . . . . . . . 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 2483 . . . . . . . . 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 1021 . . . . . . . . . . 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 6105 . . . . . . . . . 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 5105 . . . . . . . . . . . 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 18249 . . . . . . . . . . . 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 2475 . . . . . . . . . . 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 1003 . . . . . . . . . 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 2483 . . . . . . . . 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 18368 . . . . . . . 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 1003 . . . . . . . 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 6097 . . . . . . . . . . . . 13  |-  ( a  =  c  ->  (
a  .xb  G )  =  ( c  .xb  G ) )
165164fveq2d 5692 . . . . . . . . . . . 12  |-  ( a  =  c  ->  ( D `  ( a  .xb  G ) )  =  ( D `  (
c  .xb  G )
) )
166 fvex 5698 . . . . . . . . . . . 12  |-  ( D `
 ( c  .xb  G ) )  e. 
_V
167165, 26, 166fvmpt 5771 . . . . . . . . . . 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 6097 . . . . . . . . . . . . 13  |-  ( a  =  d  ->  (
a  .xb  G )  =  ( d  .xb  G ) )
170169fveq2d 5692 . . . . . . . . . . . 12  |-  ( a  =  d  ->  ( D `  ( a  .xb  G ) )  =  ( D `  (
d  .xb  G )
) )
171 fvex 5698 . . . . . . . . . . . 12  |-  ( D `
 ( d  .xb  G ) )  e. 
_V
172170, 26, 171fvmpt 5771 . . . . . . . . . . 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 6108 . . . . . . . . 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 1003 . . . . . . . 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 2483 . . . . . . 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 1184 . . . . . 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 643 . . . . 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 2806 . . . 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 2806 . . 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 1013 . . . . . . . . 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 462 . . . . . . . . . . 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 756 . . . . . . . . . . 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 988 . . . . . . . . . . 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 1213 . . . . . . . . . 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 1003 . . . . . . . . 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 1051 . . . . . . . . 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 758 . . . . . . . . . . 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 1213 . . . . . . . . . 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 1003 . . . . . . . . 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 1053 . . . . . . . . 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 1011 . . . . . . . . . . 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 6105 . . . . . . . . . 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 462 . . . . . . . . . . . . . 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 6107 . . . . . . . . . . . . 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 5105 . . . . . . . . . . . 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 986 . . . . . . . . . . . . 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 462 . . . . . . . . . . . . 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 759 . . . . . . . . . . . . . 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 4015 . . . . . . . . . . . . 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 462 . . . . . . . . . . . . 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 18249 . . . . . . . . . . . 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 2475 . . . . . . . . . . 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 1003 . . . . . . . . . 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 6107 . . . . . . . . . . . . . . 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 5105 . . . . . . . . . . . . . 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 18249 . . . . . . . . . . . . . 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 2475 . . . . . . . . . . . . 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 6106 . . . . . . . . . . . 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 462 . . . . . . . . . . . . 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 757 . . . . . . . . . . . . 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 656 . . . . . . . . . . . . 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 18268 . . . . . . . . . . . 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 2476 . . . . . . . . . . 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 1003 . . . . . . . . . 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 ) )