Metamath Proof Explorer

Theorem mat1dim0

Description: The zero 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 mat1dim0 
|- ( ( R e. Ring /\ E e. V ) -> ( 0g ` A ) = { <. O , ( 0g ` 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 
 |-  ( 0g ` R ) = ( 0g ` R )
9 1 8 mat0op 
 |-  ( ( { E } e. Fin /\ R e. Ring ) -> ( 0g ` A ) = ( x e. { E } , y e. { E } |-> ( 0g ` R ) ) )
10 7 9 syl 
 |-  ( ( R e. Ring /\ E e. V ) -> ( 0g ` A ) = ( x e. { E } , y e. { E } |-> ( 0g ` R ) ) )
11 simpr 
 |-  ( ( R e. Ring /\ E e. V ) -> E e. V )
12 fvexd 
 |-  ( ( R e. Ring /\ E e. V ) -> ( 0g ` R ) e. _V )
13 eqid 
 |-  ( x e. { E } , y e. { E } |-> ( 0g ` R ) ) = ( x e. { E } , y e. { E } |-> ( 0g ` R ) )
14 eqidd 
 |-  ( x = E -> ( 0g ` R ) = ( 0g ` R ) )
15 eqidd 
 |-  ( y = E -> ( 0g ` R ) = ( 0g ` R ) )
16 13 14 15 mposn 
 |-  ( ( E e. V /\ E e. V /\ ( 0g ` R ) e. _V ) -> ( x e. { E } , y e. { E } |-> ( 0g ` R ) ) = { <. <. E , E >. , ( 0g ` R ) >. } )
17 3 eqcomi 
 |-  <. E , E >. = O
18 17 opeq1i 
 |-  <. <. E , E >. , ( 0g ` R ) >. = <. O , ( 0g ` R ) >.
19 18 sneqi 
 |-  { <. <. E , E >. , ( 0g ` R ) >. } = { <. O , ( 0g ` R ) >. }
20 16 19 eqtrdi 
 |-  ( ( E e. V /\ E e. V /\ ( 0g ` R ) e. _V ) -> ( x e. { E } , y e. { E } |-> ( 0g ` R ) ) = { <. O , ( 0g ` R ) >. } )
21 11 11 12 20 syl3anc 
 |-  ( ( R e. Ring /\ E e. V ) -> ( x e. { E } , y e. { E } |-> ( 0g ` R ) ) = { <. O , ( 0g ` R ) >. } )
22 10 21 eqtrd 
 |-  ( ( R e. Ring /\ E e. V ) -> ( 0g ` A ) = { <. O , ( 0g ` R ) >. } )