| Step | Hyp | Ref
| Expression |
| 1 | | algrf.2 |
. 2
⊢ 𝑅 = seq𝑀((𝐹 ∘ 1st ), (𝑍 × {𝐴})) |
| 2 | | seqfn 14054 |
. . . 4
⊢ (𝑀 ∈ ℤ → seq𝑀((𝐹 ∘ 1st ), (𝑍 × {𝐴})) Fn (ℤ≥‘𝑀)) |
| 3 | 2 | adantr 480 |
. . 3
⊢ ((𝑀 ∈ ℤ ∧ 𝐴 ∈ 𝑉) → seq𝑀((𝐹 ∘ 1st ), (𝑍 × {𝐴})) Fn (ℤ≥‘𝑀)) |
| 4 | | seqfn 14054 |
. . . 4
⊢ (𝑀 ∈ ℤ → seq𝑀((𝐹 ∘ 1st ), {〈𝑀, 𝐴〉}) Fn
(ℤ≥‘𝑀)) |
| 5 | 4 | adantr 480 |
. . 3
⊢ ((𝑀 ∈ ℤ ∧ 𝐴 ∈ 𝑉) → seq𝑀((𝐹 ∘ 1st ), {〈𝑀, 𝐴〉}) Fn
(ℤ≥‘𝑀)) |
| 6 | | fveq2 6906 |
. . . . . . . 8
⊢ (𝑦 = 𝑀 → (seq𝑀((𝐹 ∘ 1st ), (𝑍 × {𝐴}))‘𝑦) = (seq𝑀((𝐹 ∘ 1st ), (𝑍 × {𝐴}))‘𝑀)) |
| 7 | | fveq2 6906 |
. . . . . . . 8
⊢ (𝑦 = 𝑀 → (seq𝑀((𝐹 ∘ 1st ), {〈𝑀, 𝐴〉})‘𝑦) = (seq𝑀((𝐹 ∘ 1st ), {〈𝑀, 𝐴〉})‘𝑀)) |
| 8 | 6, 7 | eqeq12d 2753 |
. . . . . . 7
⊢ (𝑦 = 𝑀 → ((seq𝑀((𝐹 ∘ 1st ), (𝑍 × {𝐴}))‘𝑦) = (seq𝑀((𝐹 ∘ 1st ), {〈𝑀, 𝐴〉})‘𝑦) ↔ (seq𝑀((𝐹 ∘ 1st ), (𝑍 × {𝐴}))‘𝑀) = (seq𝑀((𝐹 ∘ 1st ), {〈𝑀, 𝐴〉})‘𝑀))) |
| 9 | 8 | imbi2d 340 |
. . . . . 6
⊢ (𝑦 = 𝑀 → ((𝐴 ∈ 𝑉 → (seq𝑀((𝐹 ∘ 1st ), (𝑍 × {𝐴}))‘𝑦) = (seq𝑀((𝐹 ∘ 1st ), {〈𝑀, 𝐴〉})‘𝑦)) ↔ (𝐴 ∈ 𝑉 → (seq𝑀((𝐹 ∘ 1st ), (𝑍 × {𝐴}))‘𝑀) = (seq𝑀((𝐹 ∘ 1st ), {〈𝑀, 𝐴〉})‘𝑀)))) |
| 10 | | fveq2 6906 |
. . . . . . . 8
⊢ (𝑦 = 𝑥 → (seq𝑀((𝐹 ∘ 1st ), (𝑍 × {𝐴}))‘𝑦) = (seq𝑀((𝐹 ∘ 1st ), (𝑍 × {𝐴}))‘𝑥)) |
| 11 | | fveq2 6906 |
. . . . . . . 8
⊢ (𝑦 = 𝑥 → (seq𝑀((𝐹 ∘ 1st ), {〈𝑀, 𝐴〉})‘𝑦) = (seq𝑀((𝐹 ∘ 1st ), {〈𝑀, 𝐴〉})‘𝑥)) |
| 12 | 10, 11 | eqeq12d 2753 |
. . . . . . 7
⊢ (𝑦 = 𝑥 → ((seq𝑀((𝐹 ∘ 1st ), (𝑍 × {𝐴}))‘𝑦) = (seq𝑀((𝐹 ∘ 1st ), {〈𝑀, 𝐴〉})‘𝑦) ↔ (seq𝑀((𝐹 ∘ 1st ), (𝑍 × {𝐴}))‘𝑥) = (seq𝑀((𝐹 ∘ 1st ), {〈𝑀, 𝐴〉})‘𝑥))) |
| 13 | 12 | imbi2d 340 |
. . . . . 6
⊢ (𝑦 = 𝑥 → ((𝐴 ∈ 𝑉 → (seq𝑀((𝐹 ∘ 1st ), (𝑍 × {𝐴}))‘𝑦) = (seq𝑀((𝐹 ∘ 1st ), {〈𝑀, 𝐴〉})‘𝑦)) ↔ (𝐴 ∈ 𝑉 → (seq𝑀((𝐹 ∘ 1st ), (𝑍 × {𝐴}))‘𝑥) = (seq𝑀((𝐹 ∘ 1st ), {〈𝑀, 𝐴〉})‘𝑥)))) |
| 14 | | fveq2 6906 |
. . . . . . . 8
⊢ (𝑦 = (𝑥 + 1) → (seq𝑀((𝐹 ∘ 1st ), (𝑍 × {𝐴}))‘𝑦) = (seq𝑀((𝐹 ∘ 1st ), (𝑍 × {𝐴}))‘(𝑥 + 1))) |
| 15 | | fveq2 6906 |
. . . . . . . 8
⊢ (𝑦 = (𝑥 + 1) → (seq𝑀((𝐹 ∘ 1st ), {〈𝑀, 𝐴〉})‘𝑦) = (seq𝑀((𝐹 ∘ 1st ), {〈𝑀, 𝐴〉})‘(𝑥 + 1))) |
| 16 | 14, 15 | eqeq12d 2753 |
. . . . . . 7
⊢ (𝑦 = (𝑥 + 1) → ((seq𝑀((𝐹 ∘ 1st ), (𝑍 × {𝐴}))‘𝑦) = (seq𝑀((𝐹 ∘ 1st ), {〈𝑀, 𝐴〉})‘𝑦) ↔ (seq𝑀((𝐹 ∘ 1st ), (𝑍 × {𝐴}))‘(𝑥 + 1)) = (seq𝑀((𝐹 ∘ 1st ), {〈𝑀, 𝐴〉})‘(𝑥 + 1)))) |
| 17 | 16 | imbi2d 340 |
. . . . . 6
⊢ (𝑦 = (𝑥 + 1) → ((𝐴 ∈ 𝑉 → (seq𝑀((𝐹 ∘ 1st ), (𝑍 × {𝐴}))‘𝑦) = (seq𝑀((𝐹 ∘ 1st ), {〈𝑀, 𝐴〉})‘𝑦)) ↔ (𝐴 ∈ 𝑉 → (seq𝑀((𝐹 ∘ 1st ), (𝑍 × {𝐴}))‘(𝑥 + 1)) = (seq𝑀((𝐹 ∘ 1st ), {〈𝑀, 𝐴〉})‘(𝑥 + 1))))) |
| 18 | | seq1 14055 |
. . . . . . . . 9
⊢ (𝑀 ∈ ℤ → (seq𝑀((𝐹 ∘ 1st ), (𝑍 × {𝐴}))‘𝑀) = ((𝑍 × {𝐴})‘𝑀)) |
| 19 | 18 | adantr 480 |
. . . . . . . 8
⊢ ((𝑀 ∈ ℤ ∧ 𝐴 ∈ 𝑉) → (seq𝑀((𝐹 ∘ 1st ), (𝑍 × {𝐴}))‘𝑀) = ((𝑍 × {𝐴})‘𝑀)) |
| 20 | | seq1 14055 |
. . . . . . . . . 10
⊢ (𝑀 ∈ ℤ → (seq𝑀((𝐹 ∘ 1st ), {〈𝑀, 𝐴〉})‘𝑀) = ({〈𝑀, 𝐴〉}‘𝑀)) |
| 21 | 20 | adantr 480 |
. . . . . . . . 9
⊢ ((𝑀 ∈ ℤ ∧ 𝐴 ∈ 𝑉) → (seq𝑀((𝐹 ∘ 1st ), {〈𝑀, 𝐴〉})‘𝑀) = ({〈𝑀, 𝐴〉}‘𝑀)) |
| 22 | | id 22 |
. . . . . . . . . . 11
⊢ (𝐴 ∈ 𝑉 → 𝐴 ∈ 𝑉) |
| 23 | | uzid 12893 |
. . . . . . . . . . . 12
⊢ (𝑀 ∈ ℤ → 𝑀 ∈
(ℤ≥‘𝑀)) |
| 24 | | algrf.1 |
. . . . . . . . . . . 12
⊢ 𝑍 =
(ℤ≥‘𝑀) |
| 25 | 23, 24 | eleqtrrdi 2852 |
. . . . . . . . . . 11
⊢ (𝑀 ∈ ℤ → 𝑀 ∈ 𝑍) |
| 26 | | fvconst2g 7222 |
. . . . . . . . . . 11
⊢ ((𝐴 ∈ 𝑉 ∧ 𝑀 ∈ 𝑍) → ((𝑍 × {𝐴})‘𝑀) = 𝐴) |
| 27 | 22, 25, 26 | syl2anr 597 |
. . . . . . . . . 10
⊢ ((𝑀 ∈ ℤ ∧ 𝐴 ∈ 𝑉) → ((𝑍 × {𝐴})‘𝑀) = 𝐴) |
| 28 | | fvsng 7200 |
. . . . . . . . . 10
⊢ ((𝑀 ∈ ℤ ∧ 𝐴 ∈ 𝑉) → ({〈𝑀, 𝐴〉}‘𝑀) = 𝐴) |
| 29 | 27, 28 | eqtr4d 2780 |
. . . . . . . . 9
⊢ ((𝑀 ∈ ℤ ∧ 𝐴 ∈ 𝑉) → ((𝑍 × {𝐴})‘𝑀) = ({〈𝑀, 𝐴〉}‘𝑀)) |
| 30 | 21, 29 | eqtr4d 2780 |
. . . . . . . 8
⊢ ((𝑀 ∈ ℤ ∧ 𝐴 ∈ 𝑉) → (seq𝑀((𝐹 ∘ 1st ), {〈𝑀, 𝐴〉})‘𝑀) = ((𝑍 × {𝐴})‘𝑀)) |
| 31 | 19, 30 | eqtr4d 2780 |
. . . . . . 7
⊢ ((𝑀 ∈ ℤ ∧ 𝐴 ∈ 𝑉) → (seq𝑀((𝐹 ∘ 1st ), (𝑍 × {𝐴}))‘𝑀) = (seq𝑀((𝐹 ∘ 1st ), {〈𝑀, 𝐴〉})‘𝑀)) |
| 32 | 31 | ex 412 |
. . . . . 6
⊢ (𝑀 ∈ ℤ → (𝐴 ∈ 𝑉 → (seq𝑀((𝐹 ∘ 1st ), (𝑍 × {𝐴}))‘𝑀) = (seq𝑀((𝐹 ∘ 1st ), {〈𝑀, 𝐴〉})‘𝑀))) |
| 33 | | fveq2 6906 |
. . . . . . . . 9
⊢
((seq𝑀((𝐹 ∘ 1st ),
(𝑍 × {𝐴}))‘𝑥) = (seq𝑀((𝐹 ∘ 1st ), {〈𝑀, 𝐴〉})‘𝑥) → (𝐹‘(seq𝑀((𝐹 ∘ 1st ), (𝑍 × {𝐴}))‘𝑥)) = (𝐹‘(seq𝑀((𝐹 ∘ 1st ), {〈𝑀, 𝐴〉})‘𝑥))) |
| 34 | | seqp1 14057 |
. . . . . . . . . . . 12
⊢ (𝑥 ∈
(ℤ≥‘𝑀) → (seq𝑀((𝐹 ∘ 1st ), (𝑍 × {𝐴}))‘(𝑥 + 1)) = ((seq𝑀((𝐹 ∘ 1st ), (𝑍 × {𝐴}))‘𝑥)(𝐹 ∘ 1st )((𝑍 × {𝐴})‘(𝑥 + 1)))) |
| 35 | | fvex 6919 |
. . . . . . . . . . . . 13
⊢ (seq𝑀((𝐹 ∘ 1st ), (𝑍 × {𝐴}))‘𝑥) ∈ V |
| 36 | | fvex 6919 |
. . . . . . . . . . . . 13
⊢ ((𝑍 × {𝐴})‘(𝑥 + 1)) ∈ V |
| 37 | 35, 36 | opco1i 8150 |
. . . . . . . . . . . 12
⊢
((seq𝑀((𝐹 ∘ 1st ),
(𝑍 × {𝐴}))‘𝑥)(𝐹 ∘ 1st )((𝑍 × {𝐴})‘(𝑥 + 1))) = (𝐹‘(seq𝑀((𝐹 ∘ 1st ), (𝑍 × {𝐴}))‘𝑥)) |
| 38 | 34, 37 | eqtrdi 2793 |
. . . . . . . . . . 11
⊢ (𝑥 ∈
(ℤ≥‘𝑀) → (seq𝑀((𝐹 ∘ 1st ), (𝑍 × {𝐴}))‘(𝑥 + 1)) = (𝐹‘(seq𝑀((𝐹 ∘ 1st ), (𝑍 × {𝐴}))‘𝑥))) |
| 39 | | seqp1 14057 |
. . . . . . . . . . . 12
⊢ (𝑥 ∈
(ℤ≥‘𝑀) → (seq𝑀((𝐹 ∘ 1st ), {〈𝑀, 𝐴〉})‘(𝑥 + 1)) = ((seq𝑀((𝐹 ∘ 1st ), {〈𝑀, 𝐴〉})‘𝑥)(𝐹 ∘ 1st )({〈𝑀, 𝐴〉}‘(𝑥 + 1)))) |
| 40 | | fvex 6919 |
. . . . . . . . . . . . 13
⊢ (seq𝑀((𝐹 ∘ 1st ), {〈𝑀, 𝐴〉})‘𝑥) ∈ V |
| 41 | | fvex 6919 |
. . . . . . . . . . . . 13
⊢
({〈𝑀, 𝐴〉}‘(𝑥 + 1)) ∈ V |
| 42 | 40, 41 | opco1i 8150 |
. . . . . . . . . . . 12
⊢
((seq𝑀((𝐹 ∘ 1st ),
{〈𝑀, 𝐴〉})‘𝑥)(𝐹 ∘ 1st )({〈𝑀, 𝐴〉}‘(𝑥 + 1))) = (𝐹‘(seq𝑀((𝐹 ∘ 1st ), {〈𝑀, 𝐴〉})‘𝑥)) |
| 43 | 39, 42 | eqtrdi 2793 |
. . . . . . . . . . 11
⊢ (𝑥 ∈
(ℤ≥‘𝑀) → (seq𝑀((𝐹 ∘ 1st ), {〈𝑀, 𝐴〉})‘(𝑥 + 1)) = (𝐹‘(seq𝑀((𝐹 ∘ 1st ), {〈𝑀, 𝐴〉})‘𝑥))) |
| 44 | 38, 43 | eqeq12d 2753 |
. . . . . . . . . 10
⊢ (𝑥 ∈
(ℤ≥‘𝑀) → ((seq𝑀((𝐹 ∘ 1st ), (𝑍 × {𝐴}))‘(𝑥 + 1)) = (seq𝑀((𝐹 ∘ 1st ), {〈𝑀, 𝐴〉})‘(𝑥 + 1)) ↔ (𝐹‘(seq𝑀((𝐹 ∘ 1st ), (𝑍 × {𝐴}))‘𝑥)) = (𝐹‘(seq𝑀((𝐹 ∘ 1st ), {〈𝑀, 𝐴〉})‘𝑥)))) |
| 45 | 44 | adantl 481 |
. . . . . . . . 9
⊢ ((𝐴 ∈ 𝑉 ∧ 𝑥 ∈ (ℤ≥‘𝑀)) → ((seq𝑀((𝐹 ∘ 1st ), (𝑍 × {𝐴}))‘(𝑥 + 1)) = (seq𝑀((𝐹 ∘ 1st ), {〈𝑀, 𝐴〉})‘(𝑥 + 1)) ↔ (𝐹‘(seq𝑀((𝐹 ∘ 1st ), (𝑍 × {𝐴}))‘𝑥)) = (𝐹‘(seq𝑀((𝐹 ∘ 1st ), {〈𝑀, 𝐴〉})‘𝑥)))) |
| 46 | 33, 45 | imbitrrid 246 |
. . . . . . . 8
⊢ ((𝐴 ∈ 𝑉 ∧ 𝑥 ∈ (ℤ≥‘𝑀)) → ((seq𝑀((𝐹 ∘ 1st ), (𝑍 × {𝐴}))‘𝑥) = (seq𝑀((𝐹 ∘ 1st ), {〈𝑀, 𝐴〉})‘𝑥) → (seq𝑀((𝐹 ∘ 1st ), (𝑍 × {𝐴}))‘(𝑥 + 1)) = (seq𝑀((𝐹 ∘ 1st ), {〈𝑀, 𝐴〉})‘(𝑥 + 1)))) |
| 47 | 46 | expcom 413 |
. . . . . . 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 12948 |
. . . . 5
⊢ (𝑥 ∈
(ℤ≥‘𝑀) → (𝐴 ∈ 𝑉 → (seq𝑀((𝐹 ∘ 1st ), (𝑍 × {𝐴}))‘𝑥) = (seq𝑀((𝐹 ∘ 1st ), {〈𝑀, 𝐴〉})‘𝑥))) |
| 50 | 49 | impcom 407 |
. . . 4
⊢ ((𝐴 ∈ 𝑉 ∧ 𝑥 ∈ (ℤ≥‘𝑀)) → (seq𝑀((𝐹 ∘ 1st ), (𝑍 × {𝐴}))‘𝑥) = (seq𝑀((𝐹 ∘ 1st ), {〈𝑀, 𝐴〉})‘𝑥)) |
| 51 | 50 | adantll 714 |
. . 3
⊢ (((𝑀 ∈ ℤ ∧ 𝐴 ∈ 𝑉) ∧ 𝑥 ∈ (ℤ≥‘𝑀)) → (seq𝑀((𝐹 ∘ 1st ), (𝑍 × {𝐴}))‘𝑥) = (seq𝑀((𝐹 ∘ 1st ), {〈𝑀, 𝐴〉})‘𝑥)) |
| 52 | 3, 5, 51 | eqfnfvd 7054 |
. 2
⊢ ((𝑀 ∈ ℤ ∧ 𝐴 ∈ 𝑉) → seq𝑀((𝐹 ∘ 1st ), (𝑍 × {𝐴})) = seq𝑀((𝐹 ∘ 1st ), {〈𝑀, 𝐴〉})) |
| 53 | 1, 52 | eqtrid 2789 |
1
⊢ ((𝑀 ∈ ℤ ∧ 𝐴 ∈ 𝑉) → 𝑅 = seq𝑀((𝐹 ∘ 1st ), {〈𝑀, 𝐴〉})) |