stoweidlem55

Description: This lemma proves the existence of a function p as in the proof of Lemma 1 in BrosowskiDeutsh p. 90: p is in the subalgebra, such that 0 <= p <= 1, p__(t_0) = 0, and p > 0 on T - U. Here Z is used to represent t_0 in the paper. (Contributed by Glauco Siliprandi, 20-Apr-2017)

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

Proof

Step	Hyp	Ref	Expression
1		stoweidlem55.1	\|- F/_ t U
2		stoweidlem55.2	\|- F/ t ph
3		stoweidlem55.3	\|- K = ( topGen ` ran (,) )
4		stoweidlem55.4	\|- ( ph -> J e. Comp )
5		stoweidlem55.5	\|- T = U. J
6		stoweidlem55.6	\|- C = ( J Cn K )
7		stoweidlem55.7	\|- ( ph -> A C_ C )
8		stoweidlem55.8	\|- ( ( ph /\ f e. A /\ g e. A ) -> ( t e. T \|-> ( ( f ` t ) + ( g ` t ) ) ) e. A )
9		stoweidlem55.9	\|- ( ( ph /\ f e. A /\ g e. A ) -> ( t e. T \|-> ( ( f ` t ) x. ( g ` t ) ) ) e. A )
10		stoweidlem55.10	\|- ( ( ph /\ x e. RR ) -> ( t e. T \|-> x ) e. A )
11		stoweidlem55.11	\|- ( ( ph /\ ( r e. T /\ t e. T /\ r =/= t ) ) -> E. q e. A ( q ` r ) =/= ( q ` t ) )
12		stoweidlem55.12	\|- ( ph -> U e. J )
13		stoweidlem55.13	\|- ( ph -> Z e. U )
14		stoweidlem55.14	\|- Q = { h e. A \| ( ( h ` Z ) = 0 /\ A. t e. T ( 0 <_ ( h ` t ) /\ ( h ` t ) <_ 1 ) ) }
15		stoweidlem55.15	\|- W = { w e. J \| E. h e. Q w = { t e. T \| 0 < ( h ` t ) } }
16		0re	\|- 0 e. RR
17	10	stoweidlem4	\|- ( ( ph /\ 0 e. RR ) -> ( t e. T \|-> 0 ) e. A )
18	16 17	mpan2	\|- ( ph -> ( t e. T \|-> 0 ) e. A )
19	18	adantr	\|- ( ( ph /\ ( T \ U ) = (/) ) -> ( t e. T \|-> 0 ) e. A )
20		nfcv	\|- F/_ t T
21	20 1	nfdif	\|- F/_ t ( T \ U )
22		nfcv	\|- F/_ t (/)
23	21 22	nfeq	\|- F/ t ( T \ U ) = (/)
24	2 23	nfan	\|- F/ t ( ph /\ ( T \ U ) = (/) )
25		0le0	\|- 0 <_ 0
26		0cn	\|- 0 e. CC
27		eqid	\|- ( t e. T \|-> 0 ) = ( t e. T \|-> 0 )
28	27	fvmpt2	\|- ( ( t e. T /\ 0 e. CC ) -> ( ( t e. T \|-> 0 ) ` t ) = 0 )
29	26 28	mpan2	\|- ( t e. T -> ( ( t e. T \|-> 0 ) ` t ) = 0 )
30	25 29	breqtrrid	\|- ( t e. T -> 0 <_ ( ( t e. T \|-> 0 ) ` t ) )
31	30	adantl	\|- ( ( ( ph /\ ( T \ U ) = (/) ) /\ t e. T ) -> 0 <_ ( ( t e. T \|-> 0 ) ` t ) )
32		0le1	\|- 0 <_ 1
33	29 32	eqbrtrdi	\|- ( t e. T -> ( ( t e. T \|-> 0 ) ` t ) <_ 1 )
34	33	adantl	\|- ( ( ( ph /\ ( T \ U ) = (/) ) /\ t e. T ) -> ( ( t e. T \|-> 0 ) ` t ) <_ 1 )
35	31 34	jca	\|- ( ( ( ph /\ ( T \ U ) = (/) ) /\ t e. T ) -> ( 0 <_ ( ( t e. T \|-> 0 ) ` t ) /\ ( ( t e. T \|-> 0 ) ` t ) <_ 1 ) )
36	35	ex	\|- ( ( ph /\ ( T \ U ) = (/) ) -> ( t e. T -> ( 0 <_ ( ( t e. T \|-> 0 ) ` t ) /\ ( ( t e. T \|-> 0 ) ` t ) <_ 1 ) ) )
37	24 36	ralrimi	\|- ( ( ph /\ ( T \ U ) = (/) ) -> A. t e. T ( 0 <_ ( ( t e. T \|-> 0 ) ` t ) /\ ( ( t e. T \|-> 0 ) ` t ) <_ 1 ) )
38	13 12	jca	\|- ( ph -> ( Z e. U /\ U e. J ) )
39		elunii	\|- ( ( Z e. U /\ U e. J ) -> Z e. U. J )
40	39 5	eleqtrrdi	\|- ( ( Z e. U /\ U e. J ) -> Z e. T )
41		eqidd	\|- ( t = Z -> 0 = 0 )
42		c0ex	\|- 0 e. _V
43	41 27 42	fvmpt	\|- ( Z e. T -> ( ( t e. T \|-> 0 ) ` Z ) = 0 )
44	38 40 43	3syl	\|- ( ph -> ( ( t e. T \|-> 0 ) ` Z ) = 0 )
45	44	adantr	\|- ( ( ph /\ ( T \ U ) = (/) ) -> ( ( t e. T \|-> 0 ) ` Z ) = 0 )
46	23	rzalf	\|- ( ( T \ U ) = (/) -> A. t e. ( T \ U ) 0 < ( ( t e. T \|-> 0 ) ` t ) )
47	46	adantl	\|- ( ( ph /\ ( T \ U ) = (/) ) -> A. t e. ( T \ U ) 0 < ( ( t e. T \|-> 0 ) ` t ) )
48		nfcv	\|- F/_ t p
49		nfmpt1	\|- F/_ t ( t e. T \|-> 0 )
50	48 49	nfeq	\|- F/ t p = ( t e. T \|-> 0 )
51		fveq1	\|- ( p = ( t e. T \|-> 0 ) -> ( p ` t ) = ( ( t e. T \|-> 0 ) ` t ) )
52	51	breq2d	\|- ( p = ( t e. T \|-> 0 ) -> ( 0 <_ ( p ` t ) <-> 0 <_ ( ( t e. T \|-> 0 ) ` t ) ) )
53	51	breq1d	\|- ( p = ( t e. T \|-> 0 ) -> ( ( p ` t ) <_ 1 <-> ( ( t e. T \|-> 0 ) ` t ) <_ 1 ) )
54	52 53	anbi12d	\|- ( p = ( t e. T \|-> 0 ) -> ( ( 0 <_ ( p ` t ) /\ ( p ` t ) <_ 1 ) <-> ( 0 <_ ( ( t e. T \|-> 0 ) ` t ) /\ ( ( t e. T \|-> 0 ) ` t ) <_ 1 ) ) )
55	50 54	ralbid	\|- ( p = ( t e. T \|-> 0 ) -> ( A. t e. T ( 0 <_ ( p ` t ) /\ ( p ` t ) <_ 1 ) <-> A. t e. T ( 0 <_ ( ( t e. T \|-> 0 ) ` t ) /\ ( ( t e. T \|-> 0 ) ` t ) <_ 1 ) ) )
56		fveq1	\|- ( p = ( t e. T \|-> 0 ) -> ( p ` Z ) = ( ( t e. T \|-> 0 ) ` Z ) )
57	56	eqeq1d	\|- ( p = ( t e. T \|-> 0 ) -> ( ( p ` Z ) = 0 <-> ( ( t e. T \|-> 0 ) ` Z ) = 0 ) )
58	51	breq2d	\|- ( p = ( t e. T \|-> 0 ) -> ( 0 < ( p ` t ) <-> 0 < ( ( t e. T \|-> 0 ) ` t ) ) )
59	50 58	ralbid	\|- ( p = ( t e. T \|-> 0 ) -> ( A. t e. ( T \ U ) 0 < ( p ` t ) <-> A. t e. ( T \ U ) 0 < ( ( t e. T \|-> 0 ) ` t ) ) )
60	55 57 59	3anbi123d	\|- ( p = ( t e. T \|-> 0 ) -> ( ( A. t e. T ( 0 <_ ( p ` t ) /\ ( p ` t ) <_ 1 ) /\ ( p ` Z ) = 0 /\ A. t e. ( T \ U ) 0 < ( p ` t ) ) <-> ( A. t e. T ( 0 <_ ( ( t e. T \|-> 0 ) ` t ) /\ ( ( t e. T \|-> 0 ) ` t ) <_ 1 ) /\ ( ( t e. T \|-> 0 ) ` Z ) = 0 /\ A. t e. ( T \ U ) 0 < ( ( t e. T \|-> 0 ) ` t ) ) ) )
61	60	rspcev	\|- ( ( ( t e. T \|-> 0 ) e. A /\ ( A. t e. T ( 0 <_ ( ( t e. T \|-> 0 ) ` t ) /\ ( ( t e. T \|-> 0 ) ` t ) <_ 1 ) /\ ( ( t e. T \|-> 0 ) ` Z ) = 0 /\ A. t e. ( T \ U ) 0 < ( ( t e. T \|-> 0 ) ` t ) ) ) -> E. p e. A ( A. t e. T ( 0 <_ ( p ` t ) /\ ( p ` t ) <_ 1 ) /\ ( p ` Z ) = 0 /\ A. t e. ( T \ U ) 0 < ( p ` t ) ) )
62	19 37 45 47 61	syl13anc	\|- ( ( ph /\ ( T \ U ) = (/) ) -> E. p e. A ( A. t e. T ( 0 <_ ( p ` t ) /\ ( p ` t ) <_ 1 ) /\ ( p ` Z ) = 0 /\ A. t e. ( T \ U ) 0 < ( p ` t ) ) )
63	23	nfn	\|- F/ t -. ( T \ U ) = (/)
64	2 63	nfan	\|- F/ t ( ph /\ -. ( T \ U ) = (/) )
65	4	adantr	\|- ( ( ph /\ -. ( T \ U ) = (/) ) -> J e. Comp )
66	7	adantr	\|- ( ( ph /\ -. ( T \ U ) = (/) ) -> A C_ C )
67	8	3adant1r	\|- ( ( ( ph /\ -. ( T \ U ) = (/) ) /\ f e. A /\ g e. A ) -> ( t e. T \|-> ( ( f ` t ) + ( g ` t ) ) ) e. A )
68	9	3adant1r	\|- ( ( ( ph /\ -. ( T \ U ) = (/) ) /\ f e. A /\ g e. A ) -> ( t e. T \|-> ( ( f ` t ) x. ( g ` t ) ) ) e. A )
69	10	adantlr	\|- ( ( ( ph /\ -. ( T \ U ) = (/) ) /\ x e. RR ) -> ( t e. T \|-> x ) e. A )
70	11	adantlr	\|- ( ( ( ph /\ -. ( T \ U ) = (/) ) /\ ( r e. T /\ t e. T /\ r =/= t ) ) -> E. q e. A ( q ` r ) =/= ( q ` t ) )
71	12	adantr	\|- ( ( ph /\ -. ( T \ U ) = (/) ) -> U e. J )
72		neqne	\|- ( -. ( T \ U ) = (/) -> ( T \ U ) =/= (/) )
73	72	adantl	\|- ( ( ph /\ -. ( T \ U ) = (/) ) -> ( T \ U ) =/= (/) )
74	13	adantr	\|- ( ( ph /\ -. ( T \ U ) = (/) ) -> Z e. U )
75	1 64 3 14 15 5 6 65 66 67 68 69 70 71 73 74	stoweidlem53	\|- ( ( ph /\ -. ( T \ U ) = (/) ) -> E. p e. A ( A. t e. T ( 0 <_ ( p ` t ) /\ ( p ` t ) <_ 1 ) /\ ( p ` Z ) = 0 /\ A. t e. ( T \ U ) 0 < ( p ` t ) ) )
76	62 75	pm2.61dan	\|- ( ph -> E. p e. A ( A. t e. T ( 0 <_ ( p ` t ) /\ ( p ` t ) <_ 1 ) /\ ( p ` Z ) = 0 /\ A. t e. ( T \ U ) 0 < ( p ` t ) ) )

Metamath Proof Explorer

Theorem stoweidlem55

Proof