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 ⊢ K = Base R
mat1rhmval.a ⊢ A = E Mat R
mat1rhmval.b ⊢ B = Base A
mat1rhmval.o ⊢ O = E E
mat1rhmval.f ⊢ F = x ∈ K ⟼ O x
Assertion mat1rhmelval ⊢ R ∈ Ring ∧ E ∈ V ∧ X ∈ K → E F ⁡ X E = X

Proof

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 ∈ K ⟼ O x
6 df-ov ⊢ E F ⁡ X E = F ⁡ X ⁡ E E
7 1 2 3 4 5 mat1rhmval ⊢ R ∈ Ring ∧ E ∈ V ∧ X ∈ K → F ⁡ X = O X
8 7 fveq1d ⊢ R ∈ Ring ∧ E ∈ V ∧ X ∈ K → 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 ∈ V
12 4 11 eqeltri ⊢ O ∈ V
13 simp3 ⊢ R ∈ Ring ∧ E ∈ V ∧ X ∈ K → X ∈ K
14 fvsng ⊢ O ∈ V ∧ X ∈ K → O X ⁡ O = X
15 12 13 14 sylancr ⊢ R ∈ Ring ∧ E ∈ V ∧ X ∈ K → O X ⁡ O = X
16 10 15 eqtrid ⊢ R ∈ Ring ∧ E ∈ V ∧ X ∈ K → O X ⁡ E E = X
17 8 16 eqtrd ⊢ R ∈ Ring ∧ E ∈ V ∧ X ∈ K → F ⁡ X ⁡ E E = X
18 6 17 eqtrid ⊢ R ∈ Ring ∧ E ∈ V ∧ X ∈ K → E F ⁡ X E = X