Proof of Theorem nvi
| Step | Hyp | Ref | Expression | 
|---|
| 1 |  | eqid 2736 | . . . . . 6
⊢
(1st ‘𝑈) = (1st ‘𝑈) | 
| 2 |  | nvi.6 | . . . . . 6
⊢ 𝑁 =
(normCV‘𝑈) | 
| 3 | 1, 2 | nvop2 30628 | . . . . 5
⊢ (𝑈 ∈ NrmCVec → 𝑈 = 〈(1st
‘𝑈), 𝑁〉) | 
| 4 |  | nvi.2 | . . . . . . 7
⊢ 𝐺 = ( +𝑣
‘𝑈) | 
| 5 |  | nvi.4 | . . . . . . 7
⊢ 𝑆 = (
·𝑠OLD ‘𝑈) | 
| 6 | 1, 4, 5 | nvvop 30629 | . . . . . 6
⊢ (𝑈 ∈ NrmCVec →
(1st ‘𝑈) =
〈𝐺, 𝑆〉) | 
| 7 | 6 | opeq1d 4878 | . . . . 5
⊢ (𝑈 ∈ NrmCVec →
〈(1st ‘𝑈), 𝑁〉 = 〈〈𝐺, 𝑆〉, 𝑁〉) | 
| 8 | 3, 7 | eqtrd 2776 | . . . 4
⊢ (𝑈 ∈ NrmCVec → 𝑈 = 〈〈𝐺, 𝑆〉, 𝑁〉) | 
| 9 |  | id 22 | . . . 4
⊢ (𝑈 ∈ NrmCVec → 𝑈 ∈
NrmCVec) | 
| 10 | 8, 9 | eqeltrrd 2841 | . . 3
⊢ (𝑈 ∈ NrmCVec →
〈〈𝐺, 𝑆〉, 𝑁〉 ∈ NrmCVec) | 
| 11 |  | nvi.1 | . . . . 5
⊢ 𝑋 = (BaseSet‘𝑈) | 
| 12 | 11, 4 | bafval 30624 | . . . 4
⊢ 𝑋 = ran 𝐺 | 
| 13 |  | eqid 2736 | . . . 4
⊢
(GId‘𝐺) =
(GId‘𝐺) | 
| 14 | 12, 13 | isnv 30632 | . . 3
⊢
(〈〈𝐺,
𝑆〉, 𝑁〉 ∈ NrmCVec ↔ (〈𝐺, 𝑆〉 ∈ CVecOLD ∧ 𝑁:𝑋⟶ℝ ∧ ∀𝑥 ∈ 𝑋 (((𝑁‘𝑥) = 0 → 𝑥 = (GId‘𝐺)) ∧ ∀𝑦 ∈ ℂ (𝑁‘(𝑦𝑆𝑥)) = ((abs‘𝑦) · (𝑁‘𝑥)) ∧ ∀𝑦 ∈ 𝑋 (𝑁‘(𝑥𝐺𝑦)) ≤ ((𝑁‘𝑥) + (𝑁‘𝑦))))) | 
| 15 | 10, 14 | sylib 218 | . 2
⊢ (𝑈 ∈ NrmCVec →
(〈𝐺, 𝑆〉 ∈ CVecOLD ∧ 𝑁:𝑋⟶ℝ ∧ ∀𝑥 ∈ 𝑋 (((𝑁‘𝑥) = 0 → 𝑥 = (GId‘𝐺)) ∧ ∀𝑦 ∈ ℂ (𝑁‘(𝑦𝑆𝑥)) = ((abs‘𝑦) · (𝑁‘𝑥)) ∧ ∀𝑦 ∈ 𝑋 (𝑁‘(𝑥𝐺𝑦)) ≤ ((𝑁‘𝑥) + (𝑁‘𝑦))))) | 
| 16 |  | nvi.5 | . . . . . . . 8
⊢ 𝑍 = (0vec‘𝑈) | 
| 17 | 4, 16 | 0vfval 30626 | . . . . . . 7
⊢ (𝑈 ∈ NrmCVec → 𝑍 = (GId‘𝐺)) | 
| 18 | 17 | eqeq2d 2747 | . . . . . 6
⊢ (𝑈 ∈ NrmCVec → (𝑥 = 𝑍 ↔ 𝑥 = (GId‘𝐺))) | 
| 19 | 18 | imbi2d 340 | . . . . 5
⊢ (𝑈 ∈ NrmCVec → (((𝑁‘𝑥) = 0 → 𝑥 = 𝑍) ↔ ((𝑁‘𝑥) = 0 → 𝑥 = (GId‘𝐺)))) | 
| 20 | 19 | 3anbi1d 1441 | . . . 4
⊢ (𝑈 ∈ NrmCVec → ((((𝑁‘𝑥) = 0 → 𝑥 = 𝑍) ∧ ∀𝑦 ∈ ℂ (𝑁‘(𝑦𝑆𝑥)) = ((abs‘𝑦) · (𝑁‘𝑥)) ∧ ∀𝑦 ∈ 𝑋 (𝑁‘(𝑥𝐺𝑦)) ≤ ((𝑁‘𝑥) + (𝑁‘𝑦))) ↔ (((𝑁‘𝑥) = 0 → 𝑥 = (GId‘𝐺)) ∧ ∀𝑦 ∈ ℂ (𝑁‘(𝑦𝑆𝑥)) = ((abs‘𝑦) · (𝑁‘𝑥)) ∧ ∀𝑦 ∈ 𝑋 (𝑁‘(𝑥𝐺𝑦)) ≤ ((𝑁‘𝑥) + (𝑁‘𝑦))))) | 
| 21 | 20 | ralbidv 3177 | . . 3
⊢ (𝑈 ∈ NrmCVec →
(∀𝑥 ∈ 𝑋 (((𝑁‘𝑥) = 0 → 𝑥 = 𝑍) ∧ ∀𝑦 ∈ ℂ (𝑁‘(𝑦𝑆𝑥)) = ((abs‘𝑦) · (𝑁‘𝑥)) ∧ ∀𝑦 ∈ 𝑋 (𝑁‘(𝑥𝐺𝑦)) ≤ ((𝑁‘𝑥) + (𝑁‘𝑦))) ↔ ∀𝑥 ∈ 𝑋 (((𝑁‘𝑥) = 0 → 𝑥 = (GId‘𝐺)) ∧ ∀𝑦 ∈ ℂ (𝑁‘(𝑦𝑆𝑥)) = ((abs‘𝑦) · (𝑁‘𝑥)) ∧ ∀𝑦 ∈ 𝑋 (𝑁‘(𝑥𝐺𝑦)) ≤ ((𝑁‘𝑥) + (𝑁‘𝑦))))) | 
| 22 | 21 | 3anbi3d 1443 | . 2
⊢ (𝑈 ∈ NrmCVec →
((〈𝐺, 𝑆〉 ∈ CVecOLD
∧ 𝑁:𝑋⟶ℝ ∧ ∀𝑥 ∈ 𝑋 (((𝑁‘𝑥) = 0 → 𝑥 = 𝑍) ∧ ∀𝑦 ∈ ℂ (𝑁‘(𝑦𝑆𝑥)) = ((abs‘𝑦) · (𝑁‘𝑥)) ∧ ∀𝑦 ∈ 𝑋 (𝑁‘(𝑥𝐺𝑦)) ≤ ((𝑁‘𝑥) + (𝑁‘𝑦)))) ↔ (〈𝐺, 𝑆〉 ∈ CVecOLD ∧ 𝑁:𝑋⟶ℝ ∧ ∀𝑥 ∈ 𝑋 (((𝑁‘𝑥) = 0 → 𝑥 = (GId‘𝐺)) ∧ ∀𝑦 ∈ ℂ (𝑁‘(𝑦𝑆𝑥)) = ((abs‘𝑦) · (𝑁‘𝑥)) ∧ ∀𝑦 ∈ 𝑋 (𝑁‘(𝑥𝐺𝑦)) ≤ ((𝑁‘𝑥) + (𝑁‘𝑦)))))) | 
| 23 | 15, 22 | mpbird 257 | 1
⊢ (𝑈 ∈ NrmCVec →
(〈𝐺, 𝑆〉 ∈ CVecOLD ∧ 𝑁:𝑋⟶ℝ ∧ ∀𝑥 ∈ 𝑋 (((𝑁‘𝑥) = 0 → 𝑥 = 𝑍) ∧ ∀𝑦 ∈ ℂ (𝑁‘(𝑦𝑆𝑥)) = ((abs‘𝑦) · (𝑁‘𝑥)) ∧ ∀𝑦 ∈ 𝑋 (𝑁‘(𝑥𝐺𝑦)) ≤ ((𝑁‘𝑥) + (𝑁‘𝑦))))) |