Metamath Proof Explorer

Theorem erngmul

Description: Ring addition operation. (Contributed by NM, 10-Jun-2013)

Ref Expression
Hypotheses erngset.h ⊢ H = LHyp ⁡ K
erngset.t ⊢ T = LTrn ⁡ K ⁡ W
erngset.e ⊢ E = TEndo ⁡ K ⁡ W
erngset.d ⊢ D = EDRing ⁡ K ⁡ W
erng.m ⊢ · ˙ = ⋅ D
Assertion erngmul ⊢ K ∈ X ∧ W ∈ H ∧ U ∈ E ∧ V ∈ E → U · ˙ V = U ∘ V

Proof

Step Hyp Ref Expression
1 erngset.h ⊢ H = LHyp ⁡ K
2 erngset.t ⊢ T = LTrn ⁡ K ⁡ W
3 erngset.e ⊢ E = TEndo ⁡ K ⁡ W
4 erngset.d ⊢ D = EDRing ⁡ K ⁡ W
5 erng.m ⊢ · ˙ = ⋅ D
6 1 2 3 4 5 erngfmul ⊢ K ∈ X ∧ W ∈ H → · ˙ = s ∈ E , t ∈ E ⟼ s ∘ t
7 6 oveqd ⊢ K ∈ X ∧ W ∈ H → U · ˙ V = U s ∈ E , t ∈ E ⟼ s ∘ t V
8 coexg ⊢ U ∈ E ∧ V ∈ E → U ∘ V ∈ V
9 coeq1 ⊢ s = U → s ∘ t = U ∘ t
10 coeq2 ⊢ t = V → U ∘ t = U ∘ V
11 eqid ⊢ s ∈ E , t ∈ E ⟼ s ∘ t = s ∈ E , t ∈ E ⟼ s ∘ t
12 9 10 11 ovmpog ⊢ U ∈ E ∧ V ∈ E ∧ U ∘ V ∈ V → U s ∈ E , t ∈ E ⟼ s ∘ t V = U ∘ V
13 8 12 mpd3an3 ⊢ U ∈ E ∧ V ∈ E → U s ∈ E , t ∈ E ⟼ s ∘ t V = U ∘ V
14 7 13 sylan9eq ⊢ K ∈ X ∧ W ∈ H ∧ U ∈ E ∧ V ∈ E → U · ˙ V = U ∘ V