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	$⊢ (φ \land f \in A \land g \in A) \to (t \in T ⟼ f (t) + g (t)) \in A$
	stoweidlem8.2	$⊢ \underline{Ⅎ} t F$
	stoweidlem8.3	$⊢ \underline{Ⅎ} t G$
Assertion	stoweidlem8	$⊢ (φ \land F \in A \land G \in A) \to (t \in T ⟼ F (t) + G (t)) \in A$

Proof

Step	Hyp	Ref	Expression
1		stoweidlem8.1	$⊢ (φ \land f \in A \land g \in A) \to (t \in T ⟼ f (t) + g (t)) \in A$
2		stoweidlem8.2	$⊢ \underline{Ⅎ} t F$
3		stoweidlem8.3	$⊢ \underline{Ⅎ} t G$
4		simp3	$⊢ (φ \land F \in A \land G \in A) \to G \in A$
5		eleq1	$⊢ g = G \to (g \in A \leftrightarrow G \in A)$
6	5	3anbi3d	$⊢ g = G \to ((φ \land F \in A \land g \in A) \leftrightarrow (φ \land F \in A \land G \in A))$
7	3	nfeq2	$⊢ Ⅎ t g = G$
8		fveq1	$⊢ g = G \to g (t) = G (t)$
9	8	oveq2d	$⊢ g = G \to F (t) + g (t) = F (t) + G (t)$
10	9	adantr	$⊢ (g = G \land t \in T) \to F (t) + g (t) = F (t) + G (t)$
11	7 10	mpteq2da	$⊢ g = G \to (t \in T ⟼ F (t) + g (t)) = (t \in T ⟼ F (t) + G (t))$
12	11	eleq1d	$⊢ g = G \to ((t \in T ⟼ F (t) + g (t)) \in A \leftrightarrow (t \in T ⟼ F (t) + G (t)) \in A)$
13	6 12	imbi12d	$⊢ g = G \to (((φ \land F \in A \land g \in A) \to (t \in T ⟼ F (t) + g (t)) \in A) \leftrightarrow ((φ \land F \in A \land G \in A) \to (t \in T ⟼ F (t) + G (t)) \in A))$
14		simp2	$⊢ (φ \land F \in A \land g \in A) \to F \in A$
15		eleq1	$⊢ f = F \to (f \in A \leftrightarrow F \in A)$
16	15	3anbi2d	$⊢ f = F \to ((φ \land f \in A \land g \in A) \leftrightarrow (φ \land F \in A \land g \in A))$
17	2	nfeq2	$⊢ Ⅎ t f = F$
18		fveq1	$⊢ f = F \to f (t) = F (t)$
19	18	oveq1d	$⊢ f = F \to f (t) + g (t) = F (t) + g (t)$
20	19	adantr	$⊢ (f = F \land t \in T) \to f (t) + g (t) = F (t) + g (t)$
21	17 20	mpteq2da	$⊢ f = F \to (t \in T ⟼ f (t) + g (t)) = (t \in T ⟼ F (t) + g (t))$
22	21	eleq1d	$⊢ f = F \to ((t \in T ⟼ f (t) + g (t)) \in A \leftrightarrow (t \in T ⟼ F (t) + g (t)) \in A)$
23	16 22	imbi12d	$⊢ f = F \to (((φ \land f \in A \land g \in A) \to (t \in T ⟼ f (t) + g (t)) \in A) \leftrightarrow ((φ \land F \in A \land g \in A) \to (t \in T ⟼ F (t) + g (t)) \in A))$
24	23 1	vtoclg	$⊢ F \in A \to ((φ \land F \in A \land g \in A) \to (t \in T ⟼ F (t) + g (t)) \in A)$
25	14 24	mpcom	$⊢ (φ \land F \in A \land g \in A) \to (t \in T ⟼ F (t) + g (t)) \in A$
26	13 25	vtoclg	$⊢ G \in A \to ((φ \land F \in A \land G \in A) \to (t \in T ⟼ F (t) + G (t)) \in A)$
27	4 26	mpcom	$⊢ (φ \land F \in A \land G \in A) \to (t \in T ⟼ F (t) + G (t)) \in A$

Metamath Proof Explorer

Theorem stoweidlem8

Proof