Theorem erngplus2

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	erngplus2	⊢ ( ( ( 𝐾 ∈ 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	erngplus	⊢ ( ( ( 𝐾 ∈ 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 ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑈 ∈ 𝐸 ∧ 𝑉 ∈ 𝐸 ∧ 𝐹 ∈ 𝑇 ) ) → ( ( 𝑈 + 𝑉 ) ‘ 𝐹 ) = ( ( 𝑈 ‘ 𝐹 ) ∘ ( 𝑉 ‘ 𝐹 ) ) )