stoweidlem22

Description: If a set of real functions from a common domain is closed under addition, multiplication and it contains constants, then it is closed under subtraction. (Contributed by Glauco Siliprandi, 20-Apr-2017)

	Ref	Expression
Hypotheses	stoweidlem22.8	$⊢ Ⅎ t φ$
	stoweidlem22.9	$⊢ \underline{Ⅎ} t F$
	stoweidlem22.10	$⊢ \underline{Ⅎ} t G$
	stoweidlem22.1	$⊢ H = (t \in T ⟼ F (t) - G (t))$
	stoweidlem22.2	$⊢ I = (t \in T ⟼ - 1)$
	stoweidlem22.3	$⊢ L = (t \in T ⟼ I (t) G (t))$
	stoweidlem22.4	$⊢ (φ \land f \in A) \to f : T ⟶ ℝ$
	stoweidlem22.5	$⊢ (φ \land f \in A \land g \in A) \to (t \in T ⟼ f (t) + g (t)) \in A$
	stoweidlem22.6	$⊢ (φ \land f \in A \land g \in A) \to (t \in T ⟼ f (t) g (t)) \in A$
	stoweidlem22.7	$⊢ (φ \land x \in ℝ) \to (t \in T ⟼ x) \in A$
Assertion	stoweidlem22	$⊢ (φ \land F \in A \land G \in A) \to (t \in T ⟼ F (t) - G (t)) \in A$

Proof

