Step | Hyp | Ref
| Expression |
1 | | tngngp.t |
. . . . 5
β’ π = (πΊ toNrmGrp π) |
2 | | tngngp.x |
. . . . 5
β’ π = (BaseβπΊ) |
3 | | eqid 2737 |
. . . . 5
β’
(distβπ) =
(distβπ) |
4 | 1, 2, 3 | tngngp2 24032 |
. . . 4
β’ (π:πβΆβ β (π β NrmGrp β (πΊ β Grp β§ (distβπ) β (Metβπ)))) |
5 | 4 | simprbda 500 |
. . 3
β’ ((π:πβΆβ β§ π β NrmGrp) β πΊ β Grp) |
6 | | simplr 768 |
. . . . . . 7
β’ (((π:πβΆβ β§ π β NrmGrp) β§ π₯ β π) β π β NrmGrp) |
7 | | simpr 486 |
. . . . . . . 8
β’ (((π:πβΆβ β§ π β NrmGrp) β§ π₯ β π) β π₯ β π) |
8 | 2 | fvexi 6861 |
. . . . . . . . . . 11
β’ π β V |
9 | | reex 11149 |
. . . . . . . . . . 11
β’ β
β V |
10 | | fex2 7875 |
. . . . . . . . . . 11
β’ ((π:πβΆβ β§ π β V β§ β β V) β
π β
V) |
11 | 8, 9, 10 | mp3an23 1454 |
. . . . . . . . . 10
β’ (π:πβΆβ β π β V) |
12 | 11 | ad2antrr 725 |
. . . . . . . . 9
β’ (((π:πβΆβ β§ π β NrmGrp) β§ π₯ β π) β π β V) |
13 | 1, 2 | tngbas 24014 |
. . . . . . . . 9
β’ (π β V β π = (Baseβπ)) |
14 | 12, 13 | syl 17 |
. . . . . . . 8
β’ (((π:πβΆβ β§ π β NrmGrp) β§ π₯ β π) β π = (Baseβπ)) |
15 | 7, 14 | eleqtrd 2840 |
. . . . . . 7
β’ (((π:πβΆβ β§ π β NrmGrp) β§ π₯ β π) β π₯ β (Baseβπ)) |
16 | | eqid 2737 |
. . . . . . . 8
β’
(Baseβπ) =
(Baseβπ) |
17 | | eqid 2737 |
. . . . . . . 8
β’
(normβπ) =
(normβπ) |
18 | | eqid 2737 |
. . . . . . . 8
β’
(0gβπ) = (0gβπ) |
19 | 16, 17, 18 | nmeq0 23990 |
. . . . . . 7
β’ ((π β NrmGrp β§ π₯ β (Baseβπ)) β (((normβπ)βπ₯) = 0 β π₯ = (0gβπ))) |
20 | 6, 15, 19 | syl2anc 585 |
. . . . . 6
β’ (((π:πβΆβ β§ π β NrmGrp) β§ π₯ β π) β (((normβπ)βπ₯) = 0 β π₯ = (0gβπ))) |
21 | 5 | adantr 482 |
. . . . . . . . 9
β’ (((π:πβΆβ β§ π β NrmGrp) β§ π₯ β π) β πΊ β Grp) |
22 | | simpll 766 |
. . . . . . . . 9
β’ (((π:πβΆβ β§ π β NrmGrp) β§ π₯ β π) β π:πβΆβ) |
23 | 1, 2, 9 | tngnm 24031 |
. . . . . . . . 9
β’ ((πΊ β Grp β§ π:πβΆβ) β π = (normβπ)) |
24 | 21, 22, 23 | syl2anc 585 |
. . . . . . . 8
β’ (((π:πβΆβ β§ π β NrmGrp) β§ π₯ β π) β π = (normβπ)) |
25 | 24 | fveq1d 6849 |
. . . . . . 7
β’ (((π:πβΆβ β§ π β NrmGrp) β§ π₯ β π) β (πβπ₯) = ((normβπ)βπ₯)) |
26 | 25 | eqeq1d 2739 |
. . . . . 6
β’ (((π:πβΆβ β§ π β NrmGrp) β§ π₯ β π) β ((πβπ₯) = 0 β ((normβπ)βπ₯) = 0)) |
27 | | tngngp.z |
. . . . . . . . 9
β’ 0 =
(0gβπΊ) |
28 | 1, 27 | tng0 24018 |
. . . . . . . 8
β’ (π β V β 0 =
(0gβπ)) |
29 | 12, 28 | syl 17 |
. . . . . . 7
β’ (((π:πβΆβ β§ π β NrmGrp) β§ π₯ β π) β 0 =
(0gβπ)) |
30 | 29 | eqeq2d 2748 |
. . . . . 6
β’ (((π:πβΆβ β§ π β NrmGrp) β§ π₯ β π) β (π₯ = 0 β π₯ = (0gβπ))) |
31 | 20, 26, 30 | 3bitr4d 311 |
. . . . 5
β’ (((π:πβΆβ β§ π β NrmGrp) β§ π₯ β π) β ((πβπ₯) = 0 β π₯ = 0 )) |
32 | | simpllr 775 |
. . . . . . . 8
β’ ((((π:πβΆβ β§ π β NrmGrp) β§ π₯ β π) β§ π¦ β π) β π β NrmGrp) |
33 | 15 | adantr 482 |
. . . . . . . 8
β’ ((((π:πβΆβ β§ π β NrmGrp) β§ π₯ β π) β§ π¦ β π) β π₯ β (Baseβπ)) |
34 | 14 | eleq2d 2824 |
. . . . . . . . 9
β’ (((π:πβΆβ β§ π β NrmGrp) β§ π₯ β π) β (π¦ β π β π¦ β (Baseβπ))) |
35 | 34 | biimpa 478 |
. . . . . . . 8
β’ ((((π:πβΆβ β§ π β NrmGrp) β§ π₯ β π) β§ π¦ β π) β π¦ β (Baseβπ)) |
36 | | eqid 2737 |
. . . . . . . . 9
β’
(-gβπ) = (-gβπ) |
37 | 16, 17, 36 | nmmtri 23994 |
. . . . . . . 8
β’ ((π β NrmGrp β§ π₯ β (Baseβπ) β§ π¦ β (Baseβπ)) β ((normβπ)β(π₯(-gβπ)π¦)) β€ (((normβπ)βπ₯) + ((normβπ)βπ¦))) |
38 | 32, 33, 35, 37 | syl3anc 1372 |
. . . . . . 7
β’ ((((π:πβΆβ β§ π β NrmGrp) β§ π₯ β π) β§ π¦ β π) β ((normβπ)β(π₯(-gβπ)π¦)) β€ (((normβπ)βπ₯) + ((normβπ)βπ¦))) |
39 | | tngngp.m |
. . . . . . . . . . 11
β’ β =
(-gβπΊ) |
40 | 2, 14 | eqtr3id 2791 |
. . . . . . . . . . . 12
β’ (((π:πβΆβ β§ π β NrmGrp) β§ π₯ β π) β (BaseβπΊ) = (Baseβπ)) |
41 | | eqid 2737 |
. . . . . . . . . . . . . 14
β’
(+gβπΊ) = (+gβπΊ) |
42 | 1, 41 | tngplusg 24016 |
. . . . . . . . . . . . 13
β’ (π β V β
(+gβπΊ) =
(+gβπ)) |
43 | 12, 42 | syl 17 |
. . . . . . . . . . . 12
β’ (((π:πβΆβ β§ π β NrmGrp) β§ π₯ β π) β (+gβπΊ) = (+gβπ)) |
44 | 40, 43 | grpsubpropd 18859 |
. . . . . . . . . . 11
β’ (((π:πβΆβ β§ π β NrmGrp) β§ π₯ β π) β (-gβπΊ) = (-gβπ)) |
45 | 39, 44 | eqtrid 2789 |
. . . . . . . . . 10
β’ (((π:πβΆβ β§ π β NrmGrp) β§ π₯ β π) β β =
(-gβπ)) |
46 | 45 | oveqd 7379 |
. . . . . . . . 9
β’ (((π:πβΆβ β§ π β NrmGrp) β§ π₯ β π) β (π₯ β π¦) = (π₯(-gβπ)π¦)) |
47 | 24, 46 | fveq12d 6854 |
. . . . . . . 8
β’ (((π:πβΆβ β§ π β NrmGrp) β§ π₯ β π) β (πβ(π₯ β π¦)) = ((normβπ)β(π₯(-gβπ)π¦))) |
48 | 47 | adantr 482 |
. . . . . . 7
β’ ((((π:πβΆβ β§ π β NrmGrp) β§ π₯ β π) β§ π¦ β π) β (πβ(π₯ β π¦)) = ((normβπ)β(π₯(-gβπ)π¦))) |
49 | 24 | fveq1d 6849 |
. . . . . . . . 9
β’ (((π:πβΆβ β§ π β NrmGrp) β§ π₯ β π) β (πβπ¦) = ((normβπ)βπ¦)) |
50 | 25, 49 | oveq12d 7380 |
. . . . . . . 8
β’ (((π:πβΆβ β§ π β NrmGrp) β§ π₯ β π) β ((πβπ₯) + (πβπ¦)) = (((normβπ)βπ₯) + ((normβπ)βπ¦))) |
51 | 50 | adantr 482 |
. . . . . . 7
β’ ((((π:πβΆβ β§ π β NrmGrp) β§ π₯ β π) β§ π¦ β π) β ((πβπ₯) + (πβπ¦)) = (((normβπ)βπ₯) + ((normβπ)βπ¦))) |
52 | 38, 48, 51 | 3brtr4d 5142 |
. . . . . 6
β’ ((((π:πβΆβ β§ π β NrmGrp) β§ π₯ β π) β§ π¦ β π) β (πβ(π₯ β π¦)) β€ ((πβπ₯) + (πβπ¦))) |
53 | 52 | ralrimiva 3144 |
. . . . 5
β’ (((π:πβΆβ β§ π β NrmGrp) β§ π₯ β π) β βπ¦ β π (πβ(π₯ β π¦)) β€ ((πβπ₯) + (πβπ¦))) |
54 | 31, 53 | jca 513 |
. . . 4
β’ (((π:πβΆβ β§ π β NrmGrp) β§ π₯ β π) β (((πβπ₯) = 0 β π₯ = 0 ) β§ βπ¦ β π (πβ(π₯ β π¦)) β€ ((πβπ₯) + (πβπ¦)))) |
55 | 54 | ralrimiva 3144 |
. . 3
β’ ((π:πβΆβ β§ π β NrmGrp) β βπ₯ β π (((πβπ₯) = 0 β π₯ = 0 ) β§ βπ¦ β π (πβ(π₯ β π¦)) β€ ((πβπ₯) + (πβπ¦)))) |
56 | 5, 55 | jca 513 |
. 2
β’ ((π:πβΆβ β§ π β NrmGrp) β (πΊ β Grp β§ βπ₯ β π (((πβπ₯) = 0 β π₯ = 0 ) β§ βπ¦ β π (πβ(π₯ β π¦)) β€ ((πβπ₯) + (πβπ¦))))) |
57 | | simprl 770 |
. . 3
β’ ((π:πβΆβ β§ (πΊ β Grp β§ βπ₯ β π (((πβπ₯) = 0 β π₯ = 0 ) β§ βπ¦ β π (πβ(π₯ β π¦)) β€ ((πβπ₯) + (πβπ¦))))) β πΊ β Grp) |
58 | | simpl 484 |
. . 3
β’ ((π:πβΆβ β§ (πΊ β Grp β§ βπ₯ β π (((πβπ₯) = 0 β π₯ = 0 ) β§ βπ¦ β π (πβ(π₯ β π¦)) β€ ((πβπ₯) + (πβπ¦))))) β π:πβΆβ) |
59 | | simpl 484 |
. . . . . 6
β’ ((((πβπ₯) = 0 β π₯ = 0 ) β§ βπ¦ β π (πβ(π₯ β π¦)) β€ ((πβπ₯) + (πβπ¦))) β ((πβπ₯) = 0 β π₯ = 0 )) |
60 | 59 | ralimi 3087 |
. . . . 5
β’
(βπ₯ β
π (((πβπ₯) = 0 β π₯ = 0 ) β§ βπ¦ β π (πβ(π₯ β π¦)) β€ ((πβπ₯) + (πβπ¦))) β βπ₯ β π ((πβπ₯) = 0 β π₯ = 0 )) |
61 | 60 | ad2antll 728 |
. . . 4
β’ ((π:πβΆβ β§ (πΊ β Grp β§ βπ₯ β π (((πβπ₯) = 0 β π₯ = 0 ) β§ βπ¦ β π (πβ(π₯ β π¦)) β€ ((πβπ₯) + (πβπ¦))))) β βπ₯ β π ((πβπ₯) = 0 β π₯ = 0 )) |
62 | | fveq2 6847 |
. . . . . . 7
β’ (π₯ = π β (πβπ₯) = (πβπ)) |
63 | 62 | eqeq1d 2739 |
. . . . . 6
β’ (π₯ = π β ((πβπ₯) = 0 β (πβπ) = 0)) |
64 | | eqeq1 2741 |
. . . . . 6
β’ (π₯ = π β (π₯ = 0 β π = 0 )) |
65 | 63, 64 | bibi12d 346 |
. . . . 5
β’ (π₯ = π β (((πβπ₯) = 0 β π₯ = 0 ) β ((πβπ) = 0 β π = 0 ))) |
66 | 65 | rspccva 3583 |
. . . 4
β’
((βπ₯ β
π ((πβπ₯) = 0 β π₯ = 0 ) β§ π β π) β ((πβπ) = 0 β π = 0 )) |
67 | 61, 66 | sylan 581 |
. . 3
β’ (((π:πβΆβ β§ (πΊ β Grp β§ βπ₯ β π (((πβπ₯) = 0 β π₯ = 0 ) β§ βπ¦ β π (πβ(π₯ β π¦)) β€ ((πβπ₯) + (πβπ¦))))) β§ π β π) β ((πβπ) = 0 β π = 0 )) |
68 | | simpr 486 |
. . . . . 6
β’ ((((πβπ₯) = 0 β π₯ = 0 ) β§ βπ¦ β π (πβ(π₯ β π¦)) β€ ((πβπ₯) + (πβπ¦))) β βπ¦ β π (πβ(π₯ β π¦)) β€ ((πβπ₯) + (πβπ¦))) |
69 | 68 | ralimi 3087 |
. . . . 5
β’
(βπ₯ β
π (((πβπ₯) = 0 β π₯ = 0 ) β§ βπ¦ β π (πβ(π₯ β π¦)) β€ ((πβπ₯) + (πβπ¦))) β βπ₯ β π βπ¦ β π (πβ(π₯ β π¦)) β€ ((πβπ₯) + (πβπ¦))) |
70 | 69 | ad2antll 728 |
. . . 4
β’ ((π:πβΆβ β§ (πΊ β Grp β§ βπ₯ β π (((πβπ₯) = 0 β π₯ = 0 ) β§ βπ¦ β π (πβ(π₯ β π¦)) β€ ((πβπ₯) + (πβπ¦))))) β βπ₯ β π βπ¦ β π (πβ(π₯ β π¦)) β€ ((πβπ₯) + (πβπ¦))) |
71 | | fvoveq1 7385 |
. . . . . . 7
β’ (π₯ = π β (πβ(π₯ β π¦)) = (πβ(π β π¦))) |
72 | 62 | oveq1d 7377 |
. . . . . . 7
β’ (π₯ = π β ((πβπ₯) + (πβπ¦)) = ((πβπ) + (πβπ¦))) |
73 | 71, 72 | breq12d 5123 |
. . . . . 6
β’ (π₯ = π β ((πβ(π₯ β π¦)) β€ ((πβπ₯) + (πβπ¦)) β (πβ(π β π¦)) β€ ((πβπ) + (πβπ¦)))) |
74 | | oveq2 7370 |
. . . . . . . 8
β’ (π¦ = π β (π β π¦) = (π β π)) |
75 | 74 | fveq2d 6851 |
. . . . . . 7
β’ (π¦ = π β (πβ(π β π¦)) = (πβ(π β π))) |
76 | | fveq2 6847 |
. . . . . . . 8
β’ (π¦ = π β (πβπ¦) = (πβπ)) |
77 | 76 | oveq2d 7378 |
. . . . . . 7
β’ (π¦ = π β ((πβπ) + (πβπ¦)) = ((πβπ) + (πβπ))) |
78 | 75, 77 | breq12d 5123 |
. . . . . 6
β’ (π¦ = π β ((πβ(π β π¦)) β€ ((πβπ) + (πβπ¦)) β (πβ(π β π)) β€ ((πβπ) + (πβπ)))) |
79 | 73, 78 | rspc2va 3594 |
. . . . 5
β’ (((π β π β§ π β π) β§ βπ₯ β π βπ¦ β π (πβ(π₯ β π¦)) β€ ((πβπ₯) + (πβπ¦))) β (πβ(π β π)) β€ ((πβπ) + (πβπ))) |
80 | 79 | ancoms 460 |
. . . 4
β’
((βπ₯ β
π βπ¦ β π (πβ(π₯ β π¦)) β€ ((πβπ₯) + (πβπ¦)) β§ (π β π β§ π β π)) β (πβ(π β π)) β€ ((πβπ) + (πβπ))) |
81 | 70, 80 | sylan 581 |
. . 3
β’ (((π:πβΆβ β§ (πΊ β Grp β§ βπ₯ β π (((πβπ₯) = 0 β π₯ = 0 ) β§ βπ¦ β π (πβ(π₯ β π¦)) β€ ((πβπ₯) + (πβπ¦))))) β§ (π β π β§ π β π)) β (πβ(π β π)) β€ ((πβπ) + (πβπ))) |
82 | 1, 2, 39, 27, 57, 58, 67, 81 | tngngpd 24033 |
. 2
β’ ((π:πβΆβ β§ (πΊ β Grp β§ βπ₯ β π (((πβπ₯) = 0 β π₯ = 0 ) β§ βπ¦ β π (πβ(π₯ β π¦)) β€ ((πβπ₯) + (πβπ¦))))) β π β NrmGrp) |
83 | 56, 82 | impbida 800 |
1
β’ (π:πβΆβ β (π β NrmGrp β (πΊ β Grp β§ βπ₯ β π (((πβπ₯) = 0 β π₯ = 0 ) β§ βπ¦ β π (πβ(π₯ β π¦)) β€ ((πβπ₯) + (πβπ¦)))))) |