Step | Hyp | Ref
| Expression |
1 | | nmo0.1 |
. . 3
β’ π = (π normOp π) |
2 | | nmo0.2 |
. . 3
β’ π = (Baseβπ) |
3 | | eqid 2732 |
. . 3
β’
(normβπ) =
(normβπ) |
4 | | eqid 2732 |
. . 3
β’
(normβπ) =
(normβπ) |
5 | | eqid 2732 |
. . 3
β’
(0gβπ) = (0gβπ) |
6 | | simpl 483 |
. . 3
β’ ((π β NrmGrp β§ π β NrmGrp) β π β NrmGrp) |
7 | | simpr 485 |
. . 3
β’ ((π β NrmGrp β§ π β NrmGrp) β π β NrmGrp) |
8 | | ngpgrp 24107 |
. . . 4
β’ (π β NrmGrp β π β Grp) |
9 | | ngpgrp 24107 |
. . . 4
β’ (π β NrmGrp β π β Grp) |
10 | | nmo0.3 |
. . . . 5
β’ 0 =
(0gβπ) |
11 | 10, 2 | 0ghm 19105 |
. . . 4
β’ ((π β Grp β§ π β Grp) β (π Γ { 0 }) β (π GrpHom π)) |
12 | 8, 9, 11 | syl2an 596 |
. . 3
β’ ((π β NrmGrp β§ π β NrmGrp) β (π Γ { 0 }) β (π GrpHom π)) |
13 | | 0red 11216 |
. . 3
β’ ((π β NrmGrp β§ π β NrmGrp) β 0 β
β) |
14 | | 0le0 12312 |
. . . 4
β’ 0 β€
0 |
15 | 14 | a1i 11 |
. . 3
β’ ((π β NrmGrp β§ π β NrmGrp) β 0 β€
0) |
16 | 10 | fvexi 6905 |
. . . . . . . 8
β’ 0 β
V |
17 | 16 | fvconst2 7204 |
. . . . . . 7
β’ (π₯ β π β ((π Γ { 0 })βπ₯) = 0 ) |
18 | 17 | ad2antrl 726 |
. . . . . 6
β’ (((π β NrmGrp β§ π β NrmGrp) β§ (π₯ β π β§ π₯ β (0gβπ))) β ((π Γ { 0 })βπ₯) = 0 ) |
19 | 18 | fveq2d 6895 |
. . . . 5
β’ (((π β NrmGrp β§ π β NrmGrp) β§ (π₯ β π β§ π₯ β (0gβπ))) β ((normβπ)β((π Γ { 0 })βπ₯)) = ((normβπ)β 0 )) |
20 | 4, 10 | nm0 24137 |
. . . . . 6
β’ (π β NrmGrp β
((normβπ)β
0 ) =
0) |
21 | 20 | ad2antlr 725 |
. . . . 5
β’ (((π β NrmGrp β§ π β NrmGrp) β§ (π₯ β π β§ π₯ β (0gβπ))) β ((normβπ)β 0 ) = 0) |
22 | 19, 21 | eqtrd 2772 |
. . . 4
β’ (((π β NrmGrp β§ π β NrmGrp) β§ (π₯ β π β§ π₯ β (0gβπ))) β ((normβπ)β((π Γ { 0 })βπ₯)) = 0) |
23 | 2, 3 | nmcl 24124 |
. . . . . . . 8
β’ ((π β NrmGrp β§ π₯ β π) β ((normβπ)βπ₯) β β) |
24 | 23 | ad2ant2r 745 |
. . . . . . 7
β’ (((π β NrmGrp β§ π β NrmGrp) β§ (π₯ β π β§ π₯ β (0gβπ))) β ((normβπ)βπ₯) β β) |
25 | 24 | recnd 11241 |
. . . . . 6
β’ (((π β NrmGrp β§ π β NrmGrp) β§ (π₯ β π β§ π₯ β (0gβπ))) β ((normβπ)βπ₯) β β) |
26 | 25 | mul02d 11411 |
. . . . 5
β’ (((π β NrmGrp β§ π β NrmGrp) β§ (π₯ β π β§ π₯ β (0gβπ))) β (0 Β· ((normβπ)βπ₯)) = 0) |
27 | 14, 26 | breqtrrid 5186 |
. . . 4
β’ (((π β NrmGrp β§ π β NrmGrp) β§ (π₯ β π β§ π₯ β (0gβπ))) β 0 β€ (0 Β·
((normβπ)βπ₯))) |
28 | 22, 27 | eqbrtrd 5170 |
. . 3
β’ (((π β NrmGrp β§ π β NrmGrp) β§ (π₯ β π β§ π₯ β (0gβπ))) β ((normβπ)β((π Γ { 0 })βπ₯)) β€ (0 Β·
((normβπ)βπ₯))) |
29 | 1, 2, 3, 4, 5, 6, 7, 12, 13, 15, 28 | nmolb2d 24234 |
. 2
β’ ((π β NrmGrp β§ π β NrmGrp) β (πβ(π Γ { 0 })) β€
0) |
30 | 1 | nmoge0 24237 |
. . 3
β’ ((π β NrmGrp β§ π β NrmGrp β§ (π Γ { 0 }) β (π GrpHom π)) β 0 β€ (πβ(π Γ { 0 }))) |
31 | 12, 30 | mpd3an3 1462 |
. 2
β’ ((π β NrmGrp β§ π β NrmGrp) β 0 β€
(πβ(π Γ { 0 }))) |
32 | 1 | nmocl 24236 |
. . . 4
β’ ((π β NrmGrp β§ π β NrmGrp β§ (π Γ { 0 }) β (π GrpHom π)) β (πβ(π Γ { 0 })) β
β*) |
33 | 12, 32 | mpd3an3 1462 |
. . 3
β’ ((π β NrmGrp β§ π β NrmGrp) β (πβ(π Γ { 0 })) β
β*) |
34 | | 0xr 11260 |
. . 3
β’ 0 β
β* |
35 | | xrletri3 13132 |
. . 3
β’ (((πβ(π Γ { 0 })) β
β* β§ 0 β β*) β ((πβ(π Γ { 0 })) = 0 β ((πβ(π Γ { 0 })) β€ 0 β§ 0 β€
(πβ(π Γ { 0 }))))) |
36 | 33, 34, 35 | sylancl 586 |
. 2
β’ ((π β NrmGrp β§ π β NrmGrp) β ((πβ(π Γ { 0 })) = 0 β ((πβ(π Γ { 0 })) β€ 0 β§ 0 β€
(πβ(π Γ { 0 }))))) |
37 | 29, 31, 36 | mpbir2and 711 |
1
β’ ((π β NrmGrp β§ π β NrmGrp) β (πβ(π Γ { 0 })) = 0) |