Step | Hyp | Ref
| Expression |
1 | | algrf.2 |
. 2
⊢ 𝑅 = seq𝑀((𝐹 ∘ 1st ), (𝑍 × {𝐴})) |
2 | | seqfn 13978 |
. . . 4
⊢ (𝑀 ∈ ℤ → seq𝑀((𝐹 ∘ 1st ), (𝑍 × {𝐴})) Fn (ℤ≥‘𝑀)) |
3 | 2 | adantr 482 |
. . 3
⊢ ((𝑀 ∈ ℤ ∧ 𝐴 ∈ 𝑉) → seq𝑀((𝐹 ∘ 1st ), (𝑍 × {𝐴})) Fn (ℤ≥‘𝑀)) |
4 | | seqfn 13978 |
. . . 4
⊢ (𝑀 ∈ ℤ → seq𝑀((𝐹 ∘ 1st ), {⟨𝑀, 𝐴⟩}) Fn
(ℤ≥‘𝑀)) |
5 | 4 | adantr 482 |
. . 3
⊢ ((𝑀 ∈ ℤ ∧ 𝐴 ∈ 𝑉) → seq𝑀((𝐹 ∘ 1st ), {⟨𝑀, 𝐴⟩}) Fn
(ℤ≥‘𝑀)) |
6 | | fveq2 6892 |
. . . . . . . 8
⊢ (𝑦 = 𝑀 → (seq𝑀((𝐹 ∘ 1st ), (𝑍 × {𝐴}))‘𝑦) = (seq𝑀((𝐹 ∘ 1st ), (𝑍 × {𝐴}))‘𝑀)) |
7 | | fveq2 6892 |
. . . . . . . 8
⊢ (𝑦 = 𝑀 → (seq𝑀((𝐹 ∘ 1st ), {⟨𝑀, 𝐴⟩})‘𝑦) = (seq𝑀((𝐹 ∘ 1st ), {⟨𝑀, 𝐴⟩})‘𝑀)) |
8 | 6, 7 | eqeq12d 2749 |
. . . . . . 7
⊢ (𝑦 = 𝑀 → ((seq𝑀((𝐹 ∘ 1st ), (𝑍 × {𝐴}))‘𝑦) = (seq𝑀((𝐹 ∘ 1st ), {⟨𝑀, 𝐴⟩})‘𝑦) ↔ (seq𝑀((𝐹 ∘ 1st ), (𝑍 × {𝐴}))‘𝑀) = (seq𝑀((𝐹 ∘ 1st ), {⟨𝑀, 𝐴⟩})‘𝑀))) |
9 | 8 | imbi2d 341 |
. . . . . 6
⊢ (𝑦 = 𝑀 → ((𝐴 ∈ 𝑉 → (seq𝑀((𝐹 ∘ 1st ), (𝑍 × {𝐴}))‘𝑦) = (seq𝑀((𝐹 ∘ 1st ), {⟨𝑀, 𝐴⟩})‘𝑦)) ↔ (𝐴 ∈ 𝑉 → (seq𝑀((𝐹 ∘ 1st ), (𝑍 × {𝐴}))‘𝑀) = (seq𝑀((𝐹 ∘ 1st ), {⟨𝑀, 𝐴⟩})‘𝑀)))) |
10 | | fveq2 6892 |
. . . . . . . 8
⊢ (𝑦 = 𝑥 → (seq𝑀((𝐹 ∘ 1st ), (𝑍 × {𝐴}))‘𝑦) = (seq𝑀((𝐹 ∘ 1st ), (𝑍 × {𝐴}))‘𝑥)) |
11 | | fveq2 6892 |
. . . . . . . 8
⊢ (𝑦 = 𝑥 → (seq𝑀((𝐹 ∘ 1st ), {⟨𝑀, 𝐴⟩})‘𝑦) = (seq𝑀((𝐹 ∘ 1st ), {⟨𝑀, 𝐴⟩})‘𝑥)) |
12 | 10, 11 | eqeq12d 2749 |
. . . . . . 7
⊢ (𝑦 = 𝑥 → ((seq𝑀((𝐹 ∘ 1st ), (𝑍 × {𝐴}))‘𝑦) = (seq𝑀((𝐹 ∘ 1st ), {⟨𝑀, 𝐴⟩})‘𝑦) ↔ (seq𝑀((𝐹 ∘ 1st ), (𝑍 × {𝐴}))‘𝑥) = (seq𝑀((𝐹 ∘ 1st ), {⟨𝑀, 𝐴⟩})‘𝑥))) |
13 | 12 | imbi2d 341 |
. . . . . 6
⊢ (𝑦 = 𝑥 → ((𝐴 ∈ 𝑉 → (seq𝑀((𝐹 ∘ 1st ), (𝑍 × {𝐴}))‘𝑦) = (seq𝑀((𝐹 ∘ 1st ), {⟨𝑀, 𝐴⟩})‘𝑦)) ↔ (𝐴 ∈ 𝑉 → (seq𝑀((𝐹 ∘ 1st ), (𝑍 × {𝐴}))‘𝑥) = (seq𝑀((𝐹 ∘ 1st ), {⟨𝑀, 𝐴⟩})‘𝑥)))) |
14 | | fveq2 6892 |
. . . . . . . 8
⊢ (𝑦 = (𝑥 + 1) → (seq𝑀((𝐹 ∘ 1st ), (𝑍 × {𝐴}))‘𝑦) = (seq𝑀((𝐹 ∘ 1st ), (𝑍 × {𝐴}))‘(𝑥 + 1))) |
15 | | fveq2 6892 |
. . . . . . . 8
⊢ (𝑦 = (𝑥 + 1) → (seq𝑀((𝐹 ∘ 1st ), {⟨𝑀, 𝐴⟩})‘𝑦) = (seq𝑀((𝐹 ∘ 1st ), {⟨𝑀, 𝐴⟩})‘(𝑥 + 1))) |
16 | 14, 15 | eqeq12d 2749 |
. . . . . . 7
⊢ (𝑦 = (𝑥 + 1) → ((seq𝑀((𝐹 ∘ 1st ), (𝑍 × {𝐴}))‘𝑦) = (seq𝑀((𝐹 ∘ 1st ), {⟨𝑀, 𝐴⟩})‘𝑦) ↔ (seq𝑀((𝐹 ∘ 1st ), (𝑍 × {𝐴}))‘(𝑥 + 1)) = (seq𝑀((𝐹 ∘ 1st ), {⟨𝑀, 𝐴⟩})‘(𝑥 + 1)))) |
17 | 16 | imbi2d 341 |
. . . . . 6
⊢ (𝑦 = (𝑥 + 1) → ((𝐴 ∈ 𝑉 → (seq𝑀((𝐹 ∘ 1st ), (𝑍 × {𝐴}))‘𝑦) = (seq𝑀((𝐹 ∘ 1st ), {⟨𝑀, 𝐴⟩})‘𝑦)) ↔ (𝐴 ∈ 𝑉 → (seq𝑀((𝐹 ∘ 1st ), (𝑍 × {𝐴}))‘(𝑥 + 1)) = (seq𝑀((𝐹 ∘ 1st ), {⟨𝑀, 𝐴⟩})‘(𝑥 + 1))))) |
18 | | seq1 13979 |
. . . . . . . . 9
⊢ (𝑀 ∈ ℤ → (seq𝑀((𝐹 ∘ 1st ), (𝑍 × {𝐴}))‘𝑀) = ((𝑍 × {𝐴})‘𝑀)) |
19 | 18 | adantr 482 |
. . . . . . . 8
⊢ ((𝑀 ∈ ℤ ∧ 𝐴 ∈ 𝑉) → (seq𝑀((𝐹 ∘ 1st ), (𝑍 × {𝐴}))‘𝑀) = ((𝑍 × {𝐴})‘𝑀)) |
20 | | seq1 13979 |
. . . . . . . . . 10
⊢ (𝑀 ∈ ℤ → (seq𝑀((𝐹 ∘ 1st ), {⟨𝑀, 𝐴⟩})‘𝑀) = ({⟨𝑀, 𝐴⟩}‘𝑀)) |
21 | 20 | adantr 482 |
. . . . . . . . 9
⊢ ((𝑀 ∈ ℤ ∧ 𝐴 ∈ 𝑉) → (seq𝑀((𝐹 ∘ 1st ), {⟨𝑀, 𝐴⟩})‘𝑀) = ({⟨𝑀, 𝐴⟩}‘𝑀)) |
22 | | id 22 |
. . . . . . . . . . 11
⊢ (𝐴 ∈ 𝑉 → 𝐴 ∈ 𝑉) |
23 | | uzid 12837 |
. . . . . . . . . . . 12
⊢ (𝑀 ∈ ℤ → 𝑀 ∈
(ℤ≥‘𝑀)) |
24 | | algrf.1 |
. . . . . . . . . . . 12
⊢ 𝑍 =
(ℤ≥‘𝑀) |
25 | 23, 24 | eleqtrrdi 2845 |
. . . . . . . . . . 11
⊢ (𝑀 ∈ ℤ → 𝑀 ∈ 𝑍) |
26 | | fvconst2g 7203 |
. . . . . . . . . . 11
⊢ ((𝐴 ∈ 𝑉 ∧ 𝑀 ∈ 𝑍) → ((𝑍 × {𝐴})‘𝑀) = 𝐴) |
27 | 22, 25, 26 | syl2anr 598 |
. . . . . . . . . 10
⊢ ((𝑀 ∈ ℤ ∧ 𝐴 ∈ 𝑉) → ((𝑍 × {𝐴})‘𝑀) = 𝐴) |
28 | | fvsng 7178 |
. . . . . . . . . 10
⊢ ((𝑀 ∈ ℤ ∧ 𝐴 ∈ 𝑉) → ({⟨𝑀, 𝐴⟩}‘𝑀) = 𝐴) |
29 | 27, 28 | eqtr4d 2776 |
. . . . . . . . 9
⊢ ((𝑀 ∈ ℤ ∧ 𝐴 ∈ 𝑉) → ((𝑍 × {𝐴})‘𝑀) = ({⟨𝑀, 𝐴⟩}‘𝑀)) |
30 | 21, 29 | eqtr4d 2776 |
. . . . . . . 8
⊢ ((𝑀 ∈ ℤ ∧ 𝐴 ∈ 𝑉) → (seq𝑀((𝐹 ∘ 1st ), {⟨𝑀, 𝐴⟩})‘𝑀) = ((𝑍 × {𝐴})‘𝑀)) |
31 | 19, 30 | eqtr4d 2776 |
. . . . . . 7
⊢ ((𝑀 ∈ ℤ ∧ 𝐴 ∈ 𝑉) → (seq𝑀((𝐹 ∘ 1st ), (𝑍 × {𝐴}))‘𝑀) = (seq𝑀((𝐹 ∘ 1st ), {⟨𝑀, 𝐴⟩})‘𝑀)) |
32 | 31 | ex 414 |
. . . . . 6
⊢ (𝑀 ∈ ℤ → (𝐴 ∈ 𝑉 → (seq𝑀((𝐹 ∘ 1st ), (𝑍 × {𝐴}))‘𝑀) = (seq𝑀((𝐹 ∘ 1st ), {⟨𝑀, 𝐴⟩})‘𝑀))) |
33 | | fveq2 6892 |
. . . . . . . . 9
⊢
((seq𝑀((𝐹 ∘ 1st ),
(𝑍 × {𝐴}))‘𝑥) = (seq𝑀((𝐹 ∘ 1st ), {⟨𝑀, 𝐴⟩})‘𝑥) → (𝐹‘(seq𝑀((𝐹 ∘ 1st ), (𝑍 × {𝐴}))‘𝑥)) = (𝐹‘(seq𝑀((𝐹 ∘ 1st ), {⟨𝑀, 𝐴⟩})‘𝑥))) |
34 | | seqp1 13981 |
. . . . . . . . . . . 12
⊢ (𝑥 ∈
(ℤ≥‘𝑀) → (seq𝑀((𝐹 ∘ 1st ), (𝑍 × {𝐴}))‘(𝑥 + 1)) = ((seq𝑀((𝐹 ∘ 1st ), (𝑍 × {𝐴}))‘𝑥)(𝐹 ∘ 1st )((𝑍 × {𝐴})‘(𝑥 + 1)))) |
35 | | fvex 6905 |
. . . . . . . . . . . . 13
⊢ (seq𝑀((𝐹 ∘ 1st ), (𝑍 × {𝐴}))‘𝑥) ∈ V |
36 | | fvex 6905 |
. . . . . . . . . . . . 13
⊢ ((𝑍 × {𝐴})‘(𝑥 + 1)) ∈ V |
37 | 35, 36 | opco1i 8111 |
. . . . . . . . . . . 12
⊢
((seq𝑀((𝐹 ∘ 1st ),
(𝑍 × {𝐴}))‘𝑥)(𝐹 ∘ 1st )((𝑍 × {𝐴})‘(𝑥 + 1))) = (𝐹‘(seq𝑀((𝐹 ∘ 1st ), (𝑍 × {𝐴}))‘𝑥)) |
38 | 34, 37 | eqtrdi 2789 |
. . . . . . . . . . 11
⊢ (𝑥 ∈
(ℤ≥‘𝑀) → (seq𝑀((𝐹 ∘ 1st ), (𝑍 × {𝐴}))‘(𝑥 + 1)) = (𝐹‘(seq𝑀((𝐹 ∘ 1st ), (𝑍 × {𝐴}))‘𝑥))) |
39 | | seqp1 13981 |
. . . . . . . . . . . 12
⊢ (𝑥 ∈
(ℤ≥‘𝑀) → (seq𝑀((𝐹 ∘ 1st ), {⟨𝑀, 𝐴⟩})‘(𝑥 + 1)) = ((seq𝑀((𝐹 ∘ 1st ), {⟨𝑀, 𝐴⟩})‘𝑥)(𝐹 ∘ 1st )({⟨𝑀, 𝐴⟩}‘(𝑥 + 1)))) |
40 | | fvex 6905 |
. . . . . . . . . . . . 13
⊢ (seq𝑀((𝐹 ∘ 1st ), {⟨𝑀, 𝐴⟩})‘𝑥) ∈ V |
41 | | fvex 6905 |
. . . . . . . . . . . . 13
⊢
({⟨𝑀, 𝐴⟩}‘(𝑥 + 1)) ∈ V |
42 | 40, 41 | opco1i 8111 |
. . . . . . . . . . . 12
⊢
((seq𝑀((𝐹 ∘ 1st ),
{⟨𝑀, 𝐴⟩})‘𝑥)(𝐹 ∘ 1st )({⟨𝑀, 𝐴⟩}‘(𝑥 + 1))) = (𝐹‘(seq𝑀((𝐹 ∘ 1st ), {⟨𝑀, 𝐴⟩})‘𝑥)) |
43 | 39, 42 | eqtrdi 2789 |
. . . . . . . . . . 11
⊢ (𝑥 ∈
(ℤ≥‘𝑀) → (seq𝑀((𝐹 ∘ 1st ), {⟨𝑀, 𝐴⟩})‘(𝑥 + 1)) = (𝐹‘(seq𝑀((𝐹 ∘ 1st ), {⟨𝑀, 𝐴⟩})‘𝑥))) |
44 | 38, 43 | eqeq12d 2749 |
. . . . . . . . . 10
⊢ (𝑥 ∈
(ℤ≥‘𝑀) → ((seq𝑀((𝐹 ∘ 1st ), (𝑍 × {𝐴}))‘(𝑥 + 1)) = (seq𝑀((𝐹 ∘ 1st ), {⟨𝑀, 𝐴⟩})‘(𝑥 + 1)) ↔ (𝐹‘(seq𝑀((𝐹 ∘ 1st ), (𝑍 × {𝐴}))‘𝑥)) = (𝐹‘(seq𝑀((𝐹 ∘ 1st ), {⟨𝑀, 𝐴⟩})‘𝑥)))) |
45 | 44 | adantl 483 |
. . . . . . . . 9
⊢ ((𝐴 ∈ 𝑉 ∧ 𝑥 ∈ (ℤ≥‘𝑀)) → ((seq𝑀((𝐹 ∘ 1st ), (𝑍 × {𝐴}))‘(𝑥 + 1)) = (seq𝑀((𝐹 ∘ 1st ), {⟨𝑀, 𝐴⟩})‘(𝑥 + 1)) ↔ (𝐹‘(seq𝑀((𝐹 ∘ 1st ), (𝑍 × {𝐴}))‘𝑥)) = (𝐹‘(seq𝑀((𝐹 ∘ 1st ), {⟨𝑀, 𝐴⟩})‘𝑥)))) |
46 | 33, 45 | imbitrrid 245 |
. . . . . . . 8
⊢ ((𝐴 ∈ 𝑉 ∧ 𝑥 ∈ (ℤ≥‘𝑀)) → ((seq𝑀((𝐹 ∘ 1st ), (𝑍 × {𝐴}))‘𝑥) = (seq𝑀((𝐹 ∘ 1st ), {⟨𝑀, 𝐴⟩})‘𝑥) → (seq𝑀((𝐹 ∘ 1st ), (𝑍 × {𝐴}))‘(𝑥 + 1)) = (seq𝑀((𝐹 ∘ 1st ), {⟨𝑀, 𝐴⟩})‘(𝑥 + 1)))) |
47 | 46 | expcom 415 |
. . . . . . 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 12890 |
. . . . 5
⊢ (𝑥 ∈
(ℤ≥‘𝑀) → (𝐴 ∈ 𝑉 → (seq𝑀((𝐹 ∘ 1st ), (𝑍 × {𝐴}))‘𝑥) = (seq𝑀((𝐹 ∘ 1st ), {⟨𝑀, 𝐴⟩})‘𝑥))) |
50 | 49 | impcom 409 |
. . . 4
⊢ ((𝐴 ∈ 𝑉 ∧ 𝑥 ∈ (ℤ≥‘𝑀)) → (seq𝑀((𝐹 ∘ 1st ), (𝑍 × {𝐴}))‘𝑥) = (seq𝑀((𝐹 ∘ 1st ), {⟨𝑀, 𝐴⟩})‘𝑥)) |
51 | 50 | adantll 713 |
. . 3
⊢ (((𝑀 ∈ ℤ ∧ 𝐴 ∈ 𝑉) ∧ 𝑥 ∈ (ℤ≥‘𝑀)) → (seq𝑀((𝐹 ∘ 1st ), (𝑍 × {𝐴}))‘𝑥) = (seq𝑀((𝐹 ∘ 1st ), {⟨𝑀, 𝐴⟩})‘𝑥)) |
52 | 3, 5, 51 | eqfnfvd 7036 |
. 2
⊢ ((𝑀 ∈ ℤ ∧ 𝐴 ∈ 𝑉) → seq𝑀((𝐹 ∘ 1st ), (𝑍 × {𝐴})) = seq𝑀((𝐹 ∘ 1st ), {⟨𝑀, 𝐴⟩})) |
53 | 1, 52 | eqtrid 2785 |
1
⊢ ((𝑀 ∈ ℤ ∧ 𝐴 ∈ 𝑉) → 𝑅 = seq𝑀((𝐹 ∘ 1st ), {⟨𝑀, 𝐴⟩})) |