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 ( ( 𝜑𝐹𝐴𝐺𝐴 ) → ( 𝑡𝑇 ↦ ( ( 𝐹𝑡 ) + ( 𝐺𝑡 ) ) ) ∈ 𝐴 )