Theorem mat1rhmval

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	mat1rhmval	|- ( ( R e. Ring /\ E e. V /\ X e. K ) -> ( F ` X ) = { <. O , 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		opeq2	|- ( x = X -> <. O , x >. = <. O , X >. )
7	6	sneqd	|- ( x = X -> { <. O , x >. } = { <. O , X >. } )
8		simp3	|- ( ( R e. Ring /\ E e. V /\ X e. K ) -> X e. K )
9		snex	|- { <. O , X >. } e. _V
10	9	a1i	|- ( ( R e. Ring /\ E e. V /\ X e. K ) -> { <. O , X >. } e. _V )
11	5 7 8 10	fvmptd3	|- ( ( R e. Ring /\ E e. V /\ X e. K ) -> ( F ` X ) = { <. O , X >. } )