Step | Hyp | Ref
| Expression |
1 | | id 22 |
. . . . . . . . . . 11
β’ ((πβπΉ) = 0 β (πβπΉ) = 0) |
2 | | 0re 11216 |
. . . . . . . . . . 11
β’ 0 β
β |
3 | 1, 2 | eqeltrdi 2842 |
. . . . . . . . . 10
β’ ((πβπΉ) = 0 β (πβπΉ) β β) |
4 | | nmo0.1 |
. . . . . . . . . . . 12
β’ π = (π normOp π) |
5 | 4 | isnghm2 24241 |
. . . . . . . . . . 11
β’ ((π β NrmGrp β§ π β NrmGrp β§ πΉ β (π GrpHom π)) β (πΉ β (π NGHom π) β (πβπΉ) β β)) |
6 | 5 | biimpar 479 |
. . . . . . . . . 10
β’ (((π β NrmGrp β§ π β NrmGrp β§ πΉ β (π GrpHom π)) β§ (πβπΉ) β β) β πΉ β (π NGHom π)) |
7 | 3, 6 | sylan2 594 |
. . . . . . . . 9
β’ (((π β NrmGrp β§ π β NrmGrp β§ πΉ β (π GrpHom π)) β§ (πβπΉ) = 0) β πΉ β (π NGHom π)) |
8 | | nmo0.2 |
. . . . . . . . . 10
β’ π = (Baseβπ) |
9 | | eqid 2733 |
. . . . . . . . . 10
β’
(normβπ) =
(normβπ) |
10 | | eqid 2733 |
. . . . . . . . . 10
β’
(normβπ) =
(normβπ) |
11 | 4, 8, 9, 10 | nmoi 24245 |
. . . . . . . . 9
β’ ((πΉ β (π NGHom π) β§ π₯ β π) β ((normβπ)β(πΉβπ₯)) β€ ((πβπΉ) Β· ((normβπ)βπ₯))) |
12 | 7, 11 | sylan 581 |
. . . . . . . 8
β’ ((((π β NrmGrp β§ π β NrmGrp β§ πΉ β (π GrpHom π)) β§ (πβπΉ) = 0) β§ π₯ β π) β ((normβπ)β(πΉβπ₯)) β€ ((πβπΉ) Β· ((normβπ)βπ₯))) |
13 | | simplr 768 |
. . . . . . . . . 10
β’ ((((π β NrmGrp β§ π β NrmGrp β§ πΉ β (π GrpHom π)) β§ (πβπΉ) = 0) β§ π₯ β π) β (πβπΉ) = 0) |
14 | 13 | oveq1d 7424 |
. . . . . . . . 9
β’ ((((π β NrmGrp β§ π β NrmGrp β§ πΉ β (π GrpHom π)) β§ (πβπΉ) = 0) β§ π₯ β π) β ((πβπΉ) Β· ((normβπ)βπ₯)) = (0 Β· ((normβπ)βπ₯))) |
15 | | simpl1 1192 |
. . . . . . . . . . . 12
β’ (((π β NrmGrp β§ π β NrmGrp β§ πΉ β (π GrpHom π)) β§ (πβπΉ) = 0) β π β NrmGrp) |
16 | 8, 9 | nmcl 24125 |
. . . . . . . . . . . 12
β’ ((π β NrmGrp β§ π₯ β π) β ((normβπ)βπ₯) β β) |
17 | 15, 16 | sylan 581 |
. . . . . . . . . . 11
β’ ((((π β NrmGrp β§ π β NrmGrp β§ πΉ β (π GrpHom π)) β§ (πβπΉ) = 0) β§ π₯ β π) β ((normβπ)βπ₯) β β) |
18 | 17 | recnd 11242 |
. . . . . . . . . 10
β’ ((((π β NrmGrp β§ π β NrmGrp β§ πΉ β (π GrpHom π)) β§ (πβπΉ) = 0) β§ π₯ β π) β ((normβπ)βπ₯) β β) |
19 | 18 | mul02d 11412 |
. . . . . . . . 9
β’ ((((π β NrmGrp β§ π β NrmGrp β§ πΉ β (π GrpHom π)) β§ (πβπΉ) = 0) β§ π₯ β π) β (0 Β· ((normβπ)βπ₯)) = 0) |
20 | 14, 19 | eqtrd 2773 |
. . . . . . . 8
β’ ((((π β NrmGrp β§ π β NrmGrp β§ πΉ β (π GrpHom π)) β§ (πβπΉ) = 0) β§ π₯ β π) β ((πβπΉ) Β· ((normβπ)βπ₯)) = 0) |
21 | 12, 20 | breqtrd 5175 |
. . . . . . 7
β’ ((((π β NrmGrp β§ π β NrmGrp β§ πΉ β (π GrpHom π)) β§ (πβπΉ) = 0) β§ π₯ β π) β ((normβπ)β(πΉβπ₯)) β€ 0) |
22 | | simpll2 1214 |
. . . . . . . 8
β’ ((((π β NrmGrp β§ π β NrmGrp β§ πΉ β (π GrpHom π)) β§ (πβπΉ) = 0) β§ π₯ β π) β π β NrmGrp) |
23 | | simpl3 1194 |
. . . . . . . . . 10
β’ (((π β NrmGrp β§ π β NrmGrp β§ πΉ β (π GrpHom π)) β§ (πβπΉ) = 0) β πΉ β (π GrpHom π)) |
24 | | eqid 2733 |
. . . . . . . . . . 11
β’
(Baseβπ) =
(Baseβπ) |
25 | 8, 24 | ghmf 19096 |
. . . . . . . . . 10
β’ (πΉ β (π GrpHom π) β πΉ:πβΆ(Baseβπ)) |
26 | 23, 25 | syl 17 |
. . . . . . . . 9
β’ (((π β NrmGrp β§ π β NrmGrp β§ πΉ β (π GrpHom π)) β§ (πβπΉ) = 0) β πΉ:πβΆ(Baseβπ)) |
27 | 26 | ffvelcdmda 7087 |
. . . . . . . 8
β’ ((((π β NrmGrp β§ π β NrmGrp β§ πΉ β (π GrpHom π)) β§ (πβπΉ) = 0) β§ π₯ β π) β (πΉβπ₯) β (Baseβπ)) |
28 | 24, 10 | nmge0 24126 |
. . . . . . . 8
β’ ((π β NrmGrp β§ (πΉβπ₯) β (Baseβπ)) β 0 β€ ((normβπ)β(πΉβπ₯))) |
29 | 22, 27, 28 | syl2anc 585 |
. . . . . . 7
β’ ((((π β NrmGrp β§ π β NrmGrp β§ πΉ β (π GrpHom π)) β§ (πβπΉ) = 0) β§ π₯ β π) β 0 β€ ((normβπ)β(πΉβπ₯))) |
30 | 24, 10 | nmcl 24125 |
. . . . . . . . 9
β’ ((π β NrmGrp β§ (πΉβπ₯) β (Baseβπ)) β ((normβπ)β(πΉβπ₯)) β β) |
31 | 22, 27, 30 | syl2anc 585 |
. . . . . . . 8
β’ ((((π β NrmGrp β§ π β NrmGrp β§ πΉ β (π GrpHom π)) β§ (πβπΉ) = 0) β§ π₯ β π) β ((normβπ)β(πΉβπ₯)) β β) |
32 | | letri3 11299 |
. . . . . . . 8
β’
((((normβπ)β(πΉβπ₯)) β β β§ 0 β β)
β (((normβπ)β(πΉβπ₯)) = 0 β (((normβπ)β(πΉβπ₯)) β€ 0 β§ 0 β€ ((normβπ)β(πΉβπ₯))))) |
33 | 31, 2, 32 | sylancl 587 |
. . . . . . 7
β’ ((((π β NrmGrp β§ π β NrmGrp β§ πΉ β (π GrpHom π)) β§ (πβπΉ) = 0) β§ π₯ β π) β (((normβπ)β(πΉβπ₯)) = 0 β (((normβπ)β(πΉβπ₯)) β€ 0 β§ 0 β€ ((normβπ)β(πΉβπ₯))))) |
34 | 21, 29, 33 | mpbir2and 712 |
. . . . . 6
β’ ((((π β NrmGrp β§ π β NrmGrp β§ πΉ β (π GrpHom π)) β§ (πβπΉ) = 0) β§ π₯ β π) β ((normβπ)β(πΉβπ₯)) = 0) |
35 | | nmo0.3 |
. . . . . . . 8
β’ 0 =
(0gβπ) |
36 | 24, 10, 35 | nmeq0 24127 |
. . . . . . 7
β’ ((π β NrmGrp β§ (πΉβπ₯) β (Baseβπ)) β (((normβπ)β(πΉβπ₯)) = 0 β (πΉβπ₯) = 0 )) |
37 | 22, 27, 36 | syl2anc 585 |
. . . . . 6
β’ ((((π β NrmGrp β§ π β NrmGrp β§ πΉ β (π GrpHom π)) β§ (πβπΉ) = 0) β§ π₯ β π) β (((normβπ)β(πΉβπ₯)) = 0 β (πΉβπ₯) = 0 )) |
38 | 34, 37 | mpbid 231 |
. . . . 5
β’ ((((π β NrmGrp β§ π β NrmGrp β§ πΉ β (π GrpHom π)) β§ (πβπΉ) = 0) β§ π₯ β π) β (πΉβπ₯) = 0 ) |
39 | 38 | mpteq2dva 5249 |
. . . 4
β’ (((π β NrmGrp β§ π β NrmGrp β§ πΉ β (π GrpHom π)) β§ (πβπΉ) = 0) β (π₯ β π β¦ (πΉβπ₯)) = (π₯ β π β¦ 0 )) |
40 | 26 | feqmptd 6961 |
. . . 4
β’ (((π β NrmGrp β§ π β NrmGrp β§ πΉ β (π GrpHom π)) β§ (πβπΉ) = 0) β πΉ = (π₯ β π β¦ (πΉβπ₯))) |
41 | | fconstmpt 5739 |
. . . . 5
β’ (π Γ { 0 }) = (π₯ β π β¦ 0 ) |
42 | 41 | a1i 11 |
. . . 4
β’ (((π β NrmGrp β§ π β NrmGrp β§ πΉ β (π GrpHom π)) β§ (πβπΉ) = 0) β (π Γ { 0 }) = (π₯ β π β¦ 0 )) |
43 | 39, 40, 42 | 3eqtr4d 2783 |
. . 3
β’ (((π β NrmGrp β§ π β NrmGrp β§ πΉ β (π GrpHom π)) β§ (πβπΉ) = 0) β πΉ = (π Γ { 0 })) |
44 | 43 | ex 414 |
. 2
β’ ((π β NrmGrp β§ π β NrmGrp β§ πΉ β (π GrpHom π)) β ((πβπΉ) = 0 β πΉ = (π Γ { 0 }))) |
45 | 4, 8, 35 | nmo0 24252 |
. . . 4
β’ ((π β NrmGrp β§ π β NrmGrp) β (πβ(π Γ { 0 })) = 0) |
46 | 45 | 3adant3 1133 |
. . 3
β’ ((π β NrmGrp β§ π β NrmGrp β§ πΉ β (π GrpHom π)) β (πβ(π Γ { 0 })) = 0) |
47 | | fveqeq2 6901 |
. . 3
β’ (πΉ = (π Γ { 0 }) β ((πβπΉ) = 0 β (πβ(π Γ { 0 })) = 0)) |
48 | 46, 47 | syl5ibrcom 246 |
. 2
β’ ((π β NrmGrp β§ π β NrmGrp β§ πΉ β (π GrpHom π)) β (πΉ = (π Γ { 0 }) β (πβπΉ) = 0)) |
49 | 44, 48 | impbid 211 |
1
β’ ((π β NrmGrp β§ π β NrmGrp β§ πΉ β (π GrpHom π)) β ((πβπΉ) = 0 β πΉ = (π Γ { 0 }))) |