Step | Hyp | Ref
| Expression |
1 | | isngp.n |
. . 3
β’ π = (normβπΊ) |
2 | | isngp.z |
. . 3
β’ β =
(-gβπΊ) |
3 | | isngp.d |
. . 3
β’ π· = (distβπΊ) |
4 | | isngp2.x |
. . 3
β’ π = (BaseβπΊ) |
5 | | eqid 2730 |
. . 3
β’ (π· βΎ (π Γ π)) = (π· βΎ (π Γ π)) |
6 | 1, 2, 3, 4, 5 | isngp2 24326 |
. 2
β’ (πΊ β NrmGrp β (πΊ β Grp β§ πΊ β MetSp β§ (π β β ) = (π· βΎ (π Γ π)))) |
7 | 4, 3 | msmet2 24186 |
. . . . . . . . 9
β’ (πΊ β MetSp β (π· βΎ (π Γ π)) β (Metβπ)) |
8 | 1, 4, 3, 5 | nmf2 24322 |
. . . . . . . . 9
β’ ((πΊ β Grp β§ (π· βΎ (π Γ π)) β (Metβπ)) β π:πβΆβ) |
9 | 7, 8 | sylan2 591 |
. . . . . . . 8
β’ ((πΊ β Grp β§ πΊ β MetSp) β π:πβΆβ) |
10 | 4, 2 | grpsubf 18938 |
. . . . . . . . 9
β’ (πΊ β Grp β β :(π Γ π)βΆπ) |
11 | 10 | adantr 479 |
. . . . . . . 8
β’ ((πΊ β Grp β§ πΊ β MetSp) β β :(π Γ π)βΆπ) |
12 | | fco 6740 |
. . . . . . . 8
β’ ((π:πβΆβ β§ β :(π Γ π)βΆπ) β (π β β ):(π Γ π)βΆβ) |
13 | 9, 11, 12 | syl2anc 582 |
. . . . . . 7
β’ ((πΊ β Grp β§ πΊ β MetSp) β (π β β ):(π Γ π)βΆβ) |
14 | 13 | ffnd 6717 |
. . . . . 6
β’ ((πΊ β Grp β§ πΊ β MetSp) β (π β β ) Fn (π Γ π)) |
15 | 7 | adantl 480 |
. . . . . . 7
β’ ((πΊ β Grp β§ πΊ β MetSp) β (π· βΎ (π Γ π)) β (Metβπ)) |
16 | | metf 24056 |
. . . . . . 7
β’ ((π· βΎ (π Γ π)) β (Metβπ) β (π· βΎ (π Γ π)):(π Γ π)βΆβ) |
17 | | ffn 6716 |
. . . . . . 7
β’ ((π· βΎ (π Γ π)):(π Γ π)βΆβ β (π· βΎ (π Γ π)) Fn (π Γ π)) |
18 | 15, 16, 17 | 3syl 18 |
. . . . . 6
β’ ((πΊ β Grp β§ πΊ β MetSp) β (π· βΎ (π Γ π)) Fn (π Γ π)) |
19 | | eqfnov2 7541 |
. . . . . 6
β’ (((π β β ) Fn (π Γ π) β§ (π· βΎ (π Γ π)) Fn (π Γ π)) β ((π β β ) = (π· βΎ (π Γ π)) β βπ₯ β π βπ¦ β π (π₯(π β β )π¦) = (π₯(π· βΎ (π Γ π))π¦))) |
20 | 14, 18, 19 | syl2anc 582 |
. . . . 5
β’ ((πΊ β Grp β§ πΊ β MetSp) β ((π β β ) = (π· βΎ (π Γ π)) β βπ₯ β π βπ¦ β π (π₯(π β β )π¦) = (π₯(π· βΎ (π Γ π))π¦))) |
21 | | opelxpi 5712 |
. . . . . . . . . 10
β’ ((π₯ β π β§ π¦ β π) β β¨π₯, π¦β© β (π Γ π)) |
22 | | fvco3 6989 |
. . . . . . . . . 10
β’ (( β :(π Γ π)βΆπ β§ β¨π₯, π¦β© β (π Γ π)) β ((π β β )ββ¨π₯, π¦β©) = (πβ( β ββ¨π₯, π¦β©))) |
23 | 11, 21, 22 | syl2an 594 |
. . . . . . . . 9
β’ (((πΊ β Grp β§ πΊ β MetSp) β§ (π₯ β π β§ π¦ β π)) β ((π β β )ββ¨π₯, π¦β©) = (πβ( β ββ¨π₯, π¦β©))) |
24 | | df-ov 7414 |
. . . . . . . . 9
β’ (π₯(π β β )π¦) = ((π β β )ββ¨π₯, π¦β©) |
25 | | df-ov 7414 |
. . . . . . . . . 10
β’ (π₯ β π¦) = ( β ββ¨π₯, π¦β©) |
26 | 25 | fveq2i 6893 |
. . . . . . . . 9
β’ (πβ(π₯ β π¦)) = (πβ( β ββ¨π₯, π¦β©)) |
27 | 23, 24, 26 | 3eqtr4g 2795 |
. . . . . . . 8
β’ (((πΊ β Grp β§ πΊ β MetSp) β§ (π₯ β π β§ π¦ β π)) β (π₯(π β β )π¦) = (πβ(π₯ β π¦))) |
28 | | ovres 7575 |
. . . . . . . . 9
β’ ((π₯ β π β§ π¦ β π) β (π₯(π· βΎ (π Γ π))π¦) = (π₯π·π¦)) |
29 | 28 | adantl 480 |
. . . . . . . 8
β’ (((πΊ β Grp β§ πΊ β MetSp) β§ (π₯ β π β§ π¦ β π)) β (π₯(π· βΎ (π Γ π))π¦) = (π₯π·π¦)) |
30 | 27, 29 | eqeq12d 2746 |
. . . . . . 7
β’ (((πΊ β Grp β§ πΊ β MetSp) β§ (π₯ β π β§ π¦ β π)) β ((π₯(π β β )π¦) = (π₯(π· βΎ (π Γ π))π¦) β (πβ(π₯ β π¦)) = (π₯π·π¦))) |
31 | | eqcom 2737 |
. . . . . . 7
β’ ((πβ(π₯ β π¦)) = (π₯π·π¦) β (π₯π·π¦) = (πβ(π₯ β π¦))) |
32 | 30, 31 | bitrdi 286 |
. . . . . 6
β’ (((πΊ β Grp β§ πΊ β MetSp) β§ (π₯ β π β§ π¦ β π)) β ((π₯(π β β )π¦) = (π₯(π· βΎ (π Γ π))π¦) β (π₯π·π¦) = (πβ(π₯ β π¦)))) |
33 | 32 | 2ralbidva 3214 |
. . . . 5
β’ ((πΊ β Grp β§ πΊ β MetSp) β
(βπ₯ β π βπ¦ β π (π₯(π β β )π¦) = (π₯(π· βΎ (π Γ π))π¦) β βπ₯ β π βπ¦ β π (π₯π·π¦) = (πβ(π₯ β π¦)))) |
34 | 20, 33 | bitrd 278 |
. . . 4
β’ ((πΊ β Grp β§ πΊ β MetSp) β ((π β β ) = (π· βΎ (π Γ π)) β βπ₯ β π βπ¦ β π (π₯π·π¦) = (πβ(π₯ β π¦)))) |
35 | 34 | pm5.32i 573 |
. . 3
β’ (((πΊ β Grp β§ πΊ β MetSp) β§ (π β β ) = (π· βΎ (π Γ π))) β ((πΊ β Grp β§ πΊ β MetSp) β§ βπ₯ β π βπ¦ β π (π₯π·π¦) = (πβ(π₯ β π¦)))) |
36 | | df-3an 1087 |
. . 3
β’ ((πΊ β Grp β§ πΊ β MetSp β§ (π β β ) = (π· βΎ (π Γ π))) β ((πΊ β Grp β§ πΊ β MetSp) β§ (π β β ) = (π· βΎ (π Γ π)))) |
37 | | df-3an 1087 |
. . 3
β’ ((πΊ β Grp β§ πΊ β MetSp β§
βπ₯ β π βπ¦ β π (π₯π·π¦) = (πβ(π₯ β π¦))) β ((πΊ β Grp β§ πΊ β MetSp) β§ βπ₯ β π βπ¦ β π (π₯π·π¦) = (πβ(π₯ β π¦)))) |
38 | 35, 36, 37 | 3bitr4i 302 |
. 2
β’ ((πΊ β Grp β§ πΊ β MetSp β§ (π β β ) = (π· βΎ (π Γ π))) β (πΊ β Grp β§ πΊ β MetSp β§ βπ₯ β π βπ¦ β π (π₯π·π¦) = (πβ(π₯ β π¦)))) |
39 | 6, 38 | bitri 274 |
1
β’ (πΊ β NrmGrp β (πΊ β Grp β§ πΊ β MetSp β§
βπ₯ β π βπ¦ β π (π₯π·π¦) = (πβ(π₯ β π¦)))) |