Step | Hyp | Ref
| Expression |
1 | | algrf.2 |
. 2
⊢ 𝑅 = seq𝑀((𝐹 ∘ 1st ), (𝑍 × {𝐴})) |
2 | | seqfn 13610 |
. . . 4
⊢ (𝑀 ∈ ℤ → seq𝑀((𝐹 ∘ 1st ), (𝑍 × {𝐴})) Fn (ℤ≥‘𝑀)) |
3 | 2 | adantr 484 |
. . 3
⊢ ((𝑀 ∈ ℤ ∧ 𝐴 ∈ 𝑉) → seq𝑀((𝐹 ∘ 1st ), (𝑍 × {𝐴})) Fn (ℤ≥‘𝑀)) |
4 | | seqfn 13610 |
. . . 4
⊢ (𝑀 ∈ ℤ → seq𝑀((𝐹 ∘ 1st ), {〈𝑀, 𝐴〉}) Fn
(ℤ≥‘𝑀)) |
5 | 4 | adantr 484 |
. . 3
⊢ ((𝑀 ∈ ℤ ∧ 𝐴 ∈ 𝑉) → seq𝑀((𝐹 ∘ 1st ), {〈𝑀, 𝐴〉}) Fn
(ℤ≥‘𝑀)) |
6 | | fveq2 6735 |
. . . . . . . 8
⊢ (𝑦 = 𝑀 → (seq𝑀((𝐹 ∘ 1st ), (𝑍 × {𝐴}))‘𝑦) = (seq𝑀((𝐹 ∘ 1st ), (𝑍 × {𝐴}))‘𝑀)) |
7 | | fveq2 6735 |
. . . . . . . 8
⊢ (𝑦 = 𝑀 → (seq𝑀((𝐹 ∘ 1st ), {〈𝑀, 𝐴〉})‘𝑦) = (seq𝑀((𝐹 ∘ 1st ), {〈𝑀, 𝐴〉})‘𝑀)) |
8 | 6, 7 | eqeq12d 2754 |
. . . . . . 7
⊢ (𝑦 = 𝑀 → ((seq𝑀((𝐹 ∘ 1st ), (𝑍 × {𝐴}))‘𝑦) = (seq𝑀((𝐹 ∘ 1st ), {〈𝑀, 𝐴〉})‘𝑦) ↔ (seq𝑀((𝐹 ∘ 1st ), (𝑍 × {𝐴}))‘𝑀) = (seq𝑀((𝐹 ∘ 1st ), {〈𝑀, 𝐴〉})‘𝑀))) |
9 | 8 | imbi2d 344 |
. . . . . 6
⊢ (𝑦 = 𝑀 → ((𝐴 ∈ 𝑉 → (seq𝑀((𝐹 ∘ 1st ), (𝑍 × {𝐴}))‘𝑦) = (seq𝑀((𝐹 ∘ 1st ), {〈𝑀, 𝐴〉})‘𝑦)) ↔ (𝐴 ∈ 𝑉 → (seq𝑀((𝐹 ∘ 1st ), (𝑍 × {𝐴}))‘𝑀) = (seq𝑀((𝐹 ∘ 1st ), {〈𝑀, 𝐴〉})‘𝑀)))) |
10 | | fveq2 6735 |
. . . . . . . 8
⊢ (𝑦 = 𝑥 → (seq𝑀((𝐹 ∘ 1st ), (𝑍 × {𝐴}))‘𝑦) = (seq𝑀((𝐹 ∘ 1st ), (𝑍 × {𝐴}))‘𝑥)) |
11 | | fveq2 6735 |
. . . . . . . 8
⊢ (𝑦 = 𝑥 → (seq𝑀((𝐹 ∘ 1st ), {〈𝑀, 𝐴〉})‘𝑦) = (seq𝑀((𝐹 ∘ 1st ), {〈𝑀, 𝐴〉})‘𝑥)) |
12 | 10, 11 | eqeq12d 2754 |
. . . . . . 7
⊢ (𝑦 = 𝑥 → ((seq𝑀((𝐹 ∘ 1st ), (𝑍 × {𝐴}))‘𝑦) = (seq𝑀((𝐹 ∘ 1st ), {〈𝑀, 𝐴〉})‘𝑦) ↔ (seq𝑀((𝐹 ∘ 1st ), (𝑍 × {𝐴}))‘𝑥) = (seq𝑀((𝐹 ∘ 1st ), {〈𝑀, 𝐴〉})‘𝑥))) |
13 | 12 | imbi2d 344 |
. . . . . 6
⊢ (𝑦 = 𝑥 → ((𝐴 ∈ 𝑉 → (seq𝑀((𝐹 ∘ 1st ), (𝑍 × {𝐴}))‘𝑦) = (seq𝑀((𝐹 ∘ 1st ), {〈𝑀, 𝐴〉})‘𝑦)) ↔ (𝐴 ∈ 𝑉 → (seq𝑀((𝐹 ∘ 1st ), (𝑍 × {𝐴}))‘𝑥) = (seq𝑀((𝐹 ∘ 1st ), {〈𝑀, 𝐴〉})‘𝑥)))) |
14 | | fveq2 6735 |
. . . . . . . 8
⊢ (𝑦 = (𝑥 + 1) → (seq𝑀((𝐹 ∘ 1st ), (𝑍 × {𝐴}))‘𝑦) = (seq𝑀((𝐹 ∘ 1st ), (𝑍 × {𝐴}))‘(𝑥 + 1))) |
15 | | fveq2 6735 |
. . . . . . . 8
⊢ (𝑦 = (𝑥 + 1) → (seq𝑀((𝐹 ∘ 1st ), {〈𝑀, 𝐴〉})‘𝑦) = (seq𝑀((𝐹 ∘ 1st ), {〈𝑀, 𝐴〉})‘(𝑥 + 1))) |
16 | 14, 15 | eqeq12d 2754 |
. . . . . . 7
⊢ (𝑦 = (𝑥 + 1) → ((seq𝑀((𝐹 ∘ 1st ), (𝑍 × {𝐴}))‘𝑦) = (seq𝑀((𝐹 ∘ 1st ), {〈𝑀, 𝐴〉})‘𝑦) ↔ (seq𝑀((𝐹 ∘ 1st ), (𝑍 × {𝐴}))‘(𝑥 + 1)) = (seq𝑀((𝐹 ∘ 1st ), {〈𝑀, 𝐴〉})‘(𝑥 + 1)))) |
17 | 16 | imbi2d 344 |
. . . . . 6
⊢ (𝑦 = (𝑥 + 1) → ((𝐴 ∈ 𝑉 → (seq𝑀((𝐹 ∘ 1st ), (𝑍 × {𝐴}))‘𝑦) = (seq𝑀((𝐹 ∘ 1st ), {〈𝑀, 𝐴〉})‘𝑦)) ↔ (𝐴 ∈ 𝑉 → (seq𝑀((𝐹 ∘ 1st ), (𝑍 × {𝐴}))‘(𝑥 + 1)) = (seq𝑀((𝐹 ∘ 1st ), {〈𝑀, 𝐴〉})‘(𝑥 + 1))))) |
18 | | seq1 13611 |
. . . . . . . . 9
⊢ (𝑀 ∈ ℤ → (seq𝑀((𝐹 ∘ 1st ), (𝑍 × {𝐴}))‘𝑀) = ((𝑍 × {𝐴})‘𝑀)) |
19 | 18 | adantr 484 |
. . . . . . . 8
⊢ ((𝑀 ∈ ℤ ∧ 𝐴 ∈ 𝑉) → (seq𝑀((𝐹 ∘ 1st ), (𝑍 × {𝐴}))‘𝑀) = ((𝑍 × {𝐴})‘𝑀)) |
20 | | seq1 13611 |
. . . . . . . . . 10
⊢ (𝑀 ∈ ℤ → (seq𝑀((𝐹 ∘ 1st ), {〈𝑀, 𝐴〉})‘𝑀) = ({〈𝑀, 𝐴〉}‘𝑀)) |
21 | 20 | adantr 484 |
. . . . . . . . 9
⊢ ((𝑀 ∈ ℤ ∧ 𝐴 ∈ 𝑉) → (seq𝑀((𝐹 ∘ 1st ), {〈𝑀, 𝐴〉})‘𝑀) = ({〈𝑀, 𝐴〉}‘𝑀)) |
22 | | id 22 |
. . . . . . . . . . 11
⊢ (𝐴 ∈ 𝑉 → 𝐴 ∈ 𝑉) |
23 | | uzid 12477 |
. . . . . . . . . . . 12
⊢ (𝑀 ∈ ℤ → 𝑀 ∈
(ℤ≥‘𝑀)) |
24 | | algrf.1 |
. . . . . . . . . . . 12
⊢ 𝑍 =
(ℤ≥‘𝑀) |
25 | 23, 24 | eleqtrrdi 2850 |
. . . . . . . . . . 11
⊢ (𝑀 ∈ ℤ → 𝑀 ∈ 𝑍) |
26 | | fvconst2g 7035 |
. . . . . . . . . . 11
⊢ ((𝐴 ∈ 𝑉 ∧ 𝑀 ∈ 𝑍) → ((𝑍 × {𝐴})‘𝑀) = 𝐴) |
27 | 22, 25, 26 | syl2anr 600 |
. . . . . . . . . 10
⊢ ((𝑀 ∈ ℤ ∧ 𝐴 ∈ 𝑉) → ((𝑍 × {𝐴})‘𝑀) = 𝐴) |
28 | | fvsng 7013 |
. . . . . . . . . 10
⊢ ((𝑀 ∈ ℤ ∧ 𝐴 ∈ 𝑉) → ({〈𝑀, 𝐴〉}‘𝑀) = 𝐴) |
29 | 27, 28 | eqtr4d 2781 |
. . . . . . . . 9
⊢ ((𝑀 ∈ ℤ ∧ 𝐴 ∈ 𝑉) → ((𝑍 × {𝐴})‘𝑀) = ({〈𝑀, 𝐴〉}‘𝑀)) |
30 | 21, 29 | eqtr4d 2781 |
. . . . . . . 8
⊢ ((𝑀 ∈ ℤ ∧ 𝐴 ∈ 𝑉) → (seq𝑀((𝐹 ∘ 1st ), {〈𝑀, 𝐴〉})‘𝑀) = ((𝑍 × {𝐴})‘𝑀)) |
31 | 19, 30 | eqtr4d 2781 |
. . . . . . 7
⊢ ((𝑀 ∈ ℤ ∧ 𝐴 ∈ 𝑉) → (seq𝑀((𝐹 ∘ 1st ), (𝑍 × {𝐴}))‘𝑀) = (seq𝑀((𝐹 ∘ 1st ), {〈𝑀, 𝐴〉})‘𝑀)) |
32 | 31 | ex 416 |
. . . . . 6
⊢ (𝑀 ∈ ℤ → (𝐴 ∈ 𝑉 → (seq𝑀((𝐹 ∘ 1st ), (𝑍 × {𝐴}))‘𝑀) = (seq𝑀((𝐹 ∘ 1st ), {〈𝑀, 𝐴〉})‘𝑀))) |
33 | | fveq2 6735 |
. . . . . . . . 9
⊢
((seq𝑀((𝐹 ∘ 1st ),
(𝑍 × {𝐴}))‘𝑥) = (seq𝑀((𝐹 ∘ 1st ), {〈𝑀, 𝐴〉})‘𝑥) → (𝐹‘(seq𝑀((𝐹 ∘ 1st ), (𝑍 × {𝐴}))‘𝑥)) = (𝐹‘(seq𝑀((𝐹 ∘ 1st ), {〈𝑀, 𝐴〉})‘𝑥))) |
34 | | seqp1 13613 |
. . . . . . . . . . . 12
⊢ (𝑥 ∈
(ℤ≥‘𝑀) → (seq𝑀((𝐹 ∘ 1st ), (𝑍 × {𝐴}))‘(𝑥 + 1)) = ((seq𝑀((𝐹 ∘ 1st ), (𝑍 × {𝐴}))‘𝑥)(𝐹 ∘ 1st )((𝑍 × {𝐴})‘(𝑥 + 1)))) |
35 | | fvex 6748 |
. . . . . . . . . . . . 13
⊢ (seq𝑀((𝐹 ∘ 1st ), (𝑍 × {𝐴}))‘𝑥) ∈ V |
36 | | fvex 6748 |
. . . . . . . . . . . . 13
⊢ ((𝑍 × {𝐴})‘(𝑥 + 1)) ∈ V |
37 | 35, 36 | opco1i 7912 |
. . . . . . . . . . . 12
⊢
((seq𝑀((𝐹 ∘ 1st ),
(𝑍 × {𝐴}))‘𝑥)(𝐹 ∘ 1st )((𝑍 × {𝐴})‘(𝑥 + 1))) = (𝐹‘(seq𝑀((𝐹 ∘ 1st ), (𝑍 × {𝐴}))‘𝑥)) |
38 | 34, 37 | eqtrdi 2795 |
. . . . . . . . . . 11
⊢ (𝑥 ∈
(ℤ≥‘𝑀) → (seq𝑀((𝐹 ∘ 1st ), (𝑍 × {𝐴}))‘(𝑥 + 1)) = (𝐹‘(seq𝑀((𝐹 ∘ 1st ), (𝑍 × {𝐴}))‘𝑥))) |
39 | | seqp1 13613 |
. . . . . . . . . . . 12
⊢ (𝑥 ∈
(ℤ≥‘𝑀) → (seq𝑀((𝐹 ∘ 1st ), {〈𝑀, 𝐴〉})‘(𝑥 + 1)) = ((seq𝑀((𝐹 ∘ 1st ), {〈𝑀, 𝐴〉})‘𝑥)(𝐹 ∘ 1st )({〈𝑀, 𝐴〉}‘(𝑥 + 1)))) |
40 | | fvex 6748 |
. . . . . . . . . . . . 13
⊢ (seq𝑀((𝐹 ∘ 1st ), {〈𝑀, 𝐴〉})‘𝑥) ∈ V |
41 | | fvex 6748 |
. . . . . . . . . . . . 13
⊢
({〈𝑀, 𝐴〉}‘(𝑥 + 1)) ∈ V |
42 | 40, 41 | opco1i 7912 |
. . . . . . . . . . . 12
⊢
((seq𝑀((𝐹 ∘ 1st ),
{〈𝑀, 𝐴〉})‘𝑥)(𝐹 ∘ 1st )({〈𝑀, 𝐴〉}‘(𝑥 + 1))) = (𝐹‘(seq𝑀((𝐹 ∘ 1st ), {〈𝑀, 𝐴〉})‘𝑥)) |
43 | 39, 42 | eqtrdi 2795 |
. . . . . . . . . . 11
⊢ (𝑥 ∈
(ℤ≥‘𝑀) → (seq𝑀((𝐹 ∘ 1st ), {〈𝑀, 𝐴〉})‘(𝑥 + 1)) = (𝐹‘(seq𝑀((𝐹 ∘ 1st ), {〈𝑀, 𝐴〉})‘𝑥))) |
44 | 38, 43 | eqeq12d 2754 |
. . . . . . . . . 10
⊢ (𝑥 ∈
(ℤ≥‘𝑀) → ((seq𝑀((𝐹 ∘ 1st ), (𝑍 × {𝐴}))‘(𝑥 + 1)) = (seq𝑀((𝐹 ∘ 1st ), {〈𝑀, 𝐴〉})‘(𝑥 + 1)) ↔ (𝐹‘(seq𝑀((𝐹 ∘ 1st ), (𝑍 × {𝐴}))‘𝑥)) = (𝐹‘(seq𝑀((𝐹 ∘ 1st ), {〈𝑀, 𝐴〉})‘𝑥)))) |
45 | 44 | adantl 485 |
. . . . . . . . 9
⊢ ((𝐴 ∈ 𝑉 ∧ 𝑥 ∈ (ℤ≥‘𝑀)) → ((seq𝑀((𝐹 ∘ 1st ), (𝑍 × {𝐴}))‘(𝑥 + 1)) = (seq𝑀((𝐹 ∘ 1st ), {〈𝑀, 𝐴〉})‘(𝑥 + 1)) ↔ (𝐹‘(seq𝑀((𝐹 ∘ 1st ), (𝑍 × {𝐴}))‘𝑥)) = (𝐹‘(seq𝑀((𝐹 ∘ 1st ), {〈𝑀, 𝐴〉})‘𝑥)))) |
46 | 33, 45 | syl5ibr 249 |
. . . . . . . 8
⊢ ((𝐴 ∈ 𝑉 ∧ 𝑥 ∈ (ℤ≥‘𝑀)) → ((seq𝑀((𝐹 ∘ 1st ), (𝑍 × {𝐴}))‘𝑥) = (seq𝑀((𝐹 ∘ 1st ), {〈𝑀, 𝐴〉})‘𝑥) → (seq𝑀((𝐹 ∘ 1st ), (𝑍 × {𝐴}))‘(𝑥 + 1)) = (seq𝑀((𝐹 ∘ 1st ), {〈𝑀, 𝐴〉})‘(𝑥 + 1)))) |
47 | 46 | expcom 417 |
. . . . . . 7
⊢ (𝑥 ∈
(ℤ≥‘𝑀) → (𝐴 ∈ 𝑉 → ((seq𝑀((𝐹 ∘ 1st ), (𝑍 × {𝐴}))‘𝑥) = (seq𝑀((𝐹 ∘ 1st ), {〈𝑀, 𝐴〉})‘𝑥) → (seq𝑀((𝐹 ∘ 1st ), (𝑍 × {𝐴}))‘(𝑥 + 1)) = (seq𝑀((𝐹 ∘ 1st ), {〈𝑀, 𝐴〉})‘(𝑥 + 1))))) |
48 | 47 | a2d 29 |
. . . . . 6
⊢ (𝑥 ∈
(ℤ≥‘𝑀) → ((𝐴 ∈ 𝑉 → (seq𝑀((𝐹 ∘ 1st ), (𝑍 × {𝐴}))‘𝑥) = (seq𝑀((𝐹 ∘ 1st ), {〈𝑀, 𝐴〉})‘𝑥)) → (𝐴 ∈ 𝑉 → (seq𝑀((𝐹 ∘ 1st ), (𝑍 × {𝐴}))‘(𝑥 + 1)) = (seq𝑀((𝐹 ∘ 1st ), {〈𝑀, 𝐴〉})‘(𝑥 + 1))))) |
49 | 9, 13, 17, 13, 32, 48 | uzind4 12526 |
. . . . 5
⊢ (𝑥 ∈
(ℤ≥‘𝑀) → (𝐴 ∈ 𝑉 → (seq𝑀((𝐹 ∘ 1st ), (𝑍 × {𝐴}))‘𝑥) = (seq𝑀((𝐹 ∘ 1st ), {〈𝑀, 𝐴〉})‘𝑥))) |
50 | 49 | impcom 411 |
. . . 4
⊢ ((𝐴 ∈ 𝑉 ∧ 𝑥 ∈ (ℤ≥‘𝑀)) → (seq𝑀((𝐹 ∘ 1st ), (𝑍 × {𝐴}))‘𝑥) = (seq𝑀((𝐹 ∘ 1st ), {〈𝑀, 𝐴〉})‘𝑥)) |
51 | 50 | adantll 714 |
. . 3
⊢ (((𝑀 ∈ ℤ ∧ 𝐴 ∈ 𝑉) ∧ 𝑥 ∈ (ℤ≥‘𝑀)) → (seq𝑀((𝐹 ∘ 1st ), (𝑍 × {𝐴}))‘𝑥) = (seq𝑀((𝐹 ∘ 1st ), {〈𝑀, 𝐴〉})‘𝑥)) |
52 | 3, 5, 51 | eqfnfvd 6873 |
. 2
⊢ ((𝑀 ∈ ℤ ∧ 𝐴 ∈ 𝑉) → seq𝑀((𝐹 ∘ 1st ), (𝑍 × {𝐴})) = seq𝑀((𝐹 ∘ 1st ), {〈𝑀, 𝐴〉})) |
53 | 1, 52 | eqtrid 2790 |
1
⊢ ((𝑀 ∈ ℤ ∧ 𝐴 ∈ 𝑉) → 𝑅 = seq𝑀((𝐹 ∘ 1st ), {〈𝑀, 𝐴〉})) |