Step | Hyp | Ref
| Expression |
1 | | eqid 2737 |
. . . . 5
⊢
(BaseSet‘𝑈) =
(BaseSet‘𝑈) |
2 | | eqid 2737 |
. . . . 5
⊢
(BaseSet‘𝑊) =
(BaseSet‘𝑊) |
3 | | nmoo0.0 |
. . . . 5
⊢ 𝑍 = (𝑈 0op 𝑊) |
4 | 1, 2, 3 | 0oo 28870 |
. . . 4
⊢ ((𝑈 ∈ NrmCVec ∧ 𝑊 ∈ NrmCVec) → 𝑍:(BaseSet‘𝑈)⟶(BaseSet‘𝑊)) |
5 | | eqid 2737 |
. . . . 5
⊢
(normCV‘𝑈) = (normCV‘𝑈) |
6 | | eqid 2737 |
. . . . 5
⊢
(normCV‘𝑊) = (normCV‘𝑊) |
7 | | nmoo0.3 |
. . . . 5
⊢ 𝑁 = (𝑈 normOpOLD 𝑊) |
8 | 1, 2, 5, 6, 7 | nmooval 28844 |
. . . 4
⊢ ((𝑈 ∈ NrmCVec ∧ 𝑊 ∈ NrmCVec ∧ 𝑍:(BaseSet‘𝑈)⟶(BaseSet‘𝑊)) → (𝑁‘𝑍) = sup({𝑥 ∣ ∃𝑧 ∈ (BaseSet‘𝑈)(((normCV‘𝑈)‘𝑧) ≤ 1 ∧ 𝑥 = ((normCV‘𝑊)‘(𝑍‘𝑧)))}, ℝ*, <
)) |
9 | 4, 8 | mpd3an3 1464 |
. . 3
⊢ ((𝑈 ∈ NrmCVec ∧ 𝑊 ∈ NrmCVec) → (𝑁‘𝑍) = sup({𝑥 ∣ ∃𝑧 ∈ (BaseSet‘𝑈)(((normCV‘𝑈)‘𝑧) ≤ 1 ∧ 𝑥 = ((normCV‘𝑊)‘(𝑍‘𝑧)))}, ℝ*, <
)) |
10 | | df-sn 4542 |
. . . . 5
⊢ {0} =
{𝑥 ∣ 𝑥 = 0} |
11 | | eqid 2737 |
. . . . . . . . . . 11
⊢
(0vec‘𝑈) = (0vec‘𝑈) |
12 | 1, 11 | nvzcl 28715 |
. . . . . . . . . 10
⊢ (𝑈 ∈ NrmCVec →
(0vec‘𝑈)
∈ (BaseSet‘𝑈)) |
13 | 11, 5 | nvz0 28749 |
. . . . . . . . . . 11
⊢ (𝑈 ∈ NrmCVec →
((normCV‘𝑈)‘(0vec‘𝑈)) = 0) |
14 | | 0le1 11355 |
. . . . . . . . . . 11
⊢ 0 ≤
1 |
15 | 13, 14 | eqbrtrdi 5092 |
. . . . . . . . . 10
⊢ (𝑈 ∈ NrmCVec →
((normCV‘𝑈)‘(0vec‘𝑈)) ≤ 1) |
16 | | fveq2 6717 |
. . . . . . . . . . . 12
⊢ (𝑧 = (0vec‘𝑈) →
((normCV‘𝑈)‘𝑧) = ((normCV‘𝑈)‘(0vec‘𝑈))) |
17 | 16 | breq1d 5063 |
. . . . . . . . . . 11
⊢ (𝑧 = (0vec‘𝑈) →
(((normCV‘𝑈)‘𝑧) ≤ 1 ↔
((normCV‘𝑈)‘(0vec‘𝑈)) ≤ 1)) |
18 | 17 | rspcev 3537 |
. . . . . . . . . 10
⊢
(((0vec‘𝑈) ∈ (BaseSet‘𝑈) ∧ ((normCV‘𝑈)‘(0vec‘𝑈)) ≤ 1) → ∃𝑧 ∈ (BaseSet‘𝑈)((normCV‘𝑈)‘𝑧) ≤ 1) |
19 | 12, 15, 18 | syl2anc 587 |
. . . . . . . . 9
⊢ (𝑈 ∈ NrmCVec →
∃𝑧 ∈
(BaseSet‘𝑈)((normCV‘𝑈)‘𝑧) ≤ 1) |
20 | 19 | biantrurd 536 |
. . . . . . . 8
⊢ (𝑈 ∈ NrmCVec → (𝑥 = 0 ↔ (∃𝑧 ∈ (BaseSet‘𝑈)((normCV‘𝑈)‘𝑧) ≤ 1 ∧ 𝑥 = 0))) |
21 | 20 | adantr 484 |
. . . . . . 7
⊢ ((𝑈 ∈ NrmCVec ∧ 𝑊 ∈ NrmCVec) → (𝑥 = 0 ↔ (∃𝑧 ∈ (BaseSet‘𝑈)((normCV‘𝑈)‘𝑧) ≤ 1 ∧ 𝑥 = 0))) |
22 | | eqid 2737 |
. . . . . . . . . . . . . . 15
⊢
(0vec‘𝑊) = (0vec‘𝑊) |
23 | 1, 22, 3 | 0oval 28869 |
. . . . . . . . . . . . . 14
⊢ ((𝑈 ∈ NrmCVec ∧ 𝑊 ∈ NrmCVec ∧ 𝑧 ∈ (BaseSet‘𝑈)) → (𝑍‘𝑧) = (0vec‘𝑊)) |
24 | 23 | 3expa 1120 |
. . . . . . . . . . . . 13
⊢ (((𝑈 ∈ NrmCVec ∧ 𝑊 ∈ NrmCVec) ∧ 𝑧 ∈ (BaseSet‘𝑈)) → (𝑍‘𝑧) = (0vec‘𝑊)) |
25 | 24 | fveq2d 6721 |
. . . . . . . . . . . 12
⊢ (((𝑈 ∈ NrmCVec ∧ 𝑊 ∈ NrmCVec) ∧ 𝑧 ∈ (BaseSet‘𝑈)) →
((normCV‘𝑊)‘(𝑍‘𝑧)) = ((normCV‘𝑊)‘(0vec‘𝑊))) |
26 | 22, 6 | nvz0 28749 |
. . . . . . . . . . . . 13
⊢ (𝑊 ∈ NrmCVec →
((normCV‘𝑊)‘(0vec‘𝑊)) = 0) |
27 | 26 | ad2antlr 727 |
. . . . . . . . . . . 12
⊢ (((𝑈 ∈ NrmCVec ∧ 𝑊 ∈ NrmCVec) ∧ 𝑧 ∈ (BaseSet‘𝑈)) →
((normCV‘𝑊)‘(0vec‘𝑊)) = 0) |
28 | 25, 27 | eqtrd 2777 |
. . . . . . . . . . 11
⊢ (((𝑈 ∈ NrmCVec ∧ 𝑊 ∈ NrmCVec) ∧ 𝑧 ∈ (BaseSet‘𝑈)) →
((normCV‘𝑊)‘(𝑍‘𝑧)) = 0) |
29 | 28 | eqeq2d 2748 |
. . . . . . . . . 10
⊢ (((𝑈 ∈ NrmCVec ∧ 𝑊 ∈ NrmCVec) ∧ 𝑧 ∈ (BaseSet‘𝑈)) → (𝑥 = ((normCV‘𝑊)‘(𝑍‘𝑧)) ↔ 𝑥 = 0)) |
30 | 29 | anbi2d 632 |
. . . . . . . . 9
⊢ (((𝑈 ∈ NrmCVec ∧ 𝑊 ∈ NrmCVec) ∧ 𝑧 ∈ (BaseSet‘𝑈)) →
((((normCV‘𝑈)‘𝑧) ≤ 1 ∧ 𝑥 = ((normCV‘𝑊)‘(𝑍‘𝑧))) ↔ (((normCV‘𝑈)‘𝑧) ≤ 1 ∧ 𝑥 = 0))) |
31 | 30 | rexbidva 3215 |
. . . . . . . 8
⊢ ((𝑈 ∈ NrmCVec ∧ 𝑊 ∈ NrmCVec) →
(∃𝑧 ∈
(BaseSet‘𝑈)(((normCV‘𝑈)‘𝑧) ≤ 1 ∧ 𝑥 = ((normCV‘𝑊)‘(𝑍‘𝑧))) ↔ ∃𝑧 ∈ (BaseSet‘𝑈)(((normCV‘𝑈)‘𝑧) ≤ 1 ∧ 𝑥 = 0))) |
32 | | r19.41v 3260 |
. . . . . . . 8
⊢
(∃𝑧 ∈
(BaseSet‘𝑈)(((normCV‘𝑈)‘𝑧) ≤ 1 ∧ 𝑥 = 0) ↔ (∃𝑧 ∈ (BaseSet‘𝑈)((normCV‘𝑈)‘𝑧) ≤ 1 ∧ 𝑥 = 0)) |
33 | 31, 32 | bitr2di 291 |
. . . . . . 7
⊢ ((𝑈 ∈ NrmCVec ∧ 𝑊 ∈ NrmCVec) →
((∃𝑧 ∈
(BaseSet‘𝑈)((normCV‘𝑈)‘𝑧) ≤ 1 ∧ 𝑥 = 0) ↔ ∃𝑧 ∈ (BaseSet‘𝑈)(((normCV‘𝑈)‘𝑧) ≤ 1 ∧ 𝑥 = ((normCV‘𝑊)‘(𝑍‘𝑧))))) |
34 | 21, 33 | bitrd 282 |
. . . . . 6
⊢ ((𝑈 ∈ NrmCVec ∧ 𝑊 ∈ NrmCVec) → (𝑥 = 0 ↔ ∃𝑧 ∈ (BaseSet‘𝑈)(((normCV‘𝑈)‘𝑧) ≤ 1 ∧ 𝑥 = ((normCV‘𝑊)‘(𝑍‘𝑧))))) |
35 | 34 | abbidv 2807 |
. . . . 5
⊢ ((𝑈 ∈ NrmCVec ∧ 𝑊 ∈ NrmCVec) → {𝑥 ∣ 𝑥 = 0} = {𝑥 ∣ ∃𝑧 ∈ (BaseSet‘𝑈)(((normCV‘𝑈)‘𝑧) ≤ 1 ∧ 𝑥 = ((normCV‘𝑊)‘(𝑍‘𝑧)))}) |
36 | 10, 35 | eqtr2id 2791 |
. . . 4
⊢ ((𝑈 ∈ NrmCVec ∧ 𝑊 ∈ NrmCVec) → {𝑥 ∣ ∃𝑧 ∈ (BaseSet‘𝑈)(((normCV‘𝑈)‘𝑧) ≤ 1 ∧ 𝑥 = ((normCV‘𝑊)‘(𝑍‘𝑧)))} = {0}) |
37 | 36 | supeq1d 9062 |
. . 3
⊢ ((𝑈 ∈ NrmCVec ∧ 𝑊 ∈ NrmCVec) →
sup({𝑥 ∣ ∃𝑧 ∈ (BaseSet‘𝑈)(((normCV‘𝑈)‘𝑧) ≤ 1 ∧ 𝑥 = ((normCV‘𝑊)‘(𝑍‘𝑧)))}, ℝ*, < ) = sup({0},
ℝ*, < )) |
38 | 9, 37 | eqtrd 2777 |
. 2
⊢ ((𝑈 ∈ NrmCVec ∧ 𝑊 ∈ NrmCVec) → (𝑁‘𝑍) = sup({0}, ℝ*, <
)) |
39 | | xrltso 12731 |
. . 3
⊢ < Or
ℝ* |
40 | | 0xr 10880 |
. . 3
⊢ 0 ∈
ℝ* |
41 | | supsn 9088 |
. . 3
⊢ (( <
Or ℝ* ∧ 0 ∈ ℝ*) → sup({0},
ℝ*, < ) = 0) |
42 | 39, 40, 41 | mp2an 692 |
. 2
⊢ sup({0},
ℝ*, < ) = 0 |
43 | 38, 42 | eqtrdi 2794 |
1
⊢ ((𝑈 ∈ NrmCVec ∧ 𝑊 ∈ NrmCVec) → (𝑁‘𝑍) = 0) |