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