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 2733 |
. . 3
β’ (π· βΎ (π Γ π)) = (π· βΎ (π Γ π)) |
6 | 1, 2, 3, 4, 5 | isngp2 24106 |
. 2
β’ (πΊ β NrmGrp β (πΊ β Grp β§ πΊ β MetSp β§ (π β β ) = (π· βΎ (π Γ π)))) |
7 | 4, 3 | msmet2 23966 |
. . . . . . . . 9
β’ (πΊ β MetSp β (π· βΎ (π Γ π)) β (Metβπ)) |
8 | 1, 4, 3, 5 | nmf2 24102 |
. . . . . . . . 9
β’ ((πΊ β Grp β§ (π· βΎ (π Γ π)) β (Metβπ)) β π:πβΆβ) |
9 | 7, 8 | sylan2 594 |
. . . . . . . 8
β’ ((πΊ β Grp β§ πΊ β MetSp) β π:πβΆβ) |
10 | 4, 2 | grpsubf 18902 |
. . . . . . . . 9
β’ (πΊ β Grp β β :(π Γ π)βΆπ) |
11 | 10 | adantr 482 |
. . . . . . . 8
β’ ((πΊ β Grp β§ πΊ β MetSp) β β :(π Γ π)βΆπ) |
12 | | fco 6742 |
. . . . . . . 8
β’ ((π:πβΆβ β§ β :(π Γ π)βΆπ) β (π β β ):(π Γ π)βΆβ) |
13 | 9, 11, 12 | syl2anc 585 |
. . . . . . 7
β’ ((πΊ β Grp β§ πΊ β MetSp) β (π β β ):(π Γ π)βΆβ) |
14 | 13 | ffnd 6719 |
. . . . . 6
β’ ((πΊ β Grp β§ πΊ β MetSp) β (π β β ) Fn (π Γ π)) |
15 | 7 | adantl 483 |
. . . . . . 7
β’ ((πΊ β Grp β§ πΊ β MetSp) β (π· βΎ (π Γ π)) β (Metβπ)) |
16 | | metf 23836 |
. . . . . . 7
β’ ((π· βΎ (π Γ π)) β (Metβπ) β (π· βΎ (π Γ π)):(π Γ π)βΆβ) |
17 | | ffn 6718 |
. . . . . . 7
β’ ((π· βΎ (π Γ π)):(π Γ π)βΆβ β (π· βΎ (π Γ π)) Fn (π Γ π)) |
18 | 15, 16, 17 | 3syl 18 |
. . . . . 6
β’ ((πΊ β Grp β§ πΊ β MetSp) β (π· βΎ (π Γ π)) Fn (π Γ π)) |
19 | | eqfnov2 7539 |
. . . . . 6
β’ (((π β β ) Fn (π Γ π) β§ (π· βΎ (π Γ π)) Fn (π Γ π)) β ((π β β ) = (π· βΎ (π Γ π)) β βπ₯ β π βπ¦ β π (π₯(π β β )π¦) = (π₯(π· βΎ (π Γ π))π¦))) |
20 | 14, 18, 19 | syl2anc 585 |
. . . . 5
β’ ((πΊ β Grp β§ πΊ β MetSp) β ((π β β ) = (π· βΎ (π Γ π)) β βπ₯ β π βπ¦ β π (π₯(π β β )π¦) = (π₯(π· βΎ (π Γ π))π¦))) |
21 | | opelxpi 5714 |
. . . . . . . . . 10
β’ ((π₯ β π β§ π¦ β π) β β¨π₯, π¦β© β (π Γ π)) |
22 | | fvco3 6991 |
. . . . . . . . . 10
β’ (( β :(π Γ π)βΆπ β§ β¨π₯, π¦β© β (π Γ π)) β ((π β β )ββ¨π₯, π¦β©) = (πβ( β ββ¨π₯, π¦β©))) |
23 | 11, 21, 22 | syl2an 597 |
. . . . . . . . 9
β’ (((πΊ β Grp β§ πΊ β MetSp) β§ (π₯ β π β§ π¦ β π)) β ((π β β )ββ¨π₯, π¦β©) = (πβ( β ββ¨π₯, π¦β©))) |
24 | | df-ov 7412 |
. . . . . . . . 9
β’ (π₯(π β β )π¦) = ((π β β )ββ¨π₯, π¦β©) |
25 | | df-ov 7412 |
. . . . . . . . . 10
β’ (π₯ β π¦) = ( β ββ¨π₯, π¦β©) |
26 | 25 | fveq2i 6895 |
. . . . . . . . 9
β’ (πβ(π₯ β π¦)) = (πβ( β ββ¨π₯, π¦β©)) |
27 | 23, 24, 26 | 3eqtr4g 2798 |
. . . . . . . 8
β’ (((πΊ β Grp β§ πΊ β MetSp) β§ (π₯ β π β§ π¦ β π)) β (π₯(π β β )π¦) = (πβ(π₯ β π¦))) |
28 | | ovres 7573 |
. . . . . . . . 9
β’ ((π₯ β π β§ π¦ β π) β (π₯(π· βΎ (π Γ π))π¦) = (π₯π·π¦)) |
29 | 28 | adantl 483 |
. . . . . . . 8
β’ (((πΊ β Grp β§ πΊ β MetSp) β§ (π₯ β π β§ π¦ β π)) β (π₯(π· βΎ (π Γ π))π¦) = (π₯π·π¦)) |
30 | 27, 29 | eqeq12d 2749 |
. . . . . . 7
β’ (((πΊ β Grp β§ πΊ β MetSp) β§ (π₯ β π β§ π¦ β π)) β ((π₯(π β β )π¦) = (π₯(π· βΎ (π Γ π))π¦) β (πβ(π₯ β π¦)) = (π₯π·π¦))) |
31 | | eqcom 2740 |
. . . . . . 7
β’ ((πβ(π₯ β π¦)) = (π₯π·π¦) β (π₯π·π¦) = (πβ(π₯ β π¦))) |
32 | 30, 31 | bitrdi 287 |
. . . . . 6
β’ (((πΊ β Grp β§ πΊ β MetSp) β§ (π₯ β π β§ π¦ β π)) β ((π₯(π β β )π¦) = (π₯(π· βΎ (π Γ π))π¦) β (π₯π·π¦) = (πβ(π₯ β π¦)))) |
33 | 32 | 2ralbidva 3217 |
. . . . 5
β’ ((πΊ β Grp β§ πΊ β MetSp) β
(βπ₯ β π βπ¦ β π (π₯(π β β )π¦) = (π₯(π· βΎ (π Γ π))π¦) β βπ₯ β π βπ¦ β π (π₯π·π¦) = (πβ(π₯ β π¦)))) |
34 | 20, 33 | bitrd 279 |
. . . 4
β’ ((πΊ β Grp β§ πΊ β MetSp) β ((π β β ) = (π· βΎ (π Γ π)) β βπ₯ β π βπ¦ β π (π₯π·π¦) = (πβ(π₯ β π¦)))) |
35 | 34 | pm5.32i 576 |
. . 3
β’ (((πΊ β Grp β§ πΊ β MetSp) β§ (π β β ) = (π· βΎ (π Γ π))) β ((πΊ β Grp β§ πΊ β MetSp) β§ βπ₯ β π βπ¦ β π (π₯π·π¦) = (πβ(π₯ β π¦)))) |
36 | | df-3an 1090 |
. . 3
β’ ((πΊ β Grp β§ πΊ β MetSp β§ (π β β ) = (π· βΎ (π Γ π))) β ((πΊ β Grp β§ πΊ β MetSp) β§ (π β β ) = (π· βΎ (π Γ π)))) |
37 | | df-3an 1090 |
. . 3
β’ ((πΊ β Grp β§ πΊ β MetSp β§
βπ₯ β π βπ¦ β π (π₯π·π¦) = (πβ(π₯ β π¦))) β ((πΊ β Grp β§ πΊ β MetSp) β§ βπ₯ β π βπ¦ β π (π₯π·π¦) = (πβ(π₯ β π¦)))) |
38 | 35, 36, 37 | 3bitr4i 303 |
. 2
β’ ((πΊ β Grp β§ πΊ β MetSp β§ (π β β ) = (π· βΎ (π Γ π))) β (πΊ β Grp β§ πΊ β MetSp β§ βπ₯ β π βπ¦ β π (π₯π·π¦) = (πβ(π₯ β π¦)))) |
39 | 6, 38 | bitri 275 |
1
β’ (πΊ β NrmGrp β (πΊ β Grp β§ πΊ β MetSp β§
βπ₯ β π βπ¦ β π (π₯π·π¦) = (πβ(π₯ β π¦)))) |