Step | Hyp | Ref
| Expression |
1 | | nmoid.1 |
. . 3
β’ π = (π normOp π) |
2 | | nmoid.2 |
. . 3
β’ π = (Baseβπ) |
3 | | eqid 2724 |
. . 3
β’
(normβπ) =
(normβπ) |
4 | | nmoid.3 |
. . 3
β’ 0 =
(0gβπ) |
5 | | simpl 482 |
. . 3
β’ ((π β NrmGrp β§ { 0 } β
π) β π β NrmGrp) |
6 | | ngpgrp 24452 |
. . . . 5
β’ (π β NrmGrp β π β Grp) |
7 | 6 | adantr 480 |
. . . 4
β’ ((π β NrmGrp β§ { 0 } β
π) β π β Grp) |
8 | 2 | idghm 19152 |
. . . 4
β’ (π β Grp β ( I βΎ
π) β (π GrpHom π)) |
9 | 7, 8 | syl 17 |
. . 3
β’ ((π β NrmGrp β§ { 0 } β
π) β ( I βΎ π) β (π GrpHom π)) |
10 | | 1red 11214 |
. . 3
β’ ((π β NrmGrp β§ { 0 } β
π) β 1 β
β) |
11 | | 0le1 11736 |
. . . 4
β’ 0 β€
1 |
12 | 11 | a1i 11 |
. . 3
β’ ((π β NrmGrp β§ { 0 } β
π) β 0 β€
1) |
13 | 2, 3 | nmcl 24469 |
. . . . . 6
β’ ((π β NrmGrp β§ π₯ β π) β ((normβπ)βπ₯) β β) |
14 | 13 | ad2ant2r 744 |
. . . . 5
β’ (((π β NrmGrp β§ { 0 } β
π) β§ (π₯ β π β§ π₯ β 0 )) β
((normβπ)βπ₯) β
β) |
15 | 14 | leidd 11779 |
. . . 4
β’ (((π β NrmGrp β§ { 0 } β
π) β§ (π₯ β π β§ π₯ β 0 )) β
((normβπ)βπ₯) β€ ((normβπ)βπ₯)) |
16 | | fvresi 7164 |
. . . . . 6
β’ (π₯ β π β (( I βΎ π)βπ₯) = π₯) |
17 | 16 | ad2antrl 725 |
. . . . 5
β’ (((π β NrmGrp β§ { 0 } β
π) β§ (π₯ β π β§ π₯ β 0 )) β (( I βΎ
π)βπ₯) = π₯) |
18 | 17 | fveq2d 6886 |
. . . 4
β’ (((π β NrmGrp β§ { 0 } β
π) β§ (π₯ β π β§ π₯ β 0 )) β
((normβπ)β(( I
βΎ π)βπ₯)) = ((normβπ)βπ₯)) |
19 | 14 | recnd 11241 |
. . . . 5
β’ (((π β NrmGrp β§ { 0 } β
π) β§ (π₯ β π β§ π₯ β 0 )) β
((normβπ)βπ₯) β
β) |
20 | 19 | mullidd 11231 |
. . . 4
β’ (((π β NrmGrp β§ { 0 } β
π) β§ (π₯ β π β§ π₯ β 0 )) β (1 Β·
((normβπ)βπ₯)) = ((normβπ)βπ₯)) |
21 | 15, 18, 20 | 3brtr4d 5171 |
. . 3
β’ (((π β NrmGrp β§ { 0 } β
π) β§ (π₯ β π β§ π₯ β 0 )) β
((normβπ)β(( I
βΎ π)βπ₯)) β€ (1 Β·
((normβπ)βπ₯))) |
22 | 1, 2, 3, 3, 4, 5, 5, 9, 10, 12, 21 | nmolb2d 24579 |
. 2
β’ ((π β NrmGrp β§ { 0 } β
π) β (πβ( I βΎ π)) β€ 1) |
23 | | pssnel 4463 |
. . . 4
β’ ({ 0 } β
π β βπ₯(π₯ β π β§ Β¬ π₯ β { 0 })) |
24 | 23 | adantl 481 |
. . 3
β’ ((π β NrmGrp β§ { 0 } β
π) β βπ₯(π₯ β π β§ Β¬ π₯ β { 0 })) |
25 | | velsn 4637 |
. . . . . 6
β’ (π₯ β { 0 } β π₯ = 0 ) |
26 | 25 | biimpri 227 |
. . . . 5
β’ (π₯ = 0 β π₯ β { 0 }) |
27 | 26 | necon3bi 2959 |
. . . 4
β’ (Β¬
π₯ β { 0 } β
π₯ β 0 ) |
28 | 20, 18 | eqtr4d 2767 |
. . . . . 6
β’ (((π β NrmGrp β§ { 0 } β
π) β§ (π₯ β π β§ π₯ β 0 )) β (1 Β·
((normβπ)βπ₯)) = ((normβπ)β(( I βΎ π)βπ₯))) |
29 | 1 | nmocl 24581 |
. . . . . . . . . 10
β’ ((π β NrmGrp β§ π β NrmGrp β§ ( I βΎ
π) β (π GrpHom π)) β (πβ( I βΎ π)) β
β*) |
30 | 5, 5, 9, 29 | syl3anc 1368 |
. . . . . . . . 9
β’ ((π β NrmGrp β§ { 0 } β
π) β (πβ( I βΎ π)) β
β*) |
31 | 1 | nmoge0 24582 |
. . . . . . . . . 10
β’ ((π β NrmGrp β§ π β NrmGrp β§ ( I βΎ
π) β (π GrpHom π)) β 0 β€ (πβ( I βΎ π))) |
32 | 5, 5, 9, 31 | syl3anc 1368 |
. . . . . . . . 9
β’ ((π β NrmGrp β§ { 0 } β
π) β 0 β€ (πβ( I βΎ π))) |
33 | | xrrege0 13154 |
. . . . . . . . 9
β’ ((((πβ( I βΎ π)) β β*
β§ 1 β β) β§ (0 β€ (πβ( I βΎ π)) β§ (πβ( I βΎ π)) β€ 1)) β (πβ( I βΎ π)) β β) |
34 | 30, 10, 32, 22, 33 | syl22anc 836 |
. . . . . . . 8
β’ ((π β NrmGrp β§ { 0 } β
π) β (πβ( I βΎ π)) β
β) |
35 | 1 | isnghm2 24585 |
. . . . . . . . 9
β’ ((π β NrmGrp β§ π β NrmGrp β§ ( I βΎ
π) β (π GrpHom π)) β (( I βΎ π) β (π NGHom π) β (πβ( I βΎ π)) β β)) |
36 | 5, 5, 9, 35 | syl3anc 1368 |
. . . . . . . 8
β’ ((π β NrmGrp β§ { 0 } β
π) β (( I βΎ
π) β (π NGHom π) β (πβ( I βΎ π)) β β)) |
37 | 34, 36 | mpbird 257 |
. . . . . . 7
β’ ((π β NrmGrp β§ { 0 } β
π) β ( I βΎ π) β (π NGHom π)) |
38 | | simprl 768 |
. . . . . . 7
β’ (((π β NrmGrp β§ { 0 } β
π) β§ (π₯ β π β§ π₯ β 0 )) β π₯ β π) |
39 | 1, 2, 3, 3 | nmoi 24589 |
. . . . . . 7
β’ ((( I
βΎ π) β (π NGHom π) β§ π₯ β π) β ((normβπ)β(( I βΎ π)βπ₯)) β€ ((πβ( I βΎ π)) Β· ((normβπ)βπ₯))) |
40 | 37, 38, 39 | syl2an2r 682 |
. . . . . 6
β’ (((π β NrmGrp β§ { 0 } β
π) β§ (π₯ β π β§ π₯ β 0 )) β
((normβπ)β(( I
βΎ π)βπ₯)) β€ ((πβ( I βΎ π)) Β· ((normβπ)βπ₯))) |
41 | 28, 40 | eqbrtrd 5161 |
. . . . 5
β’ (((π β NrmGrp β§ { 0 } β
π) β§ (π₯ β π β§ π₯ β 0 )) β (1 Β·
((normβπ)βπ₯)) β€ ((πβ( I βΎ π)) Β· ((normβπ)βπ₯))) |
42 | | 1red 11214 |
. . . . . 6
β’ (((π β NrmGrp β§ { 0 } β
π) β§ (π₯ β π β§ π₯ β 0 )) β 1 β
β) |
43 | 34 | adantr 480 |
. . . . . 6
β’ (((π β NrmGrp β§ { 0 } β
π) β§ (π₯ β π β§ π₯ β 0 )) β (πβ( I βΎ π)) β
β) |
44 | 2, 3, 4 | nmrpcl 24473 |
. . . . . . . 8
β’ ((π β NrmGrp β§ π₯ β π β§ π₯ β 0 ) β
((normβπ)βπ₯) β
β+) |
45 | 44 | 3expb 1117 |
. . . . . . 7
β’ ((π β NrmGrp β§ (π₯ β π β§ π₯ β 0 )) β
((normβπ)βπ₯) β
β+) |
46 | 45 | adantlr 712 |
. . . . . 6
β’ (((π β NrmGrp β§ { 0 } β
π) β§ (π₯ β π β§ π₯ β 0 )) β
((normβπ)βπ₯) β
β+) |
47 | 42, 43, 46 | lemul1d 13060 |
. . . . 5
β’ (((π β NrmGrp β§ { 0 } β
π) β§ (π₯ β π β§ π₯ β 0 )) β (1 β€ (πβ( I βΎ π)) β (1 Β·
((normβπ)βπ₯)) β€ ((πβ( I βΎ π)) Β· ((normβπ)βπ₯)))) |
48 | 41, 47 | mpbird 257 |
. . . 4
β’ (((π β NrmGrp β§ { 0 } β
π) β§ (π₯ β π β§ π₯ β 0 )) β 1 β€ (πβ( I βΎ π))) |
49 | 27, 48 | sylanr2 680 |
. . 3
β’ (((π β NrmGrp β§ { 0 } β
π) β§ (π₯ β π β§ Β¬ π₯ β { 0 })) β 1 β€ (πβ( I βΎ π))) |
50 | 24, 49 | exlimddv 1930 |
. 2
β’ ((π β NrmGrp β§ { 0 } β
π) β 1 β€ (πβ( I βΎ π))) |
51 | | 1xr 11272 |
. . 3
β’ 1 β
β* |
52 | | xrletri3 13134 |
. . 3
β’ (((πβ( I βΎ π)) β β*
β§ 1 β β*) β ((πβ( I βΎ π)) = 1 β ((πβ( I βΎ π)) β€ 1 β§ 1 β€ (πβ( I βΎ π))))) |
53 | 30, 51, 52 | sylancl 585 |
. 2
β’ ((π β NrmGrp β§ { 0 } β
π) β ((πβ( I βΎ π)) = 1 β ((πβ( I βΎ π)) β€ 1 β§ 1 β€ (πβ( I βΎ π))))) |
54 | 22, 50, 53 | mpbir2and 710 |
1
β’ ((π β NrmGrp β§ { 0 } β
π) β (πβ( I βΎ π)) = 1) |