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