Proof of Theorem ncvs1
| Step | Hyp | Ref
| Expression |
| 1 | | simp1 1137 |
. . 3
⊢ ((𝐺 ∈ (NrmVec ∩
ℂVec) ∧ (𝐴 ∈
𝑋 ∧ 𝐴 ≠ 0 ) ∧ (1 / (𝑁‘𝐴)) ∈ 𝐾) → 𝐺 ∈ (NrmVec ∩
ℂVec)) |
| 2 | | simp3 1139 |
. . . 4
⊢ ((𝐺 ∈ (NrmVec ∩
ℂVec) ∧ (𝐴 ∈
𝑋 ∧ 𝐴 ≠ 0 ) ∧ (1 / (𝑁‘𝐴)) ∈ 𝐾) → (1 / (𝑁‘𝐴)) ∈ 𝐾) |
| 3 | | elin 3967 |
. . . . . . . . 9
⊢ (𝐺 ∈ (NrmVec ∩
ℂVec) ↔ (𝐺
∈ NrmVec ∧ 𝐺
∈ ℂVec)) |
| 4 | | nvcnlm 24717 |
. . . . . . . . . . 11
⊢ (𝐺 ∈ NrmVec → 𝐺 ∈ NrmMod) |
| 5 | | nlmngp 24698 |
. . . . . . . . . . 11
⊢ (𝐺 ∈ NrmMod → 𝐺 ∈ NrmGrp) |
| 6 | 4, 5 | syl 17 |
. . . . . . . . . 10
⊢ (𝐺 ∈ NrmVec → 𝐺 ∈ NrmGrp) |
| 7 | 6 | adantr 480 |
. . . . . . . . 9
⊢ ((𝐺 ∈ NrmVec ∧ 𝐺 ∈ ℂVec) → 𝐺 ∈ NrmGrp) |
| 8 | 3, 7 | sylbi 217 |
. . . . . . . 8
⊢ (𝐺 ∈ (NrmVec ∩
ℂVec) → 𝐺 ∈
NrmGrp) |
| 9 | | simpl 482 |
. . . . . . . 8
⊢ ((𝐴 ∈ 𝑋 ∧ 𝐴 ≠ 0 ) → 𝐴 ∈ 𝑋) |
| 10 | 8, 9 | anim12i 613 |
. . . . . . 7
⊢ ((𝐺 ∈ (NrmVec ∩
ℂVec) ∧ (𝐴 ∈
𝑋 ∧ 𝐴 ≠ 0 )) → (𝐺 ∈ NrmGrp ∧ 𝐴 ∈ 𝑋)) |
| 11 | | ncvs1.x |
. . . . . . . 8
⊢ 𝑋 = (Base‘𝐺) |
| 12 | | ncvs1.n |
. . . . . . . 8
⊢ 𝑁 = (norm‘𝐺) |
| 13 | 11, 12 | nmcl 24629 |
. . . . . . 7
⊢ ((𝐺 ∈ NrmGrp ∧ 𝐴 ∈ 𝑋) → (𝑁‘𝐴) ∈ ℝ) |
| 14 | 10, 13 | syl 17 |
. . . . . 6
⊢ ((𝐺 ∈ (NrmVec ∩
ℂVec) ∧ (𝐴 ∈
𝑋 ∧ 𝐴 ≠ 0 )) → (𝑁‘𝐴) ∈ ℝ) |
| 15 | | ncvs1.z |
. . . . . . . . . . . 12
⊢ 0 =
(0g‘𝐺) |
| 16 | 11, 12, 15 | nmeq0 24631 |
. . . . . . . . . . 11
⊢ ((𝐺 ∈ NrmGrp ∧ 𝐴 ∈ 𝑋) → ((𝑁‘𝐴) = 0 ↔ 𝐴 = 0 )) |
| 17 | 16 | bicomd 223 |
. . . . . . . . . 10
⊢ ((𝐺 ∈ NrmGrp ∧ 𝐴 ∈ 𝑋) → (𝐴 = 0 ↔ (𝑁‘𝐴) = 0)) |
| 18 | 8, 17 | sylan 580 |
. . . . . . . . 9
⊢ ((𝐺 ∈ (NrmVec ∩
ℂVec) ∧ 𝐴 ∈
𝑋) → (𝐴 = 0 ↔ (𝑁‘𝐴) = 0)) |
| 19 | 18 | necon3bid 2985 |
. . . . . . . 8
⊢ ((𝐺 ∈ (NrmVec ∩
ℂVec) ∧ 𝐴 ∈
𝑋) → (𝐴 ≠ 0 ↔ (𝑁‘𝐴) ≠ 0)) |
| 20 | 19 | biimpd 229 |
. . . . . . 7
⊢ ((𝐺 ∈ (NrmVec ∩
ℂVec) ∧ 𝐴 ∈
𝑋) → (𝐴 ≠ 0 → (𝑁‘𝐴) ≠ 0)) |
| 21 | 20 | impr 454 |
. . . . . 6
⊢ ((𝐺 ∈ (NrmVec ∩
ℂVec) ∧ (𝐴 ∈
𝑋 ∧ 𝐴 ≠ 0 )) → (𝑁‘𝐴) ≠ 0) |
| 22 | 14, 21 | rereccld 12094 |
. . . . 5
⊢ ((𝐺 ∈ (NrmVec ∩
ℂVec) ∧ (𝐴 ∈
𝑋 ∧ 𝐴 ≠ 0 )) → (1 / (𝑁‘𝐴)) ∈ ℝ) |
| 23 | 22 | 3adant3 1133 |
. . . 4
⊢ ((𝐺 ∈ (NrmVec ∩
ℂVec) ∧ (𝐴 ∈
𝑋 ∧ 𝐴 ≠ 0 ) ∧ (1 / (𝑁‘𝐴)) ∈ 𝐾) → (1 / (𝑁‘𝐴)) ∈ ℝ) |
| 24 | 2, 23 | elind 4200 |
. . 3
⊢ ((𝐺 ∈ (NrmVec ∩
ℂVec) ∧ (𝐴 ∈
𝑋 ∧ 𝐴 ≠ 0 ) ∧ (1 / (𝑁‘𝐴)) ∈ 𝐾) → (1 / (𝑁‘𝐴)) ∈ (𝐾 ∩ ℝ)) |
| 25 | | 1re 11261 |
. . . . . . . 8
⊢ 1 ∈
ℝ |
| 26 | | 0le1 11786 |
. . . . . . . 8
⊢ 0 ≤
1 |
| 27 | 25, 26 | pm3.2i 470 |
. . . . . . 7
⊢ (1 ∈
ℝ ∧ 0 ≤ 1) |
| 28 | 27 | a1i 11 |
. . . . . 6
⊢ ((𝐺 ∈ (NrmVec ∩
ℂVec) ∧ (𝐴 ∈
𝑋 ∧ 𝐴 ≠ 0 )) → (1 ∈
ℝ ∧ 0 ≤ 1)) |
| 29 | | simprr 773 |
. . . . . . 7
⊢ ((𝐺 ∈ (NrmVec ∩
ℂVec) ∧ (𝐴 ∈
𝑋 ∧ 𝐴 ≠ 0 )) → 𝐴 ≠ 0 ) |
| 30 | 11, 12, 15 | nmgt0 24643 |
. . . . . . . 8
⊢ ((𝐺 ∈ NrmGrp ∧ 𝐴 ∈ 𝑋) → (𝐴 ≠ 0 ↔ 0 < (𝑁‘𝐴))) |
| 31 | 10, 30 | syl 17 |
. . . . . . 7
⊢ ((𝐺 ∈ (NrmVec ∩
ℂVec) ∧ (𝐴 ∈
𝑋 ∧ 𝐴 ≠ 0 )) → (𝐴 ≠ 0 ↔ 0 < (𝑁‘𝐴))) |
| 32 | 29, 31 | mpbid 232 |
. . . . . 6
⊢ ((𝐺 ∈ (NrmVec ∩
ℂVec) ∧ (𝐴 ∈
𝑋 ∧ 𝐴 ≠ 0 )) → 0 < (𝑁‘𝐴)) |
| 33 | 28, 14, 32 | jca32 515 |
. . . . 5
⊢ ((𝐺 ∈ (NrmVec ∩
ℂVec) ∧ (𝐴 ∈
𝑋 ∧ 𝐴 ≠ 0 )) → ((1 ∈
ℝ ∧ 0 ≤ 1) ∧ ((𝑁‘𝐴) ∈ ℝ ∧ 0 < (𝑁‘𝐴)))) |
| 34 | 33 | 3adant3 1133 |
. . . 4
⊢ ((𝐺 ∈ (NrmVec ∩
ℂVec) ∧ (𝐴 ∈
𝑋 ∧ 𝐴 ≠ 0 ) ∧ (1 / (𝑁‘𝐴)) ∈ 𝐾) → ((1 ∈ ℝ ∧ 0 ≤ 1)
∧ ((𝑁‘𝐴) ∈ ℝ ∧ 0 <
(𝑁‘𝐴)))) |
| 35 | | divge0 12137 |
. . . 4
⊢ (((1
∈ ℝ ∧ 0 ≤ 1) ∧ ((𝑁‘𝐴) ∈ ℝ ∧ 0 < (𝑁‘𝐴))) → 0 ≤ (1 / (𝑁‘𝐴))) |
| 36 | 34, 35 | syl 17 |
. . 3
⊢ ((𝐺 ∈ (NrmVec ∩
ℂVec) ∧ (𝐴 ∈
𝑋 ∧ 𝐴 ≠ 0 ) ∧ (1 / (𝑁‘𝐴)) ∈ 𝐾) → 0 ≤ (1 / (𝑁‘𝐴))) |
| 37 | | simp2l 1200 |
. . 3
⊢ ((𝐺 ∈ (NrmVec ∩
ℂVec) ∧ (𝐴 ∈
𝑋 ∧ 𝐴 ≠ 0 ) ∧ (1 / (𝑁‘𝐴)) ∈ 𝐾) → 𝐴 ∈ 𝑋) |
| 38 | | ncvs1.s |
. . . 4
⊢ · = (
·𝑠 ‘𝐺) |
| 39 | | ncvs1.f |
. . . 4
⊢ 𝐹 = (Scalar‘𝐺) |
| 40 | | ncvs1.k |
. . . 4
⊢ 𝐾 = (Base‘𝐹) |
| 41 | 11, 12, 38, 39, 40 | ncvsge0 25187 |
. . 3
⊢ ((𝐺 ∈ (NrmVec ∩
ℂVec) ∧ ((1 / (𝑁‘𝐴)) ∈ (𝐾 ∩ ℝ) ∧ 0 ≤ (1 / (𝑁‘𝐴))) ∧ 𝐴 ∈ 𝑋) → (𝑁‘((1 / (𝑁‘𝐴)) · 𝐴)) = ((1 / (𝑁‘𝐴)) · (𝑁‘𝐴))) |
| 42 | 1, 24, 36, 37, 41 | syl121anc 1377 |
. 2
⊢ ((𝐺 ∈ (NrmVec ∩
ℂVec) ∧ (𝐴 ∈
𝑋 ∧ 𝐴 ≠ 0 ) ∧ (1 / (𝑁‘𝐴)) ∈ 𝐾) → (𝑁‘((1 / (𝑁‘𝐴)) · 𝐴)) = ((1 / (𝑁‘𝐴)) · (𝑁‘𝐴))) |
| 43 | 10 | 3adant3 1133 |
. . . . 5
⊢ ((𝐺 ∈ (NrmVec ∩
ℂVec) ∧ (𝐴 ∈
𝑋 ∧ 𝐴 ≠ 0 ) ∧ (1 / (𝑁‘𝐴)) ∈ 𝐾) → (𝐺 ∈ NrmGrp ∧ 𝐴 ∈ 𝑋)) |
| 44 | 43, 13 | syl 17 |
. . . 4
⊢ ((𝐺 ∈ (NrmVec ∩
ℂVec) ∧ (𝐴 ∈
𝑋 ∧ 𝐴 ≠ 0 ) ∧ (1 / (𝑁‘𝐴)) ∈ 𝐾) → (𝑁‘𝐴) ∈ ℝ) |
| 45 | 44 | recnd 11289 |
. . 3
⊢ ((𝐺 ∈ (NrmVec ∩
ℂVec) ∧ (𝐴 ∈
𝑋 ∧ 𝐴 ≠ 0 ) ∧ (1 / (𝑁‘𝐴)) ∈ 𝐾) → (𝑁‘𝐴) ∈ ℂ) |
| 46 | 21 | 3adant3 1133 |
. . 3
⊢ ((𝐺 ∈ (NrmVec ∩
ℂVec) ∧ (𝐴 ∈
𝑋 ∧ 𝐴 ≠ 0 ) ∧ (1 / (𝑁‘𝐴)) ∈ 𝐾) → (𝑁‘𝐴) ≠ 0) |
| 47 | 45, 46 | recid2d 12039 |
. 2
⊢ ((𝐺 ∈ (NrmVec ∩
ℂVec) ∧ (𝐴 ∈
𝑋 ∧ 𝐴 ≠ 0 ) ∧ (1 / (𝑁‘𝐴)) ∈ 𝐾) → ((1 / (𝑁‘𝐴)) · (𝑁‘𝐴)) = 1) |
| 48 | 42, 47 | eqtrd 2777 |
1
⊢ ((𝐺 ∈ (NrmVec ∩
ℂVec) ∧ (𝐴 ∈
𝑋 ∧ 𝐴 ≠ 0 ) ∧ (1 / (𝑁‘𝐴)) ∈ 𝐾) → (𝑁‘((1 / (𝑁‘𝐴)) · 𝐴)) = 1) |