stoweidlem43

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

	Ref	Expression
Hypotheses	stoweidlem43.1	\|- F/ g ph
	stoweidlem43.2	\|- F/ t ph
	stoweidlem43.3	\|- F/_ h Q
	stoweidlem43.4	\|- K = ( topGen ` ran (,) )
	stoweidlem43.5	\|- Q = { h e. A \| ( ( h ` Z ) = 0 /\ A. t e. T ( 0 <_ ( h ` t ) /\ ( h ` t ) <_ 1 ) ) }
	stoweidlem43.6	\|- T = U. J
	stoweidlem43.7	\|- ( ph -> J e. Comp )
	stoweidlem43.8	\|- ( ph -> A C_ ( J Cn K ) )
	stoweidlem43.9	\|- ( ( ph /\ f e. A /\ l e. A ) -> ( t e. T \|-> ( ( f ` t ) + ( l ` t ) ) ) e. A )
	stoweidlem43.10	\|- ( ( ph /\ f e. A /\ l e. A ) -> ( t e. T \|-> ( ( f ` t ) x. ( l ` t ) ) ) e. A )
	stoweidlem43.11	\|- ( ( ph /\ x e. RR ) -> ( t e. T \|-> x ) e. A )
	stoweidlem43.12	\|- ( ( ph /\ ( r e. T /\ t e. T /\ r =/= t ) ) -> E. g e. A ( g ` r ) =/= ( g ` t ) )
	stoweidlem43.13	\|- ( ph -> U e. J )
	stoweidlem43.14	\|- ( ph -> Z e. U )
	stoweidlem43.15	\|- ( ph -> S e. ( T \ U ) )
