Proof of Theorem nmlno0
| Step | Hyp | Ref
| Expression |
| 1 | | nmlno0.7 |
. . . . . 6
⊢ 𝐿 = (𝑈 LnOp 𝑊) |
| 2 | | oveq1 7438 |
. . . . . 6
⊢ (𝑈 = if(𝑈 ∈ NrmCVec, 𝑈, 〈〈 + , · 〉,
abs〉) → (𝑈 LnOp
𝑊) = (if(𝑈 ∈ NrmCVec, 𝑈, 〈〈 + , · 〉,
abs〉) LnOp 𝑊)) |
| 3 | 1, 2 | eqtrid 2789 |
. . . . 5
⊢ (𝑈 = if(𝑈 ∈ NrmCVec, 𝑈, 〈〈 + , · 〉,
abs〉) → 𝐿 =
(if(𝑈 ∈ NrmCVec, 𝑈, 〈〈 + , ·
〉, abs〉) LnOp 𝑊)) |
| 4 | 3 | eleq2d 2827 |
. . . 4
⊢ (𝑈 = if(𝑈 ∈ NrmCVec, 𝑈, 〈〈 + , · 〉,
abs〉) → (𝑇 ∈
𝐿 ↔ 𝑇 ∈ (if(𝑈 ∈ NrmCVec, 𝑈, 〈〈 + , · 〉,
abs〉) LnOp 𝑊))) |
| 5 | | nmlno0.3 |
. . . . . . . 8
⊢ 𝑁 = (𝑈 normOpOLD 𝑊) |
| 6 | | oveq1 7438 |
. . . . . . . 8
⊢ (𝑈 = if(𝑈 ∈ NrmCVec, 𝑈, 〈〈 + , · 〉,
abs〉) → (𝑈
normOpOLD 𝑊) =
(if(𝑈 ∈ NrmCVec, 𝑈, 〈〈 + , ·
〉, abs〉) normOpOLD 𝑊)) |
| 7 | 5, 6 | eqtrid 2789 |
. . . . . . 7
⊢ (𝑈 = if(𝑈 ∈ NrmCVec, 𝑈, 〈〈 + , · 〉,
abs〉) → 𝑁 =
(if(𝑈 ∈ NrmCVec, 𝑈, 〈〈 + , ·
〉, abs〉) normOpOLD 𝑊)) |
| 8 | 7 | fveq1d 6908 |
. . . . . 6
⊢ (𝑈 = if(𝑈 ∈ NrmCVec, 𝑈, 〈〈 + , · 〉,
abs〉) → (𝑁‘𝑇) = ((if(𝑈 ∈ NrmCVec, 𝑈, 〈〈 + , · 〉,
abs〉) normOpOLD 𝑊)‘𝑇)) |
| 9 | 8 | eqeq1d 2739 |
. . . . 5
⊢ (𝑈 = if(𝑈 ∈ NrmCVec, 𝑈, 〈〈 + , · 〉,
abs〉) → ((𝑁‘𝑇) = 0 ↔ ((if(𝑈 ∈ NrmCVec, 𝑈, 〈〈 + , · 〉,
abs〉) normOpOLD 𝑊)‘𝑇) = 0)) |
| 10 | | nmlno0.0 |
. . . . . . 7
⊢ 𝑍 = (𝑈 0op 𝑊) |
| 11 | | oveq1 7438 |
. . . . . . 7
⊢ (𝑈 = if(𝑈 ∈ NrmCVec, 𝑈, 〈〈 + , · 〉,
abs〉) → (𝑈
0op 𝑊) =
(if(𝑈 ∈ NrmCVec, 𝑈, 〈〈 + , ·
〉, abs〉) 0op 𝑊)) |
| 12 | 10, 11 | eqtrid 2789 |
. . . . . 6
⊢ (𝑈 = if(𝑈 ∈ NrmCVec, 𝑈, 〈〈 + , · 〉,
abs〉) → 𝑍 =
(if(𝑈 ∈ NrmCVec, 𝑈, 〈〈 + , ·
〉, abs〉) 0op 𝑊)) |
| 13 | 12 | eqeq2d 2748 |
. . . . 5
⊢ (𝑈 = if(𝑈 ∈ NrmCVec, 𝑈, 〈〈 + , · 〉,
abs〉) → (𝑇 =
𝑍 ↔ 𝑇 = (if(𝑈 ∈ NrmCVec, 𝑈, 〈〈 + , · 〉,
abs〉) 0op 𝑊))) |
| 14 | 9, 13 | bibi12d 345 |
. . . 4
⊢ (𝑈 = if(𝑈 ∈ NrmCVec, 𝑈, 〈〈 + , · 〉,
abs〉) → (((𝑁‘𝑇) = 0 ↔ 𝑇 = 𝑍) ↔ (((if(𝑈 ∈ NrmCVec, 𝑈, 〈〈 + , · 〉,
abs〉) normOpOLD 𝑊)‘𝑇) = 0 ↔ 𝑇 = (if(𝑈 ∈ NrmCVec, 𝑈, 〈〈 + , · 〉,
abs〉) 0op 𝑊)))) |
| 15 | 4, 14 | imbi12d 344 |
. . 3
⊢ (𝑈 = if(𝑈 ∈ NrmCVec, 𝑈, 〈〈 + , · 〉,
abs〉) → ((𝑇
∈ 𝐿 → ((𝑁‘𝑇) = 0 ↔ 𝑇 = 𝑍)) ↔ (𝑇 ∈ (if(𝑈 ∈ NrmCVec, 𝑈, 〈〈 + , · 〉,
abs〉) LnOp 𝑊) →
(((if(𝑈 ∈ NrmCVec,
𝑈, 〈〈 + ,
· 〉, abs〉) normOpOLD 𝑊)‘𝑇) = 0 ↔ 𝑇 = (if(𝑈 ∈ NrmCVec, 𝑈, 〈〈 + , · 〉,
abs〉) 0op 𝑊))))) |
| 16 | | oveq2 7439 |
. . . . 5
⊢ (𝑊 = if(𝑊 ∈ NrmCVec, 𝑊, 〈〈 + , · 〉,
abs〉) → (if(𝑈
∈ NrmCVec, 𝑈,
〈〈 + , · 〉, abs〉) LnOp 𝑊) = (if(𝑈 ∈ NrmCVec, 𝑈, 〈〈 + , · 〉,
abs〉) LnOp if(𝑊 ∈
NrmCVec, 𝑊, 〈〈 +
, · 〉, abs〉))) |
| 17 | 16 | eleq2d 2827 |
. . . 4
⊢ (𝑊 = if(𝑊 ∈ NrmCVec, 𝑊, 〈〈 + , · 〉,
abs〉) → (𝑇 ∈
(if(𝑈 ∈ NrmCVec, 𝑈, 〈〈 + , ·
〉, abs〉) LnOp 𝑊)
↔ 𝑇 ∈ (if(𝑈 ∈ NrmCVec, 𝑈, 〈〈 + , ·
〉, abs〉) LnOp if(𝑊 ∈ NrmCVec, 𝑊, 〈〈 + , · 〉,
abs〉)))) |
| 18 | | oveq2 7439 |
. . . . . . 7
⊢ (𝑊 = if(𝑊 ∈ NrmCVec, 𝑊, 〈〈 + , · 〉,
abs〉) → (if(𝑈
∈ NrmCVec, 𝑈,
〈〈 + , · 〉, abs〉) normOpOLD 𝑊) = (if(𝑈 ∈ NrmCVec, 𝑈, 〈〈 + , · 〉,
abs〉) normOpOLD if(𝑊 ∈ NrmCVec, 𝑊, 〈〈 + , · 〉,
abs〉))) |
| 19 | 18 | fveq1d 6908 |
. . . . . 6
⊢ (𝑊 = if(𝑊 ∈ NrmCVec, 𝑊, 〈〈 + , · 〉,
abs〉) → ((if(𝑈
∈ NrmCVec, 𝑈,
〈〈 + , · 〉, abs〉) normOpOLD 𝑊)‘𝑇) = ((if(𝑈 ∈ NrmCVec, 𝑈, 〈〈 + , · 〉,
abs〉) normOpOLD if(𝑊 ∈ NrmCVec, 𝑊, 〈〈 + , · 〉,
abs〉))‘𝑇)) |
| 20 | 19 | eqeq1d 2739 |
. . . . 5
⊢ (𝑊 = if(𝑊 ∈ NrmCVec, 𝑊, 〈〈 + , · 〉,
abs〉) → (((if(𝑈
∈ NrmCVec, 𝑈,
〈〈 + , · 〉, abs〉) normOpOLD 𝑊)‘𝑇) = 0 ↔ ((if(𝑈 ∈ NrmCVec, 𝑈, 〈〈 + , · 〉,
abs〉) normOpOLD if(𝑊 ∈ NrmCVec, 𝑊, 〈〈 + , · 〉,
abs〉))‘𝑇) =
0)) |
| 21 | | oveq2 7439 |
. . . . . 6
⊢ (𝑊 = if(𝑊 ∈ NrmCVec, 𝑊, 〈〈 + , · 〉,
abs〉) → (if(𝑈
∈ NrmCVec, 𝑈,
〈〈 + , · 〉, abs〉) 0op 𝑊) = (if(𝑈 ∈ NrmCVec, 𝑈, 〈〈 + , · 〉,
abs〉) 0op if(𝑊 ∈ NrmCVec, 𝑊, 〈〈 + , · 〉,
abs〉))) |
| 22 | 21 | eqeq2d 2748 |
. . . . 5
⊢ (𝑊 = if(𝑊 ∈ NrmCVec, 𝑊, 〈〈 + , · 〉,
abs〉) → (𝑇 =
(if(𝑈 ∈ NrmCVec, 𝑈, 〈〈 + , ·
〉, abs〉) 0op 𝑊) ↔ 𝑇 = (if(𝑈 ∈ NrmCVec, 𝑈, 〈〈 + , · 〉,
abs〉) 0op if(𝑊 ∈ NrmCVec, 𝑊, 〈〈 + , · 〉,
abs〉)))) |
| 23 | 20, 22 | bibi12d 345 |
. . . 4
⊢ (𝑊 = if(𝑊 ∈ NrmCVec, 𝑊, 〈〈 + , · 〉,
abs〉) → ((((if(𝑈
∈ NrmCVec, 𝑈,
〈〈 + , · 〉, abs〉) normOpOLD 𝑊)‘𝑇) = 0 ↔ 𝑇 = (if(𝑈 ∈ NrmCVec, 𝑈, 〈〈 + , · 〉,
abs〉) 0op 𝑊)) ↔ (((if(𝑈 ∈ NrmCVec, 𝑈, 〈〈 + , · 〉,
abs〉) normOpOLD if(𝑊 ∈ NrmCVec, 𝑊, 〈〈 + , · 〉,
abs〉))‘𝑇) = 0
↔ 𝑇 = (if(𝑈 ∈ NrmCVec, 𝑈, 〈〈 + , ·
〉, abs〉) 0op if(𝑊 ∈ NrmCVec, 𝑊, 〈〈 + , · 〉,
abs〉))))) |
| 24 | 17, 23 | imbi12d 344 |
. . 3
⊢ (𝑊 = if(𝑊 ∈ NrmCVec, 𝑊, 〈〈 + , · 〉,
abs〉) → ((𝑇
∈ (if(𝑈 ∈
NrmCVec, 𝑈, 〈〈 +
, · 〉, abs〉) LnOp 𝑊) → (((if(𝑈 ∈ NrmCVec, 𝑈, 〈〈 + , · 〉,
abs〉) normOpOLD 𝑊)‘𝑇) = 0 ↔ 𝑇 = (if(𝑈 ∈ NrmCVec, 𝑈, 〈〈 + , · 〉,
abs〉) 0op 𝑊))) ↔ (𝑇 ∈ (if(𝑈 ∈ NrmCVec, 𝑈, 〈〈 + , · 〉,
abs〉) LnOp if(𝑊 ∈
NrmCVec, 𝑊, 〈〈 +
, · 〉, abs〉)) → (((if(𝑈 ∈ NrmCVec, 𝑈, 〈〈 + , · 〉,
abs〉) normOpOLD if(𝑊 ∈ NrmCVec, 𝑊, 〈〈 + , · 〉,
abs〉))‘𝑇) = 0
↔ 𝑇 = (if(𝑈 ∈ NrmCVec, 𝑈, 〈〈 + , ·
〉, abs〉) 0op if(𝑊 ∈ NrmCVec, 𝑊, 〈〈 + , · 〉,
abs〉)))))) |
| 25 | | eqid 2737 |
. . . 4
⊢ (if(𝑈 ∈ NrmCVec, 𝑈, 〈〈 + , ·
〉, abs〉) normOpOLD if(𝑊 ∈ NrmCVec, 𝑊, 〈〈 + , · 〉,
abs〉)) = (if(𝑈 ∈
NrmCVec, 𝑈, 〈〈 +
, · 〉, abs〉) normOpOLD if(𝑊 ∈ NrmCVec, 𝑊, 〈〈 + , · 〉,
abs〉)) |
| 26 | | eqid 2737 |
. . . 4
⊢ (if(𝑈 ∈ NrmCVec, 𝑈, 〈〈 + , ·
〉, abs〉) 0op if(𝑊 ∈ NrmCVec, 𝑊, 〈〈 + , · 〉,
abs〉)) = (if(𝑈 ∈
NrmCVec, 𝑈, 〈〈 +
, · 〉, abs〉) 0op if(𝑊 ∈ NrmCVec, 𝑊, 〈〈 + , · 〉,
abs〉)) |
| 27 | | eqid 2737 |
. . . 4
⊢ (if(𝑈 ∈ NrmCVec, 𝑈, 〈〈 + , ·
〉, abs〉) LnOp if(𝑊 ∈ NrmCVec, 𝑊, 〈〈 + , · 〉,
abs〉)) = (if(𝑈 ∈
NrmCVec, 𝑈, 〈〈 +
, · 〉, abs〉) LnOp if(𝑊 ∈ NrmCVec, 𝑊, 〈〈 + , · 〉,
abs〉)) |
| 28 | | elimnvu 30703 |
. . . 4
⊢ if(𝑈 ∈ NrmCVec, 𝑈, 〈〈 + , ·
〉, abs〉) ∈ NrmCVec |
| 29 | | elimnvu 30703 |
. . . 4
⊢ if(𝑊 ∈ NrmCVec, 𝑊, 〈〈 + , ·
〉, abs〉) ∈ NrmCVec |
| 30 | 25, 26, 27, 28, 29 | nmlno0i 30813 |
. . 3
⊢ (𝑇 ∈ (if(𝑈 ∈ NrmCVec, 𝑈, 〈〈 + , · 〉,
abs〉) LnOp if(𝑊 ∈
NrmCVec, 𝑊, 〈〈 +
, · 〉, abs〉)) → (((if(𝑈 ∈ NrmCVec, 𝑈, 〈〈 + , · 〉,
abs〉) normOpOLD if(𝑊 ∈ NrmCVec, 𝑊, 〈〈 + , · 〉,
abs〉))‘𝑇) = 0
↔ 𝑇 = (if(𝑈 ∈ NrmCVec, 𝑈, 〈〈 + , ·
〉, abs〉) 0op if(𝑊 ∈ NrmCVec, 𝑊, 〈〈 + , · 〉,
abs〉)))) |
| 31 | 15, 24, 30 | dedth2h 4585 |
. 2
⊢ ((𝑈 ∈ NrmCVec ∧ 𝑊 ∈ NrmCVec) → (𝑇 ∈ 𝐿 → ((𝑁‘𝑇) = 0 ↔ 𝑇 = 𝑍))) |
| 32 | 31 | 3impia 1118 |
1
⊢ ((𝑈 ∈ NrmCVec ∧ 𝑊 ∈ NrmCVec ∧ 𝑇 ∈ 𝐿) → ((𝑁‘𝑇) = 0 ↔ 𝑇 = 𝑍)) |