Step | Hyp | Ref
| Expression |
1 | | nn0cn 11653 |
. . . . . . . . . . 11
⊢ (𝑘 ∈ ℕ0
→ 𝑘 ∈
ℂ) |
2 | | ax-1cn 10330 |
. . . . . . . . . . . 12
⊢ 1 ∈
ℂ |
3 | | ip1i.9 |
. . . . . . . . . . . . . 14
⊢ 𝑈 ∈
CPreHilOLD |
4 | 3 | phnvi 28243 |
. . . . . . . . . . . . 13
⊢ 𝑈 ∈ NrmCVec |
5 | | ip1i.1 |
. . . . . . . . . . . . . 14
⊢ 𝑋 = (BaseSet‘𝑈) |
6 | | ip1i.2 |
. . . . . . . . . . . . . 14
⊢ 𝐺 = ( +𝑣
‘𝑈) |
7 | | ip1i.4 |
. . . . . . . . . . . . . 14
⊢ 𝑆 = (
·𝑠OLD ‘𝑈) |
8 | 5, 6, 7 | nvdir 28058 |
. . . . . . . . . . . . 13
⊢ ((𝑈 ∈ NrmCVec ∧ (𝑘 ∈ ℂ ∧ 1 ∈
ℂ ∧ 𝐴 ∈
𝑋)) → ((𝑘 + 1)𝑆𝐴) = ((𝑘𝑆𝐴)𝐺(1𝑆𝐴))) |
9 | 4, 8 | mpan 680 |
. . . . . . . . . . . 12
⊢ ((𝑘 ∈ ℂ ∧ 1 ∈
ℂ ∧ 𝐴 ∈
𝑋) → ((𝑘 + 1)𝑆𝐴) = ((𝑘𝑆𝐴)𝐺(1𝑆𝐴))) |
10 | 2, 9 | mp3an2 1522 |
. . . . . . . . . . 11
⊢ ((𝑘 ∈ ℂ ∧ 𝐴 ∈ 𝑋) → ((𝑘 + 1)𝑆𝐴) = ((𝑘𝑆𝐴)𝐺(1𝑆𝐴))) |
11 | 1, 10 | sylan 575 |
. . . . . . . . . 10
⊢ ((𝑘 ∈ ℕ0
∧ 𝐴 ∈ 𝑋) → ((𝑘 + 1)𝑆𝐴) = ((𝑘𝑆𝐴)𝐺(1𝑆𝐴))) |
12 | 5, 7 | nvsid 28054 |
. . . . . . . . . . . . 13
⊢ ((𝑈 ∈ NrmCVec ∧ 𝐴 ∈ 𝑋) → (1𝑆𝐴) = 𝐴) |
13 | 4, 12 | mpan 680 |
. . . . . . . . . . . 12
⊢ (𝐴 ∈ 𝑋 → (1𝑆𝐴) = 𝐴) |
14 | 13 | adantl 475 |
. . . . . . . . . . 11
⊢ ((𝑘 ∈ ℕ0
∧ 𝐴 ∈ 𝑋) → (1𝑆𝐴) = 𝐴) |
15 | 14 | oveq2d 6938 |
. . . . . . . . . 10
⊢ ((𝑘 ∈ ℕ0
∧ 𝐴 ∈ 𝑋) → ((𝑘𝑆𝐴)𝐺(1𝑆𝐴)) = ((𝑘𝑆𝐴)𝐺𝐴)) |
16 | 11, 15 | eqtrd 2813 |
. . . . . . . . 9
⊢ ((𝑘 ∈ ℕ0
∧ 𝐴 ∈ 𝑋) → ((𝑘 + 1)𝑆𝐴) = ((𝑘𝑆𝐴)𝐺𝐴)) |
17 | 16 | oveq1d 6937 |
. . . . . . . 8
⊢ ((𝑘 ∈ ℕ0
∧ 𝐴 ∈ 𝑋) → (((𝑘 + 1)𝑆𝐴)𝑃𝐵) = (((𝑘𝑆𝐴)𝐺𝐴)𝑃𝐵)) |
18 | | ipasslem1.b |
. . . . . . . . . . . . 13
⊢ 𝐵 ∈ 𝑋 |
19 | | ip1i.7 |
. . . . . . . . . . . . . 14
⊢ 𝑃 =
(·𝑖OLD‘𝑈) |
20 | 5, 19 | dipcl 28139 |
. . . . . . . . . . . . 13
⊢ ((𝑈 ∈ NrmCVec ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋) → (𝐴𝑃𝐵) ∈ ℂ) |
21 | 4, 18, 20 | mp3an13 1525 |
. . . . . . . . . . . 12
⊢ (𝐴 ∈ 𝑋 → (𝐴𝑃𝐵) ∈ ℂ) |
22 | 21 | mulid2d 10395 |
. . . . . . . . . . 11
⊢ (𝐴 ∈ 𝑋 → (1 · (𝐴𝑃𝐵)) = (𝐴𝑃𝐵)) |
23 | 22 | adantl 475 |
. . . . . . . . . 10
⊢ ((𝑘 ∈ ℕ0
∧ 𝐴 ∈ 𝑋) → (1 · (𝐴𝑃𝐵)) = (𝐴𝑃𝐵)) |
24 | 23 | oveq2d 6938 |
. . . . . . . . 9
⊢ ((𝑘 ∈ ℕ0
∧ 𝐴 ∈ 𝑋) → (((𝑘𝑆𝐴)𝑃𝐵) + (1 · (𝐴𝑃𝐵))) = (((𝑘𝑆𝐴)𝑃𝐵) + (𝐴𝑃𝐵))) |
25 | 5, 7 | nvscl 28053 |
. . . . . . . . . . . 12
⊢ ((𝑈 ∈ NrmCVec ∧ 𝑘 ∈ ℂ ∧ 𝐴 ∈ 𝑋) → (𝑘𝑆𝐴) ∈ 𝑋) |
26 | 4, 25 | mp3an1 1521 |
. . . . . . . . . . 11
⊢ ((𝑘 ∈ ℂ ∧ 𝐴 ∈ 𝑋) → (𝑘𝑆𝐴) ∈ 𝑋) |
27 | 1, 26 | sylan 575 |
. . . . . . . . . 10
⊢ ((𝑘 ∈ ℕ0
∧ 𝐴 ∈ 𝑋) → (𝑘𝑆𝐴) ∈ 𝑋) |
28 | 5, 6, 7, 19, 3 | ipdiri 28257 |
. . . . . . . . . . 11
⊢ (((𝑘𝑆𝐴) ∈ 𝑋 ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋) → (((𝑘𝑆𝐴)𝐺𝐴)𝑃𝐵) = (((𝑘𝑆𝐴)𝑃𝐵) + (𝐴𝑃𝐵))) |
29 | 18, 28 | mp3an3 1523 |
. . . . . . . . . 10
⊢ (((𝑘𝑆𝐴) ∈ 𝑋 ∧ 𝐴 ∈ 𝑋) → (((𝑘𝑆𝐴)𝐺𝐴)𝑃𝐵) = (((𝑘𝑆𝐴)𝑃𝐵) + (𝐴𝑃𝐵))) |
30 | 27, 29 | sylancom 582 |
. . . . . . . . 9
⊢ ((𝑘 ∈ ℕ0
∧ 𝐴 ∈ 𝑋) → (((𝑘𝑆𝐴)𝐺𝐴)𝑃𝐵) = (((𝑘𝑆𝐴)𝑃𝐵) + (𝐴𝑃𝐵))) |
31 | 24, 30 | eqtr4d 2816 |
. . . . . . . 8
⊢ ((𝑘 ∈ ℕ0
∧ 𝐴 ∈ 𝑋) → (((𝑘𝑆𝐴)𝑃𝐵) + (1 · (𝐴𝑃𝐵))) = (((𝑘𝑆𝐴)𝐺𝐴)𝑃𝐵)) |
32 | 17, 31 | eqtr4d 2816 |
. . . . . . 7
⊢ ((𝑘 ∈ ℕ0
∧ 𝐴 ∈ 𝑋) → (((𝑘 + 1)𝑆𝐴)𝑃𝐵) = (((𝑘𝑆𝐴)𝑃𝐵) + (1 · (𝐴𝑃𝐵)))) |
33 | | oveq1 6929 |
. . . . . . 7
⊢ (((𝑘𝑆𝐴)𝑃𝐵) = (𝑘 · (𝐴𝑃𝐵)) → (((𝑘𝑆𝐴)𝑃𝐵) + (1 · (𝐴𝑃𝐵))) = ((𝑘 · (𝐴𝑃𝐵)) + (1 · (𝐴𝑃𝐵)))) |
34 | 32, 33 | sylan9eq 2833 |
. . . . . 6
⊢ (((𝑘 ∈ ℕ0
∧ 𝐴 ∈ 𝑋) ∧ ((𝑘𝑆𝐴)𝑃𝐵) = (𝑘 · (𝐴𝑃𝐵))) → (((𝑘 + 1)𝑆𝐴)𝑃𝐵) = ((𝑘 · (𝐴𝑃𝐵)) + (1 · (𝐴𝑃𝐵)))) |
35 | | adddir 10367 |
. . . . . . . . 9
⊢ ((𝑘 ∈ ℂ ∧ 1 ∈
ℂ ∧ (𝐴𝑃𝐵) ∈ ℂ) → ((𝑘 + 1) · (𝐴𝑃𝐵)) = ((𝑘 · (𝐴𝑃𝐵)) + (1 · (𝐴𝑃𝐵)))) |
36 | 2, 35 | mp3an2 1522 |
. . . . . . . 8
⊢ ((𝑘 ∈ ℂ ∧ (𝐴𝑃𝐵) ∈ ℂ) → ((𝑘 + 1) · (𝐴𝑃𝐵)) = ((𝑘 · (𝐴𝑃𝐵)) + (1 · (𝐴𝑃𝐵)))) |
37 | 1, 21, 36 | syl2an 589 |
. . . . . . 7
⊢ ((𝑘 ∈ ℕ0
∧ 𝐴 ∈ 𝑋) → ((𝑘 + 1) · (𝐴𝑃𝐵)) = ((𝑘 · (𝐴𝑃𝐵)) + (1 · (𝐴𝑃𝐵)))) |
38 | 37 | adantr 474 |
. . . . . 6
⊢ (((𝑘 ∈ ℕ0
∧ 𝐴 ∈ 𝑋) ∧ ((𝑘𝑆𝐴)𝑃𝐵) = (𝑘 · (𝐴𝑃𝐵))) → ((𝑘 + 1) · (𝐴𝑃𝐵)) = ((𝑘 · (𝐴𝑃𝐵)) + (1 · (𝐴𝑃𝐵)))) |
39 | 34, 38 | eqtr4d 2816 |
. . . . 5
⊢ (((𝑘 ∈ ℕ0
∧ 𝐴 ∈ 𝑋) ∧ ((𝑘𝑆𝐴)𝑃𝐵) = (𝑘 · (𝐴𝑃𝐵))) → (((𝑘 + 1)𝑆𝐴)𝑃𝐵) = ((𝑘 + 1) · (𝐴𝑃𝐵))) |
40 | 39 | exp31 412 |
. . . 4
⊢ (𝑘 ∈ ℕ0
→ (𝐴 ∈ 𝑋 → (((𝑘𝑆𝐴)𝑃𝐵) = (𝑘 · (𝐴𝑃𝐵)) → (((𝑘 + 1)𝑆𝐴)𝑃𝐵) = ((𝑘 + 1) · (𝐴𝑃𝐵))))) |
41 | 40 | a2d 29 |
. . 3
⊢ (𝑘 ∈ ℕ0
→ ((𝐴 ∈ 𝑋 → ((𝑘𝑆𝐴)𝑃𝐵) = (𝑘 · (𝐴𝑃𝐵))) → (𝐴 ∈ 𝑋 → (((𝑘 + 1)𝑆𝐴)𝑃𝐵) = ((𝑘 + 1) · (𝐴𝑃𝐵))))) |
42 | | eqid 2777 |
. . . . . 6
⊢
(0vec‘𝑈) = (0vec‘𝑈) |
43 | 5, 42, 19 | dip0l 28145 |
. . . . 5
⊢ ((𝑈 ∈ NrmCVec ∧ 𝐵 ∈ 𝑋) → ((0vec‘𝑈)𝑃𝐵) = 0) |
44 | 4, 18, 43 | mp2an 682 |
. . . 4
⊢
((0vec‘𝑈)𝑃𝐵) = 0 |
45 | 5, 7, 42 | nv0 28064 |
. . . . . 6
⊢ ((𝑈 ∈ NrmCVec ∧ 𝐴 ∈ 𝑋) → (0𝑆𝐴) = (0vec‘𝑈)) |
46 | 4, 45 | mpan 680 |
. . . . 5
⊢ (𝐴 ∈ 𝑋 → (0𝑆𝐴) = (0vec‘𝑈)) |
47 | 46 | oveq1d 6937 |
. . . 4
⊢ (𝐴 ∈ 𝑋 → ((0𝑆𝐴)𝑃𝐵) = ((0vec‘𝑈)𝑃𝐵)) |
48 | 21 | mul02d 10574 |
. . . 4
⊢ (𝐴 ∈ 𝑋 → (0 · (𝐴𝑃𝐵)) = 0) |
49 | 44, 47, 48 | 3eqtr4a 2839 |
. . 3
⊢ (𝐴 ∈ 𝑋 → ((0𝑆𝐴)𝑃𝐵) = (0 · (𝐴𝑃𝐵))) |
50 | | oveq1 6929 |
. . . . . 6
⊢ (𝑗 = 0 → (𝑗𝑆𝐴) = (0𝑆𝐴)) |
51 | 50 | oveq1d 6937 |
. . . . 5
⊢ (𝑗 = 0 → ((𝑗𝑆𝐴)𝑃𝐵) = ((0𝑆𝐴)𝑃𝐵)) |
52 | | oveq1 6929 |
. . . . 5
⊢ (𝑗 = 0 → (𝑗 · (𝐴𝑃𝐵)) = (0 · (𝐴𝑃𝐵))) |
53 | 51, 52 | eqeq12d 2792 |
. . . 4
⊢ (𝑗 = 0 → (((𝑗𝑆𝐴)𝑃𝐵) = (𝑗 · (𝐴𝑃𝐵)) ↔ ((0𝑆𝐴)𝑃𝐵) = (0 · (𝐴𝑃𝐵)))) |
54 | 53 | imbi2d 332 |
. . 3
⊢ (𝑗 = 0 → ((𝐴 ∈ 𝑋 → ((𝑗𝑆𝐴)𝑃𝐵) = (𝑗 · (𝐴𝑃𝐵))) ↔ (𝐴 ∈ 𝑋 → ((0𝑆𝐴)𝑃𝐵) = (0 · (𝐴𝑃𝐵))))) |
55 | | oveq1 6929 |
. . . . . 6
⊢ (𝑗 = 𝑘 → (𝑗𝑆𝐴) = (𝑘𝑆𝐴)) |
56 | 55 | oveq1d 6937 |
. . . . 5
⊢ (𝑗 = 𝑘 → ((𝑗𝑆𝐴)𝑃𝐵) = ((𝑘𝑆𝐴)𝑃𝐵)) |
57 | | oveq1 6929 |
. . . . 5
⊢ (𝑗 = 𝑘 → (𝑗 · (𝐴𝑃𝐵)) = (𝑘 · (𝐴𝑃𝐵))) |
58 | 56, 57 | eqeq12d 2792 |
. . . 4
⊢ (𝑗 = 𝑘 → (((𝑗𝑆𝐴)𝑃𝐵) = (𝑗 · (𝐴𝑃𝐵)) ↔ ((𝑘𝑆𝐴)𝑃𝐵) = (𝑘 · (𝐴𝑃𝐵)))) |
59 | 58 | imbi2d 332 |
. . 3
⊢ (𝑗 = 𝑘 → ((𝐴 ∈ 𝑋 → ((𝑗𝑆𝐴)𝑃𝐵) = (𝑗 · (𝐴𝑃𝐵))) ↔ (𝐴 ∈ 𝑋 → ((𝑘𝑆𝐴)𝑃𝐵) = (𝑘 · (𝐴𝑃𝐵))))) |
60 | | oveq1 6929 |
. . . . . 6
⊢ (𝑗 = (𝑘 + 1) → (𝑗𝑆𝐴) = ((𝑘 + 1)𝑆𝐴)) |
61 | 60 | oveq1d 6937 |
. . . . 5
⊢ (𝑗 = (𝑘 + 1) → ((𝑗𝑆𝐴)𝑃𝐵) = (((𝑘 + 1)𝑆𝐴)𝑃𝐵)) |
62 | | oveq1 6929 |
. . . . 5
⊢ (𝑗 = (𝑘 + 1) → (𝑗 · (𝐴𝑃𝐵)) = ((𝑘 + 1) · (𝐴𝑃𝐵))) |
63 | 61, 62 | eqeq12d 2792 |
. . . 4
⊢ (𝑗 = (𝑘 + 1) → (((𝑗𝑆𝐴)𝑃𝐵) = (𝑗 · (𝐴𝑃𝐵)) ↔ (((𝑘 + 1)𝑆𝐴)𝑃𝐵) = ((𝑘 + 1) · (𝐴𝑃𝐵)))) |
64 | 63 | imbi2d 332 |
. . 3
⊢ (𝑗 = (𝑘 + 1) → ((𝐴 ∈ 𝑋 → ((𝑗𝑆𝐴)𝑃𝐵) = (𝑗 · (𝐴𝑃𝐵))) ↔ (𝐴 ∈ 𝑋 → (((𝑘 + 1)𝑆𝐴)𝑃𝐵) = ((𝑘 + 1) · (𝐴𝑃𝐵))))) |
65 | | oveq1 6929 |
. . . . . 6
⊢ (𝑗 = 𝑁 → (𝑗𝑆𝐴) = (𝑁𝑆𝐴)) |
66 | 65 | oveq1d 6937 |
. . . . 5
⊢ (𝑗 = 𝑁 → ((𝑗𝑆𝐴)𝑃𝐵) = ((𝑁𝑆𝐴)𝑃𝐵)) |
67 | | oveq1 6929 |
. . . . 5
⊢ (𝑗 = 𝑁 → (𝑗 · (𝐴𝑃𝐵)) = (𝑁 · (𝐴𝑃𝐵))) |
68 | 66, 67 | eqeq12d 2792 |
. . . 4
⊢ (𝑗 = 𝑁 → (((𝑗𝑆𝐴)𝑃𝐵) = (𝑗 · (𝐴𝑃𝐵)) ↔ ((𝑁𝑆𝐴)𝑃𝐵) = (𝑁 · (𝐴𝑃𝐵)))) |
69 | 68 | imbi2d 332 |
. . 3
⊢ (𝑗 = 𝑁 → ((𝐴 ∈ 𝑋 → ((𝑗𝑆𝐴)𝑃𝐵) = (𝑗 · (𝐴𝑃𝐵))) ↔ (𝐴 ∈ 𝑋 → ((𝑁𝑆𝐴)𝑃𝐵) = (𝑁 · (𝐴𝑃𝐵))))) |
70 | 41, 49, 54, 59, 64, 69 | nn0indALT 11825 |
. 2
⊢ (𝑁 ∈ ℕ0
→ (𝐴 ∈ 𝑋 → ((𝑁𝑆𝐴)𝑃𝐵) = (𝑁 · (𝐴𝑃𝐵)))) |
71 | 70 | imp 397 |
1
⊢ ((𝑁 ∈ ℕ0
∧ 𝐴 ∈ 𝑋) → ((𝑁𝑆𝐴)𝑃𝐵) = (𝑁 · (𝐴𝑃𝐵))) |