Proof of Theorem ipasslem2
| Step | Hyp | Ref
| Expression |
| 1 | | nn0cn 12536 |
. . . . 5
⊢ (𝑁 ∈ ℕ0
→ 𝑁 ∈
ℂ) |
| 2 | 1 | negcld 11607 |
. . . 4
⊢ (𝑁 ∈ ℕ0
→ -𝑁 ∈
ℂ) |
| 3 | | ip1i.9 |
. . . . . 6
⊢ 𝑈 ∈
CPreHilOLD |
| 4 | 3 | phnvi 30835 |
. . . . 5
⊢ 𝑈 ∈ NrmCVec |
| 5 | | ipasslem1.b |
. . . . 5
⊢ 𝐵 ∈ 𝑋 |
| 6 | | ip1i.1 |
. . . . . 6
⊢ 𝑋 = (BaseSet‘𝑈) |
| 7 | | ip1i.7 |
. . . . . 6
⊢ 𝑃 =
(·𝑖OLD‘𝑈) |
| 8 | 6, 7 | dipcl 30731 |
. . . . 5
⊢ ((𝑈 ∈ NrmCVec ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋) → (𝐴𝑃𝐵) ∈ ℂ) |
| 9 | 4, 5, 8 | mp3an13 1454 |
. . . 4
⊢ (𝐴 ∈ 𝑋 → (𝐴𝑃𝐵) ∈ ℂ) |
| 10 | | mulcl 11239 |
. . . 4
⊢ ((-𝑁 ∈ ℂ ∧ (𝐴𝑃𝐵) ∈ ℂ) → (-𝑁 · (𝐴𝑃𝐵)) ∈ ℂ) |
| 11 | 2, 9, 10 | syl2an 596 |
. . 3
⊢ ((𝑁 ∈ ℕ0
∧ 𝐴 ∈ 𝑋) → (-𝑁 · (𝐴𝑃𝐵)) ∈ ℂ) |
| 12 | | ip1i.4 |
. . . . . . 7
⊢ 𝑆 = (
·𝑠OLD ‘𝑈) |
| 13 | 6, 12 | nvscl 30645 |
. . . . . 6
⊢ ((𝑈 ∈ NrmCVec ∧ -𝑁 ∈ ℂ ∧ 𝐴 ∈ 𝑋) → (-𝑁𝑆𝐴) ∈ 𝑋) |
| 14 | 4, 13 | mp3an1 1450 |
. . . . 5
⊢ ((-𝑁 ∈ ℂ ∧ 𝐴 ∈ 𝑋) → (-𝑁𝑆𝐴) ∈ 𝑋) |
| 15 | 2, 14 | sylan 580 |
. . . 4
⊢ ((𝑁 ∈ ℕ0
∧ 𝐴 ∈ 𝑋) → (-𝑁𝑆𝐴) ∈ 𝑋) |
| 16 | 6, 7 | dipcl 30731 |
. . . . 5
⊢ ((𝑈 ∈ NrmCVec ∧ (-𝑁𝑆𝐴) ∈ 𝑋 ∧ 𝐵 ∈ 𝑋) → ((-𝑁𝑆𝐴)𝑃𝐵) ∈ ℂ) |
| 17 | 4, 5, 16 | mp3an13 1454 |
. . . 4
⊢ ((-𝑁𝑆𝐴) ∈ 𝑋 → ((-𝑁𝑆𝐴)𝑃𝐵) ∈ ℂ) |
| 18 | 15, 17 | syl 17 |
. . 3
⊢ ((𝑁 ∈ ℕ0
∧ 𝐴 ∈ 𝑋) → ((-𝑁𝑆𝐴)𝑃𝐵) ∈ ℂ) |
| 19 | | ax-1cn 11213 |
. . . . . . . . . . . . 13
⊢ 1 ∈
ℂ |
| 20 | | mulneg2 11700 |
. . . . . . . . . . . . 13
⊢ ((𝑁 ∈ ℂ ∧ 1 ∈
ℂ) → (𝑁 ·
-1) = -(𝑁 ·
1)) |
| 21 | 19, 20 | mpan2 691 |
. . . . . . . . . . . 12
⊢ (𝑁 ∈ ℂ → (𝑁 · -1) = -(𝑁 · 1)) |
| 22 | | mulrid 11259 |
. . . . . . . . . . . . 13
⊢ (𝑁 ∈ ℂ → (𝑁 · 1) = 𝑁) |
| 23 | 22 | negeqd 11502 |
. . . . . . . . . . . 12
⊢ (𝑁 ∈ ℂ → -(𝑁 · 1) = -𝑁) |
| 24 | 21, 23 | eqtr2d 2778 |
. . . . . . . . . . 11
⊢ (𝑁 ∈ ℂ → -𝑁 = (𝑁 · -1)) |
| 25 | 24 | adantr 480 |
. . . . . . . . . 10
⊢ ((𝑁 ∈ ℂ ∧ 𝐴 ∈ 𝑋) → -𝑁 = (𝑁 · -1)) |
| 26 | 25 | oveq1d 7446 |
. . . . . . . . 9
⊢ ((𝑁 ∈ ℂ ∧ 𝐴 ∈ 𝑋) → (-𝑁𝑆𝐴) = ((𝑁 · -1)𝑆𝐴)) |
| 27 | | neg1cn 12380 |
. . . . . . . . . 10
⊢ -1 ∈
ℂ |
| 28 | 6, 12 | nvsass 30647 |
. . . . . . . . . . 11
⊢ ((𝑈 ∈ NrmCVec ∧ (𝑁 ∈ ℂ ∧ -1 ∈
ℂ ∧ 𝐴 ∈
𝑋)) → ((𝑁 · -1)𝑆𝐴) = (𝑁𝑆(-1𝑆𝐴))) |
| 29 | 4, 28 | mpan 690 |
. . . . . . . . . 10
⊢ ((𝑁 ∈ ℂ ∧ -1 ∈
ℂ ∧ 𝐴 ∈
𝑋) → ((𝑁 · -1)𝑆𝐴) = (𝑁𝑆(-1𝑆𝐴))) |
| 30 | 27, 29 | mp3an2 1451 |
. . . . . . . . 9
⊢ ((𝑁 ∈ ℂ ∧ 𝐴 ∈ 𝑋) → ((𝑁 · -1)𝑆𝐴) = (𝑁𝑆(-1𝑆𝐴))) |
| 31 | 26, 30 | eqtrd 2777 |
. . . . . . . 8
⊢ ((𝑁 ∈ ℂ ∧ 𝐴 ∈ 𝑋) → (-𝑁𝑆𝐴) = (𝑁𝑆(-1𝑆𝐴))) |
| 32 | 1, 31 | sylan 580 |
. . . . . . 7
⊢ ((𝑁 ∈ ℕ0
∧ 𝐴 ∈ 𝑋) → (-𝑁𝑆𝐴) = (𝑁𝑆(-1𝑆𝐴))) |
| 33 | 32 | oveq1d 7446 |
. . . . . 6
⊢ ((𝑁 ∈ ℕ0
∧ 𝐴 ∈ 𝑋) → ((-𝑁𝑆𝐴)𝑃𝐵) = ((𝑁𝑆(-1𝑆𝐴))𝑃𝐵)) |
| 34 | 6, 12 | nvscl 30645 |
. . . . . . . 8
⊢ ((𝑈 ∈ NrmCVec ∧ -1 ∈
ℂ ∧ 𝐴 ∈
𝑋) → (-1𝑆𝐴) ∈ 𝑋) |
| 35 | 4, 27, 34 | mp3an12 1453 |
. . . . . . 7
⊢ (𝐴 ∈ 𝑋 → (-1𝑆𝐴) ∈ 𝑋) |
| 36 | | ip1i.2 |
. . . . . . . 8
⊢ 𝐺 = ( +𝑣
‘𝑈) |
| 37 | 6, 36, 12, 7, 3, 5 | ipasslem1 30850 |
. . . . . . 7
⊢ ((𝑁 ∈ ℕ0
∧ (-1𝑆𝐴) ∈ 𝑋) → ((𝑁𝑆(-1𝑆𝐴))𝑃𝐵) = (𝑁 · ((-1𝑆𝐴)𝑃𝐵))) |
| 38 | 35, 37 | sylan2 593 |
. . . . . 6
⊢ ((𝑁 ∈ ℕ0
∧ 𝐴 ∈ 𝑋) → ((𝑁𝑆(-1𝑆𝐴))𝑃𝐵) = (𝑁 · ((-1𝑆𝐴)𝑃𝐵))) |
| 39 | 33, 38 | eqtrd 2777 |
. . . . 5
⊢ ((𝑁 ∈ ℕ0
∧ 𝐴 ∈ 𝑋) → ((-𝑁𝑆𝐴)𝑃𝐵) = (𝑁 · ((-1𝑆𝐴)𝑃𝐵))) |
| 40 | 39 | oveq2d 7447 |
. . . 4
⊢ ((𝑁 ∈ ℕ0
∧ 𝐴 ∈ 𝑋) → ((-𝑁 · (𝐴𝑃𝐵)) − ((-𝑁𝑆𝐴)𝑃𝐵)) = ((-𝑁 · (𝐴𝑃𝐵)) − (𝑁 · ((-1𝑆𝐴)𝑃𝐵)))) |
| 41 | 6, 7 | dipcl 30731 |
. . . . . . . 8
⊢ ((𝑈 ∈ NrmCVec ∧ (-1𝑆𝐴) ∈ 𝑋 ∧ 𝐵 ∈ 𝑋) → ((-1𝑆𝐴)𝑃𝐵) ∈ ℂ) |
| 42 | 4, 5, 41 | mp3an13 1454 |
. . . . . . 7
⊢ ((-1𝑆𝐴) ∈ 𝑋 → ((-1𝑆𝐴)𝑃𝐵) ∈ ℂ) |
| 43 | 35, 42 | syl 17 |
. . . . . 6
⊢ (𝐴 ∈ 𝑋 → ((-1𝑆𝐴)𝑃𝐵) ∈ ℂ) |
| 44 | | mulcl 11239 |
. . . . . 6
⊢ ((𝑁 ∈ ℂ ∧ ((-1𝑆𝐴)𝑃𝐵) ∈ ℂ) → (𝑁 · ((-1𝑆𝐴)𝑃𝐵)) ∈ ℂ) |
| 45 | 1, 43, 44 | syl2an 596 |
. . . . 5
⊢ ((𝑁 ∈ ℕ0
∧ 𝐴 ∈ 𝑋) → (𝑁 · ((-1𝑆𝐴)𝑃𝐵)) ∈ ℂ) |
| 46 | 11, 45 | negsubd 11626 |
. . . 4
⊢ ((𝑁 ∈ ℕ0
∧ 𝐴 ∈ 𝑋) → ((-𝑁 · (𝐴𝑃𝐵)) + -(𝑁 · ((-1𝑆𝐴)𝑃𝐵))) = ((-𝑁 · (𝐴𝑃𝐵)) − (𝑁 · ((-1𝑆𝐴)𝑃𝐵)))) |
| 47 | | mulneg1 11699 |
. . . . . . 7
⊢ ((𝑁 ∈ ℂ ∧ ((-1𝑆𝐴)𝑃𝐵) ∈ ℂ) → (-𝑁 · ((-1𝑆𝐴)𝑃𝐵)) = -(𝑁 · ((-1𝑆𝐴)𝑃𝐵))) |
| 48 | 1, 43, 47 | syl2an 596 |
. . . . . 6
⊢ ((𝑁 ∈ ℕ0
∧ 𝐴 ∈ 𝑋) → (-𝑁 · ((-1𝑆𝐴)𝑃𝐵)) = -(𝑁 · ((-1𝑆𝐴)𝑃𝐵))) |
| 49 | 48 | oveq2d 7447 |
. . . . 5
⊢ ((𝑁 ∈ ℕ0
∧ 𝐴 ∈ 𝑋) → ((-𝑁 · (𝐴𝑃𝐵)) + (-𝑁 · ((-1𝑆𝐴)𝑃𝐵))) = ((-𝑁 · (𝐴𝑃𝐵)) + -(𝑁 · ((-1𝑆𝐴)𝑃𝐵)))) |
| 50 | 2 | adantr 480 |
. . . . . . 7
⊢ ((𝑁 ∈ ℕ0
∧ 𝐴 ∈ 𝑋) → -𝑁 ∈ ℂ) |
| 51 | 9 | adantl 481 |
. . . . . . 7
⊢ ((𝑁 ∈ ℕ0
∧ 𝐴 ∈ 𝑋) → (𝐴𝑃𝐵) ∈ ℂ) |
| 52 | 43 | adantl 481 |
. . . . . . 7
⊢ ((𝑁 ∈ ℕ0
∧ 𝐴 ∈ 𝑋) → ((-1𝑆𝐴)𝑃𝐵) ∈ ℂ) |
| 53 | 50, 51, 52 | adddid 11285 |
. . . . . 6
⊢ ((𝑁 ∈ ℕ0
∧ 𝐴 ∈ 𝑋) → (-𝑁 · ((𝐴𝑃𝐵) + ((-1𝑆𝐴)𝑃𝐵))) = ((-𝑁 · (𝐴𝑃𝐵)) + (-𝑁 · ((-1𝑆𝐴)𝑃𝐵)))) |
| 54 | 6, 36, 12, 7, 3 | ipdiri 30849 |
. . . . . . . . . . 11
⊢ ((𝐴 ∈ 𝑋 ∧ (-1𝑆𝐴) ∈ 𝑋 ∧ 𝐵 ∈ 𝑋) → ((𝐴𝐺(-1𝑆𝐴))𝑃𝐵) = ((𝐴𝑃𝐵) + ((-1𝑆𝐴)𝑃𝐵))) |
| 55 | 5, 54 | mp3an3 1452 |
. . . . . . . . . 10
⊢ ((𝐴 ∈ 𝑋 ∧ (-1𝑆𝐴) ∈ 𝑋) → ((𝐴𝐺(-1𝑆𝐴))𝑃𝐵) = ((𝐴𝑃𝐵) + ((-1𝑆𝐴)𝑃𝐵))) |
| 56 | 35, 55 | mpdan 687 |
. . . . . . . . 9
⊢ (𝐴 ∈ 𝑋 → ((𝐴𝐺(-1𝑆𝐴))𝑃𝐵) = ((𝐴𝑃𝐵) + ((-1𝑆𝐴)𝑃𝐵))) |
| 57 | | eqid 2737 |
. . . . . . . . . . . . 13
⊢
(0vec‘𝑈) = (0vec‘𝑈) |
| 58 | 6, 36, 12, 57 | nvrinv 30670 |
. . . . . . . . . . . 12
⊢ ((𝑈 ∈ NrmCVec ∧ 𝐴 ∈ 𝑋) → (𝐴𝐺(-1𝑆𝐴)) = (0vec‘𝑈)) |
| 59 | 4, 58 | mpan 690 |
. . . . . . . . . . 11
⊢ (𝐴 ∈ 𝑋 → (𝐴𝐺(-1𝑆𝐴)) = (0vec‘𝑈)) |
| 60 | 59 | oveq1d 7446 |
. . . . . . . . . 10
⊢ (𝐴 ∈ 𝑋 → ((𝐴𝐺(-1𝑆𝐴))𝑃𝐵) = ((0vec‘𝑈)𝑃𝐵)) |
| 61 | 6, 57, 7 | dip0l 30737 |
. . . . . . . . . . 11
⊢ ((𝑈 ∈ NrmCVec ∧ 𝐵 ∈ 𝑋) → ((0vec‘𝑈)𝑃𝐵) = 0) |
| 62 | 4, 5, 61 | mp2an 692 |
. . . . . . . . . 10
⊢
((0vec‘𝑈)𝑃𝐵) = 0 |
| 63 | 60, 62 | eqtrdi 2793 |
. . . . . . . . 9
⊢ (𝐴 ∈ 𝑋 → ((𝐴𝐺(-1𝑆𝐴))𝑃𝐵) = 0) |
| 64 | 56, 63 | eqtr3d 2779 |
. . . . . . . 8
⊢ (𝐴 ∈ 𝑋 → ((𝐴𝑃𝐵) + ((-1𝑆𝐴)𝑃𝐵)) = 0) |
| 65 | 64 | oveq2d 7447 |
. . . . . . 7
⊢ (𝐴 ∈ 𝑋 → (-𝑁 · ((𝐴𝑃𝐵) + ((-1𝑆𝐴)𝑃𝐵))) = (-𝑁 · 0)) |
| 66 | 2 | mul01d 11460 |
. . . . . . 7
⊢ (𝑁 ∈ ℕ0
→ (-𝑁 · 0) =
0) |
| 67 | 65, 66 | sylan9eqr 2799 |
. . . . . 6
⊢ ((𝑁 ∈ ℕ0
∧ 𝐴 ∈ 𝑋) → (-𝑁 · ((𝐴𝑃𝐵) + ((-1𝑆𝐴)𝑃𝐵))) = 0) |
| 68 | 53, 67 | eqtr3d 2779 |
. . . . 5
⊢ ((𝑁 ∈ ℕ0
∧ 𝐴 ∈ 𝑋) → ((-𝑁 · (𝐴𝑃𝐵)) + (-𝑁 · ((-1𝑆𝐴)𝑃𝐵))) = 0) |
| 69 | 49, 68 | eqtr3d 2779 |
. . . 4
⊢ ((𝑁 ∈ ℕ0
∧ 𝐴 ∈ 𝑋) → ((-𝑁 · (𝐴𝑃𝐵)) + -(𝑁 · ((-1𝑆𝐴)𝑃𝐵))) = 0) |
| 70 | 40, 46, 69 | 3eqtr2d 2783 |
. . 3
⊢ ((𝑁 ∈ ℕ0
∧ 𝐴 ∈ 𝑋) → ((-𝑁 · (𝐴𝑃𝐵)) − ((-𝑁𝑆𝐴)𝑃𝐵)) = 0) |
| 71 | 11, 18, 70 | subeq0d 11628 |
. 2
⊢ ((𝑁 ∈ ℕ0
∧ 𝐴 ∈ 𝑋) → (-𝑁 · (𝐴𝑃𝐵)) = ((-𝑁𝑆𝐴)𝑃𝐵)) |
| 72 | 71 | eqcomd 2743 |
1
⊢ ((𝑁 ∈ ℕ0
∧ 𝐴 ∈ 𝑋) → ((-𝑁𝑆𝐴)𝑃𝐵) = (-𝑁 · (𝐴𝑃𝐵))) |