# 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 $⊢ φ ∧ f ∈ A ∧ g ∈ A → t ∈ T ⟼ f ⁡ t + g ⁡ t ∈ A$
stoweidlem8.2 $⊢ Ⅎ _ t F$
stoweidlem8.3 $⊢ Ⅎ _ t G$
Assertion stoweidlem8 $⊢ φ ∧ F ∈ A ∧ G ∈ A → t ∈ T ⟼ F ⁡ t + G ⁡ t ∈ A$

### Proof

Step Hyp Ref Expression
1 stoweidlem8.1 $⊢ φ ∧ f ∈ A ∧ g ∈ A → t ∈ T ⟼ f ⁡ t + g ⁡ t ∈ A$
2 stoweidlem8.2 $⊢ Ⅎ _ t F$
3 stoweidlem8.3 $⊢ Ⅎ _ t G$
4 simp3 $⊢ φ ∧ F ∈ A ∧ G ∈ A → G ∈ A$
5 eleq1 $⊢ g = G → g ∈ A ↔ G ∈ A$
6 5 3anbi3d $⊢ g = G → φ ∧ F ∈ A ∧ g ∈ A ↔ φ ∧ F ∈ A ∧ G ∈ A$
7 3 nfeq2 $⊢ Ⅎ t g = G$
8 fveq1 $⊢ g = G → g ⁡ t = G ⁡ t$
9 8 oveq2d $⊢ g = G → F ⁡ t + g ⁡ t = F ⁡ t + G ⁡ t$
10 9 adantr $⊢ g = G ∧ t ∈ T → F ⁡ t + g ⁡ t = F ⁡ t + G ⁡ t$
11 7 10 mpteq2da $⊢ g = G → t ∈ T ⟼ F ⁡ t + g ⁡ t = t ∈ T ⟼ F ⁡ t + G ⁡ t$
12 11 eleq1d $⊢ g = G → t ∈ T ⟼ F ⁡ t + g ⁡ t ∈ A ↔ t ∈ T ⟼ F ⁡ t + G ⁡ t ∈ A$
13 6 12 imbi12d $⊢ g = G → φ ∧ F ∈ A ∧ g ∈ A → t ∈ T ⟼ F ⁡ t + g ⁡ t ∈ A ↔ φ ∧ F ∈ A ∧ G ∈ A → t ∈ T ⟼ F ⁡ t + G ⁡ t ∈ A$
14 simp2 $⊢ φ ∧ F ∈ A ∧ g ∈ A → F ∈ A$
15 eleq1 $⊢ f = F → f ∈ A ↔ F ∈ A$
16 15 3anbi2d $⊢ f = F → φ ∧ f ∈ A ∧ g ∈ A ↔ φ ∧ F ∈ A ∧ g ∈ A$
17 2 nfeq2 $⊢ Ⅎ t f = F$
18 fveq1 $⊢ f = F → f ⁡ t = F ⁡ t$
19 18 oveq1d $⊢ f = F → f ⁡ t + g ⁡ t = F ⁡ t + g ⁡ t$
20 19 adantr $⊢ f = F ∧ t ∈ T → f ⁡ t + g ⁡ t = F ⁡ t + g ⁡ t$
21 17 20 mpteq2da $⊢ f = F → t ∈ T ⟼ f ⁡ t + g ⁡ t = t ∈ T ⟼ F ⁡ t + g ⁡ t$
22 21 eleq1d $⊢ f = F → t ∈ T ⟼ f ⁡ t + g ⁡ t ∈ A ↔ t ∈ T ⟼ F ⁡ t + g ⁡ t ∈ A$
23 16 22 imbi12d $⊢ f = F → φ ∧ f ∈ A ∧ g ∈ A → t ∈ T ⟼ f ⁡ t + g ⁡ t ∈ A ↔ φ ∧ F ∈ A ∧ g ∈ A → t ∈ T ⟼ F ⁡ t + g ⁡ t ∈ A$
24 23 1 vtoclg $⊢ F ∈ A → φ ∧ F ∈ A ∧ g ∈ A → t ∈ T ⟼ F ⁡ t + g ⁡ t ∈ A$
25 14 24 mpcom $⊢ φ ∧ F ∈ A ∧ g ∈ A → t ∈ T ⟼ F ⁡ t + g ⁡ t ∈ A$
26 13 25 vtoclg $⊢ G ∈ A → φ ∧ F ∈ A ∧ G ∈ A → t ∈ T ⟼ F ⁡ t + G ⁡ t ∈ A$
27 4 26 mpcom $⊢ φ ∧ F ∈ A ∧ G ∈ A → t ∈ T ⟼ F ⁡ t + G ⁡ t ∈ A$