Assertion	stoweidlem43	\|- ( ph -> E. h ( h e. Q /\ 0 < ( h ` S ) ) )

Proof

Step	Hyp	Ref	Expression
1		stoweidlem43.1	\|- F/ g ph
2		stoweidlem43.2	\|- F/ t ph
3		stoweidlem43.3	\|- F/_ h Q
4		stoweidlem43.4	\|- K = ( topGen ` ran (,) )
5		stoweidlem43.5	\|- Q = { h e. A \| ( ( h ` Z ) = 0 /\ A. t e. T ( 0 <_ ( h ` t ) /\ ( h ` t ) <_ 1 ) ) }
6		stoweidlem43.6	\|- T = U. J
7		stoweidlem43.7	\|- ( ph -> J e. Comp )
8		stoweidlem43.8	\|- ( ph -> A C_ ( J Cn K ) )
9		stoweidlem43.9	\|- ( ( ph /\ f e. A /\ l e. A ) -> ( t e. T \|-> ( ( f ` t ) + ( l ` t ) ) ) e. A )
10		stoweidlem43.10	\|- ( ( ph /\ f e. A /\ l e. A ) -> ( t e. T \|-> ( ( f ` t ) x. ( l ` t ) ) ) e. A )
11		stoweidlem43.11	\|- ( ( ph /\ x e. RR ) -> ( t e. T \|-> x ) e. A )
12		stoweidlem43.12	\|- ( ( ph /\ ( r e. T /\ t e. T /\ r =/= t ) ) -> E. g e. A ( g ` r ) =/= ( g ` t ) )
13		stoweidlem43.13	\|- ( ph -> U e. J )
14		stoweidlem43.14	\|- ( ph -> Z e. U )
15		stoweidlem43.15	\|- ( ph -> S e. ( T \ U ) )
16		nfv	\|- F/ g E. f ( f e. A /\ ( f ` S ) =/= ( f ` Z ) /\ ( f ` Z ) = 0 )
17	15	eldifad	\|- ( ph -> S e. T )
18		elunii	\|- ( ( Z e. U /\ U e. J ) -> Z e. U. J )
19	14 13 18	syl2anc	\|- ( ph -> Z e. U. J )
20	19 6	eleqtrrdi	\|- ( ph -> Z e. T )
21	15	eldifbd	\|- ( ph -> -. S e. U )
22		nelne2	\|- ( ( Z e. U /\ -. S e. U ) -> Z =/= S )
23	14 21 22	syl2anc	\|- ( ph -> Z =/= S )
24	23	necomd	\|- ( ph -> S =/= Z )
25	17 20 24	3jca	\|- ( ph -> ( S e. T /\ Z e. T /\ S =/= Z ) )
26		simpr2	\|- ( ( ph /\ ( S e. T /\ Z e. T /\ S =/= Z ) ) -> Z e. T )
27		nfv	\|- F/ t ( S e. T /\ Z e. T /\ S =/= Z )
28	2 27	nfan	\|- F/ t ( ph /\ ( S e. T /\ Z e. T /\ S =/= Z ) )
29		nfv	\|- F/ t E. g e. A ( g ` S ) =/= ( g ` Z )
30	28 29	nfim	\|- F/ t ( ( ph /\ ( S e. T /\ Z e. T /\ S =/= Z ) ) -> E. g e. A ( g ` S ) =/= ( g ` Z ) )
31		eleq1	\|- ( t = Z -> ( t e. T <-> Z e. T ) )
32		neeq2	\|- ( t = Z -> ( S =/= t <-> S =/= Z ) )
33	31 32	3anbi23d	\|- ( t = Z -> ( ( S e. T /\ t e. T /\ S =/= t ) <-> ( S e. T /\ Z e. T /\ S =/= Z ) ) )
34	33	anbi2d	\|- ( t = Z -> ( ( ph /\ ( S e. T /\ t e. T /\ S =/= t ) ) <-> ( ph /\ ( S e. T /\ Z e. T /\ S =/= Z ) ) ) )
35		fveq2	\|- ( t = Z -> ( g ` t ) = ( g ` Z ) )
36	35	neeq2d	\|- ( t = Z -> ( ( g ` S ) =/= ( g ` t ) <-> ( g ` S ) =/= ( g ` Z ) ) )
37	36	rexbidv	\|- ( t = Z -> ( E. g e. A ( g ` S ) =/= ( g ` t ) <-> E. g e. A ( g ` S ) =/= ( g ` Z ) ) )
38	34 37	imbi12d	\|- ( t = Z -> ( ( ( ph /\ ( S e. T /\ t e. T /\ S =/= t ) ) -> E. g e. A ( g ` S ) =/= ( g ` t ) ) <-> ( ( ph /\ ( S e. T /\ Z e. T /\ S =/= Z ) ) -> E. g e. A ( g ` S ) =/= ( g ` Z ) ) ) )
39		simpr1	\|- ( ( ph /\ ( S e. T /\ t e. T /\ S =/= t ) ) -> S e. T )
40		eleq1	\|- ( r = S -> ( r e. T <-> S e. T ) )
41		neeq1	\|- ( r = S -> ( r =/= t <-> S =/= t ) )
42	40 41	3anbi13d	\|- ( r = S -> ( ( r e. T /\ t e. T /\ r =/= t ) <-> ( S e. T /\ t e. T /\ S =/= t ) ) )
43	42	anbi2d	\|- ( r = S -> ( ( ph /\ ( r e. T /\ t e. T /\ r =/= t ) ) <-> ( ph /\ ( S e. T /\ t e. T /\ S =/= t ) ) ) )
44		fveq2	\|- ( r = S -> ( g ` r ) = ( g ` S ) )
45	44	neeq1d	\|- ( r = S -> ( ( g ` r ) =/= ( g ` t ) <-> ( g ` S ) =/= ( g ` t ) ) )
46	45	rexbidv	\|- ( r = S -> ( E. g e. A ( g ` r ) =/= ( g ` t ) <-> E. g e. A ( g ` S ) =/= ( g ` t ) ) )
47	43 46	imbi12d	\|- ( r = S -> ( ( ( ph /\ ( r e. T /\ t e. T /\ r =/= t ) ) -> E. g e. A ( g ` r ) =/= ( g ` t ) ) <-> ( ( ph /\ ( S e. T /\ t e. T /\ S =/= t ) ) -> E. g e. A ( g ` S ) =/= ( g ` t ) ) ) )
48	12	a1i	\|- ( r e. T -> ( ( ph /\ ( r e. T /\ t e. T /\ r =/= t ) ) -> E. g e. A ( g ` r ) =/= ( g ` t ) ) )
49	47 48	vtoclga	\|- ( S e. T -> ( ( ph /\ ( S e. T /\ t e. T /\ S =/= t ) ) -> E. g e. A ( g ` S ) =/= ( g ` t ) ) )
50	39 49	mpcom	\|- ( ( ph /\ ( S e. T /\ t e. T /\ S =/= t ) ) -> E. g e. A ( g ` S ) =/= ( g ` t ) )
51	30 38 50	vtoclg1f	\|- ( Z e. T -> ( ( ph /\ ( S e. T /\ Z e. T /\ S =/= Z ) ) -> E. g e. A ( g ` S ) =/= ( g ` Z ) ) )
52	26 51	mpcom	\|- ( ( ph /\ ( S e. T /\ Z e. T /\ S =/= Z ) ) -> E. g e. A ( g ` S ) =/= ( g ` Z ) )
53		df-rex	\|- ( E. g e. A ( g ` S ) =/= ( g ` Z ) <-> E. g ( g e. A /\ ( g ` S ) =/= ( g ` Z ) ) )
54	52 53	sylib	\|- ( ( ph /\ ( S e. T /\ Z e. T /\ S =/= Z ) ) -> E. g ( g e. A /\ ( g ` S ) =/= ( g ` Z ) ) )
55	25 54	mpdan	\|- ( ph -> E. g ( g e. A /\ ( g ` S ) =/= ( g ` Z ) ) )
56		nfv	\|- F/ t ( g e. A /\ ( g ` S ) =/= ( g ` Z ) )
57	2 56	nfan	\|- F/ t ( ph /\ ( g e. A /\ ( g ` S ) =/= ( g ` Z ) ) )
58		nfcv	\|- F/_ t g
59		eqid	\|- ( t e. T \|-> ( ( g ` t ) - ( g ` Z ) ) ) = ( t e. T \|-> ( ( g ` t ) - ( g ` Z ) ) )
60		eqid	\|- ( J Cn K ) = ( J Cn K )
61	8	sselda	\|- ( ( ph /\ f e. A ) -> f e. ( J Cn K ) )
62	4 6 60 61	fcnre	\|- ( ( ph /\ f e. A ) -> f : T --> RR )
63	62	adantlr	\|- ( ( ( ph /\ ( g e. A /\ ( g ` S ) =/= ( g ` Z ) ) ) /\ f e. A ) -> f : T --> RR )
64	9	3adant1r	\|- ( ( ( ph /\ ( g e. A /\ ( g ` S ) =/= ( g ` Z ) ) ) /\ f e. A /\ l e. A ) -> ( t e. T \|-> ( ( f ` t ) + ( l ` t ) ) ) e. A )
65	11	adantlr	\|- ( ( ( ph /\ ( g e. A /\ ( g ` S ) =/= ( g ` Z ) ) ) /\ x e. RR ) -> ( t e. T \|-> x ) e. A )
66	17	adantr	\|- ( ( ph /\ ( g e. A /\ ( g ` S ) =/= ( g ` Z ) ) ) -> S e. T )
67	20	adantr	\|- ( ( ph /\ ( g e. A /\ ( g ` S ) =/= ( g ` Z ) ) ) -> Z e. T )
68		simprl	\|- ( ( ph /\ ( g e. A /\ ( g ` S ) =/= ( g ` Z ) ) ) -> g e. A )
69		simprr	\|- ( ( ph /\ ( g e. A /\ ( g ` S ) =/= ( g ` Z ) ) ) -> ( g ` S ) =/= ( g ` Z ) )
70	57 58 59 63 64 65 66 67 68 69	stoweidlem23	\|- ( ( ph /\ ( g e. A /\ ( g ` S ) =/= ( g ` Z ) ) ) -> ( ( t e. T \|-> ( ( g ` t ) - ( g ` Z ) ) ) e. A /\ ( ( t e. T \|-> ( ( g ` t ) - ( g ` Z ) ) ) ` S ) =/= ( ( t e. T \|-> ( ( g ` t ) - ( g ` Z ) ) ) ` Z ) /\ ( ( t e. T \|-> ( ( g ` t ) - ( g ` Z ) ) ) ` Z ) = 0 ) )
71		eleq1	\|- ( f = ( t e. T \|-> ( ( g ` t ) - ( g ` Z ) ) ) -> ( f e. A <-> ( t e. T \|-> ( ( g ` t ) - ( g ` Z ) ) ) e. A ) )
72		fveq1	\|- ( f = ( t e. T \|-> ( ( g ` t ) - ( g ` Z ) ) ) -> ( f ` S ) = ( ( t e. T \|-> ( ( g ` t ) - ( g ` Z ) ) ) ` S ) )
73		fveq1	\|- ( f = ( t e. T \|-> ( ( g ` t ) - ( g ` Z ) ) ) -> ( f ` Z ) = ( ( t e. T \|-> ( ( g ` t ) - ( g ` Z ) ) ) ` Z ) )
74	72 73	neeq12d	\|- ( f = ( t e. T \|-> ( ( g ` t ) - ( g ` Z ) ) ) -> ( ( f ` S ) =/= ( f ` Z ) <-> ( ( t e. T \|-> ( ( g ` t ) - ( g ` Z ) ) ) ` S ) =/= ( ( t e. T \|-> ( ( g ` t ) - ( g ` Z ) ) ) ` Z ) ) )
75	73	eqeq1d	\|- ( f = ( t e. T \|-> ( ( g ` t ) - ( g ` Z ) ) ) -> ( ( f ` Z ) = 0 <-> ( ( t e. T \|-> ( ( g ` t ) - ( g ` Z ) ) ) ` Z ) = 0 ) )
76	71 74 75	3anbi123d	\|- ( f = ( t e. T \|-> ( ( g ` t ) - ( g ` Z ) ) ) -> ( ( f e. A /\ ( f ` S ) =/= ( f ` Z ) /\ ( f ` Z ) = 0 ) <-> ( ( t e. T \|-> ( ( g ` t ) - ( g ` Z ) ) ) e. A /\ ( ( t e. T \|-> ( ( g ` t ) - ( g ` Z ) ) ) ` S ) =/= ( ( t e. T \|-> ( ( g ` t ) - ( g ` Z ) ) ) ` Z ) /\ ( ( t e. T \|-> ( ( g ` t ) - ( g ` Z ) ) ) ` Z ) = 0 ) ) )
77	76	spcegv	\|- ( ( t e. T \|-> ( ( g ` t ) - ( g ` Z ) ) ) e. A -> ( ( ( t e. T \|-> ( ( g ` t ) - ( g ` Z ) ) ) e. A /\ ( ( t e. T \|-> ( ( g ` t ) - ( g ` Z ) ) ) ` S ) =/= ( ( t e. T \|-> ( ( g ` t ) - ( g ` Z ) ) ) ` Z ) /\ ( ( t e. T \|-> ( ( g ` t ) - ( g ` Z ) ) ) ` Z ) = 0 ) -> E. f ( f e. A /\ ( f ` S ) =/= ( f ` Z ) /\ ( f ` Z ) = 0 ) ) )
78	77	3ad2ant1	\|- ( ( ( t e. T \|-> ( ( g ` t ) - ( g ` Z ) ) ) e. A /\ ( ( t e. T \|-> ( ( g ` t ) - ( g ` Z ) ) ) ` S ) =/= ( ( t e. T \|-> ( ( g ` t ) - ( g ` Z ) ) ) ` Z ) /\ ( ( t e. T \|-> ( ( g ` t ) - ( g ` Z ) ) ) ` Z ) = 0 ) -> ( ( ( t e. T \|-> ( ( g ` t ) - ( g ` Z ) ) ) e. A /\ ( ( t e. T \|-> ( ( g ` t ) - ( g ` Z ) ) ) ` S ) =/= ( ( t e. T \|-> ( ( g ` t ) - ( g ` Z ) ) ) ` Z ) /\ ( ( t e. T \|-> ( ( g ` t ) - ( g ` Z ) ) ) ` Z ) = 0 ) -> E. f ( f e. A /\ ( f ` S ) =/= ( f ` Z ) /\ ( f ` Z ) = 0 ) ) )
79	78	pm2.43i	\|- ( ( ( t e. T \|-> ( ( g ` t ) - ( g ` Z ) ) ) e. A /\ ( ( t e. T \|-> ( ( g ` t ) - ( g ` Z ) ) ) ` S ) =/= ( ( t e. T \|-> ( ( g ` t ) - ( g ` Z ) ) ) ` Z ) /\ ( ( t e. T \|-> ( ( g ` t ) - ( g ` Z ) ) ) ` Z ) = 0 ) -> E. f ( f e. A /\ ( f ` S ) =/= ( f ` Z ) /\ ( f ` Z ) = 0 ) )
80	70 79	syl	\|- ( ( ph /\ ( g e. A /\ ( g ` S ) =/= ( g ` Z ) ) ) -> E. f ( f e. A /\ ( f ` S ) =/= ( f ` Z ) /\ ( f ` Z ) = 0 ) )
81	1 16 55 80	exlimdd	\|- ( ph -> E. f ( f e. A /\ ( f ` S ) =/= ( f ` Z ) /\ ( f ` Z ) = 0 ) )
82		nfmpt1	\|- F/_ t ( t e. T \|-> ( ( ( s e. T \|-> ( ( f ` s ) x. ( f ` s ) ) ) ` t ) / sup ( ran ( s e. T \|-> ( ( f ` s ) x. ( f ` s ) ) ) , RR , < ) ) )
83		nfcv	\|- F/_ t f
84		nfcv	\|- F/_ t ( s e. T \|-> ( ( f ` s ) x. ( f ` s ) ) )
85		nfv	\|- F/ t ( f e. A /\ ( f ` S ) =/= ( f ` Z ) /\ ( f ` Z ) = 0 )
86	2 85	nfan	\|- F/ t ( ph /\ ( f e. A /\ ( f ` S ) =/= ( f ` Z ) /\ ( f ` Z ) = 0 ) )
87		fveq2	\|- ( s = t -> ( f ` s ) = ( f ` t ) )
88	87 87	oveq12d	\|- ( s = t -> ( ( f ` s ) x. ( f ` s ) ) = ( ( f ` t ) x. ( f ` t ) ) )
89	88	cbvmptv	\|- ( s e. T \|-> ( ( f ` s ) x. ( f ` s ) ) ) = ( t e. T \|-> ( ( f ` t ) x. ( f ` t ) ) )
90		eqid	\|- sup ( ran ( s e. T \|-> ( ( f ` s ) x. ( f ` s ) ) ) , RR , < ) = sup ( ran ( s e. T \|-> ( ( f ` s ) x. ( f ` s ) ) ) , RR , < )
91		eqid	\|- ( t e. T \|-> ( ( ( s e. T \|-> ( ( f ` s ) x. ( f ` s ) ) ) ` t ) / sup ( ran ( s e. T \|-> ( ( f ` s ) x. ( f ` s ) ) ) , RR , < ) ) ) = ( t e. T \|-> ( ( ( s e. T \|-> ( ( f ` s ) x. ( f ` s ) ) ) ` t ) / sup ( ran ( s e. T \|-> ( ( f ` s ) x. ( f ` s ) ) ) , RR , < ) ) )
92	7	adantr	\|- ( ( ph /\ ( f e. A /\ ( f ` S ) =/= ( f ` Z ) /\ ( f ` Z ) = 0 ) ) -> J e. Comp )
93	8	adantr	\|- ( ( ph /\ ( f e. A /\ ( f ` S ) =/= ( f ` Z ) /\ ( f ` Z ) = 0 ) ) -> A C_ ( J Cn K ) )
94		eleq1	\|- ( f = k -> ( f e. A <-> k e. A ) )
95	94	3anbi2d	\|- ( f = k -> ( ( ph /\ f e. A /\ l e. A ) <-> ( ph /\ k e. A /\ l e. A ) ) )
96		fveq1	\|- ( f = k -> ( f ` t ) = ( k ` t ) )
97	96	oveq1d	\|- ( f = k -> ( ( f ` t ) x. ( l ` t ) ) = ( ( k ` t ) x. ( l ` t ) ) )
98	97	mpteq2dv	\|- ( f = k -> ( t e. T \|-> ( ( f ` t ) x. ( l ` t ) ) ) = ( t e. T \|-> ( ( k ` t ) x. ( l ` t ) ) ) )
99	98	eleq1d	\|- ( f = k -> ( ( t e. T \|-> ( ( f ` t ) x. ( l ` t ) ) ) e. A <-> ( t e. T \|-> ( ( k ` t ) x. ( l ` t ) ) ) e. A ) )
100	95 99	imbi12d	\|- ( f = k -> ( ( ( ph /\ f e. A /\ l e. A ) -> ( t e. T \|-> ( ( f ` t ) x. ( l ` t ) ) ) e. A ) <-> ( ( ph /\ k e. A /\ l e. A ) -> ( t e. T \|-> ( ( k ` t ) x. ( l ` t ) ) ) e. A ) ) )
101	100 10	chvarvv	\|- ( ( ph /\ k e. A /\ l e. A ) -> ( t e. T \|-> ( ( k ` t ) x. ( l ` t ) ) ) e. A )
102	101	3adant1r	\|- ( ( ( ph /\ ( f e. A /\ ( f ` S ) =/= ( f ` Z ) /\ ( f ` Z ) = 0 ) ) /\ k e. A /\ l e. A ) -> ( t e. T \|-> ( ( k ` t ) x. ( l ` t ) ) ) e. A )
103	11	adantlr	\|- ( ( ( ph /\ ( f e. A /\ ( f ` S ) =/= ( f ` Z ) /\ ( f ` Z ) = 0 ) ) /\ x e. RR ) -> ( t e. T \|-> x ) e. A )
104	17	adantr	\|- ( ( ph /\ ( f e. A /\ ( f ` S ) =/= ( f ` Z ) /\ ( f ` Z ) = 0 ) ) -> S e. T )
105	20	adantr	\|- ( ( ph /\ ( f e. A /\ ( f ` S ) =/= ( f ` Z ) /\ ( f ` Z ) = 0 ) ) -> Z e. T )
106		simpr1	\|- ( ( ph /\ ( f e. A /\ ( f ` S ) =/= ( f ` Z ) /\ ( f ` Z ) = 0 ) ) -> f e. A )
107		simpr2	\|- ( ( ph /\ ( f e. A /\ ( f ` S ) =/= ( f ` Z ) /\ ( f ` Z ) = 0 ) ) -> ( f ` S ) =/= ( f ` Z ) )
108		simpr3	\|- ( ( ph /\ ( f e. A /\ ( f ` S ) =/= ( f ` Z ) /\ ( f ` Z ) = 0 ) ) -> ( f ` Z ) = 0 )
109	3 82 83 84 86 4 5 6 89 90 91 92 93 102 103 104 105 106 107 108	stoweidlem36	\|- ( ( ph /\ ( f e. A /\ ( f ` S ) =/= ( f ` Z ) /\ ( f ` Z ) = 0 ) ) -> E. h ( h e. Q /\ 0 < ( h ` S ) ) )
110	109	ex	\|- ( ph -> ( ( f e. A /\ ( f ` S ) =/= ( f ` Z ) /\ ( f ` Z ) = 0 ) -> E. h ( h e. Q /\ 0 < ( h ` S ) ) ) )
111	110	exlimdv	\|- ( ph -> ( E. f ( f e. A /\ ( f ` S ) =/= ( f ` Z ) /\ ( f ` Z ) = 0 ) -> E. h ( h e. Q /\ 0 < ( h ` S ) ) ) )
112	81 111	mpd	\|- ( ph -> E. h ( h e. Q /\ 0 < ( h ` S ) ) )

Metamath Proof Explorer

Theorem stoweidlem43

Proof