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