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

Metamath Proof Explorer

Theorem mat1rhmelval

Description: The value of the ring homomorphism F . (Contributed by AV, 22-Dec-2019)

Ref Expression
Hypotheses mat1rhmval.k 
|- K = ( Base ` R )
mat1rhmval.a 
|- A = ( { E } Mat R )
mat1rhmval.b 
|- B = ( Base ` A )
mat1rhmval.o 
|- O = <. E , E >.
mat1rhmval.f 
|- F = ( x e. K |-> { <. O , x >. } )
Assertion mat1rhmelval 
|- ( ( R e. Ring /\ E e. V /\ X e. K ) -> ( E ( F ` X ) E ) = X )

Proof

Step Hyp Ref Expression
1 mat1rhmval.k 
 |-  K = ( Base ` R )
2 mat1rhmval.a 
 |-  A = ( { E } Mat R )
3 mat1rhmval.b 
 |-  B = ( Base ` A )
4 mat1rhmval.o 
 |-  O = <. E , E >.
5 mat1rhmval.f 
 |-  F = ( x e. K |-> { <. O , x >. } )
6 df-ov 
 |-  ( E ( F ` X ) E ) = ( ( F ` X ) ` <. E , E >. )
7 1 2 3 4 5 mat1rhmval 
 |-  ( ( R e. Ring /\ E e. V /\ X e. K ) -> ( F ` X ) = { <. O , X >. } )
8 7 fveq1d 
 |-  ( ( R e. Ring /\ E e. V /\ X e. K ) -> ( ( F ` X ) ` <. E , E >. ) = ( { <. O , X >. } ` <. E , E >. ) )
9 4 eqcomi 
 |-  <. E , E >. = O
10 9 fveq2i 
 |-  ( { <. O , X >. } ` <. E , E >. ) = ( { <. O , X >. } ` O )
11 opex 
 |-  <. E , E >. e. _V
12 4 11 eqeltri 
 |-  O e. _V
13 simp3 
 |-  ( ( R e. Ring /\ E e. V /\ X e. K ) -> X e. K )
14 fvsng 
 |-  ( ( O e. _V /\ X e. K ) -> ( { <. O , X >. } ` O ) = X )
15 12 13 14 sylancr 
 |-  ( ( R e. Ring /\ E e. V /\ X e. K ) -> ( { <. O , X >. } ` O ) = X )
16 10 15 eqtrid 
 |-  ( ( R e. Ring /\ E e. V /\ X e. K ) -> ( { <. O , X >. } ` <. E , E >. ) = X )
17 8 16 eqtrd 
 |-  ( ( R e. Ring /\ E e. V /\ X e. K ) -> ( ( F ` X ) ` <. E , E >. ) = X )
18 6 17 eqtrid 
 |-  ( ( R e. Ring /\ E e. V /\ X e. K ) -> ( E ( F ` X ) E ) = X )