Metamath Proof Explorer

Theorem mat1dimelbas

Description: A matrix with dimension 1 is an ordered pair with an ordered pair (of the one and only pair of indices) as first component. (Contributed by AV, 15-Aug-2019)

Ref Expression
Hypotheses mat1dim.a 
|- A = ( { E } Mat R )
mat1dim.b 
|- B = ( Base ` R )
mat1dim.o 
|- O = <. E , E >.
Assertion mat1dimelbas 
|- ( ( R e. Ring /\ E e. V ) -> ( M e. ( Base ` A ) <-> E. r e. B M = { <. O , r >. } ) )

Proof

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 biimtrid 
 |-  ( ( 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 >. } ) )