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	syl5eq	|- ( ( 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	syl5eq	|- ( ( R e. Ring /\ E e. V /\ X e. K ) -> ( E ( F ` X ) E ) = X )