Metamath Proof Explorer

Theorem erngmul-rN

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

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

Proof

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