Step | Hyp | Ref
| Expression |
1 | | tngngp.t |
. . . . 5
β’ π = (πΊ toNrmGrp π) |
2 | | tngngp.x |
. . . . 5
β’ π = (BaseβπΊ) |
3 | | eqid 2732 |
. . . . 5
β’
(distβπ) =
(distβπ) |
4 | 1, 2, 3 | tngngp2 24160 |
. . . 4
β’ (π:πβΆβ β (π β NrmGrp β (πΊ β Grp β§ (distβπ) β (Metβπ)))) |
5 | 4 | simprbda 499 |
. . 3
β’ ((π:πβΆβ β§ π β NrmGrp) β πΊ β Grp) |
6 | | simplr 767 |
. . . . . . 7
β’ (((π:πβΆβ β§ π β NrmGrp) β§ π₯ β π) β π β NrmGrp) |
7 | | simpr 485 |
. . . . . . . 8
β’ (((π:πβΆβ β§ π β NrmGrp) β§ π₯ β π) β π₯ β π) |
8 | 2 | fvexi 6902 |
. . . . . . . . . . 11
β’ π β V |
9 | | reex 11197 |
. . . . . . . . . . 11
β’ β
β V |
10 | | fex2 7920 |
. . . . . . . . . . 11
β’ ((π:πβΆβ β§ π β V β§ β β V) β
π β
V) |
11 | 8, 9, 10 | mp3an23 1453 |
. . . . . . . . . 10
β’ (π:πβΆβ β π β V) |
12 | 11 | ad2antrr 724 |
. . . . . . . . 9
β’ (((π:πβΆβ β§ π β NrmGrp) β§ π₯ β π) β π β V) |
13 | 1, 2 | tngbas 24142 |
. . . . . . . . 9
β’ (π β V β π = (Baseβπ)) |
14 | 12, 13 | syl 17 |
. . . . . . . 8
β’ (((π:πβΆβ β§ π β NrmGrp) β§ π₯ β π) β π = (Baseβπ)) |
15 | 7, 14 | eleqtrd 2835 |
. . . . . . 7
β’ (((π:πβΆβ β§ π β NrmGrp) β§ π₯ β π) β π₯ β (Baseβπ)) |
16 | | eqid 2732 |
. . . . . . . 8
β’
(Baseβπ) =
(Baseβπ) |
17 | | eqid 2732 |
. . . . . . . 8
β’
(normβπ) =
(normβπ) |
18 | | eqid 2732 |
. . . . . . . 8
β’
(0gβπ) = (0gβπ) |
19 | 16, 17, 18 | nmeq0 24118 |
. . . . . . 7
β’ ((π β NrmGrp β§ π₯ β (Baseβπ)) β (((normβπ)βπ₯) = 0 β π₯ = (0gβπ))) |
20 | 6, 15, 19 | syl2anc 584 |
. . . . . 6
β’ (((π:πβΆβ β§ π β NrmGrp) β§ π₯ β π) β (((normβπ)βπ₯) = 0 β π₯ = (0gβπ))) |
21 | 5 | adantr 481 |
. . . . . . . . 9
β’ (((π:πβΆβ β§ π β NrmGrp) β§ π₯ β π) β πΊ β Grp) |
22 | | simpll 765 |
. . . . . . . . 9
β’ (((π:πβΆβ β§ π β NrmGrp) β§ π₯ β π) β π:πβΆβ) |
23 | 1, 2, 9 | tngnm 24159 |
. . . . . . . . 9
β’ ((πΊ β Grp β§ π:πβΆβ) β π = (normβπ)) |
24 | 21, 22, 23 | syl2anc 584 |
. . . . . . . 8
β’ (((π:πβΆβ β§ π β NrmGrp) β§ π₯ β π) β π = (normβπ)) |
25 | 24 | fveq1d 6890 |
. . . . . . 7
β’ (((π:πβΆβ β§ π β NrmGrp) β§ π₯ β π) β (πβπ₯) = ((normβπ)βπ₯)) |
26 | 25 | eqeq1d 2734 |
. . . . . 6
β’ (((π:πβΆβ β§ π β NrmGrp) β§ π₯ β π) β ((πβπ₯) = 0 β ((normβπ)βπ₯) = 0)) |
27 | | tngngp.z |
. . . . . . . . 9
β’ 0 =
(0gβπΊ) |
28 | 1, 27 | tng0 24146 |
. . . . . . . 8
β’ (π β V β 0 =
(0gβπ)) |
29 | 12, 28 | syl 17 |
. . . . . . 7
β’ (((π:πβΆβ β§ π β NrmGrp) β§ π₯ β π) β 0 =
(0gβπ)) |
30 | 29 | eqeq2d 2743 |
. . . . . 6
β’ (((π:πβΆβ β§ π β NrmGrp) β§ π₯ β π) β (π₯ = 0 β π₯ = (0gβπ))) |
31 | 20, 26, 30 | 3bitr4d 310 |
. . . . 5
β’ (((π:πβΆβ β§ π β NrmGrp) β§ π₯ β π) β ((πβπ₯) = 0 β π₯ = 0 )) |
32 | | simpllr 774 |
. . . . . . . 8
β’ ((((π:πβΆβ β§ π β NrmGrp) β§ π₯ β π) β§ π¦ β π) β π β NrmGrp) |
33 | 15 | adantr 481 |
. . . . . . . 8
β’ ((((π:πβΆβ β§ π β NrmGrp) β§ π₯ β π) β§ π¦ β π) β π₯ β (Baseβπ)) |
34 | 14 | eleq2d 2819 |
. . . . . . . . 9
β’ (((π:πβΆβ β§ π β NrmGrp) β§ π₯ β π) β (π¦ β π β π¦ β (Baseβπ))) |
35 | 34 | biimpa 477 |
. . . . . . . 8
β’ ((((π:πβΆβ β§ π β NrmGrp) β§ π₯ β π) β§ π¦ β π) β π¦ β (Baseβπ)) |
36 | | eqid 2732 |
. . . . . . . . 9
β’
(-gβπ) = (-gβπ) |
37 | 16, 17, 36 | nmmtri 24122 |
. . . . . . . 8
β’ ((π β NrmGrp β§ π₯ β (Baseβπ) β§ π¦ β (Baseβπ)) β ((normβπ)β(π₯(-gβπ)π¦)) β€ (((normβπ)βπ₯) + ((normβπ)βπ¦))) |
38 | 32, 33, 35, 37 | syl3anc 1371 |
. . . . . . 7
β’ ((((π:πβΆβ β§ π β NrmGrp) β§ π₯ β π) β§ π¦ β π) β ((normβπ)β(π₯(-gβπ)π¦)) β€ (((normβπ)βπ₯) + ((normβπ)βπ¦))) |
39 | | tngngp.m |
. . . . . . . . . . 11
β’ β =
(-gβπΊ) |
40 | 2, 14 | eqtr3id 2786 |
. . . . . . . . . . . 12
β’ (((π:πβΆβ β§ π β NrmGrp) β§ π₯ β π) β (BaseβπΊ) = (Baseβπ)) |
41 | | eqid 2732 |
. . . . . . . . . . . . . 14
β’
(+gβπΊ) = (+gβπΊ) |
42 | 1, 41 | tngplusg 24144 |
. . . . . . . . . . . . 13
β’ (π β V β
(+gβπΊ) =
(+gβπ)) |
43 | 12, 42 | syl 17 |
. . . . . . . . . . . 12
β’ (((π:πβΆβ β§ π β NrmGrp) β§ π₯ β π) β (+gβπΊ) = (+gβπ)) |
44 | 40, 43 | grpsubpropd 18924 |
. . . . . . . . . . 11
β’ (((π:πβΆβ β§ π β NrmGrp) β§ π₯ β π) β (-gβπΊ) = (-gβπ)) |
45 | 39, 44 | eqtrid 2784 |
. . . . . . . . . 10
β’ (((π:πβΆβ β§ π β NrmGrp) β§ π₯ β π) β β =
(-gβπ)) |
46 | 45 | oveqd 7422 |
. . . . . . . . 9
β’ (((π:πβΆβ β§ π β NrmGrp) β§ π₯ β π) β (π₯ β π¦) = (π₯(-gβπ)π¦)) |
47 | 24, 46 | fveq12d 6895 |
. . . . . . . 8
β’ (((π:πβΆβ β§ π β NrmGrp) β§ π₯ β π) β (πβ(π₯ β π¦)) = ((normβπ)β(π₯(-gβπ)π¦))) |
48 | 47 | adantr 481 |
. . . . . . 7
β’ ((((π:πβΆβ β§ π β NrmGrp) β§ π₯ β π) β§ π¦ β π) β (πβ(π₯ β π¦)) = ((normβπ)β(π₯(-gβπ)π¦))) |
49 | 24 | fveq1d 6890 |
. . . . . . . . 9
β’ (((π:πβΆβ β§ π β NrmGrp) β§ π₯ β π) β (πβπ¦) = ((normβπ)βπ¦)) |
50 | 25, 49 | oveq12d 7423 |
. . . . . . . 8
β’ (((π:πβΆβ β§ π β NrmGrp) β§ π₯ β π) β ((πβπ₯) + (πβπ¦)) = (((normβπ)βπ₯) + ((normβπ)βπ¦))) |
51 | 50 | adantr 481 |
. . . . . . 7
β’ ((((π:πβΆβ β§ π β NrmGrp) β§ π₯ β π) β§ π¦ β π) β ((πβπ₯) + (πβπ¦)) = (((normβπ)βπ₯) + ((normβπ)βπ¦))) |
52 | 38, 48, 51 | 3brtr4d 5179 |
. . . . . 6
β’ ((((π:πβΆβ β§ π β NrmGrp) β§ π₯ β π) β§ π¦ β π) β (πβ(π₯ β π¦)) β€ ((πβπ₯) + (πβπ¦))) |
53 | 52 | ralrimiva 3146 |
. . . . 5
β’ (((π:πβΆβ β§ π β NrmGrp) β§ π₯ β π) β βπ¦ β π (πβ(π₯ β π¦)) β€ ((πβπ₯) + (πβπ¦))) |
54 | 31, 53 | jca 512 |
. . . 4
β’ (((π:πβΆβ β§ π β NrmGrp) β§ π₯ β π) β (((πβπ₯) = 0 β π₯ = 0 ) β§ βπ¦ β π (πβ(π₯ β π¦)) β€ ((πβπ₯) + (πβπ¦)))) |
55 | 54 | ralrimiva 3146 |
. . 3
β’ ((π:πβΆβ β§ π β NrmGrp) β βπ₯ β π (((πβπ₯) = 0 β π₯ = 0 ) β§ βπ¦ β π (πβ(π₯ β π¦)) β€ ((πβπ₯) + (πβπ¦)))) |
56 | 5, 55 | jca 512 |
. 2
β’ ((π:πβΆβ β§ π β NrmGrp) β (πΊ β Grp β§ βπ₯ β π (((πβπ₯) = 0 β π₯ = 0 ) β§ βπ¦ β π (πβ(π₯ β π¦)) β€ ((πβπ₯) + (πβπ¦))))) |
57 | | simprl 769 |
. . 3
β’ ((π:πβΆβ β§ (πΊ β Grp β§ βπ₯ β π (((πβπ₯) = 0 β π₯ = 0 ) β§ βπ¦ β π (πβ(π₯ β π¦)) β€ ((πβπ₯) + (πβπ¦))))) β πΊ β Grp) |
58 | | simpl 483 |
. . 3
β’ ((π:πβΆβ β§ (πΊ β Grp β§ βπ₯ β π (((πβπ₯) = 0 β π₯ = 0 ) β§ βπ¦ β π (πβ(π₯ β π¦)) β€ ((πβπ₯) + (πβπ¦))))) β π:πβΆβ) |
59 | | simpl 483 |
. . . . . 6
β’ ((((πβπ₯) = 0 β π₯ = 0 ) β§ βπ¦ β π (πβ(π₯ β π¦)) β€ ((πβπ₯) + (πβπ¦))) β ((πβπ₯) = 0 β π₯ = 0 )) |
60 | 59 | ralimi 3083 |
. . . . 5
β’
(βπ₯ β
π (((πβπ₯) = 0 β π₯ = 0 ) β§ βπ¦ β π (πβ(π₯ β π¦)) β€ ((πβπ₯) + (πβπ¦))) β βπ₯ β π ((πβπ₯) = 0 β π₯ = 0 )) |
61 | 60 | ad2antll 727 |
. . . 4
β’ ((π:πβΆβ β§ (πΊ β Grp β§ βπ₯ β π (((πβπ₯) = 0 β π₯ = 0 ) β§ βπ¦ β π (πβ(π₯ β π¦)) β€ ((πβπ₯) + (πβπ¦))))) β βπ₯ β π ((πβπ₯) = 0 β π₯ = 0 )) |
62 | | fveq2 6888 |
. . . . . . 7
β’ (π₯ = π β (πβπ₯) = (πβπ)) |
63 | 62 | eqeq1d 2734 |
. . . . . 6
β’ (π₯ = π β ((πβπ₯) = 0 β (πβπ) = 0)) |
64 | | eqeq1 2736 |
. . . . . 6
β’ (π₯ = π β (π₯ = 0 β π = 0 )) |
65 | 63, 64 | bibi12d 345 |
. . . . 5
β’ (π₯ = π β (((πβπ₯) = 0 β π₯ = 0 ) β ((πβπ) = 0 β π = 0 ))) |
66 | 65 | rspccva 3611 |
. . . 4
β’
((βπ₯ β
π ((πβπ₯) = 0 β π₯ = 0 ) β§ π β π) β ((πβπ) = 0 β π = 0 )) |
67 | 61, 66 | sylan 580 |
. . 3
β’ (((π:πβΆβ β§ (πΊ β Grp β§ βπ₯ β π (((πβπ₯) = 0 β π₯ = 0 ) β§ βπ¦ β π (πβ(π₯ β π¦)) β€ ((πβπ₯) + (πβπ¦))))) β§ π β π) β ((πβπ) = 0 β π = 0 )) |
68 | | simpr 485 |
. . . . . 6
β’ ((((πβπ₯) = 0 β π₯ = 0 ) β§ βπ¦ β π (πβ(π₯ β π¦)) β€ ((πβπ₯) + (πβπ¦))) β βπ¦ β π (πβ(π₯ β π¦)) β€ ((πβπ₯) + (πβπ¦))) |
69 | 68 | ralimi 3083 |
. . . . 5
β’
(βπ₯ β
π (((πβπ₯) = 0 β π₯ = 0 ) β§ βπ¦ β π (πβ(π₯ β π¦)) β€ ((πβπ₯) + (πβπ¦))) β βπ₯ β π βπ¦ β π (πβ(π₯ β π¦)) β€ ((πβπ₯) + (πβπ¦))) |
70 | 69 | ad2antll 727 |
. . . 4
β’ ((π:πβΆβ β§ (πΊ β Grp β§ βπ₯ β π (((πβπ₯) = 0 β π₯ = 0 ) β§ βπ¦ β π (πβ(π₯ β π¦)) β€ ((πβπ₯) + (πβπ¦))))) β βπ₯ β π βπ¦ β π (πβ(π₯ β π¦)) β€ ((πβπ₯) + (πβπ¦))) |
71 | | fvoveq1 7428 |
. . . . . . 7
β’ (π₯ = π β (πβ(π₯ β π¦)) = (πβ(π β π¦))) |
72 | 62 | oveq1d 7420 |
. . . . . . 7
β’ (π₯ = π β ((πβπ₯) + (πβπ¦)) = ((πβπ) + (πβπ¦))) |
73 | 71, 72 | breq12d 5160 |
. . . . . 6
β’ (π₯ = π β ((πβ(π₯ β π¦)) β€ ((πβπ₯) + (πβπ¦)) β (πβ(π β π¦)) β€ ((πβπ) + (πβπ¦)))) |
74 | | oveq2 7413 |
. . . . . . . 8
β’ (π¦ = π β (π β π¦) = (π β π)) |
75 | 74 | fveq2d 6892 |
. . . . . . 7
β’ (π¦ = π β (πβ(π β π¦)) = (πβ(π β π))) |
76 | | fveq2 6888 |
. . . . . . . 8
β’ (π¦ = π β (πβπ¦) = (πβπ)) |
77 | 76 | oveq2d 7421 |
. . . . . . 7
β’ (π¦ = π β ((πβπ) + (πβπ¦)) = ((πβπ) + (πβπ))) |
78 | 75, 77 | breq12d 5160 |
. . . . . 6
β’ (π¦ = π β ((πβ(π β π¦)) β€ ((πβπ) + (πβπ¦)) β (πβ(π β π)) β€ ((πβπ) + (πβπ)))) |
79 | 73, 78 | rspc2va 3622 |
. . . . 5
β’ (((π β π β§ π β π) β§ βπ₯ β π βπ¦ β π (πβ(π₯ β π¦)) β€ ((πβπ₯) + (πβπ¦))) β (πβ(π β π)) β€ ((πβπ) + (πβπ))) |
80 | 79 | ancoms 459 |
. . . 4
β’
((βπ₯ β
π βπ¦ β π (πβ(π₯ β π¦)) β€ ((πβπ₯) + (πβπ¦)) β§ (π β π β§ π β π)) β (πβ(π β π)) β€ ((πβπ) + (πβπ))) |
81 | 70, 80 | sylan 580 |
. . 3
β’ (((π:πβΆβ β§ (πΊ β Grp β§ βπ₯ β π (((πβπ₯) = 0 β π₯ = 0 ) β§ βπ¦ β π (πβ(π₯ β π¦)) β€ ((πβπ₯) + (πβπ¦))))) β§ (π β π β§ π β π)) β (πβ(π β π)) β€ ((πβπ) + (πβπ))) |
82 | 1, 2, 39, 27, 57, 58, 67, 81 | tngngpd 24161 |
. 2
β’ ((π:πβΆβ β§ (πΊ β Grp β§ βπ₯ β π (((πβπ₯) = 0 β π₯ = 0 ) β§ βπ¦ β π (πβ(π₯ β π¦)) β€ ((πβπ₯) + (πβπ¦))))) β π β NrmGrp) |
83 | 56, 82 | impbida 799 |
1
β’ (π:πβΆβ β (π β NrmGrp β (πΊ β Grp β§ βπ₯ β π (((πβπ₯) = 0 β π₯ = 0 ) β§ βπ¦ β π (πβ(π₯ β π¦)) β€ ((πβπ₯) + (πβπ¦)))))) |