resconn

Description: A subset of RR is simply connected iff it is connected. (Contributed by Mario Carneiro, 9-Mar-2015)

		Ref	Expression
	Hypothesis	resconn.1	$⊢ J = topGen (ran (.)) ↾_{𝑡} A$
	Assertion	resconn	$⊢ A \subseteq ℝ \to (J \in SConn \leftrightarrow J \in Conn)$

Proof

Step	Hyp	Ref	Expression
1		resconn.1	$⊢ J = topGen (ran (.)) ↾_{𝑡} A$
2		sconnpconn	$⊢ J \in SConn \to J \in PConn$
3		pconnconn	$⊢ J \in PConn \to J \in Conn$
4	2 3	syl	$⊢ J \in SConn \to J \in Conn$
5		eqid	$⊢ TopOpen (ℂ_{fld}) = TopOpen (ℂ_{fld})$
6		eqid	$⊢ topGen (ran (.)) = topGen (ran (.))$
7	5 6	rerest	$⊢ A \subseteq ℝ \to TopOpen (ℂ_{fld}) ↾_{𝑡} A = topGen (ran (.)) ↾_{𝑡} A$
8	7 1	eqtr4di	$⊢ A \subseteq ℝ \to TopOpen (ℂ_{fld}) ↾_{𝑡} A = J$
9	8	adantr	$⊢ (A \subseteq ℝ \land J \in Conn) \to TopOpen (ℂ_{fld}) ↾_{𝑡} A = J$
10		simpl	$⊢ (A \subseteq ℝ \land J \in Conn) \to A \subseteq ℝ$
11		ax-resscn	$⊢ ℝ \subseteq ℂ$
12	10 11	sstrdi	$⊢ (A \subseteq ℝ \land J \in Conn) \to A \subseteq ℂ$
13		df-3an	$⊢ (x \in A \land y \in A \land t \in [0, 1]) \leftrightarrow ((x \in A \land y \in A) \land t \in [0, 1])$
14		oveq2	$⊢ z = x \to t z = t x$
15		oveq2	$⊢ w = y \to (1 - t) w = (1 - t) y$
16	14 15	oveqan12d	$⊢ (z = x \land w = y) \to t z + (1 - t) w = t x + (1 - t) y$
17	16	eleq1d	$⊢ (z = x \land w = y) \to (t z + (1 - t) w \in A \leftrightarrow t x + (1 - t) y \in A)$
18	17	ralbidv	$⊢ (z = x \land w = y) \to (\forall t \in [0, 1] t z + (1 - t) w \in A \leftrightarrow \forall t \in [0, 1] t x + (1 - t) y \in A)$
19		oveq2	$⊢ z = y \to t z = t y$
20		oveq2	$⊢ w = x \to (1 - t) w = (1 - t) x$
21	19 20	oveqan12d	$⊢ (z = y \land w = x) \to t z + (1 - t) w = t y + (1 - t) x$
22	21	eleq1d	$⊢ (z = y \land w = x) \to (t z + (1 - t) w \in A \leftrightarrow t y + (1 - t) x \in A)$
23	22	ralbidv	$⊢ (z = y \land w = x) \to (\forall t \in [0, 1] t z + (1 - t) w \in A \leftrightarrow \forall t \in [0, 1] t y + (1 - t) x \in A)$
24		unitssre	$⊢ [0, 1] \subseteq ℝ$
25	24 11	sstri	$⊢ [0, 1] \subseteq ℂ$
26		simpr	$⊢ (((A \subseteq ℝ \land J \in Conn) \land (x \in A \land y \in A \land x \leq y)) \land s \in [0, 1]) \to s \in [0, 1]$
27	25 26	sseldi	$⊢ (((A \subseteq ℝ \land J \in Conn) \land (x \in A \land y \in A \land x \leq y)) \land s \in [0, 1]) \to s \in ℂ$
28	12	adantr	$⊢ ((A \subseteq ℝ \land J \in Conn) \land (x \in A \land y \in A \land x \leq y)) \to A \subseteq ℂ$
29		simpr2	$⊢ ((A \subseteq ℝ \land J \in Conn) \land (x \in A \land y \in A \land x \leq y)) \to y \in A$
30	28 29	sseldd	$⊢ ((A \subseteq ℝ \land J \in Conn) \land (x \in A \land y \in A \land x \leq y)) \to y \in ℂ$
31	30	adantr	$⊢ (((A \subseteq ℝ \land J \in Conn) \land (x \in A \land y \in A \land x \leq y)) \land s \in [0, 1]) \to y \in ℂ$
32	27 31	mulcld	$⊢ (((A \subseteq ℝ \land J \in Conn) \land (x \in A \land y \in A \land x \leq y)) \land s \in [0, 1]) \to s y \in ℂ$
33		ax-1cn	$⊢ 1 \in ℂ$
34		subcl	$⊢ (1 \in ℂ \land s \in ℂ) \to 1 - s \in ℂ$
35	33 27 34	sylancr	$⊢ (((A \subseteq ℝ \land J \in Conn) \land (x \in A \land y \in A \land x \leq y)) \land s \in [0, 1]) \to 1 - s \in ℂ$
36		simpr1	$⊢ ((A \subseteq ℝ \land J \in Conn) \land (x \in A \land y \in A \land x \leq y)) \to x \in A$
37	28 36	sseldd	$⊢ ((A \subseteq ℝ \land J \in Conn) \land (x \in A \land y \in A \land x \leq y)) \to x \in ℂ$
38	37	adantr	$⊢ (((A \subseteq ℝ \land J \in Conn) \land (x \in A \land y \in A \land x \leq y)) \land s \in [0, 1]) \to x \in ℂ$
39	35 38	mulcld	$⊢ (((A \subseteq ℝ \land J \in Conn) \land (x \in A \land y \in A \land x \leq y)) \land s \in [0, 1]) \to (1 - s) x \in ℂ$
40	32 39	addcomd	$⊢ (((A \subseteq ℝ \land J \in Conn) \land (x \in A \land y \in A \land x \leq y)) \land s \in [0, 1]) \to s y + (1 - s) x = (1 - s) x + s y$
41		nncan	$⊢ (1 \in ℂ \land s \in ℂ) \to 1 - (1 - s) = s$
42	33 27 41	sylancr	$⊢ (((A \subseteq ℝ \land J \in Conn) \land (x \in A \land y \in A \land x \leq y)) \land s \in [0, 1]) \to 1 - (1 - s) = s$
43	42	oveq1d	$⊢ (((A \subseteq ℝ \land J \in Conn) \land (x \in A \land y \in A \land x \leq y)) \land s \in [0, 1]) \to (1 - (1 - s)) y = s y$
44	43	oveq2d	$⊢ (((A \subseteq ℝ \land J \in Conn) \land (x \in A \land y \in A \land x \leq y)) \land s \in [0, 1]) \to (1 - s) x + (1 - (1 - s)) y = (1 - s) x + s y$
45	40 44	eqtr4d	$⊢ (((A \subseteq ℝ \land J \in Conn) \land (x \in A \land y \in A \land x \leq y)) \land s \in [0, 1]) \to s y + (1 - s) x = (1 - s) x + (1 - (1 - s)) y$
46		iirev	$⊢ s \in [0, 1] \to 1 - s \in [0, 1]$
47	46	adantl	$⊢ (((A \subseteq ℝ \land J \in Conn) \land (x \in A \land y \in A \land x \leq y)) \land s \in [0, 1]) \to 1 - s \in [0, 1]$
48	1	eleq1i	$⊢ J \in Conn \leftrightarrow topGen (ran (.)) ↾_{𝑡} A \in Conn$
49		reconn	$⊢ A \subseteq ℝ \to (topGen (ran (.)) ↾_{𝑡} A \in Conn \leftrightarrow \forall x \in A \forall y \in A [x, y] \subseteq A)$
50	48 49	syl5bb	$⊢ A \subseteq ℝ \to (J \in Conn \leftrightarrow \forall x \in A \forall y \in A [x, y] \subseteq A)$
51	50	biimpa	$⊢ (A \subseteq ℝ \land J \in Conn) \to \forall x \in A \forall y \in A [x, y] \subseteq A$
52	51	r19.21bi	$⊢ ((A \subseteq ℝ \land J \in Conn) \land x \in A) \to \forall y \in A [x, y] \subseteq A$
53	52	r19.21bi	$⊢ (((A \subseteq ℝ \land J \in Conn) \land x \in A) \land y \in A) \to [x, y] \subseteq A$
54	53	anasss	$⊢ ((A \subseteq ℝ \land J \in Conn) \land (x \in A \land y \in A)) \to [x, y] \subseteq A$
55	54	3adantr3	$⊢ ((A \subseteq ℝ \land J \in Conn) \land (x \in A \land y \in A \land x \leq y)) \to [x, y] \subseteq A$
56	55	adantr	$⊢ (((A \subseteq ℝ \land J \in Conn) \land (x \in A \land y \in A \land x \leq y)) \land t \in [0, 1]) \to [x, y] \subseteq A$
57		simpr	$⊢ (((A \subseteq ℝ \land J \in Conn) \land (x \in A \land y \in A \land x \leq y)) \land t \in [0, 1]) \to t \in [0, 1]$
58	24 57	sseldi	$⊢ (((A \subseteq ℝ \land J \in Conn) \land (x \in A \land y \in A \land x \leq y)) \land t \in [0, 1]) \to t \in ℝ$
59		simplll	$⊢ (((A \subseteq ℝ \land J \in Conn) \land (x \in A \land y \in A \land x \leq y)) \land t \in [0, 1]) \to A \subseteq ℝ$
60	36	adantr	$⊢ (((A \subseteq ℝ \land J \in Conn) \land (x \in A \land y \in A \land x \leq y)) \land t \in [0, 1]) \to x \in A$
61	59 60	sseldd	$⊢ (((A \subseteq ℝ \land J \in Conn) \land (x \in A \land y \in A \land x \leq y)) \land t \in [0, 1]) \to x \in ℝ$
62	58 61	remulcld	$⊢ (((A \subseteq ℝ \land J \in Conn) \land (x \in A \land y \in A \land x \leq y)) \land t \in [0, 1]) \to t x \in ℝ$
63		1re	$⊢ 1 \in ℝ$
64		resubcl	$⊢ (1 \in ℝ \land t \in ℝ) \to 1 - t \in ℝ$
65	63 58 64	sylancr	$⊢ (((A \subseteq ℝ \land J \in Conn) \land (x \in A \land y \in A \land x \leq y)) \land t \in [0, 1]) \to 1 - t \in ℝ$
66	29	adantr	$⊢ (((A \subseteq ℝ \land J \in Conn) \land (x \in A \land y \in A \land x \leq y)) \land t \in [0, 1]) \to y \in A$
67	59 66	sseldd	$⊢ (((A \subseteq ℝ \land J \in Conn) \land (x \in A \land y \in A \land x \leq y)) \land t \in [0, 1]) \to y \in ℝ$
68	65 67	remulcld	$⊢ (((A \subseteq ℝ \land J \in Conn) \land (x \in A \land y \in A \land x \leq y)) \land t \in [0, 1]) \to (1 - t) y \in ℝ$
69	62 68	readdcld	$⊢ (((A \subseteq ℝ \land J \in Conn) \land (x \in A \land y \in A \land x \leq y)) \land t \in [0, 1]) \to t x + (1 - t) y \in ℝ$
70	58	recnd	$⊢ (((A \subseteq ℝ \land J \in Conn) \land (x \in A \land y \in A \land x \leq y)) \land t \in [0, 1]) \to t \in ℂ$
71		pncan3	$⊢ (t \in ℂ \land 1 \in ℂ) \to t + 1 - t = 1$
72	70 33 71	sylancl	$⊢ (((A \subseteq ℝ \land J \in Conn) \land (x \in A \land y \in A \land x \leq y)) \land t \in [0, 1]) \to t + 1 - t = 1$
73	72	oveq1d	$⊢ (((A \subseteq ℝ \land J \in Conn) \land (x \in A \land y \in A \land x \leq y)) \land t \in [0, 1]) \to (t + 1 - t) x = 1 x$
74	65	recnd	$⊢ (((A \subseteq ℝ \land J \in Conn) \land (x \in A \land y \in A \land x \leq y)) \land t \in [0, 1]) \to 1 - t \in ℂ$
75	37	adantr	$⊢ (((A \subseteq ℝ \land J \in Conn) \land (x \in A \land y \in A \land x \leq y)) \land t \in [0, 1]) \to x \in ℂ$
76	70 74 75	adddird	$⊢ (((A \subseteq ℝ \land J \in Conn) \land (x \in A \land y \in A \land x \leq y)) \land t \in [0, 1]) \to (t + 1 - t) x = t x + (1 - t) x$
77	75	mulid2d	$⊢ (((A \subseteq ℝ \land J \in Conn) \land (x \in A \land y \in A \land x \leq y)) \land t \in [0, 1]) \to 1 x = x$
78	73 76 77	3eqtr3d	$⊢ (((A \subseteq ℝ \land J \in Conn) \land (x \in A \land y \in A \land x \leq y)) \land t \in [0, 1]) \to t x + (1 - t) x = x$
79	65 61	remulcld	$⊢ (((A \subseteq ℝ \land J \in Conn) \land (x \in A \land y \in A \land x \leq y)) \land t \in [0, 1]) \to (1 - t) x \in ℝ$
80		elicc01	$⊢ t \in [0, 1] \leftrightarrow (t \in ℝ \land 0 \leq t \land t \leq 1)$
81	57 80	sylib	$⊢ (((A \subseteq ℝ \land J \in Conn) \land (x \in A \land y \in A \land x \leq y)) \land t \in [0, 1]) \to (t \in ℝ \land 0 \leq t \land t \leq 1)$
82	81	simp3d	$⊢ (((A \subseteq ℝ \land J \in Conn) \land (x \in A \land y \in A \land x \leq y)) \land t \in [0, 1]) \to t \leq 1$
83		subge0	$⊢ (1 \in ℝ \land t \in ℝ) \to (0 \leq 1 - t \leftrightarrow t \leq 1)$
84	63 58 83	sylancr	$⊢ (((A \subseteq ℝ \land J \in Conn) \land (x \in A \land y \in A \land x \leq y)) \land t \in [0, 1]) \to (0 \leq 1 - t \leftrightarrow t \leq 1)$
85	82 84	mpbird	$⊢ (((A \subseteq ℝ \land J \in Conn) \land (x \in A \land y \in A \land x \leq y)) \land t \in [0, 1]) \to 0 \leq 1 - t$
86		simplr3	$⊢ (((A \subseteq ℝ \land J \in Conn) \land (x \in A \land y \in A \land x \leq y)) \land t \in [0, 1]) \to x \leq y$
87	61 67 65 85 86	lemul2ad	$⊢ (((A \subseteq ℝ \land J \in Conn) \land (x \in A \land y \in A \land x \leq y)) \land t \in [0, 1]) \to (1 - t) x \leq (1 - t) y$
88	79 68 62 87	leadd2dd	$⊢ (((A \subseteq ℝ \land J \in Conn) \land (x \in A \land y \in A \land x \leq y)) \land t \in [0, 1]) \to t x + (1 - t) x \leq t x + (1 - t) y$
89	78 88	eqbrtrrd	$⊢ (((A \subseteq ℝ \land J \in Conn) \land (x \in A \land y \in A \land x \leq y)) \land t \in [0, 1]) \to x \leq t x + (1 - t) y$
90	58 67	remulcld	$⊢ (((A \subseteq ℝ \land J \in Conn) \land (x \in A \land y \in A \land x \leq y)) \land t \in [0, 1]) \to t y \in ℝ$
91	81	simp2d	$⊢ (((A \subseteq ℝ \land J \in Conn) \land (x \in A \land y \in A \land x \leq y)) \land t \in [0, 1]) \to 0 \leq t$
92	61 67 58 91 86	lemul2ad	$⊢ (((A \subseteq ℝ \land J \in Conn) \land (x \in A \land y \in A \land x \leq y)) \land t \in [0, 1]) \to t x \leq t y$
93	62 90 68 92	leadd1dd	$⊢ (((A \subseteq ℝ \land J \in Conn) \land (x \in A \land y \in A \land x \leq y)) \land t \in [0, 1]) \to t x + (1 - t) y \leq t y + (1 - t) y$
94	72	oveq1d	$⊢ (((A \subseteq ℝ \land J \in Conn) \land (x \in A \land y \in A \land x \leq y)) \land t \in [0, 1]) \to (t + 1 - t) y = 1 y$
95	30	adantr	$⊢ (((A \subseteq ℝ \land J \in Conn) \land (x \in A \land y \in A \land x \leq y)) \land t \in [0, 1]) \to y \in ℂ$
96	70 74 95	adddird	$⊢ (((A \subseteq ℝ \land J \in Conn) \land (x \in A \land y \in A \land x \leq y)) \land t \in [0, 1]) \to (t + 1 - t) y = t y + (1 - t) y$
97	95	mulid2d	$⊢ (((A \subseteq ℝ \land J \in Conn) \land (x \in A \land y \in A \land x \leq y)) \land t \in [0, 1]) \to 1 y = y$
98	94 96 97	3eqtr3d	$⊢ (((A \subseteq ℝ \land J \in Conn) \land (x \in A \land y \in A \land x \leq y)) \land t \in [0, 1]) \to t y + (1 - t) y = y$
99	93 98	breqtrd	$⊢ (((A \subseteq ℝ \land J \in Conn) \land (x \in A \land y \in A \land x \leq y)) \land t \in [0, 1]) \to t x + (1 - t) y \leq y$
100		elicc2	$⊢ (x \in ℝ \land y \in ℝ) \to (t x + (1 - t) y \in [x, y] \leftrightarrow (t x + (1 - t) y \in ℝ \land x \leq t x + (1 - t) y \land t x + (1 - t) y \leq y))$
101	61 67 100	syl2anc	$⊢ (((A \subseteq ℝ \land J \in Conn) \land (x \in A \land y \in A \land x \leq y)) \land t \in [0, 1]) \to (t x + (1 - t) y \in [x, y] \leftrightarrow (t x + (1 - t) y \in ℝ \land x \leq t x + (1 - t) y \land t x + (1 - t) y \leq y))$
102	69 89 99 101	mpbir3and	$⊢ (((A \subseteq ℝ \land J \in Conn) \land (x \in A \land y \in A \land x \leq y)) \land t \in [0, 1]) \to t x + (1 - t) y \in [x, y]$
103	56 102	sseldd	$⊢ (((A \subseteq ℝ \land J \in Conn) \land (x \in A \land y \in A \land x \leq y)) \land t \in [0, 1]) \to t x + (1 - t) y \in A$
104	103	ralrimiva	$⊢ ((A \subseteq ℝ \land J \in Conn) \land (x \in A \land y \in A \land x \leq y)) \to \forall t \in [0, 1] t x + (1 - t) y \in A$
105	104	adantr	$⊢ (((A \subseteq ℝ \land J \in Conn) \land (x \in A \land y \in A \land x \leq y)) \land s \in [0, 1]) \to \forall t \in [0, 1] t x + (1 - t) y \in A$
106		oveq1	$⊢ t = 1 - s \to t x = (1 - s) x$
107		oveq2	$⊢ t = 1 - s \to 1 - t = 1 - (1 - s)$
108	107	oveq1d	$⊢ t = 1 - s \to (1 - t) y = (1 - (1 - s)) y$
109	106 108	oveq12d	$⊢ t = 1 - s \to t x + (1 - t) y = (1 - s) x + (1 - (1 - s)) y$
110	109	eleq1d	$⊢ t = 1 - s \to (t x + (1 - t) y \in A \leftrightarrow (1 - s) x + (1 - (1 - s)) y \in A)$
111	110	rspcv	$⊢ 1 - s \in [0, 1] \to (\forall t \in [0, 1] t x + (1 - t) y \in A \to (1 - s) x + (1 - (1 - s)) y \in A)$
112	47 105 111	sylc	$⊢ (((A \subseteq ℝ \land J \in Conn) \land (x \in A \land y \in A \land x \leq y)) \land s \in [0, 1]) \to (1 - s) x + (1 - (1 - s)) y \in A$
113	45 112	eqeltrd	$⊢ (((A \subseteq ℝ \land J \in Conn) \land (x \in A \land y \in A \land x \leq y)) \land s \in [0, 1]) \to s y + (1 - s) x \in A$
114	113	ralrimiva	$⊢ ((A \subseteq ℝ \land J \in Conn) \land (x \in A \land y \in A \land x \leq y)) \to \forall s \in [0, 1] s y + (1 - s) x \in A$
115		oveq1	$⊢ s = t \to s y = t y$
116		oveq2	$⊢ s = t \to 1 - s = 1 - t$
117	116	oveq1d	$⊢ s = t \to (1 - s) x = (1 - t) x$
118	115 117	oveq12d	$⊢ s = t \to s y + (1 - s) x = t y + (1 - t) x$
119	118	eleq1d	$⊢ s = t \to (s y + (1 - s) x \in A \leftrightarrow t y + (1 - t) x \in A)$
120	119	cbvralvw	$⊢ \forall s \in [0, 1] s y + (1 - s) x \in A \leftrightarrow \forall t \in [0, 1] t y + (1 - t) x \in A$
121	114 120	sylib	$⊢ ((A \subseteq ℝ \land J \in Conn) \land (x \in A \land y \in A \land x \leq y)) \to \forall t \in [0, 1] t y + (1 - t) x \in A$
122	18 23 10 121 104	wloglei	$⊢ ((A \subseteq ℝ \land J \in Conn) \land (x \in A \land y \in A)) \to \forall t \in [0, 1] t x + (1 - t) y \in A$
123	122	r19.21bi	$⊢ (((A \subseteq ℝ \land J \in Conn) \land (x \in A \land y \in A)) \land t \in [0, 1]) \to t x + (1 - t) y \in A$
124	123	anasss	$⊢ ((A \subseteq ℝ \land J \in Conn) \land ((x \in A \land y \in A) \land t \in [0, 1])) \to t x + (1 - t) y \in A$
125	13 124	sylan2b	$⊢ ((A \subseteq ℝ \land J \in Conn) \land (x \in A \land y \in A \land t \in [0, 1])) \to t x + (1 - t) y \in A$
126		eqid	$⊢ TopOpen (ℂ_{fld}) ↾_{𝑡} A = TopOpen (ℂ_{fld}) ↾_{𝑡} A$
127	12 125 5 126	cvxsconn	$⊢ (A \subseteq ℝ \land J \in Conn) \to TopOpen (ℂ_{fld}) ↾_{𝑡} A \in SConn$
128	9 127	eqeltrrd	$⊢ (A \subseteq ℝ \land J \in Conn) \to J \in SConn$
129	128	ex	$⊢ A \subseteq ℝ \to (J \in Conn \to J \in SConn)$
130	4 129	impbid2	$⊢ A \subseteq ℝ \to (J \in SConn \leftrightarrow J \in Conn)$

Metamath Proof Explorer

Theorem resconn

Proof