stoweidlem6

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

	Ref	Expression
Hypotheses	stoweidlem6.1	$⊢ Ⅎ t f = F$
	stoweidlem6.2	$⊢ Ⅎ t g = G$
	stoweidlem6.3	$⊢ (φ \land f \in A \land g \in A) \to (t \in T ⟼ f (t) g (t)) \in A$
Assertion	stoweidlem6	$⊢ (φ \land F \in A \land G \in A) \to (t \in T ⟼ F (t) G (t)) \in A$

Proof

Step	Hyp	Ref	Expression
1		stoweidlem6.1	$⊢ Ⅎ t f = F$
2		stoweidlem6.2	$⊢ Ⅎ t g = G$
3		stoweidlem6.3	$⊢ (φ \land f \in A \land g \in A) \to (t \in T ⟼ f (t) g (t)) \in A$
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		fveq1	$⊢ g = G \to g (t) = G (t)$
8	7	oveq2d	$⊢ g = G \to F (t) g (t) = F (t) G (t)$
9	8	adantr	$⊢ (g = G \land t \in T) \to F (t) g (t) = F (t) G (t)$
10	2 9	mpteq2da	$⊢ g = G \to (t \in T ⟼ F (t) g (t)) = (t \in T ⟼ F (t) G (t))$
11	10	eleq1d	$⊢ g = G \to ((t \in T ⟼ F (t) g (t)) \in A \leftrightarrow (t \in T ⟼ F (t) G (t)) \in A)$
12	6 11	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))$
13		simp2	$⊢ (φ \land F \in A \land g \in A) \to F \in A$
14		eleq1	$⊢ f = F \to (f \in A \leftrightarrow F \in A)$
15	14	3anbi2d	$⊢ f = F \to ((φ \land f \in A \land g \in A) \leftrightarrow (φ \land F \in A \land g \in A))$
16		fveq1	$⊢ f = F \to f (t) = F (t)$
17	16	oveq1d	$⊢ f = F \to f (t) g (t) = F (t) g (t)$
18	17	adantr	$⊢ (f = F \land t \in T) \to f (t) g (t) = F (t) g (t)$
19	1 18	mpteq2da	$⊢ f = F \to (t \in T ⟼ f (t) g (t)) = (t \in T ⟼ F (t) g (t))$
20	19	eleq1d	$⊢ f = F \to ((t \in T ⟼ f (t) g (t)) \in A \leftrightarrow (t \in T ⟼ F (t) g (t)) \in A)$
21	15 20	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))$
22	21 3	vtoclg	$⊢ F \in A \to ((φ \land F \in A \land g \in A) \to (t \in T ⟼ F (t) g (t)) \in A)$
23	13 22	mpcom	$⊢ (φ \land F \in A \land g \in A) \to (t \in T ⟼ F (t) g (t)) \in A$
24	12 23	vtoclg	$⊢ G \in A \to ((φ \land F \in A \land G \in A) \to (t \in T ⟼ F (t) G (t)) \in A)$
25	4 24	mpcom	$⊢ (φ \land F \in A \land G \in A) \to (t \in T ⟼ F (t) G (t)) \in A$

Metamath Proof Explorer

Theorem stoweidlem6

Proof