Metamath Proof Explorer

Theorem stoweidlem8

Description: Lemma for stoweid : two class variables replace two setvar variables, for the sum of two functions. (Contributed by Glauco Siliprandi, 20-Apr-2017)

Ref Expression
Hypotheses stoweidlem8.1 ⊢ ( ( 𝜑 ∧ 𝑓 ∈ 𝐴 ∧ 𝑔 ∈ 𝐴 ) → ( 𝑡 ∈ 𝑇 ↦ ( ( 𝑓 ‘ 𝑡 ) + ( 𝑔 ‘ 𝑡 ) ) ) ∈ 𝐴 )
stoweidlem8.2 ⊢ Ⅎ 𝑡 𝐹
stoweidlem8.3 ⊢ Ⅎ 𝑡 𝐺
Assertion stoweidlem8 ( ( 𝜑 ∧ 𝐹 ∈ 𝐴 ∧ 𝐺 ∈ 𝐴 ) → ( 𝑡 ∈ 𝑇 ↦ ( ( 𝐹 ‘ 𝑡 ) + ( 𝐺 ‘ 𝑡 ) ) ) ∈ 𝐴 )

Proof

Step Hyp Ref Expression
1 stoweidlem8.1 ⊢ ( ( 𝜑 ∧ 𝑓 ∈ 𝐴 ∧ 𝑔 ∈ 𝐴 ) → ( 𝑡 ∈ 𝑇 ↦ ( ( 𝑓 ‘ 𝑡 ) + ( 𝑔 ‘ 𝑡 ) ) ) ∈ 𝐴 )
2 stoweidlem8.2 ⊢ Ⅎ 𝑡 𝐹
3 stoweidlem8.3 ⊢ Ⅎ 𝑡 𝐺
4 simp3 ⊢ ( ( 𝜑 ∧ 𝐹 ∈ 𝐴 ∧ 𝐺 ∈ 𝐴 ) → 𝐺 ∈ 𝐴 )
5 eleq1 ⊢ ( 𝑔 = 𝐺 → ( 𝑔 ∈ 𝐴 ↔ 𝐺 ∈ 𝐴 ) )
6 5 3anbi3d ⊢ ( 𝑔 = 𝐺 → ( ( 𝜑 ∧ 𝐹 ∈ 𝐴 ∧ 𝑔 ∈ 𝐴 ) ↔ ( 𝜑 ∧ 𝐹 ∈ 𝐴 ∧ 𝐺 ∈ 𝐴 ) ) )
7 3 nfeq2 ⊢ Ⅎ 𝑡 𝑔 = 𝐺
8 fveq1 ⊢ ( 𝑔 = 𝐺 → ( 𝑔 ‘ 𝑡 ) = ( 𝐺 ‘ 𝑡 ) )
9 8 oveq2d ⊢ ( 𝑔 = 𝐺 → ( ( 𝐹 ‘ 𝑡 ) + ( 𝑔 ‘ 𝑡 ) ) = ( ( 𝐹 ‘ 𝑡 ) + ( 𝐺 ‘ 𝑡 ) ) )
10 9 adantr ⊢ ( ( 𝑔 = 𝐺 ∧ 𝑡 ∈ 𝑇 ) → ( ( 𝐹 ‘ 𝑡 ) + ( 𝑔 ‘ 𝑡 ) ) = ( ( 𝐹 ‘ 𝑡 ) + ( 𝐺 ‘ 𝑡 ) ) )
11 7 10 mpteq2da ⊢ ( 𝑔 = 𝐺 → ( 𝑡 ∈ 𝑇 ↦ ( ( 𝐹 ‘ 𝑡 ) + ( 𝑔 ‘ 𝑡 ) ) ) = ( 𝑡 ∈ 𝑇 ↦ ( ( 𝐹 ‘ 𝑡 ) + ( 𝐺 ‘ 𝑡 ) ) ) )
12 11 eleq1d ⊢ ( 𝑔 = 𝐺 → ( ( 𝑡 ∈ 𝑇 ↦ ( ( 𝐹 ‘ 𝑡 ) + ( 𝑔 ‘ 𝑡 ) ) ) ∈ 𝐴 ↔ ( 𝑡 ∈ 𝑇 ↦ ( ( 𝐹 ‘ 𝑡 ) + ( 𝐺 ‘ 𝑡 ) ) ) ∈ 𝐴 ) )
13 6 12 imbi12d ⊢ ( 𝑔 = 𝐺 → ( ( ( 𝜑 ∧ 𝐹 ∈ 𝐴 ∧ 𝑔 ∈ 𝐴 ) → ( 𝑡 ∈ 𝑇 ↦ ( ( 𝐹 ‘ 𝑡 ) + ( 𝑔 ‘ 𝑡 ) ) ) ∈ 𝐴 ) ↔ ( ( 𝜑 ∧ 𝐹 ∈ 𝐴 ∧ 𝐺 ∈ 𝐴 ) → ( 𝑡 ∈ 𝑇 ↦ ( ( 𝐹 ‘ 𝑡 ) + ( 𝐺 ‘ 𝑡 ) ) ) ∈ 𝐴 ) ) )
14 simp2 ⊢ ( ( 𝜑 ∧ 𝐹 ∈ 𝐴 ∧ 𝑔 ∈ 𝐴 ) → 𝐹 ∈ 𝐴 )
15 eleq1 ⊢ ( 𝑓 = 𝐹 → ( 𝑓 ∈ 𝐴 ↔ 𝐹 ∈ 𝐴 ) )
16 15 3anbi2d ⊢ ( 𝑓 = 𝐹 → ( ( 𝜑 ∧ 𝑓 ∈ 𝐴 ∧ 𝑔 ∈ 𝐴 ) ↔ ( 𝜑 ∧ 𝐹 ∈ 𝐴 ∧ 𝑔 ∈ 𝐴 ) ) )
17 2 nfeq2 ⊢ Ⅎ 𝑡 𝑓 = 𝐹
18 fveq1 ⊢ ( 𝑓 = 𝐹 → ( 𝑓 ‘ 𝑡 ) = ( 𝐹 ‘ 𝑡 ) )
19 18 oveq1d ⊢ ( 𝑓 = 𝐹 → ( ( 𝑓 ‘ 𝑡 ) + ( 𝑔 ‘ 𝑡 ) ) = ( ( 𝐹 ‘ 𝑡 ) + ( 𝑔 ‘ 𝑡 ) ) )
20 19 adantr ⊢ ( ( 𝑓 = 𝐹 ∧ 𝑡 ∈ 𝑇 ) → ( ( 𝑓 ‘ 𝑡 ) + ( 𝑔 ‘ 𝑡 ) ) = ( ( 𝐹 ‘ 𝑡 ) + ( 𝑔 ‘ 𝑡 ) ) )
21 17 20 mpteq2da ⊢ ( 𝑓 = 𝐹 → ( 𝑡 ∈ 𝑇 ↦ ( ( 𝑓 ‘ 𝑡 ) + ( 𝑔 ‘ 𝑡 ) ) ) = ( 𝑡 ∈ 𝑇 ↦ ( ( 𝐹 ‘ 𝑡 ) + ( 𝑔 ‘ 𝑡 ) ) ) )
22 21 eleq1d ⊢ ( 𝑓 = 𝐹 → ( ( 𝑡 ∈ 𝑇 ↦ ( ( 𝑓 ‘ 𝑡 ) + ( 𝑔 ‘ 𝑡 ) ) ) ∈ 𝐴 ↔ ( 𝑡 ∈ 𝑇 ↦ ( ( 𝐹 ‘ 𝑡 ) + ( 𝑔 ‘ 𝑡 ) ) ) ∈ 𝐴 ) )
23 16 22 imbi12d ⊢ ( 𝑓 = 𝐹 → ( ( ( 𝜑 ∧ 𝑓 ∈ 𝐴 ∧ 𝑔 ∈ 𝐴 ) → ( 𝑡 ∈ 𝑇 ↦ ( ( 𝑓 ‘ 𝑡 ) + ( 𝑔 ‘ 𝑡 ) ) ) ∈ 𝐴 ) ↔ ( ( 𝜑 ∧ 𝐹 ∈ 𝐴 ∧ 𝑔 ∈ 𝐴 ) → ( 𝑡 ∈ 𝑇 ↦ ( ( 𝐹 ‘ 𝑡 ) + ( 𝑔 ‘ 𝑡 ) ) ) ∈ 𝐴 ) ) )
24 23 1 vtoclg ⊢ ( 𝐹 ∈ 𝐴 → ( ( 𝜑 ∧ 𝐹 ∈ 𝐴 ∧ 𝑔 ∈ 𝐴 ) → ( 𝑡 ∈ 𝑇 ↦ ( ( 𝐹 ‘ 𝑡 ) + ( 𝑔 ‘ 𝑡 ) ) ) ∈ 𝐴 ) )
25 14 24 mpcom ⊢ ( ( 𝜑 ∧ 𝐹 ∈ 𝐴 ∧ 𝑔 ∈ 𝐴 ) → ( 𝑡 ∈ 𝑇 ↦ ( ( 𝐹 ‘ 𝑡 ) + ( 𝑔 ‘ 𝑡 ) ) ) ∈ 𝐴 )
26 13 25 vtoclg ⊢ ( 𝐺 ∈ 𝐴 → ( ( 𝜑 ∧ 𝐹 ∈ 𝐴 ∧ 𝐺 ∈ 𝐴 ) → ( 𝑡 ∈ 𝑇 ↦ ( ( 𝐹 ‘ 𝑡 ) + ( 𝐺 ‘ 𝑡 ) ) ) ∈ 𝐴 ) )
27 4 26 mpcom ⊢ ( ( 𝜑 ∧ 𝐹 ∈ 𝐴 ∧ 𝐺 ∈ 𝐴 ) → ( 𝑡 ∈ 𝑇 ↦ ( ( 𝐹 ‘ 𝑡 ) + ( 𝐺 ‘ 𝑡 ) ) ) ∈ 𝐴 )