Theorem mat1rhmelval

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	mat1rhmelval	⊢ ( ( 𝑅 ∈ 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		df-ov	⊢ ( 𝐸 ( 𝐹 ‘ 𝑋 ) 𝐸 ) = ( ( 𝐹 ‘ 𝑋 ) ‘ ⟨ 𝐸 , 𝐸 ⟩ )
7	1 2 3 4 5	mat1rhmval	⊢ ( ( 𝑅 ∈ Ring ∧ 𝐸 ∈ 𝑉 ∧ 𝑋 ∈ 𝐾 ) → ( 𝐹 ‘ 𝑋 ) = { ⟨ 𝑂 , 𝑋 ⟩ } )
8	7	fveq1d	⊢ ( ( 𝑅 ∈ Ring ∧ 𝐸 ∈ 𝑉 ∧ 𝑋 ∈ 𝐾 ) → ( ( 𝐹 ‘ 𝑋 ) ‘ ⟨ 𝐸 , 𝐸 ⟩ ) = ( { ⟨ 𝑂 , 𝑋 ⟩ } ‘ ⟨ 𝐸 , 𝐸 ⟩ ) )
9	4	eqcomi	⊢ ⟨ 𝐸 , 𝐸 ⟩ = 𝑂
10	9	fveq2i	⊢ ( { ⟨ 𝑂 , 𝑋 ⟩ } ‘ ⟨ 𝐸 , 𝐸 ⟩ ) = ( { ⟨ 𝑂 , 𝑋 ⟩ } ‘ 𝑂 )
11		opex	⊢ ⟨ 𝐸 , 𝐸 ⟩ ∈ V
12	4 11	eqeltri	⊢ 𝑂 ∈ V
13		simp3	⊢ ( ( 𝑅 ∈ Ring ∧ 𝐸 ∈ 𝑉 ∧ 𝑋 ∈ 𝐾 ) → 𝑋 ∈ 𝐾 )
14		fvsng	⊢ ( ( 𝑂 ∈ V ∧ 𝑋 ∈ 𝐾 ) → ( { ⟨ 𝑂 , 𝑋 ⟩ } ‘ 𝑂 ) = 𝑋 )
15	12 13 14	sylancr	⊢ ( ( 𝑅 ∈ Ring ∧ 𝐸 ∈ 𝑉 ∧ 𝑋 ∈ 𝐾 ) → ( { ⟨ 𝑂 , 𝑋 ⟩ } ‘ 𝑂 ) = 𝑋 )
16	10 15	syl5eq	⊢ ( ( 𝑅 ∈ Ring ∧ 𝐸 ∈ 𝑉 ∧ 𝑋 ∈ 𝐾 ) → ( { ⟨ 𝑂 , 𝑋 ⟩ } ‘ ⟨ 𝐸 , 𝐸 ⟩ ) = 𝑋 )
17	8 16	eqtrd	⊢ ( ( 𝑅 ∈ Ring ∧ 𝐸 ∈ 𝑉 ∧ 𝑋 ∈ 𝐾 ) → ( ( 𝐹 ‘ 𝑋 ) ‘ ⟨ 𝐸 , 𝐸 ⟩ ) = 𝑋 )
18	6 17	syl5eq	⊢ ( ( 𝑅 ∈ Ring ∧ 𝐸 ∈ 𝑉 ∧ 𝑋 ∈ 𝐾 ) → ( 𝐸 ( 𝐹 ‘ 𝑋 ) 𝐸 ) = 𝑋 )