| Step | Hyp | Ref | Expression | 
|---|
| 1 |  | nvtri.1 | . . . . . . 7
⊢ 𝑋 = (BaseSet‘𝑈) | 
| 2 |  | nvtri.2 | . . . . . . 7
⊢ 𝐺 = ( +𝑣
‘𝑈) | 
| 3 |  | eqid 2736 | . . . . . . . . 9
⊢ (
·𝑠OLD ‘𝑈) = ( ·𝑠OLD
‘𝑈) | 
| 4 | 3 | smfval 30625 | . . . . . . . 8
⊢ (
·𝑠OLD ‘𝑈) = (2nd ‘(1st
‘𝑈)) | 
| 5 | 4 | eqcomi 2745 | . . . . . . 7
⊢
(2nd ‘(1st ‘𝑈)) = (
·𝑠OLD ‘𝑈) | 
| 6 |  | eqid 2736 | . . . . . . 7
⊢
(0vec‘𝑈) = (0vec‘𝑈) | 
| 7 |  | nvtri.6 | . . . . . . 7
⊢ 𝑁 =
(normCV‘𝑈) | 
| 8 | 1, 2, 5, 6, 7 | nvi 30634 | . . . . . 6
⊢ (𝑈 ∈ NrmCVec →
(〈𝐺, (2nd
‘(1st ‘𝑈))〉 ∈ CVecOLD ∧
𝑁:𝑋⟶ℝ ∧ ∀𝑥 ∈ 𝑋 (((𝑁‘𝑥) = 0 → 𝑥 = (0vec‘𝑈)) ∧ ∀𝑦 ∈ ℂ (𝑁‘(𝑦(2nd ‘(1st
‘𝑈))𝑥)) = ((abs‘𝑦) · (𝑁‘𝑥)) ∧ ∀𝑦 ∈ 𝑋 (𝑁‘(𝑥𝐺𝑦)) ≤ ((𝑁‘𝑥) + (𝑁‘𝑦))))) | 
| 9 | 8 | simp3d 1144 | . . . . 5
⊢ (𝑈 ∈ NrmCVec →
∀𝑥 ∈ 𝑋 (((𝑁‘𝑥) = 0 → 𝑥 = (0vec‘𝑈)) ∧ ∀𝑦 ∈ ℂ (𝑁‘(𝑦(2nd ‘(1st
‘𝑈))𝑥)) = ((abs‘𝑦) · (𝑁‘𝑥)) ∧ ∀𝑦 ∈ 𝑋 (𝑁‘(𝑥𝐺𝑦)) ≤ ((𝑁‘𝑥) + (𝑁‘𝑦)))) | 
| 10 |  | simp3 1138 | . . . . . 6
⊢ ((((𝑁‘𝑥) = 0 → 𝑥 = (0vec‘𝑈)) ∧ ∀𝑦 ∈ ℂ (𝑁‘(𝑦(2nd ‘(1st
‘𝑈))𝑥)) = ((abs‘𝑦) · (𝑁‘𝑥)) ∧ ∀𝑦 ∈ 𝑋 (𝑁‘(𝑥𝐺𝑦)) ≤ ((𝑁‘𝑥) + (𝑁‘𝑦))) → ∀𝑦 ∈ 𝑋 (𝑁‘(𝑥𝐺𝑦)) ≤ ((𝑁‘𝑥) + (𝑁‘𝑦))) | 
| 11 | 10 | ralimi 3082 | . . . . 5
⊢
(∀𝑥 ∈
𝑋 (((𝑁‘𝑥) = 0 → 𝑥 = (0vec‘𝑈)) ∧ ∀𝑦 ∈ ℂ (𝑁‘(𝑦(2nd ‘(1st
‘𝑈))𝑥)) = ((abs‘𝑦) · (𝑁‘𝑥)) ∧ ∀𝑦 ∈ 𝑋 (𝑁‘(𝑥𝐺𝑦)) ≤ ((𝑁‘𝑥) + (𝑁‘𝑦))) → ∀𝑥 ∈ 𝑋 ∀𝑦 ∈ 𝑋 (𝑁‘(𝑥𝐺𝑦)) ≤ ((𝑁‘𝑥) + (𝑁‘𝑦))) | 
| 12 | 9, 11 | syl 17 | . . . 4
⊢ (𝑈 ∈ NrmCVec →
∀𝑥 ∈ 𝑋 ∀𝑦 ∈ 𝑋 (𝑁‘(𝑥𝐺𝑦)) ≤ ((𝑁‘𝑥) + (𝑁‘𝑦))) | 
| 13 |  | fvoveq1 7455 | . . . . . 6
⊢ (𝑥 = 𝐴 → (𝑁‘(𝑥𝐺𝑦)) = (𝑁‘(𝐴𝐺𝑦))) | 
| 14 |  | fveq2 6905 | . . . . . . 7
⊢ (𝑥 = 𝐴 → (𝑁‘𝑥) = (𝑁‘𝐴)) | 
| 15 | 14 | oveq1d 7447 | . . . . . 6
⊢ (𝑥 = 𝐴 → ((𝑁‘𝑥) + (𝑁‘𝑦)) = ((𝑁‘𝐴) + (𝑁‘𝑦))) | 
| 16 | 13, 15 | breq12d 5155 | . . . . 5
⊢ (𝑥 = 𝐴 → ((𝑁‘(𝑥𝐺𝑦)) ≤ ((𝑁‘𝑥) + (𝑁‘𝑦)) ↔ (𝑁‘(𝐴𝐺𝑦)) ≤ ((𝑁‘𝐴) + (𝑁‘𝑦)))) | 
| 17 |  | oveq2 7440 | . . . . . . 7
⊢ (𝑦 = 𝐵 → (𝐴𝐺𝑦) = (𝐴𝐺𝐵)) | 
| 18 | 17 | fveq2d 6909 | . . . . . 6
⊢ (𝑦 = 𝐵 → (𝑁‘(𝐴𝐺𝑦)) = (𝑁‘(𝐴𝐺𝐵))) | 
| 19 |  | fveq2 6905 | . . . . . . 7
⊢ (𝑦 = 𝐵 → (𝑁‘𝑦) = (𝑁‘𝐵)) | 
| 20 | 19 | oveq2d 7448 | . . . . . 6
⊢ (𝑦 = 𝐵 → ((𝑁‘𝐴) + (𝑁‘𝑦)) = ((𝑁‘𝐴) + (𝑁‘𝐵))) | 
| 21 | 18, 20 | breq12d 5155 | . . . . 5
⊢ (𝑦 = 𝐵 → ((𝑁‘(𝐴𝐺𝑦)) ≤ ((𝑁‘𝐴) + (𝑁‘𝑦)) ↔ (𝑁‘(𝐴𝐺𝐵)) ≤ ((𝑁‘𝐴) + (𝑁‘𝐵)))) | 
| 22 | 16, 21 | rspc2v 3632 | . . . 4
⊢ ((𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋) → (∀𝑥 ∈ 𝑋 ∀𝑦 ∈ 𝑋 (𝑁‘(𝑥𝐺𝑦)) ≤ ((𝑁‘𝑥) + (𝑁‘𝑦)) → (𝑁‘(𝐴𝐺𝐵)) ≤ ((𝑁‘𝐴) + (𝑁‘𝐵)))) | 
| 23 | 12, 22 | syl5 34 | . . 3
⊢ ((𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋) → (𝑈 ∈ NrmCVec → (𝑁‘(𝐴𝐺𝐵)) ≤ ((𝑁‘𝐴) + (𝑁‘𝐵)))) | 
| 24 | 23 | 3impia 1117 | . 2
⊢ ((𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ∧ 𝑈 ∈ NrmCVec) → (𝑁‘(𝐴𝐺𝐵)) ≤ ((𝑁‘𝐴) + (𝑁‘𝐵))) | 
| 25 | 24 | 3comr 1125 | 1
⊢ ((𝑈 ∈ NrmCVec ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋) → (𝑁‘(𝐴𝐺𝐵)) ≤ ((𝑁‘𝐴) + (𝑁‘𝐵))) |