Step |
Hyp |
Ref |
Expression |
1 |
|
mat1dim.a |
|- A = ( { E } Mat R ) |
2 |
|
mat1dim.b |
|- B = ( Base ` R ) |
3 |
|
mat1dim.o |
|- O = <. E , E >. |
4 |
|
snfi |
|- { E } e. Fin |
5 |
|
simpl |
|- ( ( R e. Ring /\ E e. V ) -> R e. Ring ) |
6 |
1 2
|
matbas2 |
|- ( ( { E } e. Fin /\ R e. Ring ) -> ( B ^m ( { E } X. { E } ) ) = ( Base ` A ) ) |
7 |
6
|
eqcomd |
|- ( ( { E } e. Fin /\ R e. Ring ) -> ( Base ` A ) = ( B ^m ( { E } X. { E } ) ) ) |
8 |
7
|
eleq2d |
|- ( ( { E } e. Fin /\ R e. Ring ) -> ( M e. ( Base ` A ) <-> M e. ( B ^m ( { E } X. { E } ) ) ) ) |
9 |
4 5 8
|
sylancr |
|- ( ( R e. Ring /\ E e. V ) -> ( M e. ( Base ` A ) <-> M e. ( B ^m ( { E } X. { E } ) ) ) ) |
10 |
2
|
fvexi |
|- B e. _V |
11 |
|
snex |
|- { E } e. _V |
12 |
11 11
|
pm3.2i |
|- ( { E } e. _V /\ { E } e. _V ) |
13 |
|
xpexg |
|- ( ( { E } e. _V /\ { E } e. _V ) -> ( { E } X. { E } ) e. _V ) |
14 |
12 13
|
mp1i |
|- ( ( R e. Ring /\ E e. V ) -> ( { E } X. { E } ) e. _V ) |
15 |
|
elmapg |
|- ( ( B e. _V /\ ( { E } X. { E } ) e. _V ) -> ( M e. ( B ^m ( { E } X. { E } ) ) <-> M : ( { E } X. { E } ) --> B ) ) |
16 |
10 14 15
|
sylancr |
|- ( ( R e. Ring /\ E e. V ) -> ( M e. ( B ^m ( { E } X. { E } ) ) <-> M : ( { E } X. { E } ) --> B ) ) |
17 |
9 16
|
bitrd |
|- ( ( R e. Ring /\ E e. V ) -> ( M e. ( Base ` A ) <-> M : ( { E } X. { E } ) --> B ) ) |
18 |
|
xpsng |
|- ( ( E e. V /\ E e. V ) -> ( { E } X. { E } ) = { <. E , E >. } ) |
19 |
18
|
anidms |
|- ( E e. V -> ( { E } X. { E } ) = { <. E , E >. } ) |
20 |
19
|
adantl |
|- ( ( R e. Ring /\ E e. V ) -> ( { E } X. { E } ) = { <. E , E >. } ) |
21 |
20
|
feq2d |
|- ( ( R e. Ring /\ E e. V ) -> ( M : ( { E } X. { E } ) --> B <-> M : { <. E , E >. } --> B ) ) |
22 |
|
opex |
|- <. E , E >. e. _V |
23 |
22
|
fsn2 |
|- ( M : { <. E , E >. } --> B <-> ( ( M ` <. E , E >. ) e. B /\ M = { <. <. E , E >. , ( M ` <. E , E >. ) >. } ) ) |
24 |
|
risset |
|- ( ( M ` <. E , E >. ) e. B <-> E. r e. B r = ( M ` <. E , E >. ) ) |
25 |
|
eqcom |
|- ( r = ( M ` <. E , E >. ) <-> ( M ` <. E , E >. ) = r ) |
26 |
25
|
rexbii |
|- ( E. r e. B r = ( M ` <. E , E >. ) <-> E. r e. B ( M ` <. E , E >. ) = r ) |
27 |
24 26
|
sylbb |
|- ( ( M ` <. E , E >. ) e. B -> E. r e. B ( M ` <. E , E >. ) = r ) |
28 |
27
|
ad2antrl |
|- ( ( ( R e. Ring /\ E e. V ) /\ ( ( M ` <. E , E >. ) e. B /\ M = { <. <. E , E >. , ( M ` <. E , E >. ) >. } ) ) -> E. r e. B ( M ` <. E , E >. ) = r ) |
29 |
|
eqeq1 |
|- ( M = { <. <. E , E >. , ( M ` <. E , E >. ) >. } -> ( M = { <. <. E , E >. , r >. } <-> { <. <. E , E >. , ( M ` <. E , E >. ) >. } = { <. <. E , E >. , r >. } ) ) |
30 |
|
opex |
|- <. <. E , E >. , ( M ` <. E , E >. ) >. e. _V |
31 |
|
sneqbg |
|- ( <. <. E , E >. , ( M ` <. E , E >. ) >. e. _V -> ( { <. <. E , E >. , ( M ` <. E , E >. ) >. } = { <. <. E , E >. , r >. } <-> <. <. E , E >. , ( M ` <. E , E >. ) >. = <. <. E , E >. , r >. ) ) |
32 |
30 31
|
ax-mp |
|- ( { <. <. E , E >. , ( M ` <. E , E >. ) >. } = { <. <. E , E >. , r >. } <-> <. <. E , E >. , ( M ` <. E , E >. ) >. = <. <. E , E >. , r >. ) |
33 |
|
eqid |
|- <. E , E >. = <. E , E >. |
34 |
|
vex |
|- r e. _V |
35 |
22 34
|
opth2 |
|- ( <. <. E , E >. , ( M ` <. E , E >. ) >. = <. <. E , E >. , r >. <-> ( <. E , E >. = <. E , E >. /\ ( M ` <. E , E >. ) = r ) ) |
36 |
33 35
|
mpbiran |
|- ( <. <. E , E >. , ( M ` <. E , E >. ) >. = <. <. E , E >. , r >. <-> ( M ` <. E , E >. ) = r ) |
37 |
32 36
|
bitri |
|- ( { <. <. E , E >. , ( M ` <. E , E >. ) >. } = { <. <. E , E >. , r >. } <-> ( M ` <. E , E >. ) = r ) |
38 |
29 37
|
bitrdi |
|- ( M = { <. <. E , E >. , ( M ` <. E , E >. ) >. } -> ( M = { <. <. E , E >. , r >. } <-> ( M ` <. E , E >. ) = r ) ) |
39 |
38
|
adantl |
|- ( ( ( M ` <. E , E >. ) e. B /\ M = { <. <. E , E >. , ( M ` <. E , E >. ) >. } ) -> ( M = { <. <. E , E >. , r >. } <-> ( M ` <. E , E >. ) = r ) ) |
40 |
39
|
adantl |
|- ( ( ( R e. Ring /\ E e. V ) /\ ( ( M ` <. E , E >. ) e. B /\ M = { <. <. E , E >. , ( M ` <. E , E >. ) >. } ) ) -> ( M = { <. <. E , E >. , r >. } <-> ( M ` <. E , E >. ) = r ) ) |
41 |
40
|
rexbidv |
|- ( ( ( R e. Ring /\ E e. V ) /\ ( ( M ` <. E , E >. ) e. B /\ M = { <. <. E , E >. , ( M ` <. E , E >. ) >. } ) ) -> ( E. r e. B M = { <. <. E , E >. , r >. } <-> E. r e. B ( M ` <. E , E >. ) = r ) ) |
42 |
28 41
|
mpbird |
|- ( ( ( R e. Ring /\ E e. V ) /\ ( ( M ` <. E , E >. ) e. B /\ M = { <. <. E , E >. , ( M ` <. E , E >. ) >. } ) ) -> E. r e. B M = { <. <. E , E >. , r >. } ) |
43 |
42
|
ex |
|- ( ( R e. Ring /\ E e. V ) -> ( ( ( M ` <. E , E >. ) e. B /\ M = { <. <. E , E >. , ( M ` <. E , E >. ) >. } ) -> E. r e. B M = { <. <. E , E >. , r >. } ) ) |
44 |
23 43
|
syl5bi |
|- ( ( R e. Ring /\ E e. V ) -> ( M : { <. E , E >. } --> B -> E. r e. B M = { <. <. E , E >. , r >. } ) ) |
45 |
21 44
|
sylbid |
|- ( ( R e. Ring /\ E e. V ) -> ( M : ( { E } X. { E } ) --> B -> E. r e. B M = { <. <. E , E >. , r >. } ) ) |
46 |
|
f1o2sn |
|- ( ( E e. V /\ r e. B ) -> { <. <. E , E >. , r >. } : ( { E } X. { E } ) -1-1-onto-> { r } ) |
47 |
|
f1of |
|- ( { <. <. E , E >. , r >. } : ( { E } X. { E } ) -1-1-onto-> { r } -> { <. <. E , E >. , r >. } : ( { E } X. { E } ) --> { r } ) |
48 |
46 47
|
syl |
|- ( ( E e. V /\ r e. B ) -> { <. <. E , E >. , r >. } : ( { E } X. { E } ) --> { r } ) |
49 |
48
|
adantll |
|- ( ( ( R e. Ring /\ E e. V ) /\ r e. B ) -> { <. <. E , E >. , r >. } : ( { E } X. { E } ) --> { r } ) |
50 |
|
snssi |
|- ( r e. B -> { r } C_ B ) |
51 |
50
|
adantl |
|- ( ( ( R e. Ring /\ E e. V ) /\ r e. B ) -> { r } C_ B ) |
52 |
49 51
|
fssd |
|- ( ( ( R e. Ring /\ E e. V ) /\ r e. B ) -> { <. <. E , E >. , r >. } : ( { E } X. { E } ) --> B ) |
53 |
|
feq1 |
|- ( M = { <. <. E , E >. , r >. } -> ( M : ( { E } X. { E } ) --> B <-> { <. <. E , E >. , r >. } : ( { E } X. { E } ) --> B ) ) |
54 |
52 53
|
syl5ibrcom |
|- ( ( ( R e. Ring /\ E e. V ) /\ r e. B ) -> ( M = { <. <. E , E >. , r >. } -> M : ( { E } X. { E } ) --> B ) ) |
55 |
54
|
rexlimdva |
|- ( ( R e. Ring /\ E e. V ) -> ( E. r e. B M = { <. <. E , E >. , r >. } -> M : ( { E } X. { E } ) --> B ) ) |
56 |
45 55
|
impbid |
|- ( ( R e. Ring /\ E e. V ) -> ( M : ( { E } X. { E } ) --> B <-> E. r e. B M = { <. <. E , E >. , r >. } ) ) |
57 |
3
|
eqcomi |
|- <. E , E >. = O |
58 |
57
|
opeq1i |
|- <. <. E , E >. , r >. = <. O , r >. |
59 |
58
|
sneqi |
|- { <. <. E , E >. , r >. } = { <. O , r >. } |
60 |
59
|
eqeq2i |
|- ( M = { <. <. E , E >. , r >. } <-> M = { <. O , r >. } ) |
61 |
60
|
a1i |
|- ( ( R e. Ring /\ E e. V ) -> ( M = { <. <. E , E >. , r >. } <-> M = { <. O , r >. } ) ) |
62 |
61
|
rexbidv |
|- ( ( R e. Ring /\ E e. V ) -> ( E. r e. B M = { <. <. E , E >. , r >. } <-> E. r e. B M = { <. O , r >. } ) ) |
63 |
56 62
|
bitrd |
|- ( ( R e. Ring /\ E e. V ) -> ( M : ( { E } X. { E } ) --> B <-> E. r e. B M = { <. O , r >. } ) ) |
64 |
17 63
|
bitrd |
|- ( ( R e. Ring /\ E e. V ) -> ( M e. ( Base ` A ) <-> E. r e. B M = { <. O , r >. } ) ) |