Step | Hyp | Ref
| Expression |
1 | | nmlno0lem.u |
. . . . . . . . . . . . . . 15
⊢ 𝑈 ∈ NrmCVec |
2 | | nmlno0lem.1 |
. . . . . . . . . . . . . . . 16
⊢ 𝑋 = (BaseSet‘𝑈) |
3 | | nmlno0lem.k |
. . . . . . . . . . . . . . . 16
⊢ 𝐾 =
(normCV‘𝑈) |
4 | 2, 3 | nvcl 28608 |
. . . . . . . . . . . . . . 15
⊢ ((𝑈 ∈ NrmCVec ∧ 𝑥 ∈ 𝑋) → (𝐾‘𝑥) ∈ ℝ) |
5 | 1, 4 | mpan 690 |
. . . . . . . . . . . . . 14
⊢ (𝑥 ∈ 𝑋 → (𝐾‘𝑥) ∈ ℝ) |
6 | 5 | recnd 10759 |
. . . . . . . . . . . . 13
⊢ (𝑥 ∈ 𝑋 → (𝐾‘𝑥) ∈ ℂ) |
7 | 6 | adantr 484 |
. . . . . . . . . . . 12
⊢ ((𝑥 ∈ 𝑋 ∧ (𝑇‘𝑥) ≠ 𝑄) → (𝐾‘𝑥) ∈ ℂ) |
8 | | nmlno0lem.p |
. . . . . . . . . . . . . . . . 17
⊢ 𝑃 = (0vec‘𝑈) |
9 | 2, 8, 3 | nvz 28616 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑈 ∈ NrmCVec ∧ 𝑥 ∈ 𝑋) → ((𝐾‘𝑥) = 0 ↔ 𝑥 = 𝑃)) |
10 | 1, 9 | mpan 690 |
. . . . . . . . . . . . . . 15
⊢ (𝑥 ∈ 𝑋 → ((𝐾‘𝑥) = 0 ↔ 𝑥 = 𝑃)) |
11 | | fveq2 6686 |
. . . . . . . . . . . . . . . 16
⊢ (𝑥 = 𝑃 → (𝑇‘𝑥) = (𝑇‘𝑃)) |
12 | | nmlno0lem.w |
. . . . . . . . . . . . . . . . 17
⊢ 𝑊 ∈ NrmCVec |
13 | | nmlno0lem.l |
. . . . . . . . . . . . . . . . 17
⊢ 𝑇 ∈ 𝐿 |
14 | | nmlno0lem.2 |
. . . . . . . . . . . . . . . . . 18
⊢ 𝑌 = (BaseSet‘𝑊) |
15 | | nmlno0lem.q |
. . . . . . . . . . . . . . . . . 18
⊢ 𝑄 = (0vec‘𝑊) |
16 | | nmlno0.7 |
. . . . . . . . . . . . . . . . . 18
⊢ 𝐿 = (𝑈 LnOp 𝑊) |
17 | 2, 14, 8, 15, 16 | lno0 28703 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑈 ∈ NrmCVec ∧ 𝑊 ∈ NrmCVec ∧ 𝑇 ∈ 𝐿) → (𝑇‘𝑃) = 𝑄) |
18 | 1, 12, 13, 17 | mp3an 1462 |
. . . . . . . . . . . . . . . 16
⊢ (𝑇‘𝑃) = 𝑄 |
19 | 11, 18 | eqtrdi 2790 |
. . . . . . . . . . . . . . 15
⊢ (𝑥 = 𝑃 → (𝑇‘𝑥) = 𝑄) |
20 | 10, 19 | syl6bi 256 |
. . . . . . . . . . . . . 14
⊢ (𝑥 ∈ 𝑋 → ((𝐾‘𝑥) = 0 → (𝑇‘𝑥) = 𝑄)) |
21 | 20 | necon3d 2956 |
. . . . . . . . . . . . 13
⊢ (𝑥 ∈ 𝑋 → ((𝑇‘𝑥) ≠ 𝑄 → (𝐾‘𝑥) ≠ 0)) |
22 | 21 | imp 410 |
. . . . . . . . . . . 12
⊢ ((𝑥 ∈ 𝑋 ∧ (𝑇‘𝑥) ≠ 𝑄) → (𝐾‘𝑥) ≠ 0) |
23 | 7, 22 | recne0d 11500 |
. . . . . . . . . . 11
⊢ ((𝑥 ∈ 𝑋 ∧ (𝑇‘𝑥) ≠ 𝑄) → (1 / (𝐾‘𝑥)) ≠ 0) |
24 | | simpr 488 |
. . . . . . . . . . 11
⊢ ((𝑥 ∈ 𝑋 ∧ (𝑇‘𝑥) ≠ 𝑄) → (𝑇‘𝑥) ≠ 𝑄) |
25 | 7, 22 | reccld 11499 |
. . . . . . . . . . . . . 14
⊢ ((𝑥 ∈ 𝑋 ∧ (𝑇‘𝑥) ≠ 𝑄) → (1 / (𝐾‘𝑥)) ∈ ℂ) |
26 | 2, 14, 16 | lnof 28702 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑈 ∈ NrmCVec ∧ 𝑊 ∈ NrmCVec ∧ 𝑇 ∈ 𝐿) → 𝑇:𝑋⟶𝑌) |
27 | 1, 12, 13, 26 | mp3an 1462 |
. . . . . . . . . . . . . . . 16
⊢ 𝑇:𝑋⟶𝑌 |
28 | 27 | ffvelrni 6872 |
. . . . . . . . . . . . . . 15
⊢ (𝑥 ∈ 𝑋 → (𝑇‘𝑥) ∈ 𝑌) |
29 | 28 | adantr 484 |
. . . . . . . . . . . . . 14
⊢ ((𝑥 ∈ 𝑋 ∧ (𝑇‘𝑥) ≠ 𝑄) → (𝑇‘𝑥) ∈ 𝑌) |
30 | | nmlno0lem.s |
. . . . . . . . . . . . . . . 16
⊢ 𝑆 = (
·𝑠OLD ‘𝑊) |
31 | 14, 30, 15 | nvmul0or 28597 |
. . . . . . . . . . . . . . 15
⊢ ((𝑊 ∈ NrmCVec ∧ (1 /
(𝐾‘𝑥)) ∈ ℂ ∧ (𝑇‘𝑥) ∈ 𝑌) → (((1 / (𝐾‘𝑥))𝑆(𝑇‘𝑥)) = 𝑄 ↔ ((1 / (𝐾‘𝑥)) = 0 ∨ (𝑇‘𝑥) = 𝑄))) |
32 | 12, 31 | mp3an1 1449 |
. . . . . . . . . . . . . 14
⊢ (((1 /
(𝐾‘𝑥)) ∈ ℂ ∧ (𝑇‘𝑥) ∈ 𝑌) → (((1 / (𝐾‘𝑥))𝑆(𝑇‘𝑥)) = 𝑄 ↔ ((1 / (𝐾‘𝑥)) = 0 ∨ (𝑇‘𝑥) = 𝑄))) |
33 | 25, 29, 32 | syl2anc 587 |
. . . . . . . . . . . . 13
⊢ ((𝑥 ∈ 𝑋 ∧ (𝑇‘𝑥) ≠ 𝑄) → (((1 / (𝐾‘𝑥))𝑆(𝑇‘𝑥)) = 𝑄 ↔ ((1 / (𝐾‘𝑥)) = 0 ∨ (𝑇‘𝑥) = 𝑄))) |
34 | 33 | necon3abid 2971 |
. . . . . . . . . . . 12
⊢ ((𝑥 ∈ 𝑋 ∧ (𝑇‘𝑥) ≠ 𝑄) → (((1 / (𝐾‘𝑥))𝑆(𝑇‘𝑥)) ≠ 𝑄 ↔ ¬ ((1 / (𝐾‘𝑥)) = 0 ∨ (𝑇‘𝑥) = 𝑄))) |
35 | | neanior 3027 |
. . . . . . . . . . . 12
⊢ (((1 /
(𝐾‘𝑥)) ≠ 0 ∧ (𝑇‘𝑥) ≠ 𝑄) ↔ ¬ ((1 / (𝐾‘𝑥)) = 0 ∨ (𝑇‘𝑥) = 𝑄)) |
36 | 34, 35 | bitr4di 292 |
. . . . . . . . . . 11
⊢ ((𝑥 ∈ 𝑋 ∧ (𝑇‘𝑥) ≠ 𝑄) → (((1 / (𝐾‘𝑥))𝑆(𝑇‘𝑥)) ≠ 𝑄 ↔ ((1 / (𝐾‘𝑥)) ≠ 0 ∧ (𝑇‘𝑥) ≠ 𝑄))) |
37 | 23, 24, 36 | mpbir2and 713 |
. . . . . . . . . 10
⊢ ((𝑥 ∈ 𝑋 ∧ (𝑇‘𝑥) ≠ 𝑄) → ((1 / (𝐾‘𝑥))𝑆(𝑇‘𝑥)) ≠ 𝑄) |
38 | 14, 30 | nvscl 28573 |
. . . . . . . . . . . . 13
⊢ ((𝑊 ∈ NrmCVec ∧ (1 /
(𝐾‘𝑥)) ∈ ℂ ∧ (𝑇‘𝑥) ∈ 𝑌) → ((1 / (𝐾‘𝑥))𝑆(𝑇‘𝑥)) ∈ 𝑌) |
39 | 12, 38 | mp3an1 1449 |
. . . . . . . . . . . 12
⊢ (((1 /
(𝐾‘𝑥)) ∈ ℂ ∧ (𝑇‘𝑥) ∈ 𝑌) → ((1 / (𝐾‘𝑥))𝑆(𝑇‘𝑥)) ∈ 𝑌) |
40 | 25, 29, 39 | syl2anc 587 |
. . . . . . . . . . 11
⊢ ((𝑥 ∈ 𝑋 ∧ (𝑇‘𝑥) ≠ 𝑄) → ((1 / (𝐾‘𝑥))𝑆(𝑇‘𝑥)) ∈ 𝑌) |
41 | | nmlno0lem.m |
. . . . . . . . . . . 12
⊢ 𝑀 =
(normCV‘𝑊) |
42 | 14, 15, 41 | nvgt0 28621 |
. . . . . . . . . . 11
⊢ ((𝑊 ∈ NrmCVec ∧ ((1 /
(𝐾‘𝑥))𝑆(𝑇‘𝑥)) ∈ 𝑌) → (((1 / (𝐾‘𝑥))𝑆(𝑇‘𝑥)) ≠ 𝑄 ↔ 0 < (𝑀‘((1 / (𝐾‘𝑥))𝑆(𝑇‘𝑥))))) |
43 | 12, 40, 42 | sylancr 590 |
. . . . . . . . . 10
⊢ ((𝑥 ∈ 𝑋 ∧ (𝑇‘𝑥) ≠ 𝑄) → (((1 / (𝐾‘𝑥))𝑆(𝑇‘𝑥)) ≠ 𝑄 ↔ 0 < (𝑀‘((1 / (𝐾‘𝑥))𝑆(𝑇‘𝑥))))) |
44 | 37, 43 | mpbid 235 |
. . . . . . . . 9
⊢ ((𝑥 ∈ 𝑋 ∧ (𝑇‘𝑥) ≠ 𝑄) → 0 < (𝑀‘((1 / (𝐾‘𝑥))𝑆(𝑇‘𝑥)))) |
45 | 44 | ex 416 |
. . . . . . . 8
⊢ (𝑥 ∈ 𝑋 → ((𝑇‘𝑥) ≠ 𝑄 → 0 < (𝑀‘((1 / (𝐾‘𝑥))𝑆(𝑇‘𝑥))))) |
46 | 45 | adantl 485 |
. . . . . . 7
⊢ (((𝑁‘𝑇) = 0 ∧ 𝑥 ∈ 𝑋) → ((𝑇‘𝑥) ≠ 𝑄 → 0 < (𝑀‘((1 / (𝐾‘𝑥))𝑆(𝑇‘𝑥))))) |
47 | 14, 41 | nmosetre 28711 |
. . . . . . . . . . . . . 14
⊢ ((𝑊 ∈ NrmCVec ∧ 𝑇:𝑋⟶𝑌) → {𝑦 ∣ ∃𝑧 ∈ 𝑋 ((𝐾‘𝑧) ≤ 1 ∧ 𝑦 = (𝑀‘(𝑇‘𝑧)))} ⊆ ℝ) |
48 | 12, 27, 47 | mp2an 692 |
. . . . . . . . . . . . 13
⊢ {𝑦 ∣ ∃𝑧 ∈ 𝑋 ((𝐾‘𝑧) ≤ 1 ∧ 𝑦 = (𝑀‘(𝑇‘𝑧)))} ⊆ ℝ |
49 | | ressxr 10775 |
. . . . . . . . . . . . 13
⊢ ℝ
⊆ ℝ* |
50 | 48, 49 | sstri 3896 |
. . . . . . . . . . . 12
⊢ {𝑦 ∣ ∃𝑧 ∈ 𝑋 ((𝐾‘𝑧) ≤ 1 ∧ 𝑦 = (𝑀‘(𝑇‘𝑧)))} ⊆
ℝ* |
51 | | simpl 486 |
. . . . . . . . . . . . . . 15
⊢ ((𝑥 ∈ 𝑋 ∧ (𝑇‘𝑥) ≠ 𝑄) → 𝑥 ∈ 𝑋) |
52 | | nmlno0lem.r |
. . . . . . . . . . . . . . . . 17
⊢ 𝑅 = (
·𝑠OLD ‘𝑈) |
53 | 2, 52 | nvscl 28573 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑈 ∈ NrmCVec ∧ (1 /
(𝐾‘𝑥)) ∈ ℂ ∧ 𝑥 ∈ 𝑋) → ((1 / (𝐾‘𝑥))𝑅𝑥) ∈ 𝑋) |
54 | 1, 53 | mp3an1 1449 |
. . . . . . . . . . . . . . 15
⊢ (((1 /
(𝐾‘𝑥)) ∈ ℂ ∧ 𝑥 ∈ 𝑋) → ((1 / (𝐾‘𝑥))𝑅𝑥) ∈ 𝑋) |
55 | 25, 51, 54 | syl2anc 587 |
. . . . . . . . . . . . . 14
⊢ ((𝑥 ∈ 𝑋 ∧ (𝑇‘𝑥) ≠ 𝑄) → ((1 / (𝐾‘𝑥))𝑅𝑥) ∈ 𝑋) |
56 | 19 | necon3i 2967 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑇‘𝑥) ≠ 𝑄 → 𝑥 ≠ 𝑃) |
57 | 2, 52, 8, 3 | nv1 28622 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝑈 ∈ NrmCVec ∧ 𝑥 ∈ 𝑋 ∧ 𝑥 ≠ 𝑃) → (𝐾‘((1 / (𝐾‘𝑥))𝑅𝑥)) = 1) |
58 | 1, 57 | mp3an1 1449 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑥 ∈ 𝑋 ∧ 𝑥 ≠ 𝑃) → (𝐾‘((1 / (𝐾‘𝑥))𝑅𝑥)) = 1) |
59 | 56, 58 | sylan2 596 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑥 ∈ 𝑋 ∧ (𝑇‘𝑥) ≠ 𝑄) → (𝐾‘((1 / (𝐾‘𝑥))𝑅𝑥)) = 1) |
60 | | 1re 10731 |
. . . . . . . . . . . . . . . 16
⊢ 1 ∈
ℝ |
61 | 59, 60 | eqeltrdi 2842 |
. . . . . . . . . . . . . . 15
⊢ ((𝑥 ∈ 𝑋 ∧ (𝑇‘𝑥) ≠ 𝑄) → (𝐾‘((1 / (𝐾‘𝑥))𝑅𝑥)) ∈ ℝ) |
62 | | eqle 10832 |
. . . . . . . . . . . . . . 15
⊢ (((𝐾‘((1 / (𝐾‘𝑥))𝑅𝑥)) ∈ ℝ ∧ (𝐾‘((1 / (𝐾‘𝑥))𝑅𝑥)) = 1) → (𝐾‘((1 / (𝐾‘𝑥))𝑅𝑥)) ≤ 1) |
63 | 61, 59, 62 | syl2anc 587 |
. . . . . . . . . . . . . 14
⊢ ((𝑥 ∈ 𝑋 ∧ (𝑇‘𝑥) ≠ 𝑄) → (𝐾‘((1 / (𝐾‘𝑥))𝑅𝑥)) ≤ 1) |
64 | 1, 12, 13 | 3pm3.2i 1340 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑈 ∈ NrmCVec ∧ 𝑊 ∈ NrmCVec ∧ 𝑇 ∈ 𝐿) |
65 | 2, 52, 30, 16 | lnomul 28707 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝑈 ∈ NrmCVec ∧ 𝑊 ∈ NrmCVec ∧ 𝑇 ∈ 𝐿) ∧ ((1 / (𝐾‘𝑥)) ∈ ℂ ∧ 𝑥 ∈ 𝑋)) → (𝑇‘((1 / (𝐾‘𝑥))𝑅𝑥)) = ((1 / (𝐾‘𝑥))𝑆(𝑇‘𝑥))) |
66 | 64, 65 | mpan 690 |
. . . . . . . . . . . . . . . . 17
⊢ (((1 /
(𝐾‘𝑥)) ∈ ℂ ∧ 𝑥 ∈ 𝑋) → (𝑇‘((1 / (𝐾‘𝑥))𝑅𝑥)) = ((1 / (𝐾‘𝑥))𝑆(𝑇‘𝑥))) |
67 | 25, 51, 66 | syl2anc 587 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑥 ∈ 𝑋 ∧ (𝑇‘𝑥) ≠ 𝑄) → (𝑇‘((1 / (𝐾‘𝑥))𝑅𝑥)) = ((1 / (𝐾‘𝑥))𝑆(𝑇‘𝑥))) |
68 | 67 | eqcomd 2745 |
. . . . . . . . . . . . . . 15
⊢ ((𝑥 ∈ 𝑋 ∧ (𝑇‘𝑥) ≠ 𝑄) → ((1 / (𝐾‘𝑥))𝑆(𝑇‘𝑥)) = (𝑇‘((1 / (𝐾‘𝑥))𝑅𝑥))) |
69 | 68 | fveq2d 6690 |
. . . . . . . . . . . . . 14
⊢ ((𝑥 ∈ 𝑋 ∧ (𝑇‘𝑥) ≠ 𝑄) → (𝑀‘((1 / (𝐾‘𝑥))𝑆(𝑇‘𝑥))) = (𝑀‘(𝑇‘((1 / (𝐾‘𝑥))𝑅𝑥)))) |
70 | | fveq2 6686 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑧 = ((1 / (𝐾‘𝑥))𝑅𝑥) → (𝐾‘𝑧) = (𝐾‘((1 / (𝐾‘𝑥))𝑅𝑥))) |
71 | 70 | breq1d 5050 |
. . . . . . . . . . . . . . . 16
⊢ (𝑧 = ((1 / (𝐾‘𝑥))𝑅𝑥) → ((𝐾‘𝑧) ≤ 1 ↔ (𝐾‘((1 / (𝐾‘𝑥))𝑅𝑥)) ≤ 1)) |
72 | | 2fveq3 6691 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑧 = ((1 / (𝐾‘𝑥))𝑅𝑥) → (𝑀‘(𝑇‘𝑧)) = (𝑀‘(𝑇‘((1 / (𝐾‘𝑥))𝑅𝑥)))) |
73 | 72 | eqeq2d 2750 |
. . . . . . . . . . . . . . . 16
⊢ (𝑧 = ((1 / (𝐾‘𝑥))𝑅𝑥) → ((𝑀‘((1 / (𝐾‘𝑥))𝑆(𝑇‘𝑥))) = (𝑀‘(𝑇‘𝑧)) ↔ (𝑀‘((1 / (𝐾‘𝑥))𝑆(𝑇‘𝑥))) = (𝑀‘(𝑇‘((1 / (𝐾‘𝑥))𝑅𝑥))))) |
74 | 71, 73 | anbi12d 634 |
. . . . . . . . . . . . . . 15
⊢ (𝑧 = ((1 / (𝐾‘𝑥))𝑅𝑥) → (((𝐾‘𝑧) ≤ 1 ∧ (𝑀‘((1 / (𝐾‘𝑥))𝑆(𝑇‘𝑥))) = (𝑀‘(𝑇‘𝑧))) ↔ ((𝐾‘((1 / (𝐾‘𝑥))𝑅𝑥)) ≤ 1 ∧ (𝑀‘((1 / (𝐾‘𝑥))𝑆(𝑇‘𝑥))) = (𝑀‘(𝑇‘((1 / (𝐾‘𝑥))𝑅𝑥)))))) |
75 | 74 | rspcev 3529 |
. . . . . . . . . . . . . 14
⊢ ((((1 /
(𝐾‘𝑥))𝑅𝑥) ∈ 𝑋 ∧ ((𝐾‘((1 / (𝐾‘𝑥))𝑅𝑥)) ≤ 1 ∧ (𝑀‘((1 / (𝐾‘𝑥))𝑆(𝑇‘𝑥))) = (𝑀‘(𝑇‘((1 / (𝐾‘𝑥))𝑅𝑥))))) → ∃𝑧 ∈ 𝑋 ((𝐾‘𝑧) ≤ 1 ∧ (𝑀‘((1 / (𝐾‘𝑥))𝑆(𝑇‘𝑥))) = (𝑀‘(𝑇‘𝑧)))) |
76 | 55, 63, 69, 75 | syl12anc 836 |
. . . . . . . . . . . . 13
⊢ ((𝑥 ∈ 𝑋 ∧ (𝑇‘𝑥) ≠ 𝑄) → ∃𝑧 ∈ 𝑋 ((𝐾‘𝑧) ≤ 1 ∧ (𝑀‘((1 / (𝐾‘𝑥))𝑆(𝑇‘𝑥))) = (𝑀‘(𝑇‘𝑧)))) |
77 | | fvex 6699 |
. . . . . . . . . . . . . 14
⊢ (𝑀‘((1 / (𝐾‘𝑥))𝑆(𝑇‘𝑥))) ∈ V |
78 | | eqeq1 2743 |
. . . . . . . . . . . . . . . 16
⊢ (𝑦 = (𝑀‘((1 / (𝐾‘𝑥))𝑆(𝑇‘𝑥))) → (𝑦 = (𝑀‘(𝑇‘𝑧)) ↔ (𝑀‘((1 / (𝐾‘𝑥))𝑆(𝑇‘𝑥))) = (𝑀‘(𝑇‘𝑧)))) |
79 | 78 | anbi2d 632 |
. . . . . . . . . . . . . . 15
⊢ (𝑦 = (𝑀‘((1 / (𝐾‘𝑥))𝑆(𝑇‘𝑥))) → (((𝐾‘𝑧) ≤ 1 ∧ 𝑦 = (𝑀‘(𝑇‘𝑧))) ↔ ((𝐾‘𝑧) ≤ 1 ∧ (𝑀‘((1 / (𝐾‘𝑥))𝑆(𝑇‘𝑥))) = (𝑀‘(𝑇‘𝑧))))) |
80 | 79 | rexbidv 3208 |
. . . . . . . . . . . . . 14
⊢ (𝑦 = (𝑀‘((1 / (𝐾‘𝑥))𝑆(𝑇‘𝑥))) → (∃𝑧 ∈ 𝑋 ((𝐾‘𝑧) ≤ 1 ∧ 𝑦 = (𝑀‘(𝑇‘𝑧))) ↔ ∃𝑧 ∈ 𝑋 ((𝐾‘𝑧) ≤ 1 ∧ (𝑀‘((1 / (𝐾‘𝑥))𝑆(𝑇‘𝑥))) = (𝑀‘(𝑇‘𝑧))))) |
81 | 77, 80 | elab 3578 |
. . . . . . . . . . . . 13
⊢ ((𝑀‘((1 / (𝐾‘𝑥))𝑆(𝑇‘𝑥))) ∈ {𝑦 ∣ ∃𝑧 ∈ 𝑋 ((𝐾‘𝑧) ≤ 1 ∧ 𝑦 = (𝑀‘(𝑇‘𝑧)))} ↔ ∃𝑧 ∈ 𝑋 ((𝐾‘𝑧) ≤ 1 ∧ (𝑀‘((1 / (𝐾‘𝑥))𝑆(𝑇‘𝑥))) = (𝑀‘(𝑇‘𝑧)))) |
82 | 76, 81 | sylibr 237 |
. . . . . . . . . . . 12
⊢ ((𝑥 ∈ 𝑋 ∧ (𝑇‘𝑥) ≠ 𝑄) → (𝑀‘((1 / (𝐾‘𝑥))𝑆(𝑇‘𝑥))) ∈ {𝑦 ∣ ∃𝑧 ∈ 𝑋 ((𝐾‘𝑧) ≤ 1 ∧ 𝑦 = (𝑀‘(𝑇‘𝑧)))}) |
83 | | supxrub 12812 |
. . . . . . . . . . . 12
⊢ (({𝑦 ∣ ∃𝑧 ∈ 𝑋 ((𝐾‘𝑧) ≤ 1 ∧ 𝑦 = (𝑀‘(𝑇‘𝑧)))} ⊆ ℝ* ∧ (𝑀‘((1 / (𝐾‘𝑥))𝑆(𝑇‘𝑥))) ∈ {𝑦 ∣ ∃𝑧 ∈ 𝑋 ((𝐾‘𝑧) ≤ 1 ∧ 𝑦 = (𝑀‘(𝑇‘𝑧)))}) → (𝑀‘((1 / (𝐾‘𝑥))𝑆(𝑇‘𝑥))) ≤ sup({𝑦 ∣ ∃𝑧 ∈ 𝑋 ((𝐾‘𝑧) ≤ 1 ∧ 𝑦 = (𝑀‘(𝑇‘𝑧)))}, ℝ*, <
)) |
84 | 50, 82, 83 | sylancr 590 |
. . . . . . . . . . 11
⊢ ((𝑥 ∈ 𝑋 ∧ (𝑇‘𝑥) ≠ 𝑄) → (𝑀‘((1 / (𝐾‘𝑥))𝑆(𝑇‘𝑥))) ≤ sup({𝑦 ∣ ∃𝑧 ∈ 𝑋 ((𝐾‘𝑧) ≤ 1 ∧ 𝑦 = (𝑀‘(𝑇‘𝑧)))}, ℝ*, <
)) |
85 | 84 | adantll 714 |
. . . . . . . . . 10
⊢ ((((𝑁‘𝑇) = 0 ∧ 𝑥 ∈ 𝑋) ∧ (𝑇‘𝑥) ≠ 𝑄) → (𝑀‘((1 / (𝐾‘𝑥))𝑆(𝑇‘𝑥))) ≤ sup({𝑦 ∣ ∃𝑧 ∈ 𝑋 ((𝐾‘𝑧) ≤ 1 ∧ 𝑦 = (𝑀‘(𝑇‘𝑧)))}, ℝ*, <
)) |
86 | | nmlno0.3 |
. . . . . . . . . . . . . . 15
⊢ 𝑁 = (𝑈 normOpOLD 𝑊) |
87 | 2, 14, 3, 41, 86 | nmooval 28710 |
. . . . . . . . . . . . . 14
⊢ ((𝑈 ∈ NrmCVec ∧ 𝑊 ∈ NrmCVec ∧ 𝑇:𝑋⟶𝑌) → (𝑁‘𝑇) = sup({𝑦 ∣ ∃𝑧 ∈ 𝑋 ((𝐾‘𝑧) ≤ 1 ∧ 𝑦 = (𝑀‘(𝑇‘𝑧)))}, ℝ*, <
)) |
88 | 1, 12, 27, 87 | mp3an 1462 |
. . . . . . . . . . . . 13
⊢ (𝑁‘𝑇) = sup({𝑦 ∣ ∃𝑧 ∈ 𝑋 ((𝐾‘𝑧) ≤ 1 ∧ 𝑦 = (𝑀‘(𝑇‘𝑧)))}, ℝ*, <
) |
89 | 88 | eqeq1i 2744 |
. . . . . . . . . . . 12
⊢ ((𝑁‘𝑇) = 0 ↔ sup({𝑦 ∣ ∃𝑧 ∈ 𝑋 ((𝐾‘𝑧) ≤ 1 ∧ 𝑦 = (𝑀‘(𝑇‘𝑧)))}, ℝ*, < ) =
0) |
90 | 89 | biimpi 219 |
. . . . . . . . . . 11
⊢ ((𝑁‘𝑇) = 0 → sup({𝑦 ∣ ∃𝑧 ∈ 𝑋 ((𝐾‘𝑧) ≤ 1 ∧ 𝑦 = (𝑀‘(𝑇‘𝑧)))}, ℝ*, < ) =
0) |
91 | 90 | ad2antrr 726 |
. . . . . . . . . 10
⊢ ((((𝑁‘𝑇) = 0 ∧ 𝑥 ∈ 𝑋) ∧ (𝑇‘𝑥) ≠ 𝑄) → sup({𝑦 ∣ ∃𝑧 ∈ 𝑋 ((𝐾‘𝑧) ≤ 1 ∧ 𝑦 = (𝑀‘(𝑇‘𝑧)))}, ℝ*, < ) =
0) |
92 | 85, 91 | breqtrd 5066 |
. . . . . . . . 9
⊢ ((((𝑁‘𝑇) = 0 ∧ 𝑥 ∈ 𝑋) ∧ (𝑇‘𝑥) ≠ 𝑄) → (𝑀‘((1 / (𝐾‘𝑥))𝑆(𝑇‘𝑥))) ≤ 0) |
93 | 14, 41 | nvcl 28608 |
. . . . . . . . . . . 12
⊢ ((𝑊 ∈ NrmCVec ∧ ((1 /
(𝐾‘𝑥))𝑆(𝑇‘𝑥)) ∈ 𝑌) → (𝑀‘((1 / (𝐾‘𝑥))𝑆(𝑇‘𝑥))) ∈ ℝ) |
94 | 12, 40, 93 | sylancr 590 |
. . . . . . . . . . 11
⊢ ((𝑥 ∈ 𝑋 ∧ (𝑇‘𝑥) ≠ 𝑄) → (𝑀‘((1 / (𝐾‘𝑥))𝑆(𝑇‘𝑥))) ∈ ℝ) |
95 | | 0re 10733 |
. . . . . . . . . . 11
⊢ 0 ∈
ℝ |
96 | | lenlt 10809 |
. . . . . . . . . . 11
⊢ (((𝑀‘((1 / (𝐾‘𝑥))𝑆(𝑇‘𝑥))) ∈ ℝ ∧ 0 ∈ ℝ)
→ ((𝑀‘((1 /
(𝐾‘𝑥))𝑆(𝑇‘𝑥))) ≤ 0 ↔ ¬ 0 < (𝑀‘((1 / (𝐾‘𝑥))𝑆(𝑇‘𝑥))))) |
97 | 94, 95, 96 | sylancl 589 |
. . . . . . . . . 10
⊢ ((𝑥 ∈ 𝑋 ∧ (𝑇‘𝑥) ≠ 𝑄) → ((𝑀‘((1 / (𝐾‘𝑥))𝑆(𝑇‘𝑥))) ≤ 0 ↔ ¬ 0 < (𝑀‘((1 / (𝐾‘𝑥))𝑆(𝑇‘𝑥))))) |
98 | 97 | adantll 714 |
. . . . . . . . 9
⊢ ((((𝑁‘𝑇) = 0 ∧ 𝑥 ∈ 𝑋) ∧ (𝑇‘𝑥) ≠ 𝑄) → ((𝑀‘((1 / (𝐾‘𝑥))𝑆(𝑇‘𝑥))) ≤ 0 ↔ ¬ 0 < (𝑀‘((1 / (𝐾‘𝑥))𝑆(𝑇‘𝑥))))) |
99 | 92, 98 | mpbid 235 |
. . . . . . . 8
⊢ ((((𝑁‘𝑇) = 0 ∧ 𝑥 ∈ 𝑋) ∧ (𝑇‘𝑥) ≠ 𝑄) → ¬ 0 < (𝑀‘((1 / (𝐾‘𝑥))𝑆(𝑇‘𝑥)))) |
100 | 99 | ex 416 |
. . . . . . 7
⊢ (((𝑁‘𝑇) = 0 ∧ 𝑥 ∈ 𝑋) → ((𝑇‘𝑥) ≠ 𝑄 → ¬ 0 < (𝑀‘((1 / (𝐾‘𝑥))𝑆(𝑇‘𝑥))))) |
101 | 46, 100 | pm2.65d 199 |
. . . . . 6
⊢ (((𝑁‘𝑇) = 0 ∧ 𝑥 ∈ 𝑋) → ¬ (𝑇‘𝑥) ≠ 𝑄) |
102 | | nne 2939 |
. . . . . 6
⊢ (¬
(𝑇‘𝑥) ≠ 𝑄 ↔ (𝑇‘𝑥) = 𝑄) |
103 | 101, 102 | sylib 221 |
. . . . 5
⊢ (((𝑁‘𝑇) = 0 ∧ 𝑥 ∈ 𝑋) → (𝑇‘𝑥) = 𝑄) |
104 | | nmlno0.0 |
. . . . . . . 8
⊢ 𝑍 = (𝑈 0op 𝑊) |
105 | 2, 15, 104 | 0oval 28735 |
. . . . . . 7
⊢ ((𝑈 ∈ NrmCVec ∧ 𝑊 ∈ NrmCVec ∧ 𝑥 ∈ 𝑋) → (𝑍‘𝑥) = 𝑄) |
106 | 1, 12, 105 | mp3an12 1452 |
. . . . . 6
⊢ (𝑥 ∈ 𝑋 → (𝑍‘𝑥) = 𝑄) |
107 | 106 | adantl 485 |
. . . . 5
⊢ (((𝑁‘𝑇) = 0 ∧ 𝑥 ∈ 𝑋) → (𝑍‘𝑥) = 𝑄) |
108 | 103, 107 | eqtr4d 2777 |
. . . 4
⊢ (((𝑁‘𝑇) = 0 ∧ 𝑥 ∈ 𝑋) → (𝑇‘𝑥) = (𝑍‘𝑥)) |
109 | 108 | ralrimiva 3097 |
. . 3
⊢ ((𝑁‘𝑇) = 0 → ∀𝑥 ∈ 𝑋 (𝑇‘𝑥) = (𝑍‘𝑥)) |
110 | | ffn 6514 |
. . . . 5
⊢ (𝑇:𝑋⟶𝑌 → 𝑇 Fn 𝑋) |
111 | 27, 110 | ax-mp 5 |
. . . 4
⊢ 𝑇 Fn 𝑋 |
112 | 2, 14, 104 | 0oo 28736 |
. . . . . 6
⊢ ((𝑈 ∈ NrmCVec ∧ 𝑊 ∈ NrmCVec) → 𝑍:𝑋⟶𝑌) |
113 | 1, 12, 112 | mp2an 692 |
. . . . 5
⊢ 𝑍:𝑋⟶𝑌 |
114 | | ffn 6514 |
. . . . 5
⊢ (𝑍:𝑋⟶𝑌 → 𝑍 Fn 𝑋) |
115 | 113, 114 | ax-mp 5 |
. . . 4
⊢ 𝑍 Fn 𝑋 |
116 | | eqfnfv 6821 |
. . . 4
⊢ ((𝑇 Fn 𝑋 ∧ 𝑍 Fn 𝑋) → (𝑇 = 𝑍 ↔ ∀𝑥 ∈ 𝑋 (𝑇‘𝑥) = (𝑍‘𝑥))) |
117 | 111, 115,
116 | mp2an 692 |
. . 3
⊢ (𝑇 = 𝑍 ↔ ∀𝑥 ∈ 𝑋 (𝑇‘𝑥) = (𝑍‘𝑥)) |
118 | 109, 117 | sylibr 237 |
. 2
⊢ ((𝑁‘𝑇) = 0 → 𝑇 = 𝑍) |
119 | | fveq2 6686 |
. . 3
⊢ (𝑇 = 𝑍 → (𝑁‘𝑇) = (𝑁‘𝑍)) |
120 | 86, 104 | nmoo0 28738 |
. . . 4
⊢ ((𝑈 ∈ NrmCVec ∧ 𝑊 ∈ NrmCVec) → (𝑁‘𝑍) = 0) |
121 | 1, 12, 120 | mp2an 692 |
. . 3
⊢ (𝑁‘𝑍) = 0 |
122 | 119, 121 | eqtrdi 2790 |
. 2
⊢ (𝑇 = 𝑍 → (𝑁‘𝑇) = 0) |
123 | 118, 122 | impbii 212 |
1
⊢ ((𝑁‘𝑇) = 0 ↔ 𝑇 = 𝑍) |