| Step | Hyp | Ref
| Expression |
| 1 | | nn0cn 12536 |
. . . . . . . . . . 11
⊢ (𝑘 ∈ ℕ0
→ 𝑘 ∈
ℂ) |
| 2 | | ax-1cn 11213 |
. . . . . . . . . . . 12
⊢ 1 ∈
ℂ |
| 3 | | ip1i.9 |
. . . . . . . . . . . . . 14
⊢ 𝑈 ∈
CPreHilOLD |
| 4 | 3 | phnvi 30835 |
. . . . . . . . . . . . 13
⊢ 𝑈 ∈ NrmCVec |
| 5 | | ip1i.1 |
. . . . . . . . . . . . . 14
⊢ 𝑋 = (BaseSet‘𝑈) |
| 6 | | ip1i.2 |
. . . . . . . . . . . . . 14
⊢ 𝐺 = ( +𝑣
‘𝑈) |
| 7 | | ip1i.4 |
. . . . . . . . . . . . . 14
⊢ 𝑆 = (
·𝑠OLD ‘𝑈) |
| 8 | 5, 6, 7 | nvdir 30650 |
. . . . . . . . . . . . 13
⊢ ((𝑈 ∈ NrmCVec ∧ (𝑘 ∈ ℂ ∧ 1 ∈
ℂ ∧ 𝐴 ∈
𝑋)) → ((𝑘 + 1)𝑆𝐴) = ((𝑘𝑆𝐴)𝐺(1𝑆𝐴))) |
| 9 | 4, 8 | mpan 690 |
. . . . . . . . . . . 12
⊢ ((𝑘 ∈ ℂ ∧ 1 ∈
ℂ ∧ 𝐴 ∈
𝑋) → ((𝑘 + 1)𝑆𝐴) = ((𝑘𝑆𝐴)𝐺(1𝑆𝐴))) |
| 10 | 2, 9 | mp3an2 1451 |
. . . . . . . . . . 11
⊢ ((𝑘 ∈ ℂ ∧ 𝐴 ∈ 𝑋) → ((𝑘 + 1)𝑆𝐴) = ((𝑘𝑆𝐴)𝐺(1𝑆𝐴))) |
| 11 | 1, 10 | sylan 580 |
. . . . . . . . . 10
⊢ ((𝑘 ∈ ℕ0
∧ 𝐴 ∈ 𝑋) → ((𝑘 + 1)𝑆𝐴) = ((𝑘𝑆𝐴)𝐺(1𝑆𝐴))) |
| 12 | 5, 7 | nvsid 30646 |
. . . . . . . . . . . . 13
⊢ ((𝑈 ∈ NrmCVec ∧ 𝐴 ∈ 𝑋) → (1𝑆𝐴) = 𝐴) |
| 13 | 4, 12 | mpan 690 |
. . . . . . . . . . . 12
⊢ (𝐴 ∈ 𝑋 → (1𝑆𝐴) = 𝐴) |
| 14 | 13 | adantl 481 |
. . . . . . . . . . 11
⊢ ((𝑘 ∈ ℕ0
∧ 𝐴 ∈ 𝑋) → (1𝑆𝐴) = 𝐴) |
| 15 | 14 | oveq2d 7447 |
. . . . . . . . . 10
⊢ ((𝑘 ∈ ℕ0
∧ 𝐴 ∈ 𝑋) → ((𝑘𝑆𝐴)𝐺(1𝑆𝐴)) = ((𝑘𝑆𝐴)𝐺𝐴)) |
| 16 | 11, 15 | eqtrd 2777 |
. . . . . . . . 9
⊢ ((𝑘 ∈ ℕ0
∧ 𝐴 ∈ 𝑋) → ((𝑘 + 1)𝑆𝐴) = ((𝑘𝑆𝐴)𝐺𝐴)) |
| 17 | 16 | oveq1d 7446 |
. . . . . . . 8
⊢ ((𝑘 ∈ ℕ0
∧ 𝐴 ∈ 𝑋) → (((𝑘 + 1)𝑆𝐴)𝑃𝐵) = (((𝑘𝑆𝐴)𝐺𝐴)𝑃𝐵)) |
| 18 | | ipasslem1.b |
. . . . . . . . . . . . 13
⊢ 𝐵 ∈ 𝑋 |
| 19 | | ip1i.7 |
. . . . . . . . . . . . . 14
⊢ 𝑃 =
(·𝑖OLD‘𝑈) |
| 20 | 5, 19 | dipcl 30731 |
. . . . . . . . . . . . 13
⊢ ((𝑈 ∈ NrmCVec ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋) → (𝐴𝑃𝐵) ∈ ℂ) |
| 21 | 4, 18, 20 | mp3an13 1454 |
. . . . . . . . . . . 12
⊢ (𝐴 ∈ 𝑋 → (𝐴𝑃𝐵) ∈ ℂ) |
| 22 | 21 | mullidd 11279 |
. . . . . . . . . . 11
⊢ (𝐴 ∈ 𝑋 → (1 · (𝐴𝑃𝐵)) = (𝐴𝑃𝐵)) |
| 23 | 22 | adantl 481 |
. . . . . . . . . 10
⊢ ((𝑘 ∈ ℕ0
∧ 𝐴 ∈ 𝑋) → (1 · (𝐴𝑃𝐵)) = (𝐴𝑃𝐵)) |
| 24 | 23 | oveq2d 7447 |
. . . . . . . . 9
⊢ ((𝑘 ∈ ℕ0
∧ 𝐴 ∈ 𝑋) → (((𝑘𝑆𝐴)𝑃𝐵) + (1 · (𝐴𝑃𝐵))) = (((𝑘𝑆𝐴)𝑃𝐵) + (𝐴𝑃𝐵))) |
| 25 | 5, 7 | nvscl 30645 |
. . . . . . . . . . . 12
⊢ ((𝑈 ∈ NrmCVec ∧ 𝑘 ∈ ℂ ∧ 𝐴 ∈ 𝑋) → (𝑘𝑆𝐴) ∈ 𝑋) |
| 26 | 4, 25 | mp3an1 1450 |
. . . . . . . . . . 11
⊢ ((𝑘 ∈ ℂ ∧ 𝐴 ∈ 𝑋) → (𝑘𝑆𝐴) ∈ 𝑋) |
| 27 | 1, 26 | sylan 580 |
. . . . . . . . . 10
⊢ ((𝑘 ∈ ℕ0
∧ 𝐴 ∈ 𝑋) → (𝑘𝑆𝐴) ∈ 𝑋) |
| 28 | 5, 6, 7, 19, 3 | ipdiri 30849 |
. . . . . . . . . . 11
⊢ (((𝑘𝑆𝐴) ∈ 𝑋 ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋) → (((𝑘𝑆𝐴)𝐺𝐴)𝑃𝐵) = (((𝑘𝑆𝐴)𝑃𝐵) + (𝐴𝑃𝐵))) |
| 29 | 18, 28 | mp3an3 1452 |
. . . . . . . . . 10
⊢ (((𝑘𝑆𝐴) ∈ 𝑋 ∧ 𝐴 ∈ 𝑋) → (((𝑘𝑆𝐴)𝐺𝐴)𝑃𝐵) = (((𝑘𝑆𝐴)𝑃𝐵) + (𝐴𝑃𝐵))) |
| 30 | 27, 29 | sylancom 588 |
. . . . . . . . 9
⊢ ((𝑘 ∈ ℕ0
∧ 𝐴 ∈ 𝑋) → (((𝑘𝑆𝐴)𝐺𝐴)𝑃𝐵) = (((𝑘𝑆𝐴)𝑃𝐵) + (𝐴𝑃𝐵))) |
| 31 | 24, 30 | eqtr4d 2780 |
. . . . . . . 8
⊢ ((𝑘 ∈ ℕ0
∧ 𝐴 ∈ 𝑋) → (((𝑘𝑆𝐴)𝑃𝐵) + (1 · (𝐴𝑃𝐵))) = (((𝑘𝑆𝐴)𝐺𝐴)𝑃𝐵)) |
| 32 | 17, 31 | eqtr4d 2780 |
. . . . . . 7
⊢ ((𝑘 ∈ ℕ0
∧ 𝐴 ∈ 𝑋) → (((𝑘 + 1)𝑆𝐴)𝑃𝐵) = (((𝑘𝑆𝐴)𝑃𝐵) + (1 · (𝐴𝑃𝐵)))) |
| 33 | | oveq1 7438 |
. . . . . . 7
⊢ (((𝑘𝑆𝐴)𝑃𝐵) = (𝑘 · (𝐴𝑃𝐵)) → (((𝑘𝑆𝐴)𝑃𝐵) + (1 · (𝐴𝑃𝐵))) = ((𝑘 · (𝐴𝑃𝐵)) + (1 · (𝐴𝑃𝐵)))) |
| 34 | 32, 33 | sylan9eq 2797 |
. . . . . 6
⊢ (((𝑘 ∈ ℕ0
∧ 𝐴 ∈ 𝑋) ∧ ((𝑘𝑆𝐴)𝑃𝐵) = (𝑘 · (𝐴𝑃𝐵))) → (((𝑘 + 1)𝑆𝐴)𝑃𝐵) = ((𝑘 · (𝐴𝑃𝐵)) + (1 · (𝐴𝑃𝐵)))) |
| 35 | | adddir 11252 |
. . . . . . . . 9
⊢ ((𝑘 ∈ ℂ ∧ 1 ∈
ℂ ∧ (𝐴𝑃𝐵) ∈ ℂ) → ((𝑘 + 1) · (𝐴𝑃𝐵)) = ((𝑘 · (𝐴𝑃𝐵)) + (1 · (𝐴𝑃𝐵)))) |
| 36 | 2, 35 | mp3an2 1451 |
. . . . . . . 8
⊢ ((𝑘 ∈ ℂ ∧ (𝐴𝑃𝐵) ∈ ℂ) → ((𝑘 + 1) · (𝐴𝑃𝐵)) = ((𝑘 · (𝐴𝑃𝐵)) + (1 · (𝐴𝑃𝐵)))) |
| 37 | 1, 21, 36 | syl2an 596 |
. . . . . . 7
⊢ ((𝑘 ∈ ℕ0
∧ 𝐴 ∈ 𝑋) → ((𝑘 + 1) · (𝐴𝑃𝐵)) = ((𝑘 · (𝐴𝑃𝐵)) + (1 · (𝐴𝑃𝐵)))) |
| 38 | 37 | adantr 480 |
. . . . . 6
⊢ (((𝑘 ∈ ℕ0
∧ 𝐴 ∈ 𝑋) ∧ ((𝑘𝑆𝐴)𝑃𝐵) = (𝑘 · (𝐴𝑃𝐵))) → ((𝑘 + 1) · (𝐴𝑃𝐵)) = ((𝑘 · (𝐴𝑃𝐵)) + (1 · (𝐴𝑃𝐵)))) |
| 39 | 34, 38 | eqtr4d 2780 |
. . . . 5
⊢ (((𝑘 ∈ ℕ0
∧ 𝐴 ∈ 𝑋) ∧ ((𝑘𝑆𝐴)𝑃𝐵) = (𝑘 · (𝐴𝑃𝐵))) → (((𝑘 + 1)𝑆𝐴)𝑃𝐵) = ((𝑘 + 1) · (𝐴𝑃𝐵))) |
| 40 | 39 | exp31 419 |
. . . 4
⊢ (𝑘 ∈ ℕ0
→ (𝐴 ∈ 𝑋 → (((𝑘𝑆𝐴)𝑃𝐵) = (𝑘 · (𝐴𝑃𝐵)) → (((𝑘 + 1)𝑆𝐴)𝑃𝐵) = ((𝑘 + 1) · (𝐴𝑃𝐵))))) |
| 41 | 40 | a2d 29 |
. . 3
⊢ (𝑘 ∈ ℕ0
→ ((𝐴 ∈ 𝑋 → ((𝑘𝑆𝐴)𝑃𝐵) = (𝑘 · (𝐴𝑃𝐵))) → (𝐴 ∈ 𝑋 → (((𝑘 + 1)𝑆𝐴)𝑃𝐵) = ((𝑘 + 1) · (𝐴𝑃𝐵))))) |
| 42 | | eqid 2737 |
. . . . . 6
⊢
(0vec‘𝑈) = (0vec‘𝑈) |
| 43 | 5, 42, 19 | dip0l 30737 |
. . . . 5
⊢ ((𝑈 ∈ NrmCVec ∧ 𝐵 ∈ 𝑋) → ((0vec‘𝑈)𝑃𝐵) = 0) |
| 44 | 4, 18, 43 | mp2an 692 |
. . . 4
⊢
((0vec‘𝑈)𝑃𝐵) = 0 |
| 45 | 5, 7, 42 | nv0 30656 |
. . . . . 6
⊢ ((𝑈 ∈ NrmCVec ∧ 𝐴 ∈ 𝑋) → (0𝑆𝐴) = (0vec‘𝑈)) |
| 46 | 4, 45 | mpan 690 |
. . . . 5
⊢ (𝐴 ∈ 𝑋 → (0𝑆𝐴) = (0vec‘𝑈)) |
| 47 | 46 | oveq1d 7446 |
. . . 4
⊢ (𝐴 ∈ 𝑋 → ((0𝑆𝐴)𝑃𝐵) = ((0vec‘𝑈)𝑃𝐵)) |
| 48 | 21 | mul02d 11459 |
. . . 4
⊢ (𝐴 ∈ 𝑋 → (0 · (𝐴𝑃𝐵)) = 0) |
| 49 | 44, 47, 48 | 3eqtr4a 2803 |
. . 3
⊢ (𝐴 ∈ 𝑋 → ((0𝑆𝐴)𝑃𝐵) = (0 · (𝐴𝑃𝐵))) |
| 50 | | oveq1 7438 |
. . . . . 6
⊢ (𝑗 = 0 → (𝑗𝑆𝐴) = (0𝑆𝐴)) |
| 51 | 50 | oveq1d 7446 |
. . . . 5
⊢ (𝑗 = 0 → ((𝑗𝑆𝐴)𝑃𝐵) = ((0𝑆𝐴)𝑃𝐵)) |
| 52 | | oveq1 7438 |
. . . . 5
⊢ (𝑗 = 0 → (𝑗 · (𝐴𝑃𝐵)) = (0 · (𝐴𝑃𝐵))) |
| 53 | 51, 52 | eqeq12d 2753 |
. . . 4
⊢ (𝑗 = 0 → (((𝑗𝑆𝐴)𝑃𝐵) = (𝑗 · (𝐴𝑃𝐵)) ↔ ((0𝑆𝐴)𝑃𝐵) = (0 · (𝐴𝑃𝐵)))) |
| 54 | 53 | imbi2d 340 |
. . 3
⊢ (𝑗 = 0 → ((𝐴 ∈ 𝑋 → ((𝑗𝑆𝐴)𝑃𝐵) = (𝑗 · (𝐴𝑃𝐵))) ↔ (𝐴 ∈ 𝑋 → ((0𝑆𝐴)𝑃𝐵) = (0 · (𝐴𝑃𝐵))))) |
| 55 | | oveq1 7438 |
. . . . . 6
⊢ (𝑗 = 𝑘 → (𝑗𝑆𝐴) = (𝑘𝑆𝐴)) |
| 56 | 55 | oveq1d 7446 |
. . . . 5
⊢ (𝑗 = 𝑘 → ((𝑗𝑆𝐴)𝑃𝐵) = ((𝑘𝑆𝐴)𝑃𝐵)) |
| 57 | | oveq1 7438 |
. . . . 5
⊢ (𝑗 = 𝑘 → (𝑗 · (𝐴𝑃𝐵)) = (𝑘 · (𝐴𝑃𝐵))) |
| 58 | 56, 57 | eqeq12d 2753 |
. . . 4
⊢ (𝑗 = 𝑘 → (((𝑗𝑆𝐴)𝑃𝐵) = (𝑗 · (𝐴𝑃𝐵)) ↔ ((𝑘𝑆𝐴)𝑃𝐵) = (𝑘 · (𝐴𝑃𝐵)))) |
| 59 | 58 | imbi2d 340 |
. . 3
⊢ (𝑗 = 𝑘 → ((𝐴 ∈ 𝑋 → ((𝑗𝑆𝐴)𝑃𝐵) = (𝑗 · (𝐴𝑃𝐵))) ↔ (𝐴 ∈ 𝑋 → ((𝑘𝑆𝐴)𝑃𝐵) = (𝑘 · (𝐴𝑃𝐵))))) |
| 60 | | oveq1 7438 |
. . . . . 6
⊢ (𝑗 = (𝑘 + 1) → (𝑗𝑆𝐴) = ((𝑘 + 1)𝑆𝐴)) |
| 61 | 60 | oveq1d 7446 |
. . . . 5
⊢ (𝑗 = (𝑘 + 1) → ((𝑗𝑆𝐴)𝑃𝐵) = (((𝑘 + 1)𝑆𝐴)𝑃𝐵)) |
| 62 | | oveq1 7438 |
. . . . 5
⊢ (𝑗 = (𝑘 + 1) → (𝑗 · (𝐴𝑃𝐵)) = ((𝑘 + 1) · (𝐴𝑃𝐵))) |
| 63 | 61, 62 | eqeq12d 2753 |
. . . 4
⊢ (𝑗 = (𝑘 + 1) → (((𝑗𝑆𝐴)𝑃𝐵) = (𝑗 · (𝐴𝑃𝐵)) ↔ (((𝑘 + 1)𝑆𝐴)𝑃𝐵) = ((𝑘 + 1) · (𝐴𝑃𝐵)))) |
| 64 | 63 | imbi2d 340 |
. . 3
⊢ (𝑗 = (𝑘 + 1) → ((𝐴 ∈ 𝑋 → ((𝑗𝑆𝐴)𝑃𝐵) = (𝑗 · (𝐴𝑃𝐵))) ↔ (𝐴 ∈ 𝑋 → (((𝑘 + 1)𝑆𝐴)𝑃𝐵) = ((𝑘 + 1) · (𝐴𝑃𝐵))))) |
| 65 | | oveq1 7438 |
. . . . . 6
⊢ (𝑗 = 𝑁 → (𝑗𝑆𝐴) = (𝑁𝑆𝐴)) |
| 66 | 65 | oveq1d 7446 |
. . . . 5
⊢ (𝑗 = 𝑁 → ((𝑗𝑆𝐴)𝑃𝐵) = ((𝑁𝑆𝐴)𝑃𝐵)) |
| 67 | | oveq1 7438 |
. . . . 5
⊢ (𝑗 = 𝑁 → (𝑗 · (𝐴𝑃𝐵)) = (𝑁 · (𝐴𝑃𝐵))) |
| 68 | 66, 67 | eqeq12d 2753 |
. . . 4
⊢ (𝑗 = 𝑁 → (((𝑗𝑆𝐴)𝑃𝐵) = (𝑗 · (𝐴𝑃𝐵)) ↔ ((𝑁𝑆𝐴)𝑃𝐵) = (𝑁 · (𝐴𝑃𝐵)))) |
| 69 | 68 | imbi2d 340 |
. . 3
⊢ (𝑗 = 𝑁 → ((𝐴 ∈ 𝑋 → ((𝑗𝑆𝐴)𝑃𝐵) = (𝑗 · (𝐴𝑃𝐵))) ↔ (𝐴 ∈ 𝑋 → ((𝑁𝑆𝐴)𝑃𝐵) = (𝑁 · (𝐴𝑃𝐵))))) |
| 70 | 41, 49, 54, 59, 64, 69 | nn0indALT 12714 |
. 2
⊢ (𝑁 ∈ ℕ0
→ (𝐴 ∈ 𝑋 → ((𝑁𝑆𝐴)𝑃𝐵) = (𝑁 · (𝐴𝑃𝐵)))) |
| 71 | 70 | imp 406 |
1
⊢ ((𝑁 ∈ ℕ0
∧ 𝐴 ∈ 𝑋) → ((𝑁𝑆𝐴)𝑃𝐵) = (𝑁 · (𝐴𝑃𝐵))) |