| Step | Hyp | Ref
| Expression |
| 1 | | nmoid.1 |
. . 3
⊢ 𝑁 = (𝑆 normOp 𝑆) |
| 2 | | nmoid.2 |
. . 3
⊢ 𝑉 = (Base‘𝑆) |
| 3 | | eqid 2737 |
. . 3
⊢
(norm‘𝑆) =
(norm‘𝑆) |
| 4 | | nmoid.3 |
. . 3
⊢ 0 =
(0g‘𝑆) |
| 5 | | simpl 482 |
. . 3
⊢ ((𝑆 ∈ NrmGrp ∧ { 0 } ⊊
𝑉) → 𝑆 ∈ NrmGrp) |
| 6 | | ngpgrp 24612 |
. . . . 5
⊢ (𝑆 ∈ NrmGrp → 𝑆 ∈ Grp) |
| 7 | 6 | adantr 480 |
. . . 4
⊢ ((𝑆 ∈ NrmGrp ∧ { 0 } ⊊
𝑉) → 𝑆 ∈ Grp) |
| 8 | 2 | idghm 19249 |
. . . 4
⊢ (𝑆 ∈ Grp → ( I ↾
𝑉) ∈ (𝑆 GrpHom 𝑆)) |
| 9 | 7, 8 | syl 17 |
. . 3
⊢ ((𝑆 ∈ NrmGrp ∧ { 0 } ⊊
𝑉) → ( I ↾ 𝑉) ∈ (𝑆 GrpHom 𝑆)) |
| 10 | | 1red 11262 |
. . 3
⊢ ((𝑆 ∈ NrmGrp ∧ { 0 } ⊊
𝑉) → 1 ∈
ℝ) |
| 11 | | 0le1 11786 |
. . . 4
⊢ 0 ≤
1 |
| 12 | 11 | a1i 11 |
. . 3
⊢ ((𝑆 ∈ NrmGrp ∧ { 0 } ⊊
𝑉) → 0 ≤
1) |
| 13 | 2, 3 | nmcl 24629 |
. . . . . 6
⊢ ((𝑆 ∈ NrmGrp ∧ 𝑥 ∈ 𝑉) → ((norm‘𝑆)‘𝑥) ∈ ℝ) |
| 14 | 13 | ad2ant2r 747 |
. . . . 5
⊢ (((𝑆 ∈ NrmGrp ∧ { 0 } ⊊
𝑉) ∧ (𝑥 ∈ 𝑉 ∧ 𝑥 ≠ 0 )) →
((norm‘𝑆)‘𝑥) ∈
ℝ) |
| 15 | 14 | leidd 11829 |
. . . 4
⊢ (((𝑆 ∈ NrmGrp ∧ { 0 } ⊊
𝑉) ∧ (𝑥 ∈ 𝑉 ∧ 𝑥 ≠ 0 )) →
((norm‘𝑆)‘𝑥) ≤ ((norm‘𝑆)‘𝑥)) |
| 16 | | fvresi 7193 |
. . . . . 6
⊢ (𝑥 ∈ 𝑉 → (( I ↾ 𝑉)‘𝑥) = 𝑥) |
| 17 | 16 | ad2antrl 728 |
. . . . 5
⊢ (((𝑆 ∈ NrmGrp ∧ { 0 } ⊊
𝑉) ∧ (𝑥 ∈ 𝑉 ∧ 𝑥 ≠ 0 )) → (( I ↾
𝑉)‘𝑥) = 𝑥) |
| 18 | 17 | fveq2d 6910 |
. . . 4
⊢ (((𝑆 ∈ NrmGrp ∧ { 0 } ⊊
𝑉) ∧ (𝑥 ∈ 𝑉 ∧ 𝑥 ≠ 0 )) →
((norm‘𝑆)‘(( I
↾ 𝑉)‘𝑥)) = ((norm‘𝑆)‘𝑥)) |
| 19 | 14 | recnd 11289 |
. . . . 5
⊢ (((𝑆 ∈ NrmGrp ∧ { 0 } ⊊
𝑉) ∧ (𝑥 ∈ 𝑉 ∧ 𝑥 ≠ 0 )) →
((norm‘𝑆)‘𝑥) ∈
ℂ) |
| 20 | 19 | mullidd 11279 |
. . . 4
⊢ (((𝑆 ∈ NrmGrp ∧ { 0 } ⊊
𝑉) ∧ (𝑥 ∈ 𝑉 ∧ 𝑥 ≠ 0 )) → (1 ·
((norm‘𝑆)‘𝑥)) = ((norm‘𝑆)‘𝑥)) |
| 21 | 15, 18, 20 | 3brtr4d 5175 |
. . 3
⊢ (((𝑆 ∈ NrmGrp ∧ { 0 } ⊊
𝑉) ∧ (𝑥 ∈ 𝑉 ∧ 𝑥 ≠ 0 )) →
((norm‘𝑆)‘(( I
↾ 𝑉)‘𝑥)) ≤ (1 ·
((norm‘𝑆)‘𝑥))) |
| 22 | 1, 2, 3, 3, 4, 5, 5, 9, 10, 12, 21 | nmolb2d 24739 |
. 2
⊢ ((𝑆 ∈ NrmGrp ∧ { 0 } ⊊
𝑉) → (𝑁‘( I ↾ 𝑉)) ≤ 1) |
| 23 | | pssnel 4471 |
. . . 4
⊢ ({ 0 } ⊊
𝑉 → ∃𝑥(𝑥 ∈ 𝑉 ∧ ¬ 𝑥 ∈ { 0 })) |
| 24 | 23 | adantl 481 |
. . 3
⊢ ((𝑆 ∈ NrmGrp ∧ { 0 } ⊊
𝑉) → ∃𝑥(𝑥 ∈ 𝑉 ∧ ¬ 𝑥 ∈ { 0 })) |
| 25 | | velsn 4642 |
. . . . . 6
⊢ (𝑥 ∈ { 0 } ↔ 𝑥 = 0 ) |
| 26 | 25 | biimpri 228 |
. . . . 5
⊢ (𝑥 = 0 → 𝑥 ∈ { 0 }) |
| 27 | 26 | necon3bi 2967 |
. . . 4
⊢ (¬
𝑥 ∈ { 0 } →
𝑥 ≠ 0 ) |
| 28 | 20, 18 | eqtr4d 2780 |
. . . . . 6
⊢ (((𝑆 ∈ NrmGrp ∧ { 0 } ⊊
𝑉) ∧ (𝑥 ∈ 𝑉 ∧ 𝑥 ≠ 0 )) → (1 ·
((norm‘𝑆)‘𝑥)) = ((norm‘𝑆)‘(( I ↾ 𝑉)‘𝑥))) |
| 29 | 1 | nmocl 24741 |
. . . . . . . . . 10
⊢ ((𝑆 ∈ NrmGrp ∧ 𝑆 ∈ NrmGrp ∧ ( I ↾
𝑉) ∈ (𝑆 GrpHom 𝑆)) → (𝑁‘( I ↾ 𝑉)) ∈
ℝ*) |
| 30 | 5, 5, 9, 29 | syl3anc 1373 |
. . . . . . . . 9
⊢ ((𝑆 ∈ NrmGrp ∧ { 0 } ⊊
𝑉) → (𝑁‘( I ↾ 𝑉)) ∈
ℝ*) |
| 31 | 1 | nmoge0 24742 |
. . . . . . . . . 10
⊢ ((𝑆 ∈ NrmGrp ∧ 𝑆 ∈ NrmGrp ∧ ( I ↾
𝑉) ∈ (𝑆 GrpHom 𝑆)) → 0 ≤ (𝑁‘( I ↾ 𝑉))) |
| 32 | 5, 5, 9, 31 | syl3anc 1373 |
. . . . . . . . 9
⊢ ((𝑆 ∈ NrmGrp ∧ { 0 } ⊊
𝑉) → 0 ≤ (𝑁‘( I ↾ 𝑉))) |
| 33 | | xrrege0 13216 |
. . . . . . . . 9
⊢ ((((𝑁‘( I ↾ 𝑉)) ∈ ℝ*
∧ 1 ∈ ℝ) ∧ (0 ≤ (𝑁‘( I ↾ 𝑉)) ∧ (𝑁‘( I ↾ 𝑉)) ≤ 1)) → (𝑁‘( I ↾ 𝑉)) ∈ ℝ) |
| 34 | 30, 10, 32, 22, 33 | syl22anc 839 |
. . . . . . . 8
⊢ ((𝑆 ∈ NrmGrp ∧ { 0 } ⊊
𝑉) → (𝑁‘( I ↾ 𝑉)) ∈
ℝ) |
| 35 | 1 | isnghm2 24745 |
. . . . . . . . 9
⊢ ((𝑆 ∈ NrmGrp ∧ 𝑆 ∈ NrmGrp ∧ ( I ↾
𝑉) ∈ (𝑆 GrpHom 𝑆)) → (( I ↾ 𝑉) ∈ (𝑆 NGHom 𝑆) ↔ (𝑁‘( I ↾ 𝑉)) ∈ ℝ)) |
| 36 | 5, 5, 9, 35 | syl3anc 1373 |
. . . . . . . 8
⊢ ((𝑆 ∈ NrmGrp ∧ { 0 } ⊊
𝑉) → (( I ↾
𝑉) ∈ (𝑆 NGHom 𝑆) ↔ (𝑁‘( I ↾ 𝑉)) ∈ ℝ)) |
| 37 | 34, 36 | mpbird 257 |
. . . . . . 7
⊢ ((𝑆 ∈ NrmGrp ∧ { 0 } ⊊
𝑉) → ( I ↾ 𝑉) ∈ (𝑆 NGHom 𝑆)) |
| 38 | | simprl 771 |
. . . . . . 7
⊢ (((𝑆 ∈ NrmGrp ∧ { 0 } ⊊
𝑉) ∧ (𝑥 ∈ 𝑉 ∧ 𝑥 ≠ 0 )) → 𝑥 ∈ 𝑉) |
| 39 | 1, 2, 3, 3 | nmoi 24749 |
. . . . . . 7
⊢ ((( I
↾ 𝑉) ∈ (𝑆 NGHom 𝑆) ∧ 𝑥 ∈ 𝑉) → ((norm‘𝑆)‘(( I ↾ 𝑉)‘𝑥)) ≤ ((𝑁‘( I ↾ 𝑉)) · ((norm‘𝑆)‘𝑥))) |
| 40 | 37, 38, 39 | syl2an2r 685 |
. . . . . 6
⊢ (((𝑆 ∈ NrmGrp ∧ { 0 } ⊊
𝑉) ∧ (𝑥 ∈ 𝑉 ∧ 𝑥 ≠ 0 )) →
((norm‘𝑆)‘(( I
↾ 𝑉)‘𝑥)) ≤ ((𝑁‘( I ↾ 𝑉)) · ((norm‘𝑆)‘𝑥))) |
| 41 | 28, 40 | eqbrtrd 5165 |
. . . . 5
⊢ (((𝑆 ∈ NrmGrp ∧ { 0 } ⊊
𝑉) ∧ (𝑥 ∈ 𝑉 ∧ 𝑥 ≠ 0 )) → (1 ·
((norm‘𝑆)‘𝑥)) ≤ ((𝑁‘( I ↾ 𝑉)) · ((norm‘𝑆)‘𝑥))) |
| 42 | | 1red 11262 |
. . . . . 6
⊢ (((𝑆 ∈ NrmGrp ∧ { 0 } ⊊
𝑉) ∧ (𝑥 ∈ 𝑉 ∧ 𝑥 ≠ 0 )) → 1 ∈
ℝ) |
| 43 | 34 | adantr 480 |
. . . . . 6
⊢ (((𝑆 ∈ NrmGrp ∧ { 0 } ⊊
𝑉) ∧ (𝑥 ∈ 𝑉 ∧ 𝑥 ≠ 0 )) → (𝑁‘( I ↾ 𝑉)) ∈
ℝ) |
| 44 | 2, 3, 4 | nmrpcl 24633 |
. . . . . . . 8
⊢ ((𝑆 ∈ NrmGrp ∧ 𝑥 ∈ 𝑉 ∧ 𝑥 ≠ 0 ) →
((norm‘𝑆)‘𝑥) ∈
ℝ+) |
| 45 | 44 | 3expb 1121 |
. . . . . . 7
⊢ ((𝑆 ∈ NrmGrp ∧ (𝑥 ∈ 𝑉 ∧ 𝑥 ≠ 0 )) →
((norm‘𝑆)‘𝑥) ∈
ℝ+) |
| 46 | 45 | adantlr 715 |
. . . . . 6
⊢ (((𝑆 ∈ NrmGrp ∧ { 0 } ⊊
𝑉) ∧ (𝑥 ∈ 𝑉 ∧ 𝑥 ≠ 0 )) →
((norm‘𝑆)‘𝑥) ∈
ℝ+) |
| 47 | 42, 43, 46 | lemul1d 13120 |
. . . . 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 683 |
. . 3
⊢ (((𝑆 ∈ NrmGrp ∧ { 0 } ⊊
𝑉) ∧ (𝑥 ∈ 𝑉 ∧ ¬ 𝑥 ∈ { 0 })) → 1 ≤ (𝑁‘( I ↾ 𝑉))) |
| 50 | 24, 49 | exlimddv 1935 |
. 2
⊢ ((𝑆 ∈ NrmGrp ∧ { 0 } ⊊
𝑉) → 1 ≤ (𝑁‘( I ↾ 𝑉))) |
| 51 | | 1xr 11320 |
. . 3
⊢ 1 ∈
ℝ* |
| 52 | | xrletri3 13196 |
. . 3
⊢ (((𝑁‘( I ↾ 𝑉)) ∈ ℝ*
∧ 1 ∈ ℝ*) → ((𝑁‘( I ↾ 𝑉)) = 1 ↔ ((𝑁‘( I ↾ 𝑉)) ≤ 1 ∧ 1 ≤ (𝑁‘( I ↾ 𝑉))))) |
| 53 | 30, 51, 52 | sylancl 586 |
. 2
⊢ ((𝑆 ∈ NrmGrp ∧ { 0 } ⊊
𝑉) → ((𝑁‘( I ↾ 𝑉)) = 1 ↔ ((𝑁‘( I ↾ 𝑉)) ≤ 1 ∧ 1 ≤ (𝑁‘( I ↾ 𝑉))))) |
| 54 | 22, 50, 53 | mpbir2and 713 |
1
⊢ ((𝑆 ∈ NrmGrp ∧ { 0 } ⊊
𝑉) → (𝑁‘( I ↾ 𝑉)) = 1) |