Theorem mat1rhmval

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

	Ref	Expression
Hypotheses	mat1rhmval.k	⊢ 𝐾 = ( Base ‘ 𝑅 )
	mat1rhmval.a	⊢ 𝐴 = ( { 𝐸 } Mat 𝑅 )
	mat1rhmval.b	⊢ 𝐵 = ( Base ‘ 𝐴 )
	mat1rhmval.o	⊢ 𝑂 = ⟨ 𝐸 , 𝐸 ⟩
	mat1rhmval.f	⊢ 𝐹 = ( 𝑥 ∈ 𝐾 ↦ { ⟨ 𝑂 , 𝑥 ⟩ } )
Assertion	mat1rhmval	⊢ ( ( 𝑅 ∈ Ring ∧ 𝐸 ∈ 𝑉 ∧ 𝑋 ∈ 𝐾 ) → ( 𝐹 ‘ 𝑋 ) = { ⟨ 𝑂 , 𝑋 ⟩ } )

Proof

Step	Hyp	Ref	Expression
1		mat1rhmval.k	⊢ 𝐾 = ( Base ‘ 𝑅 )
2		mat1rhmval.a	⊢ 𝐴 = ( { 𝐸 } Mat 𝑅 )
3		mat1rhmval.b	⊢ 𝐵 = ( Base ‘ 𝐴 )
4		mat1rhmval.o	⊢ 𝑂 = ⟨ 𝐸 , 𝐸 ⟩
5		mat1rhmval.f	⊢ 𝐹 = ( 𝑥 ∈ 𝐾 ↦ { ⟨ 𝑂 , 𝑥 ⟩ } )
6		opeq2	⊢ ( 𝑥 = 𝑋 → ⟨ 𝑂 , 𝑥 ⟩ = ⟨ 𝑂 , 𝑋 ⟩ )
7	6	sneqd	⊢ ( 𝑥 = 𝑋 → { ⟨ 𝑂 , 𝑥 ⟩ } = { ⟨ 𝑂 , 𝑋 ⟩ } )
8		simp3	⊢ ( ( 𝑅 ∈ Ring ∧ 𝐸 ∈ 𝑉 ∧ 𝑋 ∈ 𝐾 ) → 𝑋 ∈ 𝐾 )
9		snex	⊢ { ⟨ 𝑂 , 𝑋 ⟩ } ∈ V
10	9	a1i	⊢ ( ( 𝑅 ∈ Ring ∧ 𝐸 ∈ 𝑉 ∧ 𝑋 ∈ 𝐾 ) → { ⟨ 𝑂 , 𝑋 ⟩ } ∈ V )
11	5 7 8 10	fvmptd3	⊢ ( ( 𝑅 ∈ Ring ∧ 𝐸 ∈ 𝑉 ∧ 𝑋 ∈ 𝐾 ) → ( 𝐹 ‘ 𝑋 ) = { ⟨ 𝑂 , 𝑋 ⟩ } )