Step | Hyp | Ref
| Expression |
1 | | nmoid.1 |
. . 3
⊢ 𝑁 = (𝑆 normOp 𝑆) |
2 | | nmoid.2 |
. . 3
⊢ 𝑉 = (Base‘𝑆) |
3 | | eqid 2610 |
. . 3
⊢
(norm‘𝑆) =
(norm‘𝑆) |
4 | | nmoid.3 |
. . 3
⊢ 0 =
(0g‘𝑆) |
5 | | simpl 472 |
. . 3
⊢ ((𝑆 ∈ NrmGrp ∧ { 0 } ⊊
𝑉) → 𝑆 ∈ NrmGrp) |
6 | | ngpgrp 22213 |
. . . . 5
⊢ (𝑆 ∈ NrmGrp → 𝑆 ∈ Grp) |
7 | 6 | adantr 480 |
. . . 4
⊢ ((𝑆 ∈ NrmGrp ∧ { 0 } ⊊
𝑉) → 𝑆 ∈ Grp) |
8 | 2 | idghm 17498 |
. . . 4
⊢ (𝑆 ∈ Grp → ( I ↾
𝑉) ∈ (𝑆 GrpHom 𝑆)) |
9 | 7, 8 | syl 17 |
. . 3
⊢ ((𝑆 ∈ NrmGrp ∧ { 0 } ⊊
𝑉) → ( I ↾ 𝑉) ∈ (𝑆 GrpHom 𝑆)) |
10 | | 1red 9934 |
. . 3
⊢ ((𝑆 ∈ NrmGrp ∧ { 0 } ⊊
𝑉) → 1 ∈
ℝ) |
11 | | 0le1 10430 |
. . . 4
⊢ 0 ≤
1 |
12 | 11 | a1i 11 |
. . 3
⊢ ((𝑆 ∈ NrmGrp ∧ { 0 } ⊊
𝑉) → 0 ≤
1) |
13 | 2, 3 | nmcl 22230 |
. . . . . 6
⊢ ((𝑆 ∈ NrmGrp ∧ 𝑥 ∈ 𝑉) → ((norm‘𝑆)‘𝑥) ∈ ℝ) |
14 | 13 | ad2ant2r 779 |
. . . . 5
⊢ (((𝑆 ∈ NrmGrp ∧ { 0 } ⊊
𝑉) ∧ (𝑥 ∈ 𝑉 ∧ 𝑥 ≠ 0 )) →
((norm‘𝑆)‘𝑥) ∈
ℝ) |
15 | 14 | leidd 10473 |
. . . 4
⊢ (((𝑆 ∈ NrmGrp ∧ { 0 } ⊊
𝑉) ∧ (𝑥 ∈ 𝑉 ∧ 𝑥 ≠ 0 )) →
((norm‘𝑆)‘𝑥) ≤ ((norm‘𝑆)‘𝑥)) |
16 | | fvresi 6344 |
. . . . . 6
⊢ (𝑥 ∈ 𝑉 → (( I ↾ 𝑉)‘𝑥) = 𝑥) |
17 | 16 | ad2antrl 760 |
. . . . 5
⊢ (((𝑆 ∈ NrmGrp ∧ { 0 } ⊊
𝑉) ∧ (𝑥 ∈ 𝑉 ∧ 𝑥 ≠ 0 )) → (( I ↾
𝑉)‘𝑥) = 𝑥) |
18 | 17 | fveq2d 6107 |
. . . 4
⊢ (((𝑆 ∈ NrmGrp ∧ { 0 } ⊊
𝑉) ∧ (𝑥 ∈ 𝑉 ∧ 𝑥 ≠ 0 )) →
((norm‘𝑆)‘(( I
↾ 𝑉)‘𝑥)) = ((norm‘𝑆)‘𝑥)) |
19 | 14 | recnd 9947 |
. . . . 5
⊢ (((𝑆 ∈ NrmGrp ∧ { 0 } ⊊
𝑉) ∧ (𝑥 ∈ 𝑉 ∧ 𝑥 ≠ 0 )) →
((norm‘𝑆)‘𝑥) ∈
ℂ) |
20 | 19 | mulid2d 9937 |
. . . 4
⊢ (((𝑆 ∈ NrmGrp ∧ { 0 } ⊊
𝑉) ∧ (𝑥 ∈ 𝑉 ∧ 𝑥 ≠ 0 )) → (1 ·
((norm‘𝑆)‘𝑥)) = ((norm‘𝑆)‘𝑥)) |
21 | 15, 18, 20 | 3brtr4d 4615 |
. . 3
⊢ (((𝑆 ∈ NrmGrp ∧ { 0 } ⊊
𝑉) ∧ (𝑥 ∈ 𝑉 ∧ 𝑥 ≠ 0 )) →
((norm‘𝑆)‘(( I
↾ 𝑉)‘𝑥)) ≤ (1 ·
((norm‘𝑆)‘𝑥))) |
22 | 1, 2, 3, 3, 4, 5, 5, 9, 10, 12, 21 | nmolb2d 22332 |
. 2
⊢ ((𝑆 ∈ NrmGrp ∧ { 0 } ⊊
𝑉) → (𝑁‘( I ↾ 𝑉)) ≤ 1) |
23 | | pssnel 3991 |
. . . 4
⊢ ({ 0 } ⊊
𝑉 → ∃𝑥(𝑥 ∈ 𝑉 ∧ ¬ 𝑥 ∈ { 0 })) |
24 | 23 | adantl 481 |
. . 3
⊢ ((𝑆 ∈ NrmGrp ∧ { 0 } ⊊
𝑉) → ∃𝑥(𝑥 ∈ 𝑉 ∧ ¬ 𝑥 ∈ { 0 })) |
25 | | velsn 4141 |
. . . . . 6
⊢ (𝑥 ∈ { 0 } ↔ 𝑥 = 0 ) |
26 | 25 | biimpri 217 |
. . . . 5
⊢ (𝑥 = 0 → 𝑥 ∈ { 0 }) |
27 | 26 | necon3bi 2808 |
. . . 4
⊢ (¬
𝑥 ∈ { 0 } →
𝑥 ≠ 0 ) |
28 | 20, 18 | eqtr4d 2647 |
. . . . . 6
⊢ (((𝑆 ∈ NrmGrp ∧ { 0 } ⊊
𝑉) ∧ (𝑥 ∈ 𝑉 ∧ 𝑥 ≠ 0 )) → (1 ·
((norm‘𝑆)‘𝑥)) = ((norm‘𝑆)‘(( I ↾ 𝑉)‘𝑥))) |
29 | 1 | nmocl 22334 |
. . . . . . . . . . 11
⊢ ((𝑆 ∈ NrmGrp ∧ 𝑆 ∈ NrmGrp ∧ ( I ↾
𝑉) ∈ (𝑆 GrpHom 𝑆)) → (𝑁‘( I ↾ 𝑉)) ∈
ℝ*) |
30 | 5, 5, 9, 29 | syl3anc 1318 |
. . . . . . . . . 10
⊢ ((𝑆 ∈ NrmGrp ∧ { 0 } ⊊
𝑉) → (𝑁‘( I ↾ 𝑉)) ∈
ℝ*) |
31 | 1 | nmoge0 22335 |
. . . . . . . . . . 11
⊢ ((𝑆 ∈ NrmGrp ∧ 𝑆 ∈ NrmGrp ∧ ( I ↾
𝑉) ∈ (𝑆 GrpHom 𝑆)) → 0 ≤ (𝑁‘( I ↾ 𝑉))) |
32 | 5, 5, 9, 31 | syl3anc 1318 |
. . . . . . . . . 10
⊢ ((𝑆 ∈ NrmGrp ∧ { 0 } ⊊
𝑉) → 0 ≤ (𝑁‘( I ↾ 𝑉))) |
33 | | xrrege0 11879 |
. . . . . . . . . 10
⊢ ((((𝑁‘( I ↾ 𝑉)) ∈ ℝ*
∧ 1 ∈ ℝ) ∧ (0 ≤ (𝑁‘( I ↾ 𝑉)) ∧ (𝑁‘( I ↾ 𝑉)) ≤ 1)) → (𝑁‘( I ↾ 𝑉)) ∈ ℝ) |
34 | 30, 10, 32, 22, 33 | syl22anc 1319 |
. . . . . . . . 9
⊢ ((𝑆 ∈ NrmGrp ∧ { 0 } ⊊
𝑉) → (𝑁‘( I ↾ 𝑉)) ∈
ℝ) |
35 | 1 | isnghm2 22338 |
. . . . . . . . . 10
⊢ ((𝑆 ∈ NrmGrp ∧ 𝑆 ∈ NrmGrp ∧ ( I ↾
𝑉) ∈ (𝑆 GrpHom 𝑆)) → (( I ↾ 𝑉) ∈ (𝑆 NGHom 𝑆) ↔ (𝑁‘( I ↾ 𝑉)) ∈ ℝ)) |
36 | 5, 5, 9, 35 | syl3anc 1318 |
. . . . . . . . 9
⊢ ((𝑆 ∈ NrmGrp ∧ { 0 } ⊊
𝑉) → (( I ↾
𝑉) ∈ (𝑆 NGHom 𝑆) ↔ (𝑁‘( I ↾ 𝑉)) ∈ ℝ)) |
37 | 34, 36 | mpbird 246 |
. . . . . . . 8
⊢ ((𝑆 ∈ NrmGrp ∧ { 0 } ⊊
𝑉) → ( I ↾ 𝑉) ∈ (𝑆 NGHom 𝑆)) |
38 | 37 | adantr 480 |
. . . . . . 7
⊢ (((𝑆 ∈ NrmGrp ∧ { 0 } ⊊
𝑉) ∧ (𝑥 ∈ 𝑉 ∧ 𝑥 ≠ 0 )) → ( I ↾
𝑉) ∈ (𝑆 NGHom 𝑆)) |
39 | | simprl 790 |
. . . . . . 7
⊢ (((𝑆 ∈ NrmGrp ∧ { 0 } ⊊
𝑉) ∧ (𝑥 ∈ 𝑉 ∧ 𝑥 ≠ 0 )) → 𝑥 ∈ 𝑉) |
40 | 1, 2, 3, 3 | nmoi 22342 |
. . . . . . 7
⊢ ((( I
↾ 𝑉) ∈ (𝑆 NGHom 𝑆) ∧ 𝑥 ∈ 𝑉) → ((norm‘𝑆)‘(( I ↾ 𝑉)‘𝑥)) ≤ ((𝑁‘( I ↾ 𝑉)) · ((norm‘𝑆)‘𝑥))) |
41 | 38, 39, 40 | syl2anc 691 |
. . . . . 6
⊢ (((𝑆 ∈ NrmGrp ∧ { 0 } ⊊
𝑉) ∧ (𝑥 ∈ 𝑉 ∧ 𝑥 ≠ 0 )) →
((norm‘𝑆)‘(( I
↾ 𝑉)‘𝑥)) ≤ ((𝑁‘( I ↾ 𝑉)) · ((norm‘𝑆)‘𝑥))) |
42 | 28, 41 | eqbrtrd 4605 |
. . . . 5
⊢ (((𝑆 ∈ NrmGrp ∧ { 0 } ⊊
𝑉) ∧ (𝑥 ∈ 𝑉 ∧ 𝑥 ≠ 0 )) → (1 ·
((norm‘𝑆)‘𝑥)) ≤ ((𝑁‘( I ↾ 𝑉)) · ((norm‘𝑆)‘𝑥))) |
43 | | 1red 9934 |
. . . . . 6
⊢ (((𝑆 ∈ NrmGrp ∧ { 0 } ⊊
𝑉) ∧ (𝑥 ∈ 𝑉 ∧ 𝑥 ≠ 0 )) → 1 ∈
ℝ) |
44 | 34 | adantr 480 |
. . . . . 6
⊢ (((𝑆 ∈ NrmGrp ∧ { 0 } ⊊
𝑉) ∧ (𝑥 ∈ 𝑉 ∧ 𝑥 ≠ 0 )) → (𝑁‘( I ↾ 𝑉)) ∈
ℝ) |
45 | 2, 3, 4 | nmrpcl 22234 |
. . . . . . . 8
⊢ ((𝑆 ∈ NrmGrp ∧ 𝑥 ∈ 𝑉 ∧ 𝑥 ≠ 0 ) →
((norm‘𝑆)‘𝑥) ∈
ℝ+) |
46 | 45 | 3expb 1258 |
. . . . . . 7
⊢ ((𝑆 ∈ NrmGrp ∧ (𝑥 ∈ 𝑉 ∧ 𝑥 ≠ 0 )) →
((norm‘𝑆)‘𝑥) ∈
ℝ+) |
47 | 46 | adantlr 747 |
. . . . . 6
⊢ (((𝑆 ∈ NrmGrp ∧ { 0 } ⊊
𝑉) ∧ (𝑥 ∈ 𝑉 ∧ 𝑥 ≠ 0 )) →
((norm‘𝑆)‘𝑥) ∈
ℝ+) |
48 | 43, 44, 47 | lemul1d 11791 |
. . . . 5
⊢ (((𝑆 ∈ NrmGrp ∧ { 0 } ⊊
𝑉) ∧ (𝑥 ∈ 𝑉 ∧ 𝑥 ≠ 0 )) → (1 ≤ (𝑁‘( I ↾ 𝑉)) ↔ (1 ·
((norm‘𝑆)‘𝑥)) ≤ ((𝑁‘( I ↾ 𝑉)) · ((norm‘𝑆)‘𝑥)))) |
49 | 42, 48 | mpbird 246 |
. . . 4
⊢ (((𝑆 ∈ NrmGrp ∧ { 0 } ⊊
𝑉) ∧ (𝑥 ∈ 𝑉 ∧ 𝑥 ≠ 0 )) → 1 ≤ (𝑁‘( I ↾ 𝑉))) |
50 | 27, 49 | sylanr2 683 |
. . 3
⊢ (((𝑆 ∈ NrmGrp ∧ { 0 } ⊊
𝑉) ∧ (𝑥 ∈ 𝑉 ∧ ¬ 𝑥 ∈ { 0 })) → 1 ≤ (𝑁‘( I ↾ 𝑉))) |
51 | 24, 50 | exlimddv 1850 |
. 2
⊢ ((𝑆 ∈ NrmGrp ∧ { 0 } ⊊
𝑉) → 1 ≤ (𝑁‘( I ↾ 𝑉))) |
52 | | 1re 9918 |
. . . 4
⊢ 1 ∈
ℝ |
53 | 52 | rexri 9976 |
. . 3
⊢ 1 ∈
ℝ* |
54 | | xrletri3 11861 |
. . 3
⊢ (((𝑁‘( I ↾ 𝑉)) ∈ ℝ*
∧ 1 ∈ ℝ*) → ((𝑁‘( I ↾ 𝑉)) = 1 ↔ ((𝑁‘( I ↾ 𝑉)) ≤ 1 ∧ 1 ≤ (𝑁‘( I ↾ 𝑉))))) |
55 | 30, 53, 54 | sylancl 693 |
. 2
⊢ ((𝑆 ∈ NrmGrp ∧ { 0 } ⊊
𝑉) → ((𝑁‘( I ↾ 𝑉)) = 1 ↔ ((𝑁‘( I ↾ 𝑉)) ≤ 1 ∧ 1 ≤ (𝑁‘( I ↾ 𝑉))))) |
56 | 22, 51, 55 | mpbir2and 959 |
1
⊢ ((𝑆 ∈ NrmGrp ∧ { 0 } ⊊
𝑉) → (𝑁‘( I ↾ 𝑉)) = 1) |