Step	Hyp	Ref	Expression
1		stoweidlem22.8	$⊢ Ⅎ t φ$
2		stoweidlem22.9	$⊢ \underline{Ⅎ} t F$
3		stoweidlem22.10	$⊢ \underline{Ⅎ} t G$
4		stoweidlem22.1	$⊢ H = (t \in T ⟼ F (t) - G (t))$
5		stoweidlem22.2	$⊢ I = (t \in T ⟼ - 1)$
6		stoweidlem22.3	$⊢ L = (t \in T ⟼ I (t) G (t))$
7		stoweidlem22.4	$⊢ (φ \land f \in A) \to f : T ⟶ ℝ$
8		stoweidlem22.5	$⊢ (φ \land f \in A \land g \in A) \to (t \in T ⟼ f (t) + g (t)) \in A$
9		stoweidlem22.6	$⊢ (φ \land f \in A \land g \in A) \to (t \in T ⟼ f (t) g (t)) \in A$
10		stoweidlem22.7	$⊢ (φ \land x \in ℝ) \to (t \in T ⟼ x) \in A$
11	2	nfel1	$⊢ Ⅎ t F \in A$
12	3	nfel1	$⊢ Ⅎ t G \in A$
13	1 11 12	nf3an	$⊢ Ⅎ t (φ \land F \in A \land G \in A)$
14		simpr	$⊢ ((φ \land F \in A \land G \in A) \land t \in T) \to t \in T$
15		simpl1	$⊢ ((φ \land F \in A \land G \in A) \land t \in T) \to φ$
16		neg1rr	$⊢ - 1 \in ℝ$
17	10	stoweidlem4	$⊢ (φ \land - 1 \in ℝ) \to (t \in T ⟼ - 1) \in A$
18	16 17	mpan2	$⊢ φ \to (t \in T ⟼ - 1) \in A$
19	5 18	eqeltrid	$⊢ φ \to I \in A$
20		eleq1	$⊢ f = I \to (f \in A \leftrightarrow I \in A)$
21	20	anbi2d	$⊢ f = I \to ((φ \land f \in A) \leftrightarrow (φ \land I \in A))$
22		feq1	$⊢ f = I \to (f : T ⟶ ℝ \leftrightarrow I : T ⟶ ℝ)$
23	21 22	imbi12d	$⊢ f = I \to (((φ \land f \in A) \to f : T ⟶ ℝ) \leftrightarrow ((φ \land I \in A) \to I : T ⟶ ℝ))$
24	23 7	vtoclg	$⊢ I \in A \to ((φ \land I \in A) \to I : T ⟶ ℝ)$
25	24	anabsi7	$⊢ (φ \land I \in A) \to I : T ⟶ ℝ$
26	15 19 25	syl2anc2	$⊢ ((φ \land F \in A \land G \in A) \land t \in T) \to I : T ⟶ ℝ$
27	26 14	ffvelrnd	$⊢ ((φ \land F \in A \land G \in A) \land t \in T) \to I (t) \in ℝ$
28		simpl3	$⊢ ((φ \land F \in A \land G \in A) \land t \in T) \to G \in A$
29		eleq1	$⊢ f = G \to (f \in A \leftrightarrow G \in A)$
30	29	anbi2d	$⊢ f = G \to ((φ \land f \in A) \leftrightarrow (φ \land G \in A))$
31		feq1	$⊢ f = G \to (f : T ⟶ ℝ \leftrightarrow G : T ⟶ ℝ)$
32	30 31	imbi12d	$⊢ f = G \to (((φ \land f \in A) \to f : T ⟶ ℝ) \leftrightarrow ((φ \land G \in A) \to G : T ⟶ ℝ))$
33	32 7	vtoclg	$⊢ G \in A \to ((φ \land G \in A) \to G : T ⟶ ℝ)$
34	33	anabsi7	$⊢ (φ \land G \in A) \to G : T ⟶ ℝ$
35	34	3adant3	$⊢ (φ \land G \in A \land t \in T) \to G : T ⟶ ℝ$
36		simp3	$⊢ (φ \land G \in A \land t \in T) \to t \in T$
37	35 36	ffvelrnd	$⊢ (φ \land G \in A \land t \in T) \to G (t) \in ℝ$
38	15 28 14 37	syl3anc	$⊢ ((φ \land F \in A \land G \in A) \land t \in T) \to G (t) \in ℝ$
39	27 38	remulcld	$⊢ ((φ \land F \in A \land G \in A) \land t \in T) \to I (t) G (t) \in ℝ$
40	6	fvmpt2	$⊢ (t \in T \land I (t) G (t) \in ℝ) \to L (t) = I (t) G (t)$
41	14 39 40	syl2anc	$⊢ ((φ \land F \in A \land G \in A) \land t \in T) \to L (t) = I (t) G (t)$
42	5	fvmpt2	$⊢ (t \in T \land - 1 \in ℝ) \to I (t) = - 1$
43	16 42	mpan2	$⊢ t \in T \to I (t) = - 1$
44	43	adantl	$⊢ ((φ \land F \in A \land G \in A) \land t \in T) \to I (t) = - 1$
45	44	oveq1d	$⊢ ((φ \land F \in A \land G \in A) \land t \in T) \to I (t) G (t) = -1 G (t)$
46	38	recnd	$⊢ ((φ \land F \in A \land G \in A) \land t \in T) \to G (t) \in ℂ$
47	46	mulm1d	$⊢ ((φ \land F \in A \land G \in A) \land t \in T) \to -1 G (t) = - G (t)$
48	41 45 47	3eqtrd	$⊢ ((φ \land F \in A \land G \in A) \land t \in T) \to L (t) = - G (t)$
49	48	oveq2d	$⊢ ((φ \land F \in A \land G \in A) \land t \in T) \to F (t) + L (t) = F (t) + (- G (t))$
50		simpl2	$⊢ ((φ \land F \in A \land G \in A) \land t \in T) \to F \in A$
51		eleq1	$⊢ f = F \to (f \in A \leftrightarrow F \in A)$
52	51	anbi2d	$⊢ f = F \to ((φ \land f \in A) \leftrightarrow (φ \land F \in A))$
53		feq1	$⊢ f = F \to (f : T ⟶ ℝ \leftrightarrow F : T ⟶ ℝ)$
54	52 53	imbi12d	$⊢ f = F \to (((φ \land f \in A) \to f : T ⟶ ℝ) \leftrightarrow ((φ \land F \in A) \to F : T ⟶ ℝ))$
55	54 7	vtoclg	$⊢ F \in A \to ((φ \land F \in A) \to F : T ⟶ ℝ)$
56	55	anabsi7	$⊢ (φ \land F \in A) \to F : T ⟶ ℝ$
57	15 50 56	syl2anc	$⊢ ((φ \land F \in A \land G \in A) \land t \in T) \to F : T ⟶ ℝ$
58	57 14	ffvelrnd	$⊢ ((φ \land F \in A \land G \in A) \land t \in T) \to F (t) \in ℝ$
59	58	recnd	$⊢ ((φ \land F \in A \land G \in A) \land t \in T) \to F (t) \in ℂ$
60	59 46	negsubd	$⊢ ((φ \land F \in A \land G \in A) \land t \in T) \to F (t) + (- G (t)) = F (t) - G (t)$
61	49 60	eqtr2d	$⊢ ((φ \land F \in A \land G \in A) \land t \in T) \to F (t) - G (t) = F (t) + L (t)$
62	13 61	mpteq2da	$⊢ (φ \land F \in A \land G \in A) \to (t \in T ⟼ F (t) - G (t)) = (t \in T ⟼ F (t) + L (t))$
63	19	3ad2ant1	$⊢ (φ \land F \in A \land G \in A) \to I \in A$
64		nfmpt1	$⊢ \underline{Ⅎ} t (t \in T ⟼ - 1)$
65	5 64	nfcxfr	$⊢ \underline{Ⅎ} t I$
66	65	nfeq2	$⊢ Ⅎ t f = I$
67	3	nfeq2	$⊢ Ⅎ t g = G$
68	66 67 9	stoweidlem6	$⊢ (φ \land I \in A \land G \in A) \to (t \in T ⟼ I (t) G (t)) \in A$
69	63 68	syld3an2	$⊢ (φ \land F \in A \land G \in A) \to (t \in T ⟼ I (t) G (t)) \in A$
70	6 69	eqeltrid	$⊢ (φ \land F \in A \land G \in A) \to L \in A$
71		nfmpt1	$⊢ \underline{Ⅎ} t (t \in T ⟼ I (t) G (t))$
72	6 71	nfcxfr	$⊢ \underline{Ⅎ} t L$
73	8 2 72	stoweidlem8	$⊢ (φ \land F \in A \land L \in A) \to (t \in T ⟼ F (t) + L (t)) \in A$
74	70 73	syld3an3	$⊢ (φ \land F \in A \land G \in A) \to (t \in T ⟼ F (t) + L (t)) \in A$
75	62 74	eqeltrd	$⊢ (φ \land F \in A \land G \in A) \to (t \in T ⟼ F (t) - G (t)) \in A$

Metamath Proof Explorer

Theorem stoweidlem22

Proof