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 \in K ⟼ \{⟨O, x⟩\})$
Assertion	mat1rhmelval	$⊢ (R \in Ring \land E \in V \land X \in K) \to E F (X) E = X$

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		df-ov	$⊢ E F (X) E = F (X) (⟨E, E⟩)$
7	1 2 3 4 5	mat1rhmval	$⊢ (R \in Ring \land E \in V \land X \in K) \to F (X) = \{⟨O, X⟩\}$
8	7	fveq1d	$⊢ (R \in Ring \land E \in V \land X \in K) \to 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⟩ \in V$
12	4 11	eqeltri	$⊢ O \in V$
13		simp3	$⊢ (R \in Ring \land E \in V \land X \in K) \to X \in K$
14		fvsng	$⊢ (O \in V \land X \in K) \to \{⟨O, X⟩\} (O) = X$
15	12 13 14	sylancr	$⊢ (R \in Ring \land E \in V \land X \in K) \to \{⟨O, X⟩\} (O) = X$
16	10 15	syl5eq	$⊢ (R \in Ring \land E \in V \land X \in K) \to \{⟨O, X⟩\} (⟨E, E⟩) = X$
17	8 16	eqtrd	$⊢ (R \in Ring \land E \in V \land X \in K) \to F (X) (⟨E, E⟩) = X$
18	6 17	syl5eq	$⊢ (R \in Ring \land E \in V \land X \in K) \to E F (X) E = X$

Metamath Proof Explorer