Step | Hyp | Ref
| Expression |
1 | | nmlno0lem.u |
. . . . . . . . . . . . . . 15
⊢ 𝑈 ∈ NrmCVec |
2 | | nmlno0lem.1 |
. . . . . . . . . . . . . . . 16
⊢ 𝑋 = (BaseSet‘𝑈) |
3 | | nmlno0lem.k |
. . . . . . . . . . . . . . . 16
⊢ 𝐾 =
(normCV‘𝑈) |
4 | 2, 3 | nvcl 26900 |
. . . . . . . . . . . . . . 15
⊢ ((𝑈 ∈ NrmCVec ∧ 𝑥 ∈ 𝑋) → (𝐾‘𝑥) ∈ ℝ) |
5 | 1, 4 | mpan 702 |
. . . . . . . . . . . . . 14
⊢ (𝑥 ∈ 𝑋 → (𝐾‘𝑥) ∈ ℝ) |
6 | 5 | recnd 9947 |
. . . . . . . . . . . . 13
⊢ (𝑥 ∈ 𝑋 → (𝐾‘𝑥) ∈ ℂ) |
7 | 6 | adantr 480 |
. . . . . . . . . . . 12
⊢ ((𝑥 ∈ 𝑋 ∧ (𝑇‘𝑥) ≠ 𝑄) → (𝐾‘𝑥) ∈ ℂ) |
8 | | nmlno0lem.p |
. . . . . . . . . . . . . . . . 17
⊢ 𝑃 = (0vec‘𝑈) |
9 | 2, 8, 3 | nvz 26908 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑈 ∈ NrmCVec ∧ 𝑥 ∈ 𝑋) → ((𝐾‘𝑥) = 0 ↔ 𝑥 = 𝑃)) |
10 | 1, 9 | mpan 702 |
. . . . . . . . . . . . . . 15
⊢ (𝑥 ∈ 𝑋 → ((𝐾‘𝑥) = 0 ↔ 𝑥 = 𝑃)) |
11 | | fveq2 6103 |
. . . . . . . . . . . . . . . 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 26995 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑈 ∈ NrmCVec ∧ 𝑊 ∈ NrmCVec ∧ 𝑇 ∈ 𝐿) → (𝑇‘𝑃) = 𝑄) |
18 | 1, 12, 13, 17 | mp3an 1416 |
. . . . . . . . . . . . . . . 16
⊢ (𝑇‘𝑃) = 𝑄 |
19 | 11, 18 | syl6eq 2660 |
. . . . . . . . . . . . . . 15
⊢ (𝑥 = 𝑃 → (𝑇‘𝑥) = 𝑄) |
20 | 10, 19 | syl6bi 242 |
. . . . . . . . . . . . . 14
⊢ (𝑥 ∈ 𝑋 → ((𝐾‘𝑥) = 0 → (𝑇‘𝑥) = 𝑄)) |
21 | 20 | necon3d 2803 |
. . . . . . . . . . . . 13
⊢ (𝑥 ∈ 𝑋 → ((𝑇‘𝑥) ≠ 𝑄 → (𝐾‘𝑥) ≠ 0)) |
22 | 21 | imp 444 |
. . . . . . . . . . . 12
⊢ ((𝑥 ∈ 𝑋 ∧ (𝑇‘𝑥) ≠ 𝑄) → (𝐾‘𝑥) ≠ 0) |
23 | 7, 22 | recne0d 10674 |
. . . . . . . . . . 11
⊢ ((𝑥 ∈ 𝑋 ∧ (𝑇‘𝑥) ≠ 𝑄) → (1 / (𝐾‘𝑥)) ≠ 0) |
24 | | simpr 476 |
. . . . . . . . . . 11
⊢ ((𝑥 ∈ 𝑋 ∧ (𝑇‘𝑥) ≠ 𝑄) → (𝑇‘𝑥) ≠ 𝑄) |
25 | 7, 22 | reccld 10673 |
. . . . . . . . . . . . . 14
⊢ ((𝑥 ∈ 𝑋 ∧ (𝑇‘𝑥) ≠ 𝑄) → (1 / (𝐾‘𝑥)) ∈ ℂ) |
26 | 2, 14, 16 | lnof 26994 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑈 ∈ NrmCVec ∧ 𝑊 ∈ NrmCVec ∧ 𝑇 ∈ 𝐿) → 𝑇:𝑋⟶𝑌) |
27 | 1, 12, 13, 26 | mp3an 1416 |
. . . . . . . . . . . . . . . 16
⊢ 𝑇:𝑋⟶𝑌 |
28 | 27 | ffvelrni 6266 |
. . . . . . . . . . . . . . 15
⊢ (𝑥 ∈ 𝑋 → (𝑇‘𝑥) ∈ 𝑌) |
29 | 28 | adantr 480 |
. . . . . . . . . . . . . 14
⊢ ((𝑥 ∈ 𝑋 ∧ (𝑇‘𝑥) ≠ 𝑄) → (𝑇‘𝑥) ∈ 𝑌) |
30 | | nmlno0lem.s |
. . . . . . . . . . . . . . . 16
⊢ 𝑆 = (
·𝑠OLD ‘𝑊) |
31 | 14, 30, 15 | nvmul0or 26889 |
. . . . . . . . . . . . . . 15
⊢ ((𝑊 ∈ NrmCVec ∧ (1 /
(𝐾‘𝑥)) ∈ ℂ ∧ (𝑇‘𝑥) ∈ 𝑌) → (((1 / (𝐾‘𝑥))𝑆(𝑇‘𝑥)) = 𝑄 ↔ ((1 / (𝐾‘𝑥)) = 0 ∨ (𝑇‘𝑥) = 𝑄))) |
32 | 12, 31 | mp3an1 1403 |
. . . . . . . . . . . . . 14
⊢ (((1 /
(𝐾‘𝑥)) ∈ ℂ ∧ (𝑇‘𝑥) ∈ 𝑌) → (((1 / (𝐾‘𝑥))𝑆(𝑇‘𝑥)) = 𝑄 ↔ ((1 / (𝐾‘𝑥)) = 0 ∨ (𝑇‘𝑥) = 𝑄))) |
33 | 25, 29, 32 | syl2anc 691 |
. . . . . . . . . . . . 13
⊢ ((𝑥 ∈ 𝑋 ∧ (𝑇‘𝑥) ≠ 𝑄) → (((1 / (𝐾‘𝑥))𝑆(𝑇‘𝑥)) = 𝑄 ↔ ((1 / (𝐾‘𝑥)) = 0 ∨ (𝑇‘𝑥) = 𝑄))) |
34 | 33 | necon3abid 2818 |
. . . . . . . . . . . 12
⊢ ((𝑥 ∈ 𝑋 ∧ (𝑇‘𝑥) ≠ 𝑄) → (((1 / (𝐾‘𝑥))𝑆(𝑇‘𝑥)) ≠ 𝑄 ↔ ¬ ((1 / (𝐾‘𝑥)) = 0 ∨ (𝑇‘𝑥) = 𝑄))) |
35 | | neanior 2874 |
. . . . . . . . . . . 12
⊢ (((1 /
(𝐾‘𝑥)) ≠ 0 ∧ (𝑇‘𝑥) ≠ 𝑄) ↔ ¬ ((1 / (𝐾‘𝑥)) = 0 ∨ (𝑇‘𝑥) = 𝑄)) |
36 | 34, 35 | syl6bbr 277 |
. . . . . . . . . . 11
⊢ ((𝑥 ∈ 𝑋 ∧ (𝑇‘𝑥) ≠ 𝑄) → (((1 / (𝐾‘𝑥))𝑆(𝑇‘𝑥)) ≠ 𝑄 ↔ ((1 / (𝐾‘𝑥)) ≠ 0 ∧ (𝑇‘𝑥) ≠ 𝑄))) |
37 | 23, 24, 36 | mpbir2and 959 |
. . . . . . . . . 10
⊢ ((𝑥 ∈ 𝑋 ∧ (𝑇‘𝑥) ≠ 𝑄) → ((1 / (𝐾‘𝑥))𝑆(𝑇‘𝑥)) ≠ 𝑄) |
38 | 14, 30 | nvscl 26865 |
. . . . . . . . . . . . 13
⊢ ((𝑊 ∈ NrmCVec ∧ (1 /
(𝐾‘𝑥)) ∈ ℂ ∧ (𝑇‘𝑥) ∈ 𝑌) → ((1 / (𝐾‘𝑥))𝑆(𝑇‘𝑥)) ∈ 𝑌) |
39 | 12, 38 | mp3an1 1403 |
. . . . . . . . . . . 12
⊢ (((1 /
(𝐾‘𝑥)) ∈ ℂ ∧ (𝑇‘𝑥) ∈ 𝑌) → ((1 / (𝐾‘𝑥))𝑆(𝑇‘𝑥)) ∈ 𝑌) |
40 | 25, 29, 39 | syl2anc 691 |
. . . . . . . . . . 11
⊢ ((𝑥 ∈ 𝑋 ∧ (𝑇‘𝑥) ≠ 𝑄) → ((1 / (𝐾‘𝑥))𝑆(𝑇‘𝑥)) ∈ 𝑌) |
41 | | nmlno0lem.m |
. . . . . . . . . . . 12
⊢ 𝑀 =
(normCV‘𝑊) |
42 | 14, 15, 41 | nvgt0 26913 |
. . . . . . . . . . 11
⊢ ((𝑊 ∈ NrmCVec ∧ ((1 /
(𝐾‘𝑥))𝑆(𝑇‘𝑥)) ∈ 𝑌) → (((1 / (𝐾‘𝑥))𝑆(𝑇‘𝑥)) ≠ 𝑄 ↔ 0 < (𝑀‘((1 / (𝐾‘𝑥))𝑆(𝑇‘𝑥))))) |
43 | 12, 40, 42 | sylancr 694 |
. . . . . . . . . 10
⊢ ((𝑥 ∈ 𝑋 ∧ (𝑇‘𝑥) ≠ 𝑄) → (((1 / (𝐾‘𝑥))𝑆(𝑇‘𝑥)) ≠ 𝑄 ↔ 0 < (𝑀‘((1 / (𝐾‘𝑥))𝑆(𝑇‘𝑥))))) |
44 | 37, 43 | mpbid 221 |
. . . . . . . . 9
⊢ ((𝑥 ∈ 𝑋 ∧ (𝑇‘𝑥) ≠ 𝑄) → 0 < (𝑀‘((1 / (𝐾‘𝑥))𝑆(𝑇‘𝑥)))) |
45 | 44 | ex 449 |
. . . . . . . 8
⊢ (𝑥 ∈ 𝑋 → ((𝑇‘𝑥) ≠ 𝑄 → 0 < (𝑀‘((1 / (𝐾‘𝑥))𝑆(𝑇‘𝑥))))) |
46 | 45 | adantl 481 |
. . . . . . 7
⊢ (((𝑁‘𝑇) = 0 ∧ 𝑥 ∈ 𝑋) → ((𝑇‘𝑥) ≠ 𝑄 → 0 < (𝑀‘((1 / (𝐾‘𝑥))𝑆(𝑇‘𝑥))))) |
47 | 14, 41 | nmosetre 27003 |
. . . . . . . . . . . . . 14
⊢ ((𝑊 ∈ NrmCVec ∧ 𝑇:𝑋⟶𝑌) → {𝑦 ∣ ∃𝑧 ∈ 𝑋 ((𝐾‘𝑧) ≤ 1 ∧ 𝑦 = (𝑀‘(𝑇‘𝑧)))} ⊆ ℝ) |
48 | 12, 27, 47 | mp2an 704 |
. . . . . . . . . . . . 13
⊢ {𝑦 ∣ ∃𝑧 ∈ 𝑋 ((𝐾‘𝑧) ≤ 1 ∧ 𝑦 = (𝑀‘(𝑇‘𝑧)))} ⊆ ℝ |
49 | | ressxr 9962 |
. . . . . . . . . . . . 13
⊢ ℝ
⊆ ℝ* |
50 | 48, 49 | sstri 3577 |
. . . . . . . . . . . 12
⊢ {𝑦 ∣ ∃𝑧 ∈ 𝑋 ((𝐾‘𝑧) ≤ 1 ∧ 𝑦 = (𝑀‘(𝑇‘𝑧)))} ⊆
ℝ* |
51 | | simpl 472 |
. . . . . . . . . . . . . . 15
⊢ ((𝑥 ∈ 𝑋 ∧ (𝑇‘𝑥) ≠ 𝑄) → 𝑥 ∈ 𝑋) |
52 | | nmlno0lem.r |
. . . . . . . . . . . . . . . . 17
⊢ 𝑅 = (
·𝑠OLD ‘𝑈) |
53 | 2, 52 | nvscl 26865 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑈 ∈ NrmCVec ∧ (1 /
(𝐾‘𝑥)) ∈ ℂ ∧ 𝑥 ∈ 𝑋) → ((1 / (𝐾‘𝑥))𝑅𝑥) ∈ 𝑋) |
54 | 1, 53 | mp3an1 1403 |
. . . . . . . . . . . . . . 15
⊢ (((1 /
(𝐾‘𝑥)) ∈ ℂ ∧ 𝑥 ∈ 𝑋) → ((1 / (𝐾‘𝑥))𝑅𝑥) ∈ 𝑋) |
55 | 25, 51, 54 | syl2anc 691 |
. . . . . . . . . . . . . 14
⊢ ((𝑥 ∈ 𝑋 ∧ (𝑇‘𝑥) ≠ 𝑄) → ((1 / (𝐾‘𝑥))𝑅𝑥) ∈ 𝑋) |
56 | 19 | necon3i 2814 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑇‘𝑥) ≠ 𝑄 → 𝑥 ≠ 𝑃) |
57 | 2, 52, 8, 3 | nv1 26914 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝑈 ∈ NrmCVec ∧ 𝑥 ∈ 𝑋 ∧ 𝑥 ≠ 𝑃) → (𝐾‘((1 / (𝐾‘𝑥))𝑅𝑥)) = 1) |
58 | 1, 57 | mp3an1 1403 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑥 ∈ 𝑋 ∧ 𝑥 ≠ 𝑃) → (𝐾‘((1 / (𝐾‘𝑥))𝑅𝑥)) = 1) |
59 | 56, 58 | sylan2 490 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑥 ∈ 𝑋 ∧ (𝑇‘𝑥) ≠ 𝑄) → (𝐾‘((1 / (𝐾‘𝑥))𝑅𝑥)) = 1) |
60 | | 1re 9918 |
. . . . . . . . . . . . . . . 16
⊢ 1 ∈
ℝ |
61 | 59, 60 | syl6eqel 2696 |
. . . . . . . . . . . . . . 15
⊢ ((𝑥 ∈ 𝑋 ∧ (𝑇‘𝑥) ≠ 𝑄) → (𝐾‘((1 / (𝐾‘𝑥))𝑅𝑥)) ∈ ℝ) |
62 | | eqle 10018 |
. . . . . . . . . . . . . . 15
⊢ (((𝐾‘((1 / (𝐾‘𝑥))𝑅𝑥)) ∈ ℝ ∧ (𝐾‘((1 / (𝐾‘𝑥))𝑅𝑥)) = 1) → (𝐾‘((1 / (𝐾‘𝑥))𝑅𝑥)) ≤ 1) |
63 | 61, 59, 62 | syl2anc 691 |
. . . . . . . . . . . . . 14
⊢ ((𝑥 ∈ 𝑋 ∧ (𝑇‘𝑥) ≠ 𝑄) → (𝐾‘((1 / (𝐾‘𝑥))𝑅𝑥)) ≤ 1) |
64 | 1, 12, 13 | 3pm3.2i 1232 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑈 ∈ NrmCVec ∧ 𝑊 ∈ NrmCVec ∧ 𝑇 ∈ 𝐿) |
65 | 2, 52, 30, 16 | lnomul 26999 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝑈 ∈ NrmCVec ∧ 𝑊 ∈ NrmCVec ∧ 𝑇 ∈ 𝐿) ∧ ((1 / (𝐾‘𝑥)) ∈ ℂ ∧ 𝑥 ∈ 𝑋)) → (𝑇‘((1 / (𝐾‘𝑥))𝑅𝑥)) = ((1 / (𝐾‘𝑥))𝑆(𝑇‘𝑥))) |
66 | 64, 65 | mpan 702 |
. . . . . . . . . . . . . . . . 17
⊢ (((1 /
(𝐾‘𝑥)) ∈ ℂ ∧ 𝑥 ∈ 𝑋) → (𝑇‘((1 / (𝐾‘𝑥))𝑅𝑥)) = ((1 / (𝐾‘𝑥))𝑆(𝑇‘𝑥))) |
67 | 25, 51, 66 | syl2anc 691 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑥 ∈ 𝑋 ∧ (𝑇‘𝑥) ≠ 𝑄) → (𝑇‘((1 / (𝐾‘𝑥))𝑅𝑥)) = ((1 / (𝐾‘𝑥))𝑆(𝑇‘𝑥))) |
68 | 67 | eqcomd 2616 |
. . . . . . . . . . . . . . 15
⊢ ((𝑥 ∈ 𝑋 ∧ (𝑇‘𝑥) ≠ 𝑄) → ((1 / (𝐾‘𝑥))𝑆(𝑇‘𝑥)) = (𝑇‘((1 / (𝐾‘𝑥))𝑅𝑥))) |
69 | 68 | fveq2d 6107 |
. . . . . . . . . . . . . 14
⊢ ((𝑥 ∈ 𝑋 ∧ (𝑇‘𝑥) ≠ 𝑄) → (𝑀‘((1 / (𝐾‘𝑥))𝑆(𝑇‘𝑥))) = (𝑀‘(𝑇‘((1 / (𝐾‘𝑥))𝑅𝑥)))) |
70 | | fveq2 6103 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑧 = ((1 / (𝐾‘𝑥))𝑅𝑥) → (𝐾‘𝑧) = (𝐾‘((1 / (𝐾‘𝑥))𝑅𝑥))) |
71 | 70 | breq1d 4593 |
. . . . . . . . . . . . . . . 16
⊢ (𝑧 = ((1 / (𝐾‘𝑥))𝑅𝑥) → ((𝐾‘𝑧) ≤ 1 ↔ (𝐾‘((1 / (𝐾‘𝑥))𝑅𝑥)) ≤ 1)) |
72 | | fveq2 6103 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑧 = ((1 / (𝐾‘𝑥))𝑅𝑥) → (𝑇‘𝑧) = (𝑇‘((1 / (𝐾‘𝑥))𝑅𝑥))) |
73 | 72 | fveq2d 6107 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑧 = ((1 / (𝐾‘𝑥))𝑅𝑥) → (𝑀‘(𝑇‘𝑧)) = (𝑀‘(𝑇‘((1 / (𝐾‘𝑥))𝑅𝑥)))) |
74 | 73 | eqeq2d 2620 |
. . . . . . . . . . . . . . . 16
⊢ (𝑧 = ((1 / (𝐾‘𝑥))𝑅𝑥) → ((𝑀‘((1 / (𝐾‘𝑥))𝑆(𝑇‘𝑥))) = (𝑀‘(𝑇‘𝑧)) ↔ (𝑀‘((1 / (𝐾‘𝑥))𝑆(𝑇‘𝑥))) = (𝑀‘(𝑇‘((1 / (𝐾‘𝑥))𝑅𝑥))))) |
75 | 71, 74 | anbi12d 743 |
. . . . . . . . . . . . . . 15
⊢ (𝑧 = ((1 / (𝐾‘𝑥))𝑅𝑥) → (((𝐾‘𝑧) ≤ 1 ∧ (𝑀‘((1 / (𝐾‘𝑥))𝑆(𝑇‘𝑥))) = (𝑀‘(𝑇‘𝑧))) ↔ ((𝐾‘((1 / (𝐾‘𝑥))𝑅𝑥)) ≤ 1 ∧ (𝑀‘((1 / (𝐾‘𝑥))𝑆(𝑇‘𝑥))) = (𝑀‘(𝑇‘((1 / (𝐾‘𝑥))𝑅𝑥)))))) |
76 | 75 | rspcev 3282 |
. . . . . . . . . . . . . 14
⊢ ((((1 /
(𝐾‘𝑥))𝑅𝑥) ∈ 𝑋 ∧ ((𝐾‘((1 / (𝐾‘𝑥))𝑅𝑥)) ≤ 1 ∧ (𝑀‘((1 / (𝐾‘𝑥))𝑆(𝑇‘𝑥))) = (𝑀‘(𝑇‘((1 / (𝐾‘𝑥))𝑅𝑥))))) → ∃𝑧 ∈ 𝑋 ((𝐾‘𝑧) ≤ 1 ∧ (𝑀‘((1 / (𝐾‘𝑥))𝑆(𝑇‘𝑥))) = (𝑀‘(𝑇‘𝑧)))) |
77 | 55, 63, 69, 76 | syl12anc 1316 |
. . . . . . . . . . . . 13
⊢ ((𝑥 ∈ 𝑋 ∧ (𝑇‘𝑥) ≠ 𝑄) → ∃𝑧 ∈ 𝑋 ((𝐾‘𝑧) ≤ 1 ∧ (𝑀‘((1 / (𝐾‘𝑥))𝑆(𝑇‘𝑥))) = (𝑀‘(𝑇‘𝑧)))) |
78 | | fvex 6113 |
. . . . . . . . . . . . . 14
⊢ (𝑀‘((1 / (𝐾‘𝑥))𝑆(𝑇‘𝑥))) ∈ V |
79 | | eqeq1 2614 |
. . . . . . . . . . . . . . . 16
⊢ (𝑦 = (𝑀‘((1 / (𝐾‘𝑥))𝑆(𝑇‘𝑥))) → (𝑦 = (𝑀‘(𝑇‘𝑧)) ↔ (𝑀‘((1 / (𝐾‘𝑥))𝑆(𝑇‘𝑥))) = (𝑀‘(𝑇‘𝑧)))) |
80 | 79 | anbi2d 736 |
. . . . . . . . . . . . . . 15
⊢ (𝑦 = (𝑀‘((1 / (𝐾‘𝑥))𝑆(𝑇‘𝑥))) → (((𝐾‘𝑧) ≤ 1 ∧ 𝑦 = (𝑀‘(𝑇‘𝑧))) ↔ ((𝐾‘𝑧) ≤ 1 ∧ (𝑀‘((1 / (𝐾‘𝑥))𝑆(𝑇‘𝑥))) = (𝑀‘(𝑇‘𝑧))))) |
81 | 80 | rexbidv 3034 |
. . . . . . . . . . . . . 14
⊢ (𝑦 = (𝑀‘((1 / (𝐾‘𝑥))𝑆(𝑇‘𝑥))) → (∃𝑧 ∈ 𝑋 ((𝐾‘𝑧) ≤ 1 ∧ 𝑦 = (𝑀‘(𝑇‘𝑧))) ↔ ∃𝑧 ∈ 𝑋 ((𝐾‘𝑧) ≤ 1 ∧ (𝑀‘((1 / (𝐾‘𝑥))𝑆(𝑇‘𝑥))) = (𝑀‘(𝑇‘𝑧))))) |
82 | 78, 81 | elab 3319 |
. . . . . . . . . . . . 13
⊢ ((𝑀‘((1 / (𝐾‘𝑥))𝑆(𝑇‘𝑥))) ∈ {𝑦 ∣ ∃𝑧 ∈ 𝑋 ((𝐾‘𝑧) ≤ 1 ∧ 𝑦 = (𝑀‘(𝑇‘𝑧)))} ↔ ∃𝑧 ∈ 𝑋 ((𝐾‘𝑧) ≤ 1 ∧ (𝑀‘((1 / (𝐾‘𝑥))𝑆(𝑇‘𝑥))) = (𝑀‘(𝑇‘𝑧)))) |
83 | 77, 82 | sylibr 223 |
. . . . . . . . . . . 12
⊢ ((𝑥 ∈ 𝑋 ∧ (𝑇‘𝑥) ≠ 𝑄) → (𝑀‘((1 / (𝐾‘𝑥))𝑆(𝑇‘𝑥))) ∈ {𝑦 ∣ ∃𝑧 ∈ 𝑋 ((𝐾‘𝑧) ≤ 1 ∧ 𝑦 = (𝑀‘(𝑇‘𝑧)))}) |
84 | | supxrub 12026 |
. . . . . . . . . . . 12
⊢ (({𝑦 ∣ ∃𝑧 ∈ 𝑋 ((𝐾‘𝑧) ≤ 1 ∧ 𝑦 = (𝑀‘(𝑇‘𝑧)))} ⊆ ℝ* ∧ (𝑀‘((1 / (𝐾‘𝑥))𝑆(𝑇‘𝑥))) ∈ {𝑦 ∣ ∃𝑧 ∈ 𝑋 ((𝐾‘𝑧) ≤ 1 ∧ 𝑦 = (𝑀‘(𝑇‘𝑧)))}) → (𝑀‘((1 / (𝐾‘𝑥))𝑆(𝑇‘𝑥))) ≤ sup({𝑦 ∣ ∃𝑧 ∈ 𝑋 ((𝐾‘𝑧) ≤ 1 ∧ 𝑦 = (𝑀‘(𝑇‘𝑧)))}, ℝ*, <
)) |
85 | 50, 83, 84 | sylancr 694 |
. . . . . . . . . . 11
⊢ ((𝑥 ∈ 𝑋 ∧ (𝑇‘𝑥) ≠ 𝑄) → (𝑀‘((1 / (𝐾‘𝑥))𝑆(𝑇‘𝑥))) ≤ sup({𝑦 ∣ ∃𝑧 ∈ 𝑋 ((𝐾‘𝑧) ≤ 1 ∧ 𝑦 = (𝑀‘(𝑇‘𝑧)))}, ℝ*, <
)) |
86 | 85 | adantll 746 |
. . . . . . . . . 10
⊢ ((((𝑁‘𝑇) = 0 ∧ 𝑥 ∈ 𝑋) ∧ (𝑇‘𝑥) ≠ 𝑄) → (𝑀‘((1 / (𝐾‘𝑥))𝑆(𝑇‘𝑥))) ≤ sup({𝑦 ∣ ∃𝑧 ∈ 𝑋 ((𝐾‘𝑧) ≤ 1 ∧ 𝑦 = (𝑀‘(𝑇‘𝑧)))}, ℝ*, <
)) |
87 | | nmlno0.3 |
. . . . . . . . . . . . . . 15
⊢ 𝑁 = (𝑈 normOpOLD 𝑊) |
88 | 2, 14, 3, 41, 87 | nmooval 27002 |
. . . . . . . . . . . . . 14
⊢ ((𝑈 ∈ NrmCVec ∧ 𝑊 ∈ NrmCVec ∧ 𝑇:𝑋⟶𝑌) → (𝑁‘𝑇) = sup({𝑦 ∣ ∃𝑧 ∈ 𝑋 ((𝐾‘𝑧) ≤ 1 ∧ 𝑦 = (𝑀‘(𝑇‘𝑧)))}, ℝ*, <
)) |
89 | 1, 12, 27, 88 | mp3an 1416 |
. . . . . . . . . . . . 13
⊢ (𝑁‘𝑇) = sup({𝑦 ∣ ∃𝑧 ∈ 𝑋 ((𝐾‘𝑧) ≤ 1 ∧ 𝑦 = (𝑀‘(𝑇‘𝑧)))}, ℝ*, <
) |
90 | 89 | eqeq1i 2615 |
. . . . . . . . . . . 12
⊢ ((𝑁‘𝑇) = 0 ↔ sup({𝑦 ∣ ∃𝑧 ∈ 𝑋 ((𝐾‘𝑧) ≤ 1 ∧ 𝑦 = (𝑀‘(𝑇‘𝑧)))}, ℝ*, < ) =
0) |
91 | 90 | biimpi 205 |
. . . . . . . . . . 11
⊢ ((𝑁‘𝑇) = 0 → sup({𝑦 ∣ ∃𝑧 ∈ 𝑋 ((𝐾‘𝑧) ≤ 1 ∧ 𝑦 = (𝑀‘(𝑇‘𝑧)))}, ℝ*, < ) =
0) |
92 | 91 | ad2antrr 758 |
. . . . . . . . . 10
⊢ ((((𝑁‘𝑇) = 0 ∧ 𝑥 ∈ 𝑋) ∧ (𝑇‘𝑥) ≠ 𝑄) → sup({𝑦 ∣ ∃𝑧 ∈ 𝑋 ((𝐾‘𝑧) ≤ 1 ∧ 𝑦 = (𝑀‘(𝑇‘𝑧)))}, ℝ*, < ) =
0) |
93 | 86, 92 | breqtrd 4609 |
. . . . . . . . 9
⊢ ((((𝑁‘𝑇) = 0 ∧ 𝑥 ∈ 𝑋) ∧ (𝑇‘𝑥) ≠ 𝑄) → (𝑀‘((1 / (𝐾‘𝑥))𝑆(𝑇‘𝑥))) ≤ 0) |
94 | 14, 41 | nvcl 26900 |
. . . . . . . . . . . 12
⊢ ((𝑊 ∈ NrmCVec ∧ ((1 /
(𝐾‘𝑥))𝑆(𝑇‘𝑥)) ∈ 𝑌) → (𝑀‘((1 / (𝐾‘𝑥))𝑆(𝑇‘𝑥))) ∈ ℝ) |
95 | 12, 40, 94 | sylancr 694 |
. . . . . . . . . . 11
⊢ ((𝑥 ∈ 𝑋 ∧ (𝑇‘𝑥) ≠ 𝑄) → (𝑀‘((1 / (𝐾‘𝑥))𝑆(𝑇‘𝑥))) ∈ ℝ) |
96 | | 0re 9919 |
. . . . . . . . . . 11
⊢ 0 ∈
ℝ |
97 | | lenlt 9995 |
. . . . . . . . . . 11
⊢ (((𝑀‘((1 / (𝐾‘𝑥))𝑆(𝑇‘𝑥))) ∈ ℝ ∧ 0 ∈ ℝ)
→ ((𝑀‘((1 /
(𝐾‘𝑥))𝑆(𝑇‘𝑥))) ≤ 0 ↔ ¬ 0 < (𝑀‘((1 / (𝐾‘𝑥))𝑆(𝑇‘𝑥))))) |
98 | 95, 96, 97 | sylancl 693 |
. . . . . . . . . 10
⊢ ((𝑥 ∈ 𝑋 ∧ (𝑇‘𝑥) ≠ 𝑄) → ((𝑀‘((1 / (𝐾‘𝑥))𝑆(𝑇‘𝑥))) ≤ 0 ↔ ¬ 0 < (𝑀‘((1 / (𝐾‘𝑥))𝑆(𝑇‘𝑥))))) |
99 | 98 | adantll 746 |
. . . . . . . . 9
⊢ ((((𝑁‘𝑇) = 0 ∧ 𝑥 ∈ 𝑋) ∧ (𝑇‘𝑥) ≠ 𝑄) → ((𝑀‘((1 / (𝐾‘𝑥))𝑆(𝑇‘𝑥))) ≤ 0 ↔ ¬ 0 < (𝑀‘((1 / (𝐾‘𝑥))𝑆(𝑇‘𝑥))))) |
100 | 93, 99 | mpbid 221 |
. . . . . . . 8
⊢ ((((𝑁‘𝑇) = 0 ∧ 𝑥 ∈ 𝑋) ∧ (𝑇‘𝑥) ≠ 𝑄) → ¬ 0 < (𝑀‘((1 / (𝐾‘𝑥))𝑆(𝑇‘𝑥)))) |
101 | 100 | ex 449 |
. . . . . . 7
⊢ (((𝑁‘𝑇) = 0 ∧ 𝑥 ∈ 𝑋) → ((𝑇‘𝑥) ≠ 𝑄 → ¬ 0 < (𝑀‘((1 / (𝐾‘𝑥))𝑆(𝑇‘𝑥))))) |
102 | 46, 101 | pm2.65d 186 |
. . . . . 6
⊢ (((𝑁‘𝑇) = 0 ∧ 𝑥 ∈ 𝑋) → ¬ (𝑇‘𝑥) ≠ 𝑄) |
103 | | nne 2786 |
. . . . . 6
⊢ (¬
(𝑇‘𝑥) ≠ 𝑄 ↔ (𝑇‘𝑥) = 𝑄) |
104 | 102, 103 | sylib 207 |
. . . . 5
⊢ (((𝑁‘𝑇) = 0 ∧ 𝑥 ∈ 𝑋) → (𝑇‘𝑥) = 𝑄) |
105 | | nmlno0.0 |
. . . . . . . 8
⊢ 𝑍 = (𝑈 0op 𝑊) |
106 | 2, 15, 105 | 0oval 27027 |
. . . . . . 7
⊢ ((𝑈 ∈ NrmCVec ∧ 𝑊 ∈ NrmCVec ∧ 𝑥 ∈ 𝑋) → (𝑍‘𝑥) = 𝑄) |
107 | 1, 12, 106 | mp3an12 1406 |
. . . . . 6
⊢ (𝑥 ∈ 𝑋 → (𝑍‘𝑥) = 𝑄) |
108 | 107 | adantl 481 |
. . . . 5
⊢ (((𝑁‘𝑇) = 0 ∧ 𝑥 ∈ 𝑋) → (𝑍‘𝑥) = 𝑄) |
109 | 104, 108 | eqtr4d 2647 |
. . . 4
⊢ (((𝑁‘𝑇) = 0 ∧ 𝑥 ∈ 𝑋) → (𝑇‘𝑥) = (𝑍‘𝑥)) |
110 | 109 | ralrimiva 2949 |
. . 3
⊢ ((𝑁‘𝑇) = 0 → ∀𝑥 ∈ 𝑋 (𝑇‘𝑥) = (𝑍‘𝑥)) |
111 | | ffn 5958 |
. . . . 5
⊢ (𝑇:𝑋⟶𝑌 → 𝑇 Fn 𝑋) |
112 | 27, 111 | ax-mp 5 |
. . . 4
⊢ 𝑇 Fn 𝑋 |
113 | 2, 14, 105 | 0oo 27028 |
. . . . . 6
⊢ ((𝑈 ∈ NrmCVec ∧ 𝑊 ∈ NrmCVec) → 𝑍:𝑋⟶𝑌) |
114 | 1, 12, 113 | mp2an 704 |
. . . . 5
⊢ 𝑍:𝑋⟶𝑌 |
115 | | ffn 5958 |
. . . . 5
⊢ (𝑍:𝑋⟶𝑌 → 𝑍 Fn 𝑋) |
116 | 114, 115 | ax-mp 5 |
. . . 4
⊢ 𝑍 Fn 𝑋 |
117 | | eqfnfv 6219 |
. . . 4
⊢ ((𝑇 Fn 𝑋 ∧ 𝑍 Fn 𝑋) → (𝑇 = 𝑍 ↔ ∀𝑥 ∈ 𝑋 (𝑇‘𝑥) = (𝑍‘𝑥))) |
118 | 112, 116,
117 | mp2an 704 |
. . 3
⊢ (𝑇 = 𝑍 ↔ ∀𝑥 ∈ 𝑋 (𝑇‘𝑥) = (𝑍‘𝑥)) |
119 | 110, 118 | sylibr 223 |
. 2
⊢ ((𝑁‘𝑇) = 0 → 𝑇 = 𝑍) |
120 | | fveq2 6103 |
. . 3
⊢ (𝑇 = 𝑍 → (𝑁‘𝑇) = (𝑁‘𝑍)) |
121 | 87, 105 | nmoo0 27030 |
. . . 4
⊢ ((𝑈 ∈ NrmCVec ∧ 𝑊 ∈ NrmCVec) → (𝑁‘𝑍) = 0) |
122 | 1, 12, 121 | mp2an 704 |
. . 3
⊢ (𝑁‘𝑍) = 0 |
123 | 120, 122 | syl6eq 2660 |
. 2
⊢ (𝑇 = 𝑍 → (𝑁‘𝑇) = 0) |
124 | 119, 123 | impbii 198 |
1
⊢ ((𝑁‘𝑇) = 0 ↔ 𝑇 = 𝑍) |