supminfxr2

Description: The extended real suprema of a set of extended reals is the extended real negative of the extended real infima of that set's image under extended real negation. (Contributed by Glauco Siliprandi, 2-Jan-2022)

		Ref	Expression
	Hypothesis	supminfxr2.1	\|- ( ph -> A C_ RR* )
	Assertion	supminfxr2	\|- ( ph -> sup ( A , RR* , < ) = -e inf ( { x e. RR* \| -e x e. A } , RR* , < ) )

Proof

Step	Hyp	Ref	Expression
1		supminfxr2.1	\|- ( ph -> A C_ RR* )
2		xnegmnf	\|- -e -oo = +oo
3	2	eqcomi	\|- +oo = -e -oo
4	3	a1i	\|- ( ( ph /\ +oo e. A ) -> +oo = -e -oo )
5		supxrpnf	\|- ( ( A C_ RR* /\ +oo e. A ) -> sup ( A , RR* , < ) = +oo )
6	1 5	sylan	\|- ( ( ph /\ +oo e. A ) -> sup ( A , RR* , < ) = +oo )
7		ssrab2	\|- { y e. RR* \| -e y e. A } C_ RR*
8	7	a1i	\|- ( +oo e. A -> { y e. RR* \| -e y e. A } C_ RR* )
9		xnegeq	\|- ( y = -oo -> -e y = -e -oo )
10	2	a1i	\|- ( y = -oo -> -e -oo = +oo )
11	9 10	eqtrd	\|- ( y = -oo -> -e y = +oo )
12	11	eleq1d	\|- ( y = -oo -> ( -e y e. A <-> +oo e. A ) )
13		mnfxr	\|- -oo e. RR*
14	13	a1i	\|- ( +oo e. A -> -oo e. RR* )
15		id	\|- ( +oo e. A -> +oo e. A )
16	12 14 15	elrabd	\|- ( +oo e. A -> -oo e. { y e. RR* \| -e y e. A } )
17		infxrmnf	\|- ( ( { y e. RR* \| -e y e. A } C_ RR* /\ -oo e. { y e. RR* \| -e y e. A } ) -> inf ( { y e. RR* \| -e y e. A } , RR* , < ) = -oo )
18	8 16 17	syl2anc	\|- ( +oo e. A -> inf ( { y e. RR* \| -e y e. A } , RR* , < ) = -oo )
19	18	adantl	\|- ( ( ph /\ +oo e. A ) -> inf ( { y e. RR* \| -e y e. A } , RR* , < ) = -oo )
20	19	xnegeqd	\|- ( ( ph /\ +oo e. A ) -> -e inf ( { y e. RR* \| -e y e. A } , RR* , < ) = -e -oo )
21	4 6 20	3eqtr4d	\|- ( ( ph /\ +oo e. A ) -> sup ( A , RR* , < ) = -e inf ( { y e. RR* \| -e y e. A } , RR* , < ) )
22	1	ssdifssd	\|- ( ph -> ( A \ { -oo } ) C_ RR* )
23	22	adantr	\|- ( ( ph /\ -. +oo e. A ) -> ( A \ { -oo } ) C_ RR* )
24		difssd	\|- ( -. +oo e. A -> ( A \ { -oo } ) C_ A )
25		id	\|- ( -. +oo e. A -> -. +oo e. A )
26		ssnel	\|- ( ( ( A \ { -oo } ) C_ A /\ -. +oo e. A ) -> -. +oo e. ( A \ { -oo } ) )
27	24 25 26	syl2anc	\|- ( -. +oo e. A -> -. +oo e. ( A \ { -oo } ) )
28	27	adantl	\|- ( ( ph /\ -. +oo e. A ) -> -. +oo e. ( A \ { -oo } ) )
29		neldifsnd	\|- ( ( ph /\ -. +oo e. A ) -> -. -oo e. ( A \ { -oo } ) )
30	23 28 29	xrssre	\|- ( ( ph /\ -. +oo e. A ) -> ( A \ { -oo } ) C_ RR )
31	30	supminfxr	\|- ( ( ph /\ -. +oo e. A ) -> sup ( ( A \ { -oo } ) , RR* , < ) = -e inf ( { y e. RR \| -u y e. ( A \ { -oo } ) } , RR* , < ) )
32		supxrmnf2	\|- ( A C_ RR* -> sup ( ( A \ { -oo } ) , RR* , < ) = sup ( A , RR* , < ) )
33	1 32	syl	\|- ( ph -> sup ( ( A \ { -oo } ) , RR* , < ) = sup ( A , RR* , < ) )
34	33	eqcomd	\|- ( ph -> sup ( A , RR* , < ) = sup ( ( A \ { -oo } ) , RR* , < ) )
35	34	adantr	\|- ( ( ph /\ -. +oo e. A ) -> sup ( A , RR* , < ) = sup ( ( A \ { -oo } ) , RR* , < ) )
36		rexr	\|- ( y e. RR -> y e. RR* )
37	36	adantr	\|- ( ( y e. RR /\ -u y e. ( A \ { -oo } ) ) -> y e. RR* )
38		simpl	\|- ( ( y e. RR /\ -u y e. ( A \ { -oo } ) ) -> y e. RR )
39	38	rexnegd	\|- ( ( y e. RR /\ -u y e. ( A \ { -oo } ) ) -> -e y = -u y )
40		eldifi	\|- ( -u y e. ( A \ { -oo } ) -> -u y e. A )
41	40	adantl	\|- ( ( y e. RR /\ -u y e. ( A \ { -oo } ) ) -> -u y e. A )
42	39 41	eqeltrd	\|- ( ( y e. RR /\ -u y e. ( A \ { -oo } ) ) -> -e y e. A )
43	37 42	jca	\|- ( ( y e. RR /\ -u y e. ( A \ { -oo } ) ) -> ( y e. RR* /\ -e y e. A ) )
44		rabid	\|- ( y e. { y e. RR* \| -e y e. A } <-> ( y e. RR* /\ -e y e. A ) )
45	43 44	sylibr	\|- ( ( y e. RR /\ -u y e. ( A \ { -oo } ) ) -> y e. { y e. RR* \| -e y e. A } )
46		renepnf	\|- ( y e. RR -> y =/= +oo )
47		elsni	\|- ( y e. { +oo } -> y = +oo )
48	47	necon3ai	\|- ( y =/= +oo -> -. y e. { +oo } )
49	46 48	syl	\|- ( y e. RR -> -. y e. { +oo } )
50	38 49	syl	\|- ( ( y e. RR /\ -u y e. ( A \ { -oo } ) ) -> -. y e. { +oo } )
51	45 50	eldifd	\|- ( ( y e. RR /\ -u y e. ( A \ { -oo } ) ) -> y e. ( { y e. RR* \| -e y e. A } \ { +oo } ) )
52	51	ex	\|- ( y e. RR -> ( -u y e. ( A \ { -oo } ) -> y e. ( { y e. RR* \| -e y e. A } \ { +oo } ) ) )
53	52	rgen	\|- A. y e. RR ( -u y e. ( A \ { -oo } ) -> y e. ( { y e. RR* \| -e y e. A } \ { +oo } ) )
54	53	a1i	\|- ( -. +oo e. A -> A. y e. RR ( -u y e. ( A \ { -oo } ) -> y e. ( { y e. RR* \| -e y e. A } \ { +oo } ) ) )
55		nfrab1	\|- F/_ y { y e. RR* \| -e y e. A }
56		nfcv	\|- F/_ y { +oo }
57	55 56	nfdif	\|- F/_ y ( { y e. RR* \| -e y e. A } \ { +oo } )
58	57	rabssf	\|- ( { y e. RR \| -u y e. ( A \ { -oo } ) } C_ ( { y e. RR* \| -e y e. A } \ { +oo } ) <-> A. y e. RR ( -u y e. ( A \ { -oo } ) -> y e. ( { y e. RR* \| -e y e. A } \ { +oo } ) ) )
59	54 58	sylibr	\|- ( -. +oo e. A -> { y e. RR \| -u y e. ( A \ { -oo } ) } C_ ( { y e. RR* \| -e y e. A } \ { +oo } ) )
60		nfv	\|- F/ y -. +oo e. A
61		nfcv	\|- F/_ y RR
62		eldifi	\|- ( y e. ( { y e. RR* \| -e y e. A } \ { +oo } ) -> y e. { y e. RR* \| -e y e. A } )
63	7 62	sselid	\|- ( y e. ( { y e. RR* \| -e y e. A } \ { +oo } ) -> y e. RR* )
64	63	adantl	\|- ( ( -. +oo e. A /\ y e. ( { y e. RR* \| -e y e. A } \ { +oo } ) ) -> y e. RR* )
65	44	simprbi	\|- ( y e. { y e. RR* \| -e y e. A } -> -e y e. A )
66	62 65	syl	\|- ( y e. ( { y e. RR* \| -e y e. A } \ { +oo } ) -> -e y e. A )
67	12	biimpac	\|- ( ( -e y e. A /\ y = -oo ) -> +oo e. A )
68	67	adantll	\|- ( ( ( -. +oo e. A /\ -e y e. A ) /\ y = -oo ) -> +oo e. A )
69		simpll	\|- ( ( ( -. +oo e. A /\ -e y e. A ) /\ y = -oo ) -> -. +oo e. A )
70	68 69	pm2.65da	\|- ( ( -. +oo e. A /\ -e y e. A ) -> -. y = -oo )
71	70	neqned	\|- ( ( -. +oo e. A /\ -e y e. A ) -> y =/= -oo )
72	66 71	sylan2	\|- ( ( -. +oo e. A /\ y e. ( { y e. RR* \| -e y e. A } \ { +oo } ) ) -> y =/= -oo )
73		eldifsni	\|- ( y e. ( { y e. RR* \| -e y e. A } \ { +oo } ) -> y =/= +oo )
74	73	adantl	\|- ( ( -. +oo e. A /\ y e. ( { y e. RR* \| -e y e. A } \ { +oo } ) ) -> y =/= +oo )
75	64 72 74	xrred	\|- ( ( -. +oo e. A /\ y e. ( { y e. RR* \| -e y e. A } \ { +oo } ) ) -> y e. RR )
76	60 57 61 75	ssdf2	\|- ( -. +oo e. A -> ( { y e. RR* \| -e y e. A } \ { +oo } ) C_ RR )
77	75	rexnegd	\|- ( ( -. +oo e. A /\ y e. ( { y e. RR* \| -e y e. A } \ { +oo } ) ) -> -e y = -u y )
78	66	adantl	\|- ( ( -. +oo e. A /\ y e. ( { y e. RR* \| -e y e. A } \ { +oo } ) ) -> -e y e. A )
79	63	adantr	\|- ( ( y e. ( { y e. RR* \| -e y e. A } \ { +oo } ) /\ -e y e. { -oo } ) -> y e. RR* )
80		elsni	\|- ( -e y e. { -oo } -> -e y = -oo )
81	80	adantl	\|- ( ( y e. ( { y e. RR* \| -e y e. A } \ { +oo } ) /\ -e y e. { -oo } ) -> -e y = -oo )
82		xnegeq	\|- ( -e y = -oo -> -e -e y = -e -oo )
83	2	a1i	\|- ( -e y = -oo -> -e -oo = +oo )
84	82 83	eqtr2d	\|- ( -e y = -oo -> +oo = -e -e y )
85	84	adantl	\|- ( ( y e. RR* /\ -e y = -oo ) -> +oo = -e -e y )
86		xnegneg	\|- ( y e. RR* -> -e -e y = y )
87	86	adantr	\|- ( ( y e. RR* /\ -e y = -oo ) -> -e -e y = y )
88	85 87	eqtr2d	\|- ( ( y e. RR* /\ -e y = -oo ) -> y = +oo )
89	79 81 88	syl2anc	\|- ( ( y e. ( { y e. RR* \| -e y e. A } \ { +oo } ) /\ -e y e. { -oo } ) -> y = +oo )
90	73	neneqd	\|- ( y e. ( { y e. RR* \| -e y e. A } \ { +oo } ) -> -. y = +oo )
91	90	adantr	\|- ( ( y e. ( { y e. RR* \| -e y e. A } \ { +oo } ) /\ -e y e. { -oo } ) -> -. y = +oo )
92	89 91	pm2.65da	\|- ( y e. ( { y e. RR* \| -e y e. A } \ { +oo } ) -> -. -e y e. { -oo } )
93	92	adantl	\|- ( ( -. +oo e. A /\ y e. ( { y e. RR* \| -e y e. A } \ { +oo } ) ) -> -. -e y e. { -oo } )
94	78 93	eldifd	\|- ( ( -. +oo e. A /\ y e. ( { y e. RR* \| -e y e. A } \ { +oo } ) ) -> -e y e. ( A \ { -oo } ) )
95	77 94	eqeltrrd	\|- ( ( -. +oo e. A /\ y e. ( { y e. RR* \| -e y e. A } \ { +oo } ) ) -> -u y e. ( A \ { -oo } ) )
96	95	ralrimiva	\|- ( -. +oo e. A -> A. y e. ( { y e. RR* \| -e y e. A } \ { +oo } ) -u y e. ( A \ { -oo } ) )
97	76 96	jca	\|- ( -. +oo e. A -> ( ( { y e. RR* \| -e y e. A } \ { +oo } ) C_ RR /\ A. y e. ( { y e. RR* \| -e y e. A } \ { +oo } ) -u y e. ( A \ { -oo } ) ) )
98	57 61	ssrabf	\|- ( ( { y e. RR* \| -e y e. A } \ { +oo } ) C_ { y e. RR \| -u y e. ( A \ { -oo } ) } <-> ( ( { y e. RR* \| -e y e. A } \ { +oo } ) C_ RR /\ A. y e. ( { y e. RR* \| -e y e. A } \ { +oo } ) -u y e. ( A \ { -oo } ) ) )
99	97 98	sylibr	\|- ( -. +oo e. A -> ( { y e. RR* \| -e y e. A } \ { +oo } ) C_ { y e. RR \| -u y e. ( A \ { -oo } ) } )
100	59 99	eqssd	\|- ( -. +oo e. A -> { y e. RR \| -u y e. ( A \ { -oo } ) } = ( { y e. RR* \| -e y e. A } \ { +oo } ) )
101	100	infeq1d	\|- ( -. +oo e. A -> inf ( { y e. RR \| -u y e. ( A \ { -oo } ) } , RR* , < ) = inf ( ( { y e. RR* \| -e y e. A } \ { +oo } ) , RR* , < ) )
102		infxrpnf2	\|- ( { y e. RR* \| -e y e. A } C_ RR* -> inf ( ( { y e. RR* \| -e y e. A } \ { +oo } ) , RR* , < ) = inf ( { y e. RR* \| -e y e. A } , RR* , < ) )
103	7 102	ax-mp	\|- inf ( ( { y e. RR* \| -e y e. A } \ { +oo } ) , RR* , < ) = inf ( { y e. RR* \| -e y e. A } , RR* , < )
104	103	a1i	\|- ( -. +oo e. A -> inf ( ( { y e. RR* \| -e y e. A } \ { +oo } ) , RR* , < ) = inf ( { y e. RR* \| -e y e. A } , RR* , < ) )
105	101 104	eqtr2d	\|- ( -. +oo e. A -> inf ( { y e. RR* \| -e y e. A } , RR* , < ) = inf ( { y e. RR \| -u y e. ( A \ { -oo } ) } , RR* , < ) )
106	105	xnegeqd	\|- ( -. +oo e. A -> -e inf ( { y e. RR* \| -e y e. A } , RR* , < ) = -e inf ( { y e. RR \| -u y e. ( A \ { -oo } ) } , RR* , < ) )
107	106	adantl	\|- ( ( ph /\ -. +oo e. A ) -> -e inf ( { y e. RR* \| -e y e. A } , RR* , < ) = -e inf ( { y e. RR \| -u y e. ( A \ { -oo } ) } , RR* , < ) )
108	31 35 107	3eqtr4d	\|- ( ( ph /\ -. +oo e. A ) -> sup ( A , RR* , < ) = -e inf ( { y e. RR* \| -e y e. A } , RR* , < ) )
109	21 108	pm2.61dan	\|- ( ph -> sup ( A , RR* , < ) = -e inf ( { y e. RR* \| -e y e. A } , RR* , < ) )
110		xnegeq	\|- ( y = x -> -e y = -e x )
111	110	eleq1d	\|- ( y = x -> ( -e y e. A <-> -e x e. A ) )
112	111	cbvrabv	\|- { y e. RR* \| -e y e. A } = { x e. RR* \| -e x e. A }
113	112	infeq1i	\|- inf ( { y e. RR* \| -e y e. A } , RR* , < ) = inf ( { x e. RR* \| -e x e. A } , RR* , < )
114	113	xnegeqi	\|- -e inf ( { y e. RR* \| -e y e. A } , RR* , < ) = -e inf ( { x e. RR* \| -e x e. A } , RR* , < )
115	114	a1i	\|- ( ph -> -e inf ( { y e. RR* \| -e y e. A } , RR* , < ) = -e inf ( { x e. RR* \| -e x e. A } , RR* , < ) )
116	109 115	eqtrd	\|- ( ph -> sup ( A , RR* , < ) = -e inf ( { x e. RR* \| -e x e. A } , RR* , < ) )

Metamath Proof Explorer

Theorem supminfxr2

Proof