This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 eqtrid ⊢ ( ( 𝑅 ∈ Ring ∧ 𝐸 ∈ 𝑉 ∧ 𝑋 ∈ 𝐾 ) → ( { ⟨ 𝑂 , 𝑋 ⟩ } ‘ ⟨ 𝐸 , 𝐸 ⟩ ) = 𝑋 )
17 8 16 eqtrd ⊢ ( ( 𝑅 ∈ Ring ∧ 𝐸 ∈ 𝑉 ∧ 𝑋 ∈ 𝐾 ) → ( ( 𝐹 ‘ 𝑋 ) ‘ ⟨ 𝐸 , 𝐸 ⟩ ) = 𝑋 )
18 6 17 eqtrid ⊢ ( ( 𝑅 ∈ Ring ∧ 𝐸 ∈ 𝑉 ∧ 𝑋 ∈ 𝐾 ) → ( 𝐸 ( 𝐹 ‘ 𝑋 ) 𝐸 ) = 𝑋 )