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

Metamath Proof Explorer

Theorem erngplus

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

Ref Expression
Hypotheses erngset.h ⊢ 𝐻 = ( LHyp ‘ 𝐾 )
erngset.t ⊢ 𝑇 = ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 )
erngset.e ⊢ 𝐸 = ( ( TEndo ‘ 𝐾 ) ‘ 𝑊 )
erngset.d ⊢ 𝐷 = ( ( EDRing ‘ 𝐾 ) ‘ 𝑊 )
erng.p ⊢ + = ( +g ‘ 𝐷 )
Assertion erngplus ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑈 ∈ 𝐸 ∧ 𝑉 ∈ 𝐸 ) ) → ( 𝑈 + 𝑉 ) = ( 𝑓 ∈ 𝑇 ↦ ( ( 𝑈 ‘ 𝑓 ) ∘ ( 𝑉 ‘ 𝑓 ) ) ) )

Proof

Step Hyp Ref Expression
1 erngset.h ⊢ 𝐻 = ( LHyp ‘ 𝐾 )
2 erngset.t ⊢ 𝑇 = ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 )
3 erngset.e ⊢ 𝐸 = ( ( TEndo ‘ 𝐾 ) ‘ 𝑊 )
4 erngset.d ⊢ 𝐷 = ( ( EDRing ‘ 𝐾 ) ‘ 𝑊 )
5 erng.p ⊢ + = ( +g ‘ 𝐷 )
6 1 2 3 4 5 erngfplus ⊢ ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) → + = ( 𝑠 ∈ 𝐸 , 𝑡 ∈ 𝐸 ↦ ( 𝑔 ∈ 𝑇 ↦ ( ( 𝑠 ‘ 𝑔 ) ∘ ( 𝑡 ‘ 𝑔 ) ) ) ) )
7 6 oveqd ⊢ ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) → ( 𝑈 + 𝑉 ) = ( 𝑈 ( 𝑠 ∈ 𝐸 , 𝑡 ∈ 𝐸 ↦ ( 𝑔 ∈ 𝑇 ↦ ( ( 𝑠 ‘ 𝑔 ) ∘ ( 𝑡 ‘ 𝑔 ) ) ) ) 𝑉 ) )
8 eqid ⊢ ( 𝑠 ∈ 𝐸 , 𝑡 ∈ 𝐸 ↦ ( 𝑔 ∈ 𝑇 ↦ ( ( 𝑠 ‘ 𝑔 ) ∘ ( 𝑡 ‘ 𝑔 ) ) ) ) = ( 𝑠 ∈ 𝐸 , 𝑡 ∈ 𝐸 ↦ ( 𝑔 ∈ 𝑇 ↦ ( ( 𝑠 ‘ 𝑔 ) ∘ ( 𝑡 ‘ 𝑔 ) ) ) )
9 8 2 tendopl ⊢ ( ( 𝑈 ∈ 𝐸 ∧ 𝑉 ∈ 𝐸 ) → ( 𝑈 ( 𝑠 ∈ 𝐸 , 𝑡 ∈ 𝐸 ↦ ( 𝑔 ∈ 𝑇 ↦ ( ( 𝑠 ‘ 𝑔 ) ∘ ( 𝑡 ‘ 𝑔 ) ) ) ) 𝑉 ) = ( 𝑓 ∈ 𝑇 ↦ ( ( 𝑈 ‘ 𝑓 ) ∘ ( 𝑉 ‘ 𝑓 ) ) ) )
10 7 9 sylan9eq ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑈 ∈ 𝐸 ∧ 𝑉 ∈ 𝐸 ) ) → ( 𝑈 + 𝑉 ) = ( 𝑓 ∈ 𝑇 ↦ ( ( 𝑈 ‘ 𝑓 ) ∘ ( 𝑉 ‘ 𝑓 ) ) ) )