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