Metamath Proof Explorer


Theorem mat1dimbas

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 mat1dimbas
|- ( ( R e. Ring /\ E e. V /\ X e. B ) -> { <. O , X >. } e. ( Base ` A ) )

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 risset
 |-  ( X e. B <-> E. r e. B r = X )
5 eqcom
 |-  ( X = r <-> r = X )
6 5 rexbii
 |-  ( E. r e. B X = r <-> E. r e. B r = X )
7 4 6 sylbb2
 |-  ( X e. B -> E. r e. B X = r )
8 7 3ad2ant3
 |-  ( ( R e. Ring /\ E e. V /\ X e. B ) -> E. r e. B X = r )
9 opex
 |-  <. E , E >. e. _V
10 3 9 eqeltri
 |-  O e. _V
11 simp3
 |-  ( ( R e. Ring /\ E e. V /\ X e. B ) -> X e. B )
12 opthg
 |-  ( ( O e. _V /\ X e. B ) -> ( <. O , X >. = <. O , r >. <-> ( O = O /\ X = r ) ) )
13 10 11 12 sylancr
 |-  ( ( R e. Ring /\ E e. V /\ X e. B ) -> ( <. O , X >. = <. O , r >. <-> ( O = O /\ X = r ) ) )
14 opex
 |-  <. O , X >. e. _V
15 sneqbg
 |-  ( <. O , X >. e. _V -> ( { <. O , X >. } = { <. O , r >. } <-> <. O , X >. = <. O , r >. ) )
16 14 15 ax-mp
 |-  ( { <. O , X >. } = { <. O , r >. } <-> <. O , X >. = <. O , r >. )
17 eqid
 |-  O = O
18 17 biantrur
 |-  ( X = r <-> ( O = O /\ X = r ) )
19 13 16 18 3bitr4g
 |-  ( ( R e. Ring /\ E e. V /\ X e. B ) -> ( { <. O , X >. } = { <. O , r >. } <-> X = r ) )
20 19 rexbidv
 |-  ( ( R e. Ring /\ E e. V /\ X e. B ) -> ( E. r e. B { <. O , X >. } = { <. O , r >. } <-> E. r e. B X = r ) )
21 8 20 mpbird
 |-  ( ( R e. Ring /\ E e. V /\ X e. B ) -> E. r e. B { <. O , X >. } = { <. O , r >. } )
22 1 2 3 mat1dimelbas
 |-  ( ( R e. Ring /\ E e. V ) -> ( { <. O , X >. } e. ( Base ` A ) <-> E. r e. B { <. O , X >. } = { <. O , r >. } ) )
23 22 3adant3
 |-  ( ( R e. Ring /\ E e. V /\ X e. B ) -> ( { <. O , X >. } e. ( Base ` A ) <-> E. r e. B { <. O , X >. } = { <. O , r >. } ) )
24 21 23 mpbird
 |-  ( ( R e. Ring /\ E e. V /\ X e. B ) -> { <. O , X >. } e. ( Base ` A ) )