stoweidlem23

Description: This lemma is used to prove the existence of a function p_t as in the beginning of Lemma 1 BrosowskiDeutsh p. 90: for all t in T - U, there exists a function p in the subalgebra, such that p_t ( t_0 ) = 0 , p_t ( t ) > 0, and 0 <= p_t <= 1. (Contributed by Glauco Siliprandi, 20-Apr-2017)

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

Proof

Step	Hyp	Ref	Expression
1		stoweidlem23.1	$⊢ Ⅎ t φ$
2		stoweidlem23.2	$⊢ \underline{Ⅎ} t G$
3		stoweidlem23.3	$⊢ H = (t \in T ⟼ G (t) - G (Z))$
4		stoweidlem23.4	$⊢ (φ \land f \in A) \to f : T ⟶ ℝ$
5		stoweidlem23.5	$⊢ (φ \land f \in A \land g \in A) \to (t \in T ⟼ f (t) + g (t)) \in A$
6		stoweidlem23.6	$⊢ (φ \land x \in ℝ) \to (t \in T ⟼ x) \in A$
7		stoweidlem23.7	$⊢ φ \to S \in T$
8		stoweidlem23.8	$⊢ φ \to Z \in T$
9		stoweidlem23.9	$⊢ φ \to G \in A$
10		stoweidlem23.10	$⊢ φ \to G (S) \neq G (Z)$
11	9	ancli	$⊢ φ \to (φ \land G \in A)$
12		eleq1	$⊢ f = G \to (f \in A \leftrightarrow G \in A)$
13	12	anbi2d	$⊢ f = G \to ((φ \land f \in A) \leftrightarrow (φ \land G \in A))$
14		feq1	$⊢ f = G \to (f : T ⟶ ℝ \leftrightarrow G : T ⟶ ℝ)$
15	13 14	imbi12d	$⊢ f = G \to (((φ \land f \in A) \to f : T ⟶ ℝ) \leftrightarrow ((φ \land G \in A) \to G : T ⟶ ℝ))$
16	15 4	vtoclg	$⊢ G \in A \to ((φ \land G \in A) \to G : T ⟶ ℝ)$
17	9 11 16	sylc	$⊢ φ \to G : T ⟶ ℝ$
18	17	ffvelrnda	$⊢ (φ \land t \in T) \to G (t) \in ℝ$
19	18	recnd	$⊢ (φ \land t \in T) \to G (t) \in ℂ$
20	17 8	ffvelrnd	$⊢ φ \to G (Z) \in ℝ$
21	20	adantr	$⊢ (φ \land t \in T) \to G (Z) \in ℝ$
22	21	recnd	$⊢ (φ \land t \in T) \to G (Z) \in ℂ$
23	19 22	negsubd	$⊢ (φ \land t \in T) \to G (t) + (- G (Z)) = G (t) - G (Z)$
24	1 23	mpteq2da	$⊢ φ \to (t \in T ⟼ G (t) + (- G (Z))) = (t \in T ⟼ G (t) - G (Z))$
25		simpr	$⊢ (φ \land t \in T) \to t \in T$
26	20	renegcld	$⊢ φ \to - G (Z) \in ℝ$
27	26	adantr	$⊢ (φ \land t \in T) \to - G (Z) \in ℝ$
28		eqid	$⊢ (t \in T ⟼ - G (Z)) = (t \in T ⟼ - G (Z))$
29	28	fvmpt2	$⊢ (t \in T \land - G (Z) \in ℝ) \to (t \in T ⟼ - G (Z)) (t) = - G (Z)$
30	25 27 29	syl2anc	$⊢ (φ \land t \in T) \to (t \in T ⟼ - G (Z)) (t) = - G (Z)$
31	30	oveq2d	$⊢ (φ \land t \in T) \to G (t) + (t \in T ⟼ - G (Z)) (t) = G (t) + (- G (Z))$
32	1 31	mpteq2da	$⊢ φ \to (t \in T ⟼ G (t) + (t \in T ⟼ - G (Z)) (t)) = (t \in T ⟼ G (t) + (- G (Z)))$
33	26	ancli	$⊢ φ \to (φ \land - G (Z) \in ℝ)$
34		eleq1	$⊢ x = - G (Z) \to (x \in ℝ \leftrightarrow - G (Z) \in ℝ)$
35	34	anbi2d	$⊢ x = - G (Z) \to ((φ \land x \in ℝ) \leftrightarrow (φ \land - G (Z) \in ℝ))$
36		nfcv	$⊢ \underline{Ⅎ} t Z$
37	2 36	nffv	$⊢ \underline{Ⅎ} t G (Z)$
38	37	nfneg	$⊢ \underline{Ⅎ} t (- G (Z))$
39	38	nfeq2	$⊢ Ⅎ t x = - G (Z)$
40		simpl	$⊢ (x = - G (Z) \land t \in T) \to x = - G (Z)$
41	39 40	mpteq2da	$⊢ x = - G (Z) \to (t \in T ⟼ x) = (t \in T ⟼ - G (Z))$
42	41	eleq1d	$⊢ x = - G (Z) \to ((t \in T ⟼ x) \in A \leftrightarrow (t \in T ⟼ - G (Z)) \in A)$
43	35 42	imbi12d	$⊢ x = - G (Z) \to (((φ \land x \in ℝ) \to (t \in T ⟼ x) \in A) \leftrightarrow ((φ \land - G (Z) \in ℝ) \to (t \in T ⟼ - G (Z)) \in A))$
44	43 6	vtoclg	$⊢ - G (Z) \in ℝ \to ((φ \land - G (Z) \in ℝ) \to (t \in T ⟼ - G (Z)) \in A)$
45	26 33 44	sylc	$⊢ φ \to (t \in T ⟼ - G (Z)) \in A$
46		nfmpt1	$⊢ \underline{Ⅎ} t (t \in T ⟼ - G (Z))$
47	5 2 46	stoweidlem8	$⊢ (φ \land G \in A \land (t \in T ⟼ - G (Z)) \in A) \to (t \in T ⟼ G (t) + (t \in T ⟼ - G (Z)) (t)) \in A$
48	9 45 47	mpd3an23	$⊢ φ \to (t \in T ⟼ G (t) + (t \in T ⟼ - G (Z)) (t)) \in A$
49	32 48	eqeltrrd	$⊢ φ \to (t \in T ⟼ G (t) + (- G (Z))) \in A$
50	24 49	eqeltrrd	$⊢ φ \to (t \in T ⟼ G (t) - G (Z)) \in A$
51	3 50	eqeltrid	$⊢ φ \to H \in A$
52	17 7	ffvelrnd	$⊢ φ \to G (S) \in ℝ$
53	52	recnd	$⊢ φ \to G (S) \in ℂ$
54	20	recnd	$⊢ φ \to G (Z) \in ℂ$
55	53 54 10	subne0d	$⊢ φ \to G (S) - G (Z) \neq 0$
56	52 20	resubcld	$⊢ φ \to G (S) - G (Z) \in ℝ$
57		nfcv	$⊢ \underline{Ⅎ} t S$
58	2 57	nffv	$⊢ \underline{Ⅎ} t G (S)$
59		nfcv	$⊢ \underline{Ⅎ} t -$
60	58 59 37	nfov	$⊢ \underline{Ⅎ} t (G (S) - G (Z))$
61		fveq2	$⊢ t = S \to G (t) = G (S)$
62	61	oveq1d	$⊢ t = S \to G (t) - G (Z) = G (S) - G (Z)$
63	57 60 62 3	fvmptf	$⊢ (S \in T \land G (S) - G (Z) \in ℝ) \to H (S) = G (S) - G (Z)$
64	7 56 63	syl2anc	$⊢ φ \to H (S) = G (S) - G (Z)$
65	20 20	resubcld	$⊢ φ \to G (Z) - G (Z) \in ℝ$
66	37 59 37	nfov	$⊢ \underline{Ⅎ} t (G (Z) - G (Z))$
67		fveq2	$⊢ t = Z \to G (t) = G (Z)$
68	67	oveq1d	$⊢ t = Z \to G (t) - G (Z) = G (Z) - G (Z)$
69	36 66 68 3	fvmptf	$⊢ (Z \in T \land G (Z) - G (Z) \in ℝ) \to H (Z) = G (Z) - G (Z)$
70	8 65 69	syl2anc	$⊢ φ \to H (Z) = G (Z) - G (Z)$
71	54	subidd	$⊢ φ \to G (Z) - G (Z) = 0$
72	70 71	eqtrd	$⊢ φ \to H (Z) = 0$
73	55 64 72	3netr4d	$⊢ φ \to H (S) \neq H (Z)$
74	51 73 72	3jca	$⊢ φ \to (H \in A \land H (S) \neq H (Z) \land H (Z) = 0)$

Metamath Proof Explorer

Theorem stoweidlem23

Proof