Step |
Hyp |
Ref |
Expression |
1 |
|
scmatid.a |
|- A = ( N Mat R ) |
2 |
|
scmatid.b |
|- B = ( Base ` A ) |
3 |
|
scmatid.e |
|- E = ( Base ` R ) |
4 |
|
scmatid.0 |
|- .0. = ( 0g ` R ) |
5 |
|
scmatid.s |
|- S = ( N ScMat R ) |
6 |
|
eqid |
|- ( 1r ` A ) = ( 1r ` A ) |
7 |
|
eqid |
|- ( .s ` A ) = ( .s ` A ) |
8 |
3 1 2 6 7 5
|
scmatscmid |
|- ( ( N e. Fin /\ R e. Ring /\ X e. S ) -> E. c e. E X = ( c ( .s ` A ) ( 1r ` A ) ) ) |
9 |
8
|
3expa |
|- ( ( ( N e. Fin /\ R e. Ring ) /\ X e. S ) -> E. c e. E X = ( c ( .s ` A ) ( 1r ` A ) ) ) |
10 |
9
|
adantrr |
|- ( ( ( N e. Fin /\ R e. Ring ) /\ ( X e. S /\ Y e. S ) ) -> E. c e. E X = ( c ( .s ` A ) ( 1r ` A ) ) ) |
11 |
3 1 2 6 7 5
|
scmatscmid |
|- ( ( N e. Fin /\ R e. Ring /\ Y e. S ) -> E. d e. E Y = ( d ( .s ` A ) ( 1r ` A ) ) ) |
12 |
11
|
3expia |
|- ( ( N e. Fin /\ R e. Ring ) -> ( Y e. S -> E. d e. E Y = ( d ( .s ` A ) ( 1r ` A ) ) ) ) |
13 |
|
oveq12 |
|- ( ( X = ( c ( .s ` A ) ( 1r ` A ) ) /\ Y = ( d ( .s ` A ) ( 1r ` A ) ) ) -> ( X ( +g ` A ) Y ) = ( ( c ( .s ` A ) ( 1r ` A ) ) ( +g ` A ) ( d ( .s ` A ) ( 1r ` A ) ) ) ) |
14 |
13
|
adantl |
|- ( ( ( ( ( N e. Fin /\ R e. Ring ) /\ d e. E ) /\ c e. E ) /\ ( X = ( c ( .s ` A ) ( 1r ` A ) ) /\ Y = ( d ( .s ` A ) ( 1r ` A ) ) ) ) -> ( X ( +g ` A ) Y ) = ( ( c ( .s ` A ) ( 1r ` A ) ) ( +g ` A ) ( d ( .s ` A ) ( 1r ` A ) ) ) ) |
15 |
1
|
matlmod |
|- ( ( N e. Fin /\ R e. Ring ) -> A e. LMod ) |
16 |
15
|
ad2antrr |
|- ( ( ( ( N e. Fin /\ R e. Ring ) /\ d e. E ) /\ c e. E ) -> A e. LMod ) |
17 |
1
|
matsca2 |
|- ( ( N e. Fin /\ R e. Ring ) -> R = ( Scalar ` A ) ) |
18 |
17
|
fveq2d |
|- ( ( N e. Fin /\ R e. Ring ) -> ( Base ` R ) = ( Base ` ( Scalar ` A ) ) ) |
19 |
3 18
|
eqtrid |
|- ( ( N e. Fin /\ R e. Ring ) -> E = ( Base ` ( Scalar ` A ) ) ) |
20 |
19
|
eleq2d |
|- ( ( N e. Fin /\ R e. Ring ) -> ( c e. E <-> c e. ( Base ` ( Scalar ` A ) ) ) ) |
21 |
20
|
biimpd |
|- ( ( N e. Fin /\ R e. Ring ) -> ( c e. E -> c e. ( Base ` ( Scalar ` A ) ) ) ) |
22 |
21
|
adantr |
|- ( ( ( N e. Fin /\ R e. Ring ) /\ d e. E ) -> ( c e. E -> c e. ( Base ` ( Scalar ` A ) ) ) ) |
23 |
22
|
imp |
|- ( ( ( ( N e. Fin /\ R e. Ring ) /\ d e. E ) /\ c e. E ) -> c e. ( Base ` ( Scalar ` A ) ) ) |
24 |
19
|
eleq2d |
|- ( ( N e. Fin /\ R e. Ring ) -> ( d e. E <-> d e. ( Base ` ( Scalar ` A ) ) ) ) |
25 |
24
|
biimpa |
|- ( ( ( N e. Fin /\ R e. Ring ) /\ d e. E ) -> d e. ( Base ` ( Scalar ` A ) ) ) |
26 |
25
|
adantr |
|- ( ( ( ( N e. Fin /\ R e. Ring ) /\ d e. E ) /\ c e. E ) -> d e. ( Base ` ( Scalar ` A ) ) ) |
27 |
1
|
matring |
|- ( ( N e. Fin /\ R e. Ring ) -> A e. Ring ) |
28 |
2 6
|
ringidcl |
|- ( A e. Ring -> ( 1r ` A ) e. B ) |
29 |
27 28
|
syl |
|- ( ( N e. Fin /\ R e. Ring ) -> ( 1r ` A ) e. B ) |
30 |
29
|
ad2antrr |
|- ( ( ( ( N e. Fin /\ R e. Ring ) /\ d e. E ) /\ c e. E ) -> ( 1r ` A ) e. B ) |
31 |
|
eqid |
|- ( +g ` A ) = ( +g ` A ) |
32 |
|
eqid |
|- ( Scalar ` A ) = ( Scalar ` A ) |
33 |
|
eqid |
|- ( Base ` ( Scalar ` A ) ) = ( Base ` ( Scalar ` A ) ) |
34 |
|
eqid |
|- ( +g ` ( Scalar ` A ) ) = ( +g ` ( Scalar ` A ) ) |
35 |
2 31 32 7 33 34
|
lmodvsdir |
|- ( ( A e. LMod /\ ( c e. ( Base ` ( Scalar ` A ) ) /\ d e. ( Base ` ( Scalar ` A ) ) /\ ( 1r ` A ) e. B ) ) -> ( ( c ( +g ` ( Scalar ` A ) ) d ) ( .s ` A ) ( 1r ` A ) ) = ( ( c ( .s ` A ) ( 1r ` A ) ) ( +g ` A ) ( d ( .s ` A ) ( 1r ` A ) ) ) ) |
36 |
16 23 26 30 35
|
syl13anc |
|- ( ( ( ( N e. Fin /\ R e. Ring ) /\ d e. E ) /\ c e. E ) -> ( ( c ( +g ` ( Scalar ` A ) ) d ) ( .s ` A ) ( 1r ` A ) ) = ( ( c ( .s ` A ) ( 1r ` A ) ) ( +g ` A ) ( d ( .s ` A ) ( 1r ` A ) ) ) ) |
37 |
36
|
eqcomd |
|- ( ( ( ( N e. Fin /\ R e. Ring ) /\ d e. E ) /\ c e. E ) -> ( ( c ( .s ` A ) ( 1r ` A ) ) ( +g ` A ) ( d ( .s ` A ) ( 1r ` A ) ) ) = ( ( c ( +g ` ( Scalar ` A ) ) d ) ( .s ` A ) ( 1r ` A ) ) ) |
38 |
|
simpll |
|- ( ( ( ( N e. Fin /\ R e. Ring ) /\ d e. E ) /\ c e. E ) -> ( N e. Fin /\ R e. Ring ) ) |
39 |
17
|
eqcomd |
|- ( ( N e. Fin /\ R e. Ring ) -> ( Scalar ` A ) = R ) |
40 |
39
|
ad2antrr |
|- ( ( ( ( N e. Fin /\ R e. Ring ) /\ d e. E ) /\ c e. E ) -> ( Scalar ` A ) = R ) |
41 |
40
|
fveq2d |
|- ( ( ( ( N e. Fin /\ R e. Ring ) /\ d e. E ) /\ c e. E ) -> ( +g ` ( Scalar ` A ) ) = ( +g ` R ) ) |
42 |
41
|
oveqd |
|- ( ( ( ( N e. Fin /\ R e. Ring ) /\ d e. E ) /\ c e. E ) -> ( c ( +g ` ( Scalar ` A ) ) d ) = ( c ( +g ` R ) d ) ) |
43 |
|
ringgrp |
|- ( R e. Ring -> R e. Grp ) |
44 |
43
|
adantl |
|- ( ( N e. Fin /\ R e. Ring ) -> R e. Grp ) |
45 |
44
|
ad2antrr |
|- ( ( ( ( N e. Fin /\ R e. Ring ) /\ d e. E ) /\ c e. E ) -> R e. Grp ) |
46 |
|
simpr |
|- ( ( ( ( N e. Fin /\ R e. Ring ) /\ d e. E ) /\ c e. E ) -> c e. E ) |
47 |
|
simplr |
|- ( ( ( ( N e. Fin /\ R e. Ring ) /\ d e. E ) /\ c e. E ) -> d e. E ) |
48 |
|
eqid |
|- ( +g ` R ) = ( +g ` R ) |
49 |
3 48
|
grpcl |
|- ( ( R e. Grp /\ c e. E /\ d e. E ) -> ( c ( +g ` R ) d ) e. E ) |
50 |
45 46 47 49
|
syl3anc |
|- ( ( ( ( N e. Fin /\ R e. Ring ) /\ d e. E ) /\ c e. E ) -> ( c ( +g ` R ) d ) e. E ) |
51 |
42 50
|
eqeltrd |
|- ( ( ( ( N e. Fin /\ R e. Ring ) /\ d e. E ) /\ c e. E ) -> ( c ( +g ` ( Scalar ` A ) ) d ) e. E ) |
52 |
3 1 2 7
|
matvscl |
|- ( ( ( N e. Fin /\ R e. Ring ) /\ ( ( c ( +g ` ( Scalar ` A ) ) d ) e. E /\ ( 1r ` A ) e. B ) ) -> ( ( c ( +g ` ( Scalar ` A ) ) d ) ( .s ` A ) ( 1r ` A ) ) e. B ) |
53 |
38 51 30 52
|
syl12anc |
|- ( ( ( ( N e. Fin /\ R e. Ring ) /\ d e. E ) /\ c e. E ) -> ( ( c ( +g ` ( Scalar ` A ) ) d ) ( .s ` A ) ( 1r ` A ) ) e. B ) |
54 |
|
oveq1 |
|- ( e = ( c ( +g ` ( Scalar ` A ) ) d ) -> ( e ( .s ` A ) ( 1r ` A ) ) = ( ( c ( +g ` ( Scalar ` A ) ) d ) ( .s ` A ) ( 1r ` A ) ) ) |
55 |
54
|
eqeq2d |
|- ( e = ( c ( +g ` ( Scalar ` A ) ) d ) -> ( ( ( c ( +g ` ( Scalar ` A ) ) d ) ( .s ` A ) ( 1r ` A ) ) = ( e ( .s ` A ) ( 1r ` A ) ) <-> ( ( c ( +g ` ( Scalar ` A ) ) d ) ( .s ` A ) ( 1r ` A ) ) = ( ( c ( +g ` ( Scalar ` A ) ) d ) ( .s ` A ) ( 1r ` A ) ) ) ) |
56 |
55
|
adantl |
|- ( ( ( ( ( N e. Fin /\ R e. Ring ) /\ d e. E ) /\ c e. E ) /\ e = ( c ( +g ` ( Scalar ` A ) ) d ) ) -> ( ( ( c ( +g ` ( Scalar ` A ) ) d ) ( .s ` A ) ( 1r ` A ) ) = ( e ( .s ` A ) ( 1r ` A ) ) <-> ( ( c ( +g ` ( Scalar ` A ) ) d ) ( .s ` A ) ( 1r ` A ) ) = ( ( c ( +g ` ( Scalar ` A ) ) d ) ( .s ` A ) ( 1r ` A ) ) ) ) |
57 |
|
eqidd |
|- ( ( ( ( N e. Fin /\ R e. Ring ) /\ d e. E ) /\ c e. E ) -> ( ( c ( +g ` ( Scalar ` A ) ) d ) ( .s ` A ) ( 1r ` A ) ) = ( ( c ( +g ` ( Scalar ` A ) ) d ) ( .s ` A ) ( 1r ` A ) ) ) |
58 |
51 56 57
|
rspcedvd |
|- ( ( ( ( N e. Fin /\ R e. Ring ) /\ d e. E ) /\ c e. E ) -> E. e e. E ( ( c ( +g ` ( Scalar ` A ) ) d ) ( .s ` A ) ( 1r ` A ) ) = ( e ( .s ` A ) ( 1r ` A ) ) ) |
59 |
3 1 2 6 7 5
|
scmatel |
|- ( ( N e. Fin /\ R e. Ring ) -> ( ( ( c ( +g ` ( Scalar ` A ) ) d ) ( .s ` A ) ( 1r ` A ) ) e. S <-> ( ( ( c ( +g ` ( Scalar ` A ) ) d ) ( .s ` A ) ( 1r ` A ) ) e. B /\ E. e e. E ( ( c ( +g ` ( Scalar ` A ) ) d ) ( .s ` A ) ( 1r ` A ) ) = ( e ( .s ` A ) ( 1r ` A ) ) ) ) ) |
60 |
59
|
ad2antrr |
|- ( ( ( ( N e. Fin /\ R e. Ring ) /\ d e. E ) /\ c e. E ) -> ( ( ( c ( +g ` ( Scalar ` A ) ) d ) ( .s ` A ) ( 1r ` A ) ) e. S <-> ( ( ( c ( +g ` ( Scalar ` A ) ) d ) ( .s ` A ) ( 1r ` A ) ) e. B /\ E. e e. E ( ( c ( +g ` ( Scalar ` A ) ) d ) ( .s ` A ) ( 1r ` A ) ) = ( e ( .s ` A ) ( 1r ` A ) ) ) ) ) |
61 |
53 58 60
|
mpbir2and |
|- ( ( ( ( N e. Fin /\ R e. Ring ) /\ d e. E ) /\ c e. E ) -> ( ( c ( +g ` ( Scalar ` A ) ) d ) ( .s ` A ) ( 1r ` A ) ) e. S ) |
62 |
37 61
|
eqeltrd |
|- ( ( ( ( N e. Fin /\ R e. Ring ) /\ d e. E ) /\ c e. E ) -> ( ( c ( .s ` A ) ( 1r ` A ) ) ( +g ` A ) ( d ( .s ` A ) ( 1r ` A ) ) ) e. S ) |
63 |
62
|
adantr |
|- ( ( ( ( ( N e. Fin /\ R e. Ring ) /\ d e. E ) /\ c e. E ) /\ ( X = ( c ( .s ` A ) ( 1r ` A ) ) /\ Y = ( d ( .s ` A ) ( 1r ` A ) ) ) ) -> ( ( c ( .s ` A ) ( 1r ` A ) ) ( +g ` A ) ( d ( .s ` A ) ( 1r ` A ) ) ) e. S ) |
64 |
14 63
|
eqeltrd |
|- ( ( ( ( ( N e. Fin /\ R e. Ring ) /\ d e. E ) /\ c e. E ) /\ ( X = ( c ( .s ` A ) ( 1r ` A ) ) /\ Y = ( d ( .s ` A ) ( 1r ` A ) ) ) ) -> ( X ( +g ` A ) Y ) e. S ) |
65 |
64
|
exp32 |
|- ( ( ( ( N e. Fin /\ R e. Ring ) /\ d e. E ) /\ c e. E ) -> ( X = ( c ( .s ` A ) ( 1r ` A ) ) -> ( Y = ( d ( .s ` A ) ( 1r ` A ) ) -> ( X ( +g ` A ) Y ) e. S ) ) ) |
66 |
65
|
rexlimdva |
|- ( ( ( N e. Fin /\ R e. Ring ) /\ d e. E ) -> ( E. c e. E X = ( c ( .s ` A ) ( 1r ` A ) ) -> ( Y = ( d ( .s ` A ) ( 1r ` A ) ) -> ( X ( +g ` A ) Y ) e. S ) ) ) |
67 |
66
|
com23 |
|- ( ( ( N e. Fin /\ R e. Ring ) /\ d e. E ) -> ( Y = ( d ( .s ` A ) ( 1r ` A ) ) -> ( E. c e. E X = ( c ( .s ` A ) ( 1r ` A ) ) -> ( X ( +g ` A ) Y ) e. S ) ) ) |
68 |
67
|
rexlimdva |
|- ( ( N e. Fin /\ R e. Ring ) -> ( E. d e. E Y = ( d ( .s ` A ) ( 1r ` A ) ) -> ( E. c e. E X = ( c ( .s ` A ) ( 1r ` A ) ) -> ( X ( +g ` A ) Y ) e. S ) ) ) |
69 |
12 68
|
syldc |
|- ( Y e. S -> ( ( N e. Fin /\ R e. Ring ) -> ( E. c e. E X = ( c ( .s ` A ) ( 1r ` A ) ) -> ( X ( +g ` A ) Y ) e. S ) ) ) |
70 |
69
|
adantl |
|- ( ( X e. S /\ Y e. S ) -> ( ( N e. Fin /\ R e. Ring ) -> ( E. c e. E X = ( c ( .s ` A ) ( 1r ` A ) ) -> ( X ( +g ` A ) Y ) e. S ) ) ) |
71 |
70
|
impcom |
|- ( ( ( N e. Fin /\ R e. Ring ) /\ ( X e. S /\ Y e. S ) ) -> ( E. c e. E X = ( c ( .s ` A ) ( 1r ` A ) ) -> ( X ( +g ` A ) Y ) e. S ) ) |
72 |
10 71
|
mpd |
|- ( ( ( N e. Fin /\ R e. Ring ) /\ ( X e. S /\ Y e. S ) ) -> ( X ( +g ` A ) Y ) e. S ) |