Metamath Proof Explorer


Theorem txsconn

Description: The topological product of two simply connected spaces is simply connected. (Contributed by Mario Carneiro, 12-Feb-2015)

Ref Expression
Assertion txsconn R SConn S SConn R × t S SConn

Proof

Step Hyp Ref Expression
1 sconnpconn R SConn R PConn
2 sconnpconn S SConn S PConn
3 txpconn R PConn S PConn R × t S PConn
4 1 2 3 syl2an R SConn S SConn R × t S PConn
5 simpll R SConn S SConn f II Cn R × t S f 0 = f 1 R SConn
6 simprl R SConn S SConn f II Cn R × t S f 0 = f 1 f II Cn R × t S
7 sconntop R SConn R Top
8 7 ad2antrr R SConn S SConn f II Cn R × t S f 0 = f 1 R Top
9 eqid R = R
10 9 toptopon R Top R TopOn R
11 8 10 sylib R SConn S SConn f II Cn R × t S f 0 = f 1 R TopOn R
12 sconntop S SConn S Top
13 12 ad2antlr R SConn S SConn f II Cn R × t S f 0 = f 1 S Top
14 eqid S = S
15 14 toptopon S Top S TopOn S
16 13 15 sylib R SConn S SConn f II Cn R × t S f 0 = f 1 S TopOn S
17 tx1cn R TopOn R S TopOn S 1 st R × S R × t S Cn R
18 11 16 17 syl2anc R SConn S SConn f II Cn R × t S f 0 = f 1 1 st R × S R × t S Cn R
19 cnco f II Cn R × t S 1 st R × S R × t S Cn R 1 st R × S f II Cn R
20 6 18 19 syl2anc R SConn S SConn f II Cn R × t S f 0 = f 1 1 st R × S f II Cn R
21 simprr R SConn S SConn f II Cn R × t S f 0 = f 1 f 0 = f 1
22 21 fveq2d R SConn S SConn f II Cn R × t S f 0 = f 1 1 st R × S f 0 = 1 st R × S f 1
23 iitopon II TopOn 0 1
24 23 a1i R SConn S SConn f II Cn R × t S f 0 = f 1 II TopOn 0 1
25 txtopon R TopOn R S TopOn S R × t S TopOn R × S
26 11 16 25 syl2anc R SConn S SConn f II Cn R × t S f 0 = f 1 R × t S TopOn R × S
27 cnf2 II TopOn 0 1 R × t S TopOn R × S f II Cn R × t S f : 0 1 R × S
28 24 26 6 27 syl3anc R SConn S SConn f II Cn R × t S f 0 = f 1 f : 0 1 R × S
29 0elunit 0 0 1
30 fvco3 f : 0 1 R × S 0 0 1 1 st R × S f 0 = 1 st R × S f 0
31 28 29 30 sylancl R SConn S SConn f II Cn R × t S f 0 = f 1 1 st R × S f 0 = 1 st R × S f 0
32 1elunit 1 0 1
33 fvco3 f : 0 1 R × S 1 0 1 1 st R × S f 1 = 1 st R × S f 1
34 28 32 33 sylancl R SConn S SConn f II Cn R × t S f 0 = f 1 1 st R × S f 1 = 1 st R × S f 1
35 22 31 34 3eqtr4d R SConn S SConn f II Cn R × t S f 0 = f 1 1 st R × S f 0 = 1 st R × S f 1
36 sconnpht R SConn 1 st R × S f II Cn R 1 st R × S f 0 = 1 st R × S f 1 1 st R × S f ph R 0 1 × 1 st R × S f 0
37 5 20 35 36 syl3anc R SConn S SConn f II Cn R × t S f 0 = f 1 1 st R × S f ph R 0 1 × 1 st R × S f 0
38 isphtpc 1 st R × S f ph R 0 1 × 1 st R × S f 0 1 st R × S f II Cn R 0 1 × 1 st R × S f 0 II Cn R 1 st R × S f PHtpy R 0 1 × 1 st R × S f 0
39 37 38 sylib R SConn S SConn f II Cn R × t S f 0 = f 1 1 st R × S f II Cn R 0 1 × 1 st R × S f 0 II Cn R 1 st R × S f PHtpy R 0 1 × 1 st R × S f 0
40 39 simp3d R SConn S SConn f II Cn R × t S f 0 = f 1 1 st R × S f PHtpy R 0 1 × 1 st R × S f 0
41 n0 1 st R × S f PHtpy R 0 1 × 1 st R × S f 0 g g 1 st R × S f PHtpy R 0 1 × 1 st R × S f 0
42 40 41 sylib R SConn S SConn f II Cn R × t S f 0 = f 1 g g 1 st R × S f PHtpy R 0 1 × 1 st R × S f 0
43 simplr R SConn S SConn f II Cn R × t S f 0 = f 1 S SConn
44 tx2cn R TopOn R S TopOn S 2 nd R × S R × t S Cn S
45 11 16 44 syl2anc R SConn S SConn f II Cn R × t S f 0 = f 1 2 nd R × S R × t S Cn S
46 cnco f II Cn R × t S 2 nd R × S R × t S Cn S 2 nd R × S f II Cn S
47 6 45 46 syl2anc R SConn S SConn f II Cn R × t S f 0 = f 1 2 nd R × S f II Cn S
48 21 fveq2d R SConn S SConn f II Cn R × t S f 0 = f 1 2 nd R × S f 0 = 2 nd R × S f 1
49 fvco3 f : 0 1 R × S 0 0 1 2 nd R × S f 0 = 2 nd R × S f 0
50 28 29 49 sylancl R SConn S SConn f II Cn R × t S f 0 = f 1 2 nd R × S f 0 = 2 nd R × S f 0
51 fvco3 f : 0 1 R × S 1 0 1 2 nd R × S f 1 = 2 nd R × S f 1
52 28 32 51 sylancl R SConn S SConn f II Cn R × t S f 0 = f 1 2 nd R × S f 1 = 2 nd R × S f 1
53 48 50 52 3eqtr4d R SConn S SConn f II Cn R × t S f 0 = f 1 2 nd R × S f 0 = 2 nd R × S f 1
54 sconnpht S SConn 2 nd R × S f II Cn S 2 nd R × S f 0 = 2 nd R × S f 1 2 nd R × S f ph S 0 1 × 2 nd R × S f 0
55 43 47 53 54 syl3anc R SConn S SConn f II Cn R × t S f 0 = f 1 2 nd R × S f ph S 0 1 × 2 nd R × S f 0
56 isphtpc 2 nd R × S f ph S 0 1 × 2 nd R × S f 0 2 nd R × S f II Cn S 0 1 × 2 nd R × S f 0 II Cn S 2 nd R × S f PHtpy S 0 1 × 2 nd R × S f 0
57 55 56 sylib R SConn S SConn f II Cn R × t S f 0 = f 1 2 nd R × S f II Cn S 0 1 × 2 nd R × S f 0 II Cn S 2 nd R × S f PHtpy S 0 1 × 2 nd R × S f 0
58 57 simp3d R SConn S SConn f II Cn R × t S f 0 = f 1 2 nd R × S f PHtpy S 0 1 × 2 nd R × S f 0
59 n0 2 nd R × S f PHtpy S 0 1 × 2 nd R × S f 0 h h 2 nd R × S f PHtpy S 0 1 × 2 nd R × S f 0
60 58 59 sylib R SConn S SConn f II Cn R × t S f 0 = f 1 h h 2 nd R × S f PHtpy S 0 1 × 2 nd R × S f 0
61 exdistrv g h g 1 st R × S f PHtpy R 0 1 × 1 st R × S f 0 h 2 nd R × S f PHtpy S 0 1 × 2 nd R × S f 0 g g 1 st R × S f PHtpy R 0 1 × 1 st R × S f 0 h h 2 nd R × S f PHtpy S 0 1 × 2 nd R × S f 0
62 8 adantr R SConn S SConn f II Cn R × t S f 0 = f 1 g 1 st R × S f PHtpy R 0 1 × 1 st R × S f 0 h 2 nd R × S f PHtpy S 0 1 × 2 nd R × S f 0 R Top
63 13 adantr R SConn S SConn f II Cn R × t S f 0 = f 1 g 1 st R × S f PHtpy R 0 1 × 1 st R × S f 0 h 2 nd R × S f PHtpy S 0 1 × 2 nd R × S f 0 S Top
64 6 adantr R SConn S SConn f II Cn R × t S f 0 = f 1 g 1 st R × S f PHtpy R 0 1 × 1 st R × S f 0 h 2 nd R × S f PHtpy S 0 1 × 2 nd R × S f 0 f II Cn R × t S
65 eqid 1 st R × S f = 1 st R × S f
66 eqid 2 nd R × S f = 2 nd R × S f
67 simprl R SConn S SConn f II Cn R × t S f 0 = f 1 g 1 st R × S f PHtpy R 0 1 × 1 st R × S f 0 h 2 nd R × S f PHtpy S 0 1 × 2 nd R × S f 0 g 1 st R × S f PHtpy R 0 1 × 1 st R × S f 0
68 simprr R SConn S SConn f II Cn R × t S f 0 = f 1 g 1 st R × S f PHtpy R 0 1 × 1 st R × S f 0 h 2 nd R × S f PHtpy S 0 1 × 2 nd R × S f 0 h 2 nd R × S f PHtpy S 0 1 × 2 nd R × S f 0
69 62 63 64 65 66 67 68 txsconnlem R SConn S SConn f II Cn R × t S f 0 = f 1 g 1 st R × S f PHtpy R 0 1 × 1 st R × S f 0 h 2 nd R × S f PHtpy S 0 1 × 2 nd R × S f 0 f ph R × t S 0 1 × f 0
70 69 ex R SConn S SConn f II Cn R × t S f 0 = f 1 g 1 st R × S f PHtpy R 0 1 × 1 st R × S f 0 h 2 nd R × S f PHtpy S 0 1 × 2 nd R × S f 0 f ph R × t S 0 1 × f 0
71 70 exlimdvv R SConn S SConn f II Cn R × t S f 0 = f 1 g h g 1 st R × S f PHtpy R 0 1 × 1 st R × S f 0 h 2 nd R × S f PHtpy S 0 1 × 2 nd R × S f 0 f ph R × t S 0 1 × f 0
72 61 71 syl5bir R SConn S SConn f II Cn R × t S f 0 = f 1 g g 1 st R × S f PHtpy R 0 1 × 1 st R × S f 0 h h 2 nd R × S f PHtpy S 0 1 × 2 nd R × S f 0 f ph R × t S 0 1 × f 0
73 42 60 72 mp2and R SConn S SConn f II Cn R × t S f 0 = f 1 f ph R × t S 0 1 × f 0
74 73 expr R SConn S SConn f II Cn R × t S f 0 = f 1 f ph R × t S 0 1 × f 0
75 74 ralrimiva R SConn S SConn f II Cn R × t S f 0 = f 1 f ph R × t S 0 1 × f 0
76 issconn R × t S SConn R × t S PConn f II Cn R × t S f 0 = f 1 f ph R × t S 0 1 × f 0
77 4 75 76 sylanbrc R SConn S SConn R × t S SConn