mat1rhmcl

Description: The value of the ring homomorphism F is a matrix with dimension 1. (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 \in K ⟼ \{⟨O, x⟩\})$
Assertion	mat1rhmcl	$⊢ (R \in Ring \land E \in V \land X \in K) \to F (X) \in B$

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 \in K ⟼ \{⟨O, x⟩\})$
6	2 1 4	mat1dimbas	$⊢ (R \in Ring \land E \in V \land X \in K) \to \{⟨O, X⟩\} \in {Base}_{A}$
7	1 2 3 4 5	mat1rhmval	$⊢ (R \in Ring \land E \in V \land X \in K) \to F (X) = \{⟨O, X⟩\}$
8	3	a1i	$⊢ (R \in Ring \land E \in V \land X \in K) \to B = {Base}_{A}$
9	6 7 8	3eltr4d	$⊢ (R \in Ring \land E \in V \land X \in K) \to F (X) \in B$

Metamath Proof Explorer