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

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 ⊢ 𝐻 = ( LHyp ‘ 𝐾 )
erngset.t-r ⊢ 𝑇 = ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 )
erngset.e-r ⊢ 𝐸 = ( ( TEndo ‘ 𝐾 ) ‘ 𝑊 )
erngset.d-r ⊢ 𝐷 = ( ( EDRingR ‘ 𝐾 ) ‘ 𝑊 )
erng.m-r ⊢ · = ( .r ‘ 𝐷 )
Assertion erngmul-rN ( ( ( 𝐾 ∈ 𝑋 ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑈 ∈ 𝐸 ∧ 𝑉 ∈ 𝐸 ) ) → ( 𝑈 · 𝑉 ) = ( 𝑉 ∘ 𝑈 ) )

Proof

Step Hyp Ref Expression
1 erngset.h-r ⊢ 𝐻 = ( LHyp ‘ 𝐾 )
2 erngset.t-r ⊢ 𝑇 = ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 )
3 erngset.e-r ⊢ 𝐸 = ( ( TEndo ‘ 𝐾 ) ‘ 𝑊 )
4 erngset.d-r ⊢ 𝐷 = ( ( EDRingR ‘ 𝐾 ) ‘ 𝑊 )
5 erng.m-r ⊢ · = ( .r ‘ 𝐷 )
6 1 2 3 4 5 erngfmul-rN ⊢ ( ( 𝐾 ∈ 𝑋 ∧ 𝑊 ∈ 𝐻 ) → · = ( 𝑠 ∈ 𝐸 , 𝑡 ∈ 𝐸 ↦ ( 𝑡 ∘ 𝑠 ) ) )
7 6 adantr ⊢ ( ( ( 𝐾 ∈ 𝑋 ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑈 ∈ 𝐸 ∧ 𝑉 ∈ 𝐸 ) ) → · = ( 𝑠 ∈ 𝐸 , 𝑡 ∈ 𝐸 ↦ ( 𝑡 ∘ 𝑠 ) ) )
8 7 oveqd ⊢ ( ( ( 𝐾 ∈ 𝑋 ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑈 ∈ 𝐸 ∧ 𝑉 ∈ 𝐸 ) ) → ( 𝑈 · 𝑉 ) = ( 𝑈 ( 𝑠 ∈ 𝐸 , 𝑡 ∈ 𝐸 ↦ ( 𝑡 ∘ 𝑠 ) ) 𝑉 ) )
9 coexg ⊢ ( ( 𝑉 ∈ 𝐸 ∧ 𝑈 ∈ 𝐸 ) → ( 𝑉 ∘ 𝑈 ) ∈ V )
10 9 ancoms ⊢ ( ( 𝑈 ∈ 𝐸 ∧ 𝑉 ∈ 𝐸 ) → ( 𝑉 ∘ 𝑈 ) ∈ V )
11 coeq2 ⊢ ( 𝑠 = 𝑈 → ( 𝑡 ∘ 𝑠 ) = ( 𝑡 ∘ 𝑈 ) )
12 coeq1 ⊢ ( 𝑡 = 𝑉 → ( 𝑡 ∘ 𝑈 ) = ( 𝑉 ∘ 𝑈 ) )
13 eqid ⊢ ( 𝑠 ∈ 𝐸 , 𝑡 ∈ 𝐸 ↦ ( 𝑡 ∘ 𝑠 ) ) = ( 𝑠 ∈ 𝐸 , 𝑡 ∈ 𝐸 ↦ ( 𝑡 ∘ 𝑠 ) )
14 11 12 13 ovmpog ⊢ ( ( 𝑈 ∈ 𝐸 ∧ 𝑉 ∈ 𝐸 ∧ ( 𝑉 ∘ 𝑈 ) ∈ V ) → ( 𝑈 ( 𝑠 ∈ 𝐸 , 𝑡 ∈ 𝐸 ↦ ( 𝑡 ∘ 𝑠 ) ) 𝑉 ) = ( 𝑉 ∘ 𝑈 ) )
15 10 14 mpd3an3 ⊢ ( ( 𝑈 ∈ 𝐸 ∧ 𝑉 ∈ 𝐸 ) → ( 𝑈 ( 𝑠 ∈ 𝐸 , 𝑡 ∈ 𝐸 ↦ ( 𝑡 ∘ 𝑠 ) ) 𝑉 ) = ( 𝑉 ∘ 𝑈 ) )
16 15 adantl ⊢ ( ( ( 𝐾 ∈ 𝑋 ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑈 ∈ 𝐸 ∧ 𝑉 ∈ 𝐸 ) ) → ( 𝑈 ( 𝑠 ∈ 𝐸 , 𝑡 ∈ 𝐸 ↦ ( 𝑡 ∘ 𝑠 ) ) 𝑉 ) = ( 𝑉 ∘ 𝑈 ) )
17 8 16 eqtrd ⊢ ( ( ( 𝐾 ∈ 𝑋 ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑈 ∈ 𝐸 ∧ 𝑉 ∈ 𝐸 ) ) → ( 𝑈 · 𝑉 ) = ( 𝑉 ∘ 𝑈 ) )