This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem mat1dimid

Description: The identity of the algebra of matrices with dimension 1. (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 mat1dimid 
|- ( ( R e. Ring /\ E e. V ) -> ( 1r ` A ) = { <. O , ( 1r ` 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 4 a1i 
 |-  ( E e. V -> { E } e. Fin )
6 5 anim2i 
 |-  ( ( R e. Ring /\ E e. V ) -> ( R e. Ring /\ { E } e. Fin ) )
7 6 ancomd 
 |-  ( ( R e. Ring /\ E e. V ) -> ( { E } e. Fin /\ R e. Ring ) )
8 eqid 
 |-  ( 1r ` R ) = ( 1r ` R )
9 eqid 
 |-  ( 0g ` R ) = ( 0g ` R )
10 1 8 9 mat1 
 |-  ( ( { E } e. Fin /\ R e. Ring ) -> ( 1r ` A ) = ( x e. { E } , y e. { E } |-> if ( x = y , ( 1r ` R ) , ( 0g ` R ) ) ) )
11 7 10 syl 
 |-  ( ( R e. Ring /\ E e. V ) -> ( 1r ` A ) = ( x e. { E } , y e. { E } |-> if ( x = y , ( 1r ` R ) , ( 0g ` R ) ) ) )
12 simpr 
 |-  ( ( R e. Ring /\ E e. V ) -> E e. V )
13 fvex 
 |-  ( 1r ` R ) e. _V
14 fvex 
 |-  ( 0g ` R ) e. _V
15 13 14 ifex 
 |-  if ( E = E , ( 1r ` R ) , ( 0g ` R ) ) e. _V
16 15 a1i 
 |-  ( ( R e. Ring /\ E e. V ) -> if ( E = E , ( 1r ` R ) , ( 0g ` R ) ) e. _V )
17 eqid 
 |-  ( x e. { E } , y e. { E } |-> if ( x = y , ( 1r ` R ) , ( 0g ` R ) ) ) = ( x e. { E } , y e. { E } |-> if ( x = y , ( 1r ` R ) , ( 0g ` R ) ) )
18 eqeq1 
 |-  ( x = E -> ( x = y <-> E = y ) )
19 18 ifbid 
 |-  ( x = E -> if ( x = y , ( 1r ` R ) , ( 0g ` R ) ) = if ( E = y , ( 1r ` R ) , ( 0g ` R ) ) )
20 eqeq2 
 |-  ( y = E -> ( E = y <-> E = E ) )
21 20 ifbid 
 |-  ( y = E -> if ( E = y , ( 1r ` R ) , ( 0g ` R ) ) = if ( E = E , ( 1r ` R ) , ( 0g ` R ) ) )
22 17 19 21 mposn 
 |-  ( ( E e. V /\ E e. V /\ if ( E = E , ( 1r ` R ) , ( 0g ` R ) ) e. _V ) -> ( x e. { E } , y e. { E } |-> if ( x = y , ( 1r ` R ) , ( 0g ` R ) ) ) = { <. <. E , E >. , if ( E = E , ( 1r ` R ) , ( 0g ` R ) ) >. } )
23 12 12 16 22 syl3anc 
 |-  ( ( R e. Ring /\ E e. V ) -> ( x e. { E } , y e. { E } |-> if ( x = y , ( 1r ` R ) , ( 0g ` R ) ) ) = { <. <. E , E >. , if ( E = E , ( 1r ` R ) , ( 0g ` R ) ) >. } )
24 eqid 
 |-  E = E
25 24 iftruei 
 |-  if ( E = E , ( 1r ` R ) , ( 0g ` R ) ) = ( 1r ` R )
26 25 opeq2i 
 |-  <. <. E , E >. , if ( E = E , ( 1r ` R ) , ( 0g ` R ) ) >. = <. <. E , E >. , ( 1r ` R ) >.
27 26 sneqi 
 |-  { <. <. E , E >. , if ( E = E , ( 1r ` R ) , ( 0g ` R ) ) >. } = { <. <. E , E >. , ( 1r ` R ) >. }
28 23 27 eqtrdi 
 |-  ( ( R e. Ring /\ E e. V ) -> ( x e. { E } , y e. { E } |-> if ( x = y , ( 1r ` R ) , ( 0g ` R ) ) ) = { <. <. E , E >. , ( 1r ` R ) >. } )
29 3 opeq1i 
 |-  <. O , ( 1r ` R ) >. = <. <. E , E >. , ( 1r ` R ) >.
30 29 sneqi 
 |-  { <. O , ( 1r ` R ) >. } = { <. <. E , E >. , ( 1r ` R ) >. }
31 28 30 eqtr4di 
 |-  ( ( R e. Ring /\ E e. V ) -> ( x e. { E } , y e. { E } |-> if ( x = y , ( 1r ` R ) , ( 0g ` R ) ) ) = { <. O , ( 1r ` R ) >. } )
32 11 31 eqtrd 
 |-  ( ( R e. Ring /\ E e. V ) -> ( 1r ` A ) = { <. O , ( 1r ` R ) >. } )