Step | Hyp | Ref
| Expression |
1 | | pconnpi1.x |
. . 3
β’ π = βͺ
π½ |
2 | 1 | pconncn 33875 |
. 2
β’ ((π½ β PConn β§ π΄ β π β§ π΅ β π) β βπ β (II Cn π½)((πβ0) = π΄ β§ (πβ1) = π΅)) |
3 | | eqid 2733 |
. . . . 5
β’ (π½ Ο1 (πβ0)) = (π½ Ο1 (πβ0)) |
4 | | eqid 2733 |
. . . . 5
β’ (π½ Ο1 (πβ1)) = (π½ Ο1 (πβ1)) |
5 | | eqid 2733 |
. . . . 5
β’
(Baseβ(π½
Ο1 (πβ0))) = (Baseβ(π½ Ο1 (πβ0))) |
6 | | eqid 2733 |
. . . . 5
β’ ran
(β β βͺ (Baseβ(π½ Ο1 (πβ0))) β¦ β¨[β]( βphβπ½), [((π₯ β (0[,]1) β¦ (πβ(1 β π₯)))(*πβπ½)(β(*πβπ½)π))]( βphβπ½)β©) = ran (β β βͺ (Baseβ(π½ Ο1 (πβ0))) β¦ β¨[β]( βphβπ½), [((π₯ β (0[,]1) β¦ (πβ(1 β π₯)))(*πβπ½)(β(*πβπ½)π))]( βphβπ½)β©) |
7 | | simpl1 1192 |
. . . . . . 7
β’ (((π½ β PConn β§ π΄ β π β§ π΅ β π) β§ (π β (II Cn π½) β§ ((πβ0) = π΄ β§ (πβ1) = π΅))) β π½ β PConn) |
8 | | pconntop 33876 |
. . . . . . 7
β’ (π½ β PConn β π½ β Top) |
9 | 7, 8 | syl 17 |
. . . . . 6
β’ (((π½ β PConn β§ π΄ β π β§ π΅ β π) β§ (π β (II Cn π½) β§ ((πβ0) = π΄ β§ (πβ1) = π΅))) β π½ β Top) |
10 | 1 | toptopon 22282 |
. . . . . 6
β’ (π½ β Top β π½ β (TopOnβπ)) |
11 | 9, 10 | sylib 217 |
. . . . 5
β’ (((π½ β PConn β§ π΄ β π β§ π΅ β π) β§ (π β (II Cn π½) β§ ((πβ0) = π΄ β§ (πβ1) = π΅))) β π½ β (TopOnβπ)) |
12 | | simprl 770 |
. . . . 5
β’ (((π½ β PConn β§ π΄ β π β§ π΅ β π) β§ (π β (II Cn π½) β§ ((πβ0) = π΄ β§ (πβ1) = π΅))) β π β (II Cn π½)) |
13 | | oveq2 7366 |
. . . . . . 7
β’ (π₯ = π¦ β (1 β π₯) = (1 β π¦)) |
14 | 13 | fveq2d 6847 |
. . . . . 6
β’ (π₯ = π¦ β (πβ(1 β π₯)) = (πβ(1 β π¦))) |
15 | 14 | cbvmptv 5219 |
. . . . 5
β’ (π₯ β (0[,]1) β¦ (πβ(1 β π₯))) = (π¦ β (0[,]1) β¦ (πβ(1 β π¦))) |
16 | 3, 4, 5, 6, 11, 12, 15 | pi1xfrgim 24437 |
. . . 4
β’ (((π½ β PConn β§ π΄ β π β§ π΅ β π) β§ (π β (II Cn π½) β§ ((πβ0) = π΄ β§ (πβ1) = π΅))) β ran (β β βͺ
(Baseβ(π½
Ο1 (πβ0))) β¦ β¨[β]( βphβπ½), [((π₯ β (0[,]1) β¦ (πβ(1 β π₯)))(*πβπ½)(β(*πβπ½)π))]( βphβπ½)β©) β ((π½ Ο1 (πβ0)) GrpIso (π½ Ο1 (πβ1)))) |
17 | | simprrl 780 |
. . . . . . 7
β’ (((π½ β PConn β§ π΄ β π β§ π΅ β π) β§ (π β (II Cn π½) β§ ((πβ0) = π΄ β§ (πβ1) = π΅))) β (πβ0) = π΄) |
18 | 17 | oveq2d 7374 |
. . . . . 6
β’ (((π½ β PConn β§ π΄ β π β§ π΅ β π) β§ (π β (II Cn π½) β§ ((πβ0) = π΄ β§ (πβ1) = π΅))) β (π½ Ο1 (πβ0)) = (π½ Ο1 π΄)) |
19 | | pconnpi1.p |
. . . . . 6
β’ π = (π½ Ο1 π΄) |
20 | 18, 19 | eqtr4di 2791 |
. . . . 5
β’ (((π½ β PConn β§ π΄ β π β§ π΅ β π) β§ (π β (II Cn π½) β§ ((πβ0) = π΄ β§ (πβ1) = π΅))) β (π½ Ο1 (πβ0)) = π) |
21 | | simprrr 781 |
. . . . . . 7
β’ (((π½ β PConn β§ π΄ β π β§ π΅ β π) β§ (π β (II Cn π½) β§ ((πβ0) = π΄ β§ (πβ1) = π΅))) β (πβ1) = π΅) |
22 | 21 | oveq2d 7374 |
. . . . . 6
β’ (((π½ β PConn β§ π΄ β π β§ π΅ β π) β§ (π β (II Cn π½) β§ ((πβ0) = π΄ β§ (πβ1) = π΅))) β (π½ Ο1 (πβ1)) = (π½ Ο1 π΅)) |
23 | | pconnpi1.q |
. . . . . 6
β’ π = (π½ Ο1 π΅) |
24 | 22, 23 | eqtr4di 2791 |
. . . . 5
β’ (((π½ β PConn β§ π΄ β π β§ π΅ β π) β§ (π β (II Cn π½) β§ ((πβ0) = π΄ β§ (πβ1) = π΅))) β (π½ Ο1 (πβ1)) = π) |
25 | 20, 24 | oveq12d 7376 |
. . . 4
β’ (((π½ β PConn β§ π΄ β π β§ π΅ β π) β§ (π β (II Cn π½) β§ ((πβ0) = π΄ β§ (πβ1) = π΅))) β ((π½ Ο1 (πβ0)) GrpIso (π½ Ο1 (πβ1))) = (π GrpIso π)) |
26 | 16, 25 | eleqtrd 2836 |
. . 3
β’ (((π½ β PConn β§ π΄ β π β§ π΅ β π) β§ (π β (II Cn π½) β§ ((πβ0) = π΄ β§ (πβ1) = π΅))) β ran (β β βͺ
(Baseβ(π½
Ο1 (πβ0))) β¦ β¨[β]( βphβπ½), [((π₯ β (0[,]1) β¦ (πβ(1 β π₯)))(*πβπ½)(β(*πβπ½)π))]( βphβπ½)β©) β (π GrpIso π)) |
27 | | brgici 19065 |
. . 3
β’ (ran
(β β βͺ (Baseβ(π½ Ο1 (πβ0))) β¦ β¨[β]( βphβπ½), [((π₯ β (0[,]1) β¦ (πβ(1 β π₯)))(*πβπ½)(β(*πβπ½)π))]( βphβπ½)β©) β (π GrpIso π) β π βπ π) |
28 | 26, 27 | syl 17 |
. 2
β’ (((π½ β PConn β§ π΄ β π β§ π΅ β π) β§ (π β (II Cn π½) β§ ((πβ0) = π΄ β§ (πβ1) = π΅))) β π βπ π) |
29 | 2, 28 | rexlimddv 3155 |
1
β’ ((π½ β PConn β§ π΄ β π β§ π΅ β π) β π βπ π) |