Step | Hyp | Ref
| Expression |
1 | | isngp.n |
. . 3
β’ π = (normβπΊ) |
2 | | isngp.z |
. . 3
β’ β =
(-gβπΊ) |
3 | | isngp.d |
. . 3
β’ π· = (distβπΊ) |
4 | 1, 2, 3 | isngp 23975 |
. 2
β’ (πΊ β NrmGrp β (πΊ β Grp β§ πΊ β MetSp β§ (π β β ) β π·)) |
5 | | isngp2.e |
. . . . . . 7
β’ πΈ = (π· βΎ (π Γ π)) |
6 | | resss 5966 |
. . . . . . 7
β’ (π· βΎ (π Γ π)) β π· |
7 | 5, 6 | eqsstri 3982 |
. . . . . 6
β’ πΈ β π· |
8 | | sseq1 3973 |
. . . . . 6
β’ ((π β β ) = πΈ β ((π β β ) β π· β πΈ β π·)) |
9 | 7, 8 | mpbiri 258 |
. . . . 5
β’ ((π β β ) = πΈ β (π β β ) β π·) |
10 | | isngp2.x |
. . . . . . . . . . . 12
β’ π = (BaseβπΊ) |
11 | 3 | reseq1i 5937 |
. . . . . . . . . . . . 13
β’ (π· βΎ (π Γ π)) = ((distβπΊ) βΎ (π Γ π)) |
12 | 5, 11 | eqtri 2761 |
. . . . . . . . . . . 12
β’ πΈ = ((distβπΊ) βΎ (π Γ π)) |
13 | 10, 12 | msmet 23833 |
. . . . . . . . . . 11
β’ (πΊ β MetSp β πΈ β (Metβπ)) |
14 | 1, 10, 3, 5 | nmf2 23972 |
. . . . . . . . . . 11
β’ ((πΊ β Grp β§ πΈ β (Metβπ)) β π:πβΆβ) |
15 | 13, 14 | sylan2 594 |
. . . . . . . . . 10
β’ ((πΊ β Grp β§ πΊ β MetSp) β π:πβΆβ) |
16 | 10, 2 | grpsubf 18834 |
. . . . . . . . . . 11
β’ (πΊ β Grp β β :(π Γ π)βΆπ) |
17 | 16 | ad2antrr 725 |
. . . . . . . . . 10
β’ (((πΊ β Grp β§ πΊ β MetSp) β§ (π β β ) β π·) β β :(π Γ π)βΆπ) |
18 | | fco 6696 |
. . . . . . . . . 10
β’ ((π:πβΆβ β§ β :(π Γ π)βΆπ) β (π β β ):(π Γ π)βΆβ) |
19 | 15, 17, 18 | syl2an2r 684 |
. . . . . . . . 9
β’ (((πΊ β Grp β§ πΊ β MetSp) β§ (π β β ) β π·) β (π β β ):(π Γ π)βΆβ) |
20 | 19 | fdmd 6683 |
. . . . . . . 8
β’ (((πΊ β Grp β§ πΊ β MetSp) β§ (π β β ) β π·) β dom (π β β ) = (π Γ π)) |
21 | 20 | reseq2d 5941 |
. . . . . . 7
β’ (((πΊ β Grp β§ πΊ β MetSp) β§ (π β β ) β π·) β (πΈ βΎ dom (π β β )) = (πΈ βΎ (π Γ π))) |
22 | 10, 12 | msf 23834 |
. . . . . . . . . 10
β’ (πΊ β MetSp β πΈ:(π Γ π)βΆβ) |
23 | 22 | ad2antlr 726 |
. . . . . . . . 9
β’ (((πΊ β Grp β§ πΊ β MetSp) β§ (π β β ) β π·) β πΈ:(π Γ π)βΆβ) |
24 | 23 | ffund 6676 |
. . . . . . . 8
β’ (((πΊ β Grp β§ πΊ β MetSp) β§ (π β β ) β π·) β Fun πΈ) |
25 | | simpr 486 |
. . . . . . . . . 10
β’ (((πΊ β Grp β§ πΊ β MetSp) β§ (π β β ) β π·) β (π β β ) β π·) |
26 | | ssv 3972 |
. . . . . . . . . . . 12
β’ β
β V |
27 | | fss 6689 |
. . . . . . . . . . . 12
β’ (((π β β ):(π Γ π)βΆβ β§ β β V)
β (π β β
):(π Γ π)βΆV) |
28 | 19, 26, 27 | sylancl 587 |
. . . . . . . . . . 11
β’ (((πΊ β Grp β§ πΊ β MetSp) β§ (π β β ) β π·) β (π β β ):(π Γ π)βΆV) |
29 | | fssxp 6700 |
. . . . . . . . . . 11
β’ ((π β β ):(π Γ π)βΆV β (π β β ) β ((π Γ π) Γ V)) |
30 | 28, 29 | syl 17 |
. . . . . . . . . 10
β’ (((πΊ β Grp β§ πΊ β MetSp) β§ (π β β ) β π·) β (π β β ) β ((π Γ π) Γ V)) |
31 | 25, 30 | ssind 4196 |
. . . . . . . . 9
β’ (((πΊ β Grp β§ πΊ β MetSp) β§ (π β β ) β π·) β (π β β ) β (π· β© ((π Γ π) Γ V))) |
32 | | df-res 5649 |
. . . . . . . . . 10
β’ (π· βΎ (π Γ π)) = (π· β© ((π Γ π) Γ V)) |
33 | 5, 32 | eqtri 2761 |
. . . . . . . . 9
β’ πΈ = (π· β© ((π Γ π) Γ V)) |
34 | 31, 33 | sseqtrrdi 3999 |
. . . . . . . 8
β’ (((πΊ β Grp β§ πΊ β MetSp) β§ (π β β ) β π·) β (π β β ) β πΈ) |
35 | | funssres 6549 |
. . . . . . . 8
β’ ((Fun
πΈ β§ (π β β ) β πΈ) β (πΈ βΎ dom (π β β )) = (π β β )) |
36 | 24, 34, 35 | syl2anc 585 |
. . . . . . 7
β’ (((πΊ β Grp β§ πΊ β MetSp) β§ (π β β ) β π·) β (πΈ βΎ dom (π β β )) = (π β β )) |
37 | | ffn 6672 |
. . . . . . . 8
β’ (πΈ:(π Γ π)βΆβ β πΈ Fn (π Γ π)) |
38 | | fnresdm 6624 |
. . . . . . . 8
β’ (πΈ Fn (π Γ π) β (πΈ βΎ (π Γ π)) = πΈ) |
39 | 23, 37, 38 | 3syl 18 |
. . . . . . 7
β’ (((πΊ β Grp β§ πΊ β MetSp) β§ (π β β ) β π·) β (πΈ βΎ (π Γ π)) = πΈ) |
40 | 21, 36, 39 | 3eqtr3d 2781 |
. . . . . 6
β’ (((πΊ β Grp β§ πΊ β MetSp) β§ (π β β ) β π·) β (π β β ) = πΈ) |
41 | 40 | ex 414 |
. . . . 5
β’ ((πΊ β Grp β§ πΊ β MetSp) β ((π β β ) β π· β (π β β ) = πΈ)) |
42 | 9, 41 | impbid2 225 |
. . . 4
β’ ((πΊ β Grp β§ πΊ β MetSp) β ((π β β ) = πΈ β (π β β ) β π·)) |
43 | 42 | pm5.32i 576 |
. . 3
β’ (((πΊ β Grp β§ πΊ β MetSp) β§ (π β β ) = πΈ) β ((πΊ β Grp β§ πΊ β MetSp) β§ (π β β ) β π·)) |
44 | | df-3an 1090 |
. . 3
β’ ((πΊ β Grp β§ πΊ β MetSp β§ (π β β ) = πΈ) β ((πΊ β Grp β§ πΊ β MetSp) β§ (π β β ) = πΈ)) |
45 | | df-3an 1090 |
. . 3
β’ ((πΊ β Grp β§ πΊ β MetSp β§ (π β β ) β π·) β ((πΊ β Grp β§ πΊ β MetSp) β§ (π β β ) β π·)) |
46 | 43, 44, 45 | 3bitr4i 303 |
. 2
β’ ((πΊ β Grp β§ πΊ β MetSp β§ (π β β ) = πΈ) β (πΊ β Grp β§ πΊ β MetSp β§ (π β β ) β π·)) |
47 | 4, 46 | bitr4i 278 |
1
β’ (πΊ β NrmGrp β (πΊ β Grp β§ πΊ β MetSp β§ (π β β ) = πΈ)) |