Theorem 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	⊢ Ⅎ 𝑡 𝜑
	stoweidlem22.9	⊢ Ⅎ 𝑡 𝐹
	stoweidlem22.10	⊢ Ⅎ 𝑡 𝐺
	stoweidlem22.1	⊢ 𝐻 = ( 𝑡 ∈ 𝑇 ↦ ( ( 𝐹 ‘ 𝑡 ) − ( 𝐺 ‘ 𝑡 ) ) )
	stoweidlem22.2	⊢ 𝐼 = ( 𝑡 ∈ 𝑇 ↦ - 1 )
	stoweidlem22.3	⊢ 𝐿 = ( 𝑡 ∈ 𝑇 ↦ ( ( 𝐼 ‘ 𝑡 ) · ( 𝐺 ‘ 𝑡 ) ) )
	stoweidlem22.4	⊢ ( ( 𝜑 ∧ 𝑓 ∈ 𝐴 ) → 𝑓 : 𝑇 ⟶ ℝ )
	stoweidlem22.5	⊢ ( ( 𝜑 ∧ 𝑓 ∈ 𝐴 ∧ 𝑔 ∈ 𝐴 ) → ( 𝑡 ∈ 𝑇 ↦ ( ( 𝑓 ‘ 𝑡 ) + ( 𝑔 ‘ 𝑡 ) ) ) ∈ 𝐴 )
	stoweidlem22.6	⊢ ( ( 𝜑 ∧ 𝑓 ∈ 𝐴 ∧ 𝑔 ∈ 𝐴 ) → ( 𝑡 ∈ 𝑇 ↦ ( ( 𝑓 ‘ 𝑡 ) · ( 𝑔 ‘ 𝑡 ) ) ) ∈ 𝐴 )
	stoweidlem22.7	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℝ ) → ( 𝑡 ∈ 𝑇 ↦ 𝑥 ) ∈ 𝐴 )
Assertion	stoweidlem22	⊢ ( ( 𝜑 ∧ 𝐹 ∈ 𝐴 ∧ 𝐺 ∈ 𝐴 ) → ( 𝑡 ∈ 𝑇 ↦ ( ( 𝐹 ‘ 𝑡 ) − ( 𝐺 ‘ 𝑡 ) ) ) ∈ 𝐴 )

Proof

