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

Metamath Proof Explorer

Theorem erngplus2-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.p-r ⊢ + = ( +g ‘ 𝐷 )
Assertion erngplus2-rN ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑈 ∈ 𝐸 ∧ 𝑉 ∈ 𝐸 ∧ 𝐹 ∈ 𝑇 ) ) → ( ( 𝑈 + 𝑉 ) ‘ 𝐹 ) = ( ( 𝑈 ‘ 𝐹 ) ∘ ( 𝑉 ‘ 𝐹 ) ) )

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.p-r ⊢ + = ( +g ‘ 𝐷 )
6 1 2 3 4 5 erngplus-rN ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑈 ∈ 𝐸 ∧ 𝑉 ∈ 𝐸 ) ) → ( 𝑈 + 𝑉 ) = ( 𝑓 ∈ 𝑇 ↦ ( ( 𝑈 ‘ 𝑓 ) ∘ ( 𝑉 ‘ 𝑓 ) ) ) )
7 6 3adantr3 ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑈 ∈ 𝐸 ∧ 𝑉 ∈ 𝐸 ∧ 𝐹 ∈ 𝑇 ) ) → ( 𝑈 + 𝑉 ) = ( 𝑓 ∈ 𝑇 ↦ ( ( 𝑈 ‘ 𝑓 ) ∘ ( 𝑉 ‘ 𝑓 ) ) ) )
8 fveq2 ⊢ ( 𝑓 = 𝐹 → ( 𝑈 ‘ 𝑓 ) = ( 𝑈 ‘ 𝐹 ) )
9 fveq2 ⊢ ( 𝑓 = 𝐹 → ( 𝑉 ‘ 𝑓 ) = ( 𝑉 ‘ 𝐹 ) )
10 8 9 coeq12d ⊢ ( 𝑓 = 𝐹 → ( ( 𝑈 ‘ 𝑓 ) ∘ ( 𝑉 ‘ 𝑓 ) ) = ( ( 𝑈 ‘ 𝐹 ) ∘ ( 𝑉 ‘ 𝐹 ) ) )
11 10 adantl ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑈 ∈ 𝐸 ∧ 𝑉 ∈ 𝐸 ∧ 𝐹 ∈ 𝑇 ) ) ∧ 𝑓 = 𝐹 ) → ( ( 𝑈 ‘ 𝑓 ) ∘ ( 𝑉 ‘ 𝑓 ) ) = ( ( 𝑈 ‘ 𝐹 ) ∘ ( 𝑉 ‘ 𝐹 ) ) )
12 simpr3 ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑈 ∈ 𝐸 ∧ 𝑉 ∈ 𝐸 ∧ 𝐹 ∈ 𝑇 ) ) → 𝐹 ∈ 𝑇 )
13 fvex ⊢ ( 𝑈 ‘ 𝐹 ) ∈ V
14 fvex ⊢ ( 𝑉 ‘ 𝐹 ) ∈ V
15 13 14 coex ⊢ ( ( 𝑈 ‘ 𝐹 ) ∘ ( 𝑉 ‘ 𝐹 ) ) ∈ V
16 15 a1i ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑈 ∈ 𝐸 ∧ 𝑉 ∈ 𝐸 ∧ 𝐹 ∈ 𝑇 ) ) → ( ( 𝑈 ‘ 𝐹 ) ∘ ( 𝑉 ‘ 𝐹 ) ) ∈ V )
17 7 11 12 16 fvmptd ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑈 ∈ 𝐸 ∧ 𝑉 ∈ 𝐸 ∧ 𝐹 ∈ 𝑇 ) ) → ( ( 𝑈 + 𝑉 ) ‘ 𝐹 ) = ( ( 𝑈 ‘ 𝐹 ) ∘ ( 𝑉 ‘ 𝐹 ) ) )