| Step | Hyp | Ref
| Expression |
|---|
| 1 | | pconnpi1.x |
. . 3
β’ π = βͺ
π½ |
| 2 | 1 | pconncn 34203 |
. 2
β’ ((π½ β PConn β§ π΄ β π β§ π΅ β π) β βπ β (II Cn π½)((πβ0) = π΄ β§ (πβ1) = π΅)) |
| 3 | | eqid 2732 |
. . . . 5
β’ (π½ Ο1 (πβ0)) = (π½ Ο1 (πβ0)) |
| 4 | | eqid 2732 |
. . . . 5
β’ (π½ Ο1 (πβ1)) = (π½ Ο1 (πβ1)) |
| 5 | | eqid 2732 |
. . . . 5
β’
(Baseβ(π½
Ο1 (πβ0))) = (Baseβ(π½ Ο1 (πβ0))) |
| 6 | | eqid 2732 |
. . . . 5
β’ ran
(β β βͺ (Baseβ(π½ Ο1 (πβ0))) β¦ β¨[β]( βphβπ½), [((π₯ β (0[,]1) β¦ (πβ(1 β π₯)))(*πβπ½)(β(*πβπ½)π))]( βphβπ½)β©) = ran (β β βͺ (Baseβ(π½ Ο1 (πβ0))) β¦ β¨[β]( βphβπ½), [((π₯ β (0[,]1) β¦ (πβ(1 β π₯)))(*πβπ½)(β(*πβπ½)π))]( βphβπ½)β©) |
| 7 | | simpl1 1191 |
. . . . . . 7
β’ (((π½ β PConn β§ π΄ β π β§ π΅ β π) β§ (π β (II Cn π½) β§ ((πβ0) = π΄ β§ (πβ1) = π΅))) β π½ β PConn) |
| 8 | | pconntop 34204 |
. . . . . . 7
β’ (π½ β PConn β π½ β Top) |
| 9 | 7, 8 | syl 17 |
. . . . . 6
β’ (((π½ β PConn β§ π΄ β π β§ π΅ β π) β§ (π β (II Cn π½) β§ ((πβ0) = π΄ β§ (πβ1) = π΅))) β π½ β Top) |
| 10 | 1 | toptopon 22410 |
. . . . . 6
β’ (π½ β Top β π½ β (TopOnβπ)) |
| 11 | 9, 10 | sylib 217 |
. . . . 5
β’ (((π½ β PConn β§ π΄ β π β§ π΅ β π) β§ (π β (II Cn π½) β§ ((πβ0) = π΄ β§ (πβ1) = π΅))) β π½ β (TopOnβπ)) |
| 12 | | simprl 769 |
. . . . 5
β’ (((π½ β PConn β§ π΄ β π β§ π΅ β π) β§ (π β (II Cn π½) β§ ((πβ0) = π΄ β§ (πβ1) = π΅))) β π β (II Cn π½)) |
| 13 | | oveq2 7413 |
. . . . . . 7
β’ (π₯ = π¦ β (1 β π₯) = (1 β π¦)) |
| 14 | 13 | fveq2d 6892 |
. . . . . 6
β’ (π₯ = π¦ β (πβ(1 β π₯)) = (πβ(1 β π¦))) |
| 15 | 14 | cbvmptv 5260 |
. . . . 5
β’ (π₯ β (0[,]1) β¦ (πβ(1 β π₯))) = (π¦ β (0[,]1) β¦ (πβ(1 β π¦))) |
| 16 | 3, 4, 5, 6, 11, 12, 15 | pi1xfrgim 24565 |
. . . 4
β’ (((π½ β PConn β§ π΄ β π β§ π΅ β π) β§ (π β (II Cn π½) β§ ((πβ0) = π΄ β§ (πβ1) = π΅))) β ran (β β βͺ
(Baseβ(π½
Ο1 (πβ0))) β¦ β¨[β]( βphβπ½), [((π₯ β (0[,]1) β¦ (πβ(1 β π₯)))(*πβπ½)(β(*πβπ½)π))]( βphβπ½)β©) β ((π½ Ο1 (πβ0)) GrpIso (π½ Ο1 (πβ1)))) |
| 17 | | simprrl 779 |
. . . . . . 7
β’ (((π½ β PConn β§ π΄ β π β§ π΅ β π) β§ (π β (II Cn π½) β§ ((πβ0) = π΄ β§ (πβ1) = π΅))) β (πβ0) = π΄) |
| 18 | 17 | oveq2d 7421 |
. . . . . 6
β’ (((π½ β PConn β§ π΄ β π β§ π΅ β π) β§ (π β (II Cn π½) β§ ((πβ0) = π΄ β§ (πβ1) = π΅))) β (π½ Ο1 (πβ0)) = (π½ Ο1 π΄)) |
| 19 | | pconnpi1.p |
. . . . . 6
β’ π = (π½ Ο1 π΄) |
| 20 | 18, 19 | eqtr4di 2790 |
. . . . 5
β’ (((π½ β PConn β§ π΄ β π β§ π΅ β π) β§ (π β (II Cn π½) β§ ((πβ0) = π΄ β§ (πβ1) = π΅))) β (π½ Ο1 (πβ0)) = π) |
| 21 | | simprrr 780 |
. . . . . . 7
β’ (((π½ β PConn β§ π΄ β π β§ π΅ β π) β§ (π β (II Cn π½) β§ ((πβ0) = π΄ β§ (πβ1) = π΅))) β (πβ1) = π΅) |
| 22 | 21 | oveq2d 7421 |
. . . . . 6
β’ (((π½ β PConn β§ π΄ β π β§ π΅ β π) β§ (π β (II Cn π½) β§ ((πβ0) = π΄ β§ (πβ1) = π΅))) β (π½ Ο1 (πβ1)) = (π½ Ο1 π΅)) |
| 23 | | pconnpi1.q |
. . . . . 6
β’ π = (π½ Ο1 π΅) |
| 24 | 22, 23 | eqtr4di 2790 |
. . . . 5
β’ (((π½ β PConn β§ π΄ β π β§ π΅ β π) β§ (π β (II Cn π½) β§ ((πβ0) = π΄ β§ (πβ1) = π΅))) β (π½ Ο1 (πβ1)) = π) |
| 25 | 20, 24 | oveq12d 7423 |
. . . 4
β’ (((π½ β PConn β§ π΄ β π β§ π΅ β π) β§ (π β (II Cn π½) β§ ((πβ0) = π΄ β§ (πβ1) = π΅))) β ((π½ Ο1 (πβ0)) GrpIso (π½ Ο1 (πβ1))) = (π GrpIso π)) |
| 26 | 16, 25 | eleqtrd 2835 |
. . 3
β’ (((π½ β PConn β§ π΄ β π β§ π΅ β π) β§ (π β (II Cn π½) β§ ((πβ0) = π΄ β§ (πβ1) = π΅))) β ran (β β βͺ
(Baseβ(π½
Ο1 (πβ0))) β¦ β¨[β]( βphβπ½), [((π₯ β (0[,]1) β¦ (πβ(1 β π₯)))(*πβπ½)(β(*πβπ½)π))]( βphβπ½)β©) β (π GrpIso π)) |
| 27 | | brgici 19138 |
. . 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 3161 |
1
β’ ((π½ β PConn β§ π΄ β π β§ π΅ β π) β π βπ π) |