Step	Hyp	Ref	Expression
1		stoweidlem22.8	⊢ Ⅎ 𝑡 𝜑
2		stoweidlem22.9	⊢ Ⅎ 𝑡 𝐹
3		stoweidlem22.10	⊢ Ⅎ 𝑡 𝐺
4		stoweidlem22.1	⊢ 𝐻 = ( 𝑡 ∈ 𝑇 ↦ ( ( 𝐹 ‘ 𝑡 ) − ( 𝐺 ‘ 𝑡 ) ) )
5		stoweidlem22.2	⊢ 𝐼 = ( 𝑡 ∈ 𝑇 ↦ - 1 )
6		stoweidlem22.3	⊢ 𝐿 = ( 𝑡 ∈ 𝑇 ↦ ( ( 𝐼 ‘ 𝑡 ) · ( 𝐺 ‘ 𝑡 ) ) )
7		stoweidlem22.4	⊢ ( ( 𝜑 ∧ 𝑓 ∈ 𝐴 ) → 𝑓 : 𝑇 ⟶ ℝ )
8		stoweidlem22.5	⊢ ( ( 𝜑 ∧ 𝑓 ∈ 𝐴 ∧ 𝑔 ∈ 𝐴 ) → ( 𝑡 ∈ 𝑇 ↦ ( ( 𝑓 ‘ 𝑡 ) + ( 𝑔 ‘ 𝑡 ) ) ) ∈ 𝐴 )
9		stoweidlem22.6	⊢ ( ( 𝜑 ∧ 𝑓 ∈ 𝐴 ∧ 𝑔 ∈ 𝐴 ) → ( 𝑡 ∈ 𝑇 ↦ ( ( 𝑓 ‘ 𝑡 ) · ( 𝑔 ‘ 𝑡 ) ) ) ∈ 𝐴 )
10		stoweidlem22.7	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℝ ) → ( 𝑡 ∈ 𝑇 ↦ 𝑥 ) ∈ 𝐴 )
11	2	nfel1	⊢ Ⅎ 𝑡 𝐹 ∈ 𝐴
12	3	nfel1	⊢ Ⅎ 𝑡 𝐺 ∈ 𝐴
13	1 11 12	nf3an	⊢ Ⅎ 𝑡 ( 𝜑 ∧ 𝐹 ∈ 𝐴 ∧ 𝐺 ∈ 𝐴 )
14		simpr	⊢ ( ( ( 𝜑 ∧ 𝐹 ∈ 𝐴 ∧ 𝐺 ∈ 𝐴 ) ∧ 𝑡 ∈ 𝑇 ) → 𝑡 ∈ 𝑇 )
15		simpl1	⊢ ( ( ( 𝜑 ∧ 𝐹 ∈ 𝐴 ∧ 𝐺 ∈ 𝐴 ) ∧ 𝑡 ∈ 𝑇 ) → 𝜑 )
16		neg1rr	⊢ - 1 ∈ ℝ
17	10	stoweidlem4	⊢ ( ( 𝜑 ∧ - 1 ∈ ℝ ) → ( 𝑡 ∈ 𝑇 ↦ - 1 ) ∈ 𝐴 )
18	16 17	mpan2	⊢ ( 𝜑 → ( 𝑡 ∈ 𝑇 ↦ - 1 ) ∈ 𝐴 )
19	5 18	eqeltrid	⊢ ( 𝜑 → 𝐼 ∈ 𝐴 )
20		eleq1	⊢ ( 𝑓 = 𝐼 → ( 𝑓 ∈ 𝐴 ↔ 𝐼 ∈ 𝐴 ) )
21	20	anbi2d	⊢ ( 𝑓 = 𝐼 → ( ( 𝜑 ∧ 𝑓 ∈ 𝐴 ) ↔ ( 𝜑 ∧ 𝐼 ∈ 𝐴 ) ) )
22		feq1	⊢ ( 𝑓 = 𝐼 → ( 𝑓 : 𝑇 ⟶ ℝ ↔ 𝐼 : 𝑇 ⟶ ℝ ) )
23	21 22	imbi12d	⊢ ( 𝑓 = 𝐼 → ( ( ( 𝜑 ∧ 𝑓 ∈ 𝐴 ) → 𝑓 : 𝑇 ⟶ ℝ ) ↔ ( ( 𝜑 ∧ 𝐼 ∈ 𝐴 ) → 𝐼 : 𝑇 ⟶ ℝ ) ) )
24	23 7	vtoclg	⊢ ( 𝐼 ∈ 𝐴 → ( ( 𝜑 ∧ 𝐼 ∈ 𝐴 ) → 𝐼 : 𝑇 ⟶ ℝ ) )
25	24	anabsi7	⊢ ( ( 𝜑 ∧ 𝐼 ∈ 𝐴 ) → 𝐼 : 𝑇 ⟶ ℝ )
26	15 19 25	syl2anc2	⊢ ( ( ( 𝜑 ∧ 𝐹 ∈ 𝐴 ∧ 𝐺 ∈ 𝐴 ) ∧ 𝑡 ∈ 𝑇 ) → 𝐼 : 𝑇 ⟶ ℝ )
27	26 14	ffvelcdmd	⊢ ( ( ( 𝜑 ∧ 𝐹 ∈ 𝐴 ∧ 𝐺 ∈ 𝐴 ) ∧ 𝑡 ∈ 𝑇 ) → ( 𝐼 ‘ 𝑡 ) ∈ ℝ )
28		simpl3	⊢ ( ( ( 𝜑 ∧ 𝐹 ∈ 𝐴 ∧ 𝐺 ∈ 𝐴 ) ∧ 𝑡 ∈ 𝑇 ) → 𝐺 ∈ 𝐴 )
29		eleq1	⊢ ( 𝑓 = 𝐺 → ( 𝑓 ∈ 𝐴 ↔ 𝐺 ∈ 𝐴 ) )
30	29	anbi2d	⊢ ( 𝑓 = 𝐺 → ( ( 𝜑 ∧ 𝑓 ∈ 𝐴 ) ↔ ( 𝜑 ∧ 𝐺 ∈ 𝐴 ) ) )
31		feq1	⊢ ( 𝑓 = 𝐺 → ( 𝑓 : 𝑇 ⟶ ℝ ↔ 𝐺 : 𝑇 ⟶ ℝ ) )
32	30 31	imbi12d	⊢ ( 𝑓 = 𝐺 → ( ( ( 𝜑 ∧ 𝑓 ∈ 𝐴 ) → 𝑓 : 𝑇 ⟶ ℝ ) ↔ ( ( 𝜑 ∧ 𝐺 ∈ 𝐴 ) → 𝐺 : 𝑇 ⟶ ℝ ) ) )
33	32 7	vtoclg	⊢ ( 𝐺 ∈ 𝐴 → ( ( 𝜑 ∧ 𝐺 ∈ 𝐴 ) → 𝐺 : 𝑇 ⟶ ℝ ) )
34	33	anabsi7	⊢ ( ( 𝜑 ∧ 𝐺 ∈ 𝐴 ) → 𝐺 : 𝑇 ⟶ ℝ )
35	34	3adant3	⊢ ( ( 𝜑 ∧ 𝐺 ∈ 𝐴 ∧ 𝑡 ∈ 𝑇 ) → 𝐺 : 𝑇 ⟶ ℝ )
36		simp3	⊢ ( ( 𝜑 ∧ 𝐺 ∈ 𝐴 ∧ 𝑡 ∈ 𝑇 ) → 𝑡 ∈ 𝑇 )
37	35 36	ffvelcdmd	⊢ ( ( 𝜑 ∧ 𝐺 ∈ 𝐴 ∧ 𝑡 ∈ 𝑇 ) → ( 𝐺 ‘ 𝑡 ) ∈ ℝ )
38	15 28 14 37	syl3anc	⊢ ( ( ( 𝜑 ∧ 𝐹 ∈ 𝐴 ∧ 𝐺 ∈ 𝐴 ) ∧ 𝑡 ∈ 𝑇 ) → ( 𝐺 ‘ 𝑡 ) ∈ ℝ )
39	27 38	remulcld	⊢ ( ( ( 𝜑 ∧ 𝐹 ∈ 𝐴 ∧ 𝐺 ∈ 𝐴 ) ∧ 𝑡 ∈ 𝑇 ) → ( ( 𝐼 ‘ 𝑡 ) · ( 𝐺 ‘ 𝑡 ) ) ∈ ℝ )
40	6	fvmpt2	⊢ ( ( 𝑡 ∈ 𝑇 ∧ ( ( 𝐼 ‘ 𝑡 ) · ( 𝐺 ‘ 𝑡 ) ) ∈ ℝ ) → ( 𝐿 ‘ 𝑡 ) = ( ( 𝐼 ‘ 𝑡 ) · ( 𝐺 ‘ 𝑡 ) ) )
41	14 39 40	syl2anc	⊢ ( ( ( 𝜑 ∧ 𝐹 ∈ 𝐴 ∧ 𝐺 ∈ 𝐴 ) ∧ 𝑡 ∈ 𝑇 ) → ( 𝐿 ‘ 𝑡 ) = ( ( 𝐼 ‘ 𝑡 ) · ( 𝐺 ‘ 𝑡 ) ) )
42	5	fvmpt2	⊢ ( ( 𝑡 ∈ 𝑇 ∧ - 1 ∈ ℝ ) → ( 𝐼 ‘ 𝑡 ) = - 1 )
43	16 42	mpan2	⊢ ( 𝑡 ∈ 𝑇 → ( 𝐼 ‘ 𝑡 ) = - 1 )
44	43	adantl	⊢ ( ( ( 𝜑 ∧ 𝐹 ∈ 𝐴 ∧ 𝐺 ∈ 𝐴 ) ∧ 𝑡 ∈ 𝑇 ) → ( 𝐼 ‘ 𝑡 ) = - 1 )
45	44	oveq1d	⊢ ( ( ( 𝜑 ∧ 𝐹 ∈ 𝐴 ∧ 𝐺 ∈ 𝐴 ) ∧ 𝑡 ∈ 𝑇 ) → ( ( 𝐼 ‘ 𝑡 ) · ( 𝐺 ‘ 𝑡 ) ) = ( - 1 · ( 𝐺 ‘ 𝑡 ) ) )
46	38	recnd	⊢ ( ( ( 𝜑 ∧ 𝐹 ∈ 𝐴 ∧ 𝐺 ∈ 𝐴 ) ∧ 𝑡 ∈ 𝑇 ) → ( 𝐺 ‘ 𝑡 ) ∈ ℂ )
47	46	mulm1d	⊢ ( ( ( 𝜑 ∧ 𝐹 ∈ 𝐴 ∧ 𝐺 ∈ 𝐴 ) ∧ 𝑡 ∈ 𝑇 ) → ( - 1 · ( 𝐺 ‘ 𝑡 ) ) = - ( 𝐺 ‘ 𝑡 ) )
48	41 45 47	3eqtrd	⊢ ( ( ( 𝜑 ∧ 𝐹 ∈ 𝐴 ∧ 𝐺 ∈ 𝐴 ) ∧ 𝑡 ∈ 𝑇 ) → ( 𝐿 ‘ 𝑡 ) = - ( 𝐺 ‘ 𝑡 ) )
49	48	oveq2d	⊢ ( ( ( 𝜑 ∧ 𝐹 ∈ 𝐴 ∧ 𝐺 ∈ 𝐴 ) ∧ 𝑡 ∈ 𝑇 ) → ( ( 𝐹 ‘ 𝑡 ) + ( 𝐿 ‘ 𝑡 ) ) = ( ( 𝐹 ‘ 𝑡 ) + - ( 𝐺 ‘ 𝑡 ) ) )
50		simpl2	⊢ ( ( ( 𝜑 ∧ 𝐹 ∈ 𝐴 ∧ 𝐺 ∈ 𝐴 ) ∧ 𝑡 ∈ 𝑇 ) → 𝐹 ∈ 𝐴 )
51		eleq1	⊢ ( 𝑓 = 𝐹 → ( 𝑓 ∈ 𝐴 ↔ 𝐹 ∈ 𝐴 ) )
52	51	anbi2d	⊢ ( 𝑓 = 𝐹 → ( ( 𝜑 ∧ 𝑓 ∈ 𝐴 ) ↔ ( 𝜑 ∧ 𝐹 ∈ 𝐴 ) ) )
53		feq1	⊢ ( 𝑓 = 𝐹 → ( 𝑓 : 𝑇 ⟶ ℝ ↔ 𝐹 : 𝑇 ⟶ ℝ ) )
54	52 53	imbi12d	⊢ ( 𝑓 = 𝐹 → ( ( ( 𝜑 ∧ 𝑓 ∈ 𝐴 ) → 𝑓 : 𝑇 ⟶ ℝ ) ↔ ( ( 𝜑 ∧ 𝐹 ∈ 𝐴 ) → 𝐹 : 𝑇 ⟶ ℝ ) ) )
55	54 7	vtoclg	⊢ ( 𝐹 ∈ 𝐴 → ( ( 𝜑 ∧ 𝐹 ∈ 𝐴 ) → 𝐹 : 𝑇 ⟶ ℝ ) )
56	55	anabsi7	⊢ ( ( 𝜑 ∧ 𝐹 ∈ 𝐴 ) → 𝐹 : 𝑇 ⟶ ℝ )
57	15 50 56	syl2anc	⊢ ( ( ( 𝜑 ∧ 𝐹 ∈ 𝐴 ∧ 𝐺 ∈ 𝐴 ) ∧ 𝑡 ∈ 𝑇 ) → 𝐹 : 𝑇 ⟶ ℝ )
58	57 14	ffvelcdmd	⊢ ( ( ( 𝜑 ∧ 𝐹 ∈ 𝐴 ∧ 𝐺 ∈ 𝐴 ) ∧ 𝑡 ∈ 𝑇 ) → ( 𝐹 ‘ 𝑡 ) ∈ ℝ )
59	58	recnd	⊢ ( ( ( 𝜑 ∧ 𝐹 ∈ 𝐴 ∧ 𝐺 ∈ 𝐴 ) ∧ 𝑡 ∈ 𝑇 ) → ( 𝐹 ‘ 𝑡 ) ∈ ℂ )
60	59 46	negsubd	⊢ ( ( ( 𝜑 ∧ 𝐹 ∈ 𝐴 ∧ 𝐺 ∈ 𝐴 ) ∧ 𝑡 ∈ 𝑇 ) → ( ( 𝐹 ‘ 𝑡 ) + - ( 𝐺 ‘ 𝑡 ) ) = ( ( 𝐹 ‘ 𝑡 ) − ( 𝐺 ‘ 𝑡 ) ) )
61	49 60	eqtr2d	⊢ ( ( ( 𝜑 ∧ 𝐹 ∈ 𝐴 ∧ 𝐺 ∈ 𝐴 ) ∧ 𝑡 ∈ 𝑇 ) → ( ( 𝐹 ‘ 𝑡 ) − ( 𝐺 ‘ 𝑡 ) ) = ( ( 𝐹 ‘ 𝑡 ) + ( 𝐿 ‘ 𝑡 ) ) )
62	13 61	mpteq2da	⊢ ( ( 𝜑 ∧ 𝐹 ∈ 𝐴 ∧ 𝐺 ∈ 𝐴 ) → ( 𝑡 ∈ 𝑇 ↦ ( ( 𝐹 ‘ 𝑡 ) − ( 𝐺 ‘ 𝑡 ) ) ) = ( 𝑡 ∈ 𝑇 ↦ ( ( 𝐹 ‘ 𝑡 ) + ( 𝐿 ‘ 𝑡 ) ) ) )
63	19	3ad2ant1	⊢ ( ( 𝜑 ∧ 𝐹 ∈ 𝐴 ∧ 𝐺 ∈ 𝐴 ) → 𝐼 ∈ 𝐴 )
64		nfmpt1	⊢ Ⅎ 𝑡 ( 𝑡 ∈ 𝑇 ↦ - 1 )
65	5 64	nfcxfr	⊢ Ⅎ 𝑡 𝐼
66	65	nfeq2	⊢ Ⅎ 𝑡 𝑓 = 𝐼
67	3	nfeq2	⊢ Ⅎ 𝑡 𝑔 = 𝐺
68	66 67 9	stoweidlem6	⊢ ( ( 𝜑 ∧ 𝐼 ∈ 𝐴 ∧ 𝐺 ∈ 𝐴 ) → ( 𝑡 ∈ 𝑇 ↦ ( ( 𝐼 ‘ 𝑡 ) · ( 𝐺 ‘ 𝑡 ) ) ) ∈ 𝐴 )
69	63 68	syld3an2	⊢ ( ( 𝜑 ∧ 𝐹 ∈ 𝐴 ∧ 𝐺 ∈ 𝐴 ) → ( 𝑡 ∈ 𝑇 ↦ ( ( 𝐼 ‘ 𝑡 ) · ( 𝐺 ‘ 𝑡 ) ) ) ∈ 𝐴 )
70	6 69	eqeltrid	⊢ ( ( 𝜑 ∧ 𝐹 ∈ 𝐴 ∧ 𝐺 ∈ 𝐴 ) → 𝐿 ∈ 𝐴 )
71		nfmpt1	⊢ Ⅎ 𝑡 ( 𝑡 ∈ 𝑇 ↦ ( ( 𝐼 ‘ 𝑡 ) · ( 𝐺 ‘ 𝑡 ) ) )
72	6 71	nfcxfr	⊢ Ⅎ 𝑡 𝐿
73	8 2 72	stoweidlem8	⊢ ( ( 𝜑 ∧ 𝐹 ∈ 𝐴 ∧ 𝐿 ∈ 𝐴 ) → ( 𝑡 ∈ 𝑇 ↦ ( ( 𝐹 ‘ 𝑡 ) + ( 𝐿 ‘ 𝑡 ) ) ) ∈ 𝐴 )
74	70 73	syld3an3	⊢ ( ( 𝜑 ∧ 𝐹 ∈ 𝐴 ∧ 𝐺 ∈ 𝐴 ) → ( 𝑡 ∈ 𝑇 ↦ ( ( 𝐹 ‘ 𝑡 ) + ( 𝐿 ‘ 𝑡 ) ) ) ∈ 𝐴 )
75	62 74	eqeltrd	⊢ ( ( 𝜑 ∧ 𝐹 ∈ 𝐴 ∧ 𝐺 ∈ 𝐴 ) → ( 𝑡 ∈ 𝑇 ↦ ( ( 𝐹 ‘ 𝑡 ) − ( 𝐺 ‘ 𝑡 ) ) ) ∈ 𝐴 )