| Step | Hyp | Ref
| Expression |
| 1 | | mulgval.t |
. 2
⊢ · =
(.g‘𝐺) |
| 2 | | eqidd 2738 |
. . . . 5
⊢ (𝑤 = 𝐺 → ℤ = ℤ) |
| 3 | | fveq2 6906 |
. . . . . 6
⊢ (𝑤 = 𝐺 → (Base‘𝑤) = (Base‘𝐺)) |
| 4 | | mulgval.b |
. . . . . 6
⊢ 𝐵 = (Base‘𝐺) |
| 5 | 3, 4 | eqtr4di 2795 |
. . . . 5
⊢ (𝑤 = 𝐺 → (Base‘𝑤) = 𝐵) |
| 6 | | fveq2 6906 |
. . . . . . 7
⊢ (𝑤 = 𝐺 → (0g‘𝑤) = (0g‘𝐺)) |
| 7 | | mulgval.o |
. . . . . . 7
⊢ 0 =
(0g‘𝐺) |
| 8 | 6, 7 | eqtr4di 2795 |
. . . . . 6
⊢ (𝑤 = 𝐺 → (0g‘𝑤) = 0 ) |
| 9 | | fvex 6919 |
. . . . . . . . 9
⊢
(+g‘𝑤) ∈ V |
| 10 | | 1z 12647 |
. . . . . . . . 9
⊢ 1 ∈
ℤ |
| 11 | 9, 10 | seqexw 14058 |
. . . . . . . 8
⊢
seq1((+g‘𝑤), (ℕ × {𝑥})) ∈ V |
| 12 | 11 | a1i 11 |
. . . . . . 7
⊢ (𝑤 = 𝐺 → seq1((+g‘𝑤), (ℕ × {𝑥})) ∈ V) |
| 13 | | id 22 |
. . . . . . . . . 10
⊢ (𝑠 =
seq1((+g‘𝑤), (ℕ × {𝑥})) → 𝑠 = seq1((+g‘𝑤), (ℕ × {𝑥}))) |
| 14 | | fveq2 6906 |
. . . . . . . . . . . 12
⊢ (𝑤 = 𝐺 → (+g‘𝑤) = (+g‘𝐺)) |
| 15 | | mulgval.p |
. . . . . . . . . . . 12
⊢ + =
(+g‘𝐺) |
| 16 | 14, 15 | eqtr4di 2795 |
. . . . . . . . . . 11
⊢ (𝑤 = 𝐺 → (+g‘𝑤) = + ) |
| 17 | 16 | seqeq2d 14049 |
. . . . . . . . . 10
⊢ (𝑤 = 𝐺 → seq1((+g‘𝑤), (ℕ × {𝑥})) = seq1( + , (ℕ × {𝑥}))) |
| 18 | 13, 17 | sylan9eqr 2799 |
. . . . . . . . 9
⊢ ((𝑤 = 𝐺 ∧ 𝑠 = seq1((+g‘𝑤), (ℕ × {𝑥}))) → 𝑠 = seq1( + , (ℕ × {𝑥}))) |
| 19 | 18 | fveq1d 6908 |
. . . . . . . 8
⊢ ((𝑤 = 𝐺 ∧ 𝑠 = seq1((+g‘𝑤), (ℕ × {𝑥}))) → (𝑠‘𝑛) = (seq1( + , (ℕ × {𝑥}))‘𝑛)) |
| 20 | | simpl 482 |
. . . . . . . . . . 11
⊢ ((𝑤 = 𝐺 ∧ 𝑠 = seq1((+g‘𝑤), (ℕ × {𝑥}))) → 𝑤 = 𝐺) |
| 21 | 20 | fveq2d 6910 |
. . . . . . . . . 10
⊢ ((𝑤 = 𝐺 ∧ 𝑠 = seq1((+g‘𝑤), (ℕ × {𝑥}))) →
(invg‘𝑤) =
(invg‘𝐺)) |
| 22 | | mulgval.i |
. . . . . . . . . 10
⊢ 𝐼 = (invg‘𝐺) |
| 23 | 21, 22 | eqtr4di 2795 |
. . . . . . . . 9
⊢ ((𝑤 = 𝐺 ∧ 𝑠 = seq1((+g‘𝑤), (ℕ × {𝑥}))) →
(invg‘𝑤) =
𝐼) |
| 24 | 18 | fveq1d 6908 |
. . . . . . . . 9
⊢ ((𝑤 = 𝐺 ∧ 𝑠 = seq1((+g‘𝑤), (ℕ × {𝑥}))) → (𝑠‘-𝑛) = (seq1( + , (ℕ × {𝑥}))‘-𝑛)) |
| 25 | 23, 24 | fveq12d 6913 |
. . . . . . . 8
⊢ ((𝑤 = 𝐺 ∧ 𝑠 = seq1((+g‘𝑤), (ℕ × {𝑥}))) →
((invg‘𝑤)‘(𝑠‘-𝑛)) = (𝐼‘(seq1( + , (ℕ × {𝑥}))‘-𝑛))) |
| 26 | 19, 25 | ifeq12d 4547 |
. . . . . . 7
⊢ ((𝑤 = 𝐺 ∧ 𝑠 = seq1((+g‘𝑤), (ℕ × {𝑥}))) → if(0 < 𝑛, (𝑠‘𝑛), ((invg‘𝑤)‘(𝑠‘-𝑛))) = if(0 < 𝑛, (seq1( + , (ℕ × {𝑥}))‘𝑛), (𝐼‘(seq1( + , (ℕ × {𝑥}))‘-𝑛)))) |
| 27 | 12, 26 | csbied 3935 |
. . . . . 6
⊢ (𝑤 = 𝐺 →
⦋seq1((+g‘𝑤), (ℕ × {𝑥})) / 𝑠⦌if(0 < 𝑛, (𝑠‘𝑛), ((invg‘𝑤)‘(𝑠‘-𝑛))) = if(0 < 𝑛, (seq1( + , (ℕ × {𝑥}))‘𝑛), (𝐼‘(seq1( + , (ℕ × {𝑥}))‘-𝑛)))) |
| 28 | 8, 27 | ifeq12d 4547 |
. . . . 5
⊢ (𝑤 = 𝐺 → if(𝑛 = 0, (0g‘𝑤),
⦋seq1((+g‘𝑤), (ℕ × {𝑥})) / 𝑠⦌if(0 < 𝑛, (𝑠‘𝑛), ((invg‘𝑤)‘(𝑠‘-𝑛)))) = if(𝑛 = 0, 0 , if(0 < 𝑛, (seq1( + , (ℕ × {𝑥}))‘𝑛), (𝐼‘(seq1( + , (ℕ × {𝑥}))‘-𝑛))))) |
| 29 | 2, 5, 28 | mpoeq123dv 7508 |
. . . 4
⊢ (𝑤 = 𝐺 → (𝑛 ∈ ℤ, 𝑥 ∈ (Base‘𝑤) ↦ if(𝑛 = 0, (0g‘𝑤),
⦋seq1((+g‘𝑤), (ℕ × {𝑥})) / 𝑠⦌if(0 < 𝑛, (𝑠‘𝑛), ((invg‘𝑤)‘(𝑠‘-𝑛))))) = (𝑛 ∈ ℤ, 𝑥 ∈ 𝐵 ↦ if(𝑛 = 0, 0 , if(0 < 𝑛, (seq1( + , (ℕ × {𝑥}))‘𝑛), (𝐼‘(seq1( + , (ℕ × {𝑥}))‘-𝑛)))))) |
| 30 | | df-mulg 19086 |
. . . 4
⊢
.g = (𝑤
∈ V ↦ (𝑛 ∈
ℤ, 𝑥 ∈
(Base‘𝑤) ↦
if(𝑛 = 0,
(0g‘𝑤),
⦋seq1((+g‘𝑤), (ℕ × {𝑥})) / 𝑠⦌if(0 < 𝑛, (𝑠‘𝑛), ((invg‘𝑤)‘(𝑠‘-𝑛)))))) |
| 31 | | zex 12622 |
. . . . 5
⊢ ℤ
∈ V |
| 32 | 4 | fvexi 6920 |
. . . . 5
⊢ 𝐵 ∈ V |
| 33 | | snex 5436 |
. . . . . 6
⊢ { 0 } ∈
V |
| 34 | 15 | fvexi 6920 |
. . . . . . . . 9
⊢ + ∈
V |
| 35 | 34 | rnex 7932 |
. . . . . . . 8
⊢ ran + ∈
V |
| 36 | 35, 32 | unex 7764 |
. . . . . . 7
⊢ (ran
+ ∪
𝐵) ∈
V |
| 37 | 22 | fvexi 6920 |
. . . . . . . . 9
⊢ 𝐼 ∈ V |
| 38 | 37 | rnex 7932 |
. . . . . . . 8
⊢ ran 𝐼 ∈ V |
| 39 | | p0ex 5384 |
. . . . . . . 8
⊢ {∅}
∈ V |
| 40 | 38, 39 | unex 7764 |
. . . . . . 7
⊢ (ran
𝐼 ∪ {∅}) ∈
V |
| 41 | 36, 40 | unex 7764 |
. . . . . 6
⊢ ((ran
+ ∪
𝐵) ∪ (ran 𝐼 ∪ {∅})) ∈
V |
| 42 | 33, 41 | unex 7764 |
. . . . 5
⊢ ({ 0 } ∪ ((ran
+ ∪
𝐵) ∪ (ran 𝐼 ∪ {∅}))) ∈
V |
| 43 | | ssun1 4178 |
. . . . . . . . 9
⊢ { 0 } ⊆ ({
0 } ∪
((ran +
∪ 𝐵) ∪ (ran 𝐼 ∪
{∅}))) |
| 44 | 7 | fvexi 6920 |
. . . . . . . . . 10
⊢ 0 ∈
V |
| 45 | 44 | snid 4662 |
. . . . . . . . 9
⊢ 0 ∈ {
0
} |
| 46 | 43, 45 | sselii 3980 |
. . . . . . . 8
⊢ 0 ∈ ({
0 } ∪
((ran +
∪ 𝐵) ∪ (ran 𝐼 ∪
{∅}))) |
| 47 | 46 | a1i 11 |
. . . . . . 7
⊢ ((𝑛 ∈ ℤ ∧ 𝑥 ∈ 𝐵) → 0 ∈ ({ 0 } ∪ ((ran
+ ∪
𝐵) ∪ (ran 𝐼 ∪
{∅})))) |
| 48 | | ssun2 4179 |
. . . . . . . . . . . . . 14
⊢ 𝐵 ⊆ (ran + ∪ 𝐵) |
| 49 | | ssun1 4178 |
. . . . . . . . . . . . . 14
⊢ (ran
+ ∪
𝐵) ⊆ ((ran + ∪ 𝐵) ∪ (ran 𝐼 ∪ {∅})) |
| 50 | 48, 49 | sstri 3993 |
. . . . . . . . . . . . 13
⊢ 𝐵 ⊆ ((ran + ∪ 𝐵) ∪ (ran 𝐼 ∪ {∅})) |
| 51 | | ssun2 4179 |
. . . . . . . . . . . . 13
⊢ ((ran
+ ∪
𝐵) ∪ (ran 𝐼 ∪ {∅})) ⊆ ({
0 } ∪
((ran +
∪ 𝐵) ∪ (ran 𝐼 ∪
{∅}))) |
| 52 | 50, 51 | sstri 3993 |
. . . . . . . . . . . 12
⊢ 𝐵 ⊆ ({ 0 } ∪ ((ran + ∪ 𝐵) ∪ (ran 𝐼 ∪ {∅}))) |
| 53 | | fveq2 6906 |
. . . . . . . . . . . . . 14
⊢ (𝑛 = 1 → (seq1( + , (ℕ
× {𝑥}))‘𝑛) = (seq1( + , (ℕ × {𝑥}))‘1)) |
| 54 | 53 | adantl 481 |
. . . . . . . . . . . . 13
⊢ ((𝑥 ∈ 𝐵 ∧ 𝑛 = 1) → (seq1( + , (ℕ × {𝑥}))‘𝑛) = (seq1( + , (ℕ × {𝑥}))‘1)) |
| 55 | | seq1 14055 |
. . . . . . . . . . . . . . . 16
⊢ (1 ∈
ℤ → (seq1( + , (ℕ × {𝑥}))‘1) = ((ℕ ×
{𝑥})‘1)) |
| 56 | 10, 55 | ax-mp 5 |
. . . . . . . . . . . . . . 15
⊢ (seq1(
+ ,
(ℕ × {𝑥}))‘1) = ((ℕ × {𝑥})‘1) |
| 57 | | 1nn 12277 |
. . . . . . . . . . . . . . . . . 18
⊢ 1 ∈
ℕ |
| 58 | | vex 3484 |
. . . . . . . . . . . . . . . . . . 19
⊢ 𝑥 ∈ V |
| 59 | 58 | fvconst2 7224 |
. . . . . . . . . . . . . . . . . 18
⊢ (1 ∈
ℕ → ((ℕ × {𝑥})‘1) = 𝑥) |
| 60 | 57, 59 | ax-mp 5 |
. . . . . . . . . . . . . . . . 17
⊢ ((ℕ
× {𝑥})‘1) =
𝑥 |
| 61 | 60 | eleq1i 2832 |
. . . . . . . . . . . . . . . 16
⊢
(((ℕ × {𝑥})‘1) ∈ 𝐵 ↔ 𝑥 ∈ 𝐵) |
| 62 | 61 | biimpri 228 |
. . . . . . . . . . . . . . 15
⊢ (𝑥 ∈ 𝐵 → ((ℕ × {𝑥})‘1) ∈ 𝐵) |
| 63 | 56, 62 | eqeltrid 2845 |
. . . . . . . . . . . . . 14
⊢ (𝑥 ∈ 𝐵 → (seq1( + , (ℕ × {𝑥}))‘1) ∈ 𝐵) |
| 64 | 63 | adantr 480 |
. . . . . . . . . . . . 13
⊢ ((𝑥 ∈ 𝐵 ∧ 𝑛 = 1) → (seq1( + , (ℕ × {𝑥}))‘1) ∈ 𝐵) |
| 65 | 54, 64 | eqeltrd 2841 |
. . . . . . . . . . . 12
⊢ ((𝑥 ∈ 𝐵 ∧ 𝑛 = 1) → (seq1( + , (ℕ × {𝑥}))‘𝑛) ∈ 𝐵) |
| 66 | 52, 65 | sselid 3981 |
. . . . . . . . . . 11
⊢ ((𝑥 ∈ 𝐵 ∧ 𝑛 = 1) → (seq1( + , (ℕ × {𝑥}))‘𝑛) ∈ ({ 0 } ∪ ((ran + ∪ 𝐵) ∪ (ran 𝐼 ∪ {∅})))) |
| 67 | 66 | ad4ant24 754 |
. . . . . . . . . 10
⊢ ((((𝑛 ∈ ℤ ∧ 𝑥 ∈ 𝐵) ∧ 𝑛 ∈ (ℤ≥‘1))
∧ 𝑛 = 1) → (seq1(
+ ,
(ℕ × {𝑥}))‘𝑛) ∈ ({ 0 } ∪ ((ran + ∪ 𝐵) ∪ (ran 𝐼 ∪ {∅})))) |
| 68 | | zcn 12618 |
. . . . . . . . . . . . . . 15
⊢ (𝑛 ∈ ℤ → 𝑛 ∈
ℂ) |
| 69 | | npcan1 11688 |
. . . . . . . . . . . . . . 15
⊢ (𝑛 ∈ ℂ → ((𝑛 − 1) + 1) = 𝑛) |
| 70 | 68, 69 | syl 17 |
. . . . . . . . . . . . . 14
⊢ (𝑛 ∈ ℤ → ((𝑛 − 1) + 1) = 𝑛) |
| 71 | 70 | fveq2d 6910 |
. . . . . . . . . . . . 13
⊢ (𝑛 ∈ ℤ → (seq1(
+ ,
(ℕ × {𝑥}))‘((𝑛 − 1) + 1)) = (seq1( + , (ℕ × {𝑥}))‘𝑛)) |
| 72 | 71 | adantr 480 |
. . . . . . . . . . . 12
⊢ ((𝑛 ∈ ℤ ∧ (𝑛 − 1) ∈
(ℤ≥‘1)) → (seq1( + , (ℕ × {𝑥}))‘((𝑛 − 1) + 1)) = (seq1( + , (ℕ × {𝑥}))‘𝑛)) |
| 73 | | seqp1 14057 |
. . . . . . . . . . . . . 14
⊢ ((𝑛 − 1) ∈
(ℤ≥‘1) → (seq1( + , (ℕ × {𝑥}))‘((𝑛 − 1) + 1)) = ((seq1( + , (ℕ
× {𝑥}))‘(𝑛 − 1)) + ((ℕ × {𝑥})‘((𝑛 − 1) + 1)))) |
| 74 | | ssun1 4178 |
. . . . . . . . . . . . . . . . 17
⊢ ran + ⊆ (ran
+ ∪
𝐵) |
| 75 | | ssun2 4179 |
. . . . . . . . . . . . . . . . 17
⊢ {∅}
⊆ (ran 𝐼 ∪
{∅}) |
| 76 | | unss12 4188 |
. . . . . . . . . . . . . . . . 17
⊢ ((ran
+ ⊆
(ran +
∪ 𝐵) ∧ {∅}
⊆ (ran 𝐼 ∪
{∅})) → (ran + ∪ {∅}) ⊆
((ran +
∪ 𝐵) ∪ (ran 𝐼 ∪
{∅}))) |
| 77 | 74, 75, 76 | mp2an 692 |
. . . . . . . . . . . . . . . 16
⊢ (ran
+ ∪
{∅}) ⊆ ((ran + ∪ 𝐵) ∪ (ran 𝐼 ∪ {∅})) |
| 78 | 77, 51 | sstri 3993 |
. . . . . . . . . . . . . . 15
⊢ (ran
+ ∪
{∅}) ⊆ ({ 0 } ∪ ((ran + ∪ 𝐵) ∪ (ran 𝐼 ∪ {∅}))) |
| 79 | | df-ov 7434 |
. . . . . . . . . . . . . . . 16
⊢ ((seq1(
+ ,
(ℕ × {𝑥}))‘(𝑛 − 1)) + ((ℕ × {𝑥})‘((𝑛 − 1) + 1))) = ( + ‘〈(seq1( + , (ℕ
× {𝑥}))‘(𝑛 − 1)), ((ℕ ×
{𝑥})‘((𝑛 − 1) +
1))〉) |
| 80 | | fvrn0 6936 |
. . . . . . . . . . . . . . . 16
⊢ ( +
‘〈(seq1( + , (ℕ × {𝑥}))‘(𝑛 − 1)), ((ℕ × {𝑥})‘((𝑛 − 1) + 1))〉) ∈ (ran + ∪
{∅}) |
| 81 | 79, 80 | eqeltri 2837 |
. . . . . . . . . . . . . . 15
⊢ ((seq1(
+ ,
(ℕ × {𝑥}))‘(𝑛 − 1)) + ((ℕ × {𝑥})‘((𝑛 − 1) + 1))) ∈ (ran + ∪
{∅}) |
| 82 | 78, 81 | sselii 3980 |
. . . . . . . . . . . . . 14
⊢ ((seq1(
+ ,
(ℕ × {𝑥}))‘(𝑛 − 1)) + ((ℕ × {𝑥})‘((𝑛 − 1) + 1))) ∈ ({ 0 } ∪ ((ran
+ ∪
𝐵) ∪ (ran 𝐼 ∪
{∅}))) |
| 83 | 73, 82 | eqeltrdi 2849 |
. . . . . . . . . . . . 13
⊢ ((𝑛 − 1) ∈
(ℤ≥‘1) → (seq1( + , (ℕ × {𝑥}))‘((𝑛 − 1) + 1)) ∈ ({ 0 } ∪ ((ran
+ ∪
𝐵) ∪ (ran 𝐼 ∪
{∅})))) |
| 84 | 83 | adantl 481 |
. . . . . . . . . . . 12
⊢ ((𝑛 ∈ ℤ ∧ (𝑛 − 1) ∈
(ℤ≥‘1)) → (seq1( + , (ℕ × {𝑥}))‘((𝑛 − 1) + 1)) ∈ ({ 0 } ∪ ((ran
+ ∪
𝐵) ∪ (ran 𝐼 ∪
{∅})))) |
| 85 | 72, 84 | eqeltrrd 2842 |
. . . . . . . . . . 11
⊢ ((𝑛 ∈ ℤ ∧ (𝑛 − 1) ∈
(ℤ≥‘1)) → (seq1( + , (ℕ × {𝑥}))‘𝑛) ∈ ({ 0 } ∪ ((ran + ∪ 𝐵) ∪ (ran 𝐼 ∪ {∅})))) |
| 86 | 85 | ad4ant14 752 |
. . . . . . . . . 10
⊢ ((((𝑛 ∈ ℤ ∧ 𝑥 ∈ 𝐵) ∧ 𝑛 ∈ (ℤ≥‘1))
∧ (𝑛 − 1) ∈
(ℤ≥‘1)) → (seq1( + , (ℕ × {𝑥}))‘𝑛) ∈ ({ 0 } ∪ ((ran + ∪ 𝐵) ∪ (ran 𝐼 ∪ {∅})))) |
| 87 | | uzm1 12916 |
. . . . . . . . . . 11
⊢ (𝑛 ∈
(ℤ≥‘1) → (𝑛 = 1 ∨ (𝑛 − 1) ∈
(ℤ≥‘1))) |
| 88 | 87 | adantl 481 |
. . . . . . . . . 10
⊢ (((𝑛 ∈ ℤ ∧ 𝑥 ∈ 𝐵) ∧ 𝑛 ∈ (ℤ≥‘1))
→ (𝑛 = 1 ∨ (𝑛 − 1) ∈
(ℤ≥‘1))) |
| 89 | 67, 86, 88 | mpjaodan 961 |
. . . . . . . . 9
⊢ (((𝑛 ∈ ℤ ∧ 𝑥 ∈ 𝐵) ∧ 𝑛 ∈ (ℤ≥‘1))
→ (seq1( + , (ℕ × {𝑥}))‘𝑛) ∈ ({ 0 } ∪ ((ran + ∪ 𝐵) ∪ (ran 𝐼 ∪ {∅})))) |
| 90 | | simpr 484 |
. . . . . . . . . . . 12
⊢ (((𝑛 ∈ ℤ ∧ 𝑥 ∈ 𝐵) ∧ ¬ 𝑛 ∈ (ℤ≥‘1))
→ ¬ 𝑛 ∈
(ℤ≥‘1)) |
| 91 | | seqfn 14054 |
. . . . . . . . . . . . . . 15
⊢ (1 ∈
ℤ → seq1( + , (ℕ × {𝑥})) Fn
(ℤ≥‘1)) |
| 92 | 10, 91 | ax-mp 5 |
. . . . . . . . . . . . . 14
⊢ seq1(
+ ,
(ℕ × {𝑥})) Fn
(ℤ≥‘1) |
| 93 | 92 | fndmi 6672 |
. . . . . . . . . . . . 13
⊢ dom seq1(
+ ,
(ℕ × {𝑥})) =
(ℤ≥‘1) |
| 94 | 93 | eleq2i 2833 |
. . . . . . . . . . . 12
⊢ (𝑛 ∈ dom seq1( + , (ℕ
× {𝑥})) ↔ 𝑛 ∈
(ℤ≥‘1)) |
| 95 | 90, 94 | sylnibr 329 |
. . . . . . . . . . 11
⊢ (((𝑛 ∈ ℤ ∧ 𝑥 ∈ 𝐵) ∧ ¬ 𝑛 ∈ (ℤ≥‘1))
→ ¬ 𝑛 ∈ dom
seq1( + ,
(ℕ × {𝑥}))) |
| 96 | | ndmfv 6941 |
. . . . . . . . . . 11
⊢ (¬
𝑛 ∈ dom seq1( + , (ℕ
× {𝑥})) → (seq1(
+ ,
(ℕ × {𝑥}))‘𝑛) = ∅) |
| 97 | 95, 96 | syl 17 |
. . . . . . . . . 10
⊢ (((𝑛 ∈ ℤ ∧ 𝑥 ∈ 𝐵) ∧ ¬ 𝑛 ∈ (ℤ≥‘1))
→ (seq1( + , (ℕ × {𝑥}))‘𝑛) = ∅) |
| 98 | | ssun2 4179 |
. . . . . . . . . . . . . 14
⊢ (ran
𝐼 ∪ {∅}) ⊆
((ran +
∪ 𝐵) ∪ (ran 𝐼 ∪
{∅})) |
| 99 | 75, 98 | sstri 3993 |
. . . . . . . . . . . . 13
⊢ {∅}
⊆ ((ran + ∪ 𝐵) ∪ (ran 𝐼 ∪ {∅})) |
| 100 | 99, 51 | sstri 3993 |
. . . . . . . . . . . 12
⊢ {∅}
⊆ ({ 0 } ∪ ((ran + ∪ 𝐵) ∪ (ran 𝐼 ∪ {∅}))) |
| 101 | | 0ex 5307 |
. . . . . . . . . . . . 13
⊢ ∅
∈ V |
| 102 | 101 | snid 4662 |
. . . . . . . . . . . 12
⊢ ∅
∈ {∅} |
| 103 | 100, 102 | sselii 3980 |
. . . . . . . . . . 11
⊢ ∅
∈ ({ 0 } ∪ ((ran + ∪ 𝐵) ∪ (ran 𝐼 ∪ {∅}))) |
| 104 | 103 | a1i 11 |
. . . . . . . . . 10
⊢ (((𝑛 ∈ ℤ ∧ 𝑥 ∈ 𝐵) ∧ ¬ 𝑛 ∈ (ℤ≥‘1))
→ ∅ ∈ ({ 0 } ∪ ((ran + ∪ 𝐵) ∪ (ran 𝐼 ∪ {∅})))) |
| 105 | 97, 104 | eqeltrd 2841 |
. . . . . . . . 9
⊢ (((𝑛 ∈ ℤ ∧ 𝑥 ∈ 𝐵) ∧ ¬ 𝑛 ∈ (ℤ≥‘1))
→ (seq1( + , (ℕ × {𝑥}))‘𝑛) ∈ ({ 0 } ∪ ((ran + ∪ 𝐵) ∪ (ran 𝐼 ∪ {∅})))) |
| 106 | 89, 105 | pm2.61dan 813 |
. . . . . . . 8
⊢ ((𝑛 ∈ ℤ ∧ 𝑥 ∈ 𝐵) → (seq1( + , (ℕ × {𝑥}))‘𝑛) ∈ ({ 0 } ∪ ((ran + ∪ 𝐵) ∪ (ran 𝐼 ∪ {∅})))) |
| 107 | 98, 51 | sstri 3993 |
. . . . . . . . . 10
⊢ (ran
𝐼 ∪ {∅}) ⊆
({ 0 }
∪ ((ran + ∪ 𝐵) ∪ (ran 𝐼 ∪ {∅}))) |
| 108 | | fvrn0 6936 |
. . . . . . . . . 10
⊢ (𝐼‘(seq1( + , (ℕ × {𝑥}))‘-𝑛)) ∈ (ran 𝐼 ∪ {∅}) |
| 109 | 107, 108 | sselii 3980 |
. . . . . . . . 9
⊢ (𝐼‘(seq1( + , (ℕ × {𝑥}))‘-𝑛)) ∈ ({ 0 } ∪ ((ran + ∪ 𝐵) ∪ (ran 𝐼 ∪ {∅}))) |
| 110 | 109 | a1i 11 |
. . . . . . . 8
⊢ ((𝑛 ∈ ℤ ∧ 𝑥 ∈ 𝐵) → (𝐼‘(seq1( + , (ℕ × {𝑥}))‘-𝑛)) ∈ ({ 0 } ∪ ((ran + ∪ 𝐵) ∪ (ran 𝐼 ∪ {∅})))) |
| 111 | 106, 110 | ifcld 4572 |
. . . . . . 7
⊢ ((𝑛 ∈ ℤ ∧ 𝑥 ∈ 𝐵) → if(0 < 𝑛, (seq1( + , (ℕ × {𝑥}))‘𝑛), (𝐼‘(seq1( + , (ℕ × {𝑥}))‘-𝑛))) ∈ ({ 0 } ∪ ((ran + ∪ 𝐵) ∪ (ran 𝐼 ∪ {∅})))) |
| 112 | 47, 111 | ifcld 4572 |
. . . . . 6
⊢ ((𝑛 ∈ ℤ ∧ 𝑥 ∈ 𝐵) → if(𝑛 = 0, 0 , if(0 < 𝑛, (seq1( + , (ℕ × {𝑥}))‘𝑛), (𝐼‘(seq1( + , (ℕ × {𝑥}))‘-𝑛)))) ∈ ({ 0 } ∪ ((ran + ∪ 𝐵) ∪ (ran 𝐼 ∪ {∅})))) |
| 113 | 112 | rgen2 3199 |
. . . . 5
⊢
∀𝑛 ∈
ℤ ∀𝑥 ∈
𝐵 if(𝑛 = 0, 0 , if(0 < 𝑛, (seq1( + , (ℕ × {𝑥}))‘𝑛), (𝐼‘(seq1( + , (ℕ × {𝑥}))‘-𝑛)))) ∈ ({ 0 } ∪ ((ran + ∪ 𝐵) ∪ (ran 𝐼 ∪ {∅}))) |
| 114 | 31, 32, 42, 113 | mpoexw 8103 |
. . . 4
⊢ (𝑛 ∈ ℤ, 𝑥 ∈ 𝐵 ↦ if(𝑛 = 0, 0 , if(0 < 𝑛, (seq1( + , (ℕ × {𝑥}))‘𝑛), (𝐼‘(seq1( + , (ℕ × {𝑥}))‘-𝑛))))) ∈ V |
| 115 | 29, 30, 114 | fvmpt 7016 |
. . 3
⊢ (𝐺 ∈ V →
(.g‘𝐺) =
(𝑛 ∈ ℤ, 𝑥 ∈ 𝐵 ↦ if(𝑛 = 0, 0 , if(0 < 𝑛, (seq1( + , (ℕ × {𝑥}))‘𝑛), (𝐼‘(seq1( + , (ℕ × {𝑥}))‘-𝑛)))))) |
| 116 | | fvprc 6898 |
. . . 4
⊢ (¬
𝐺 ∈ V →
(.g‘𝐺) =
∅) |
| 117 | | eqid 2737 |
. . . . . . 7
⊢ (𝑛 ∈ ℤ, 𝑥 ∈ 𝐵 ↦ if(𝑛 = 0, 0 , if(0 < 𝑛, (seq1( + , (ℕ × {𝑥}))‘𝑛), (𝐼‘(seq1( + , (ℕ × {𝑥}))‘-𝑛))))) = (𝑛 ∈ ℤ, 𝑥 ∈ 𝐵 ↦ if(𝑛 = 0, 0 , if(0 < 𝑛, (seq1( + , (ℕ × {𝑥}))‘𝑛), (𝐼‘(seq1( + , (ℕ × {𝑥}))‘-𝑛))))) |
| 118 | | fvex 6919 |
. . . . . . . . 9
⊢ (seq1(
+ ,
(ℕ × {𝑥}))‘𝑛) ∈ V |
| 119 | | fvex 6919 |
. . . . . . . . 9
⊢ (𝐼‘(seq1( + , (ℕ × {𝑥}))‘-𝑛)) ∈ V |
| 120 | 118, 119 | ifex 4576 |
. . . . . . . 8
⊢ if(0 <
𝑛, (seq1( + , (ℕ
× {𝑥}))‘𝑛), (𝐼‘(seq1( + , (ℕ × {𝑥}))‘-𝑛))) ∈ V |
| 121 | 44, 120 | ifex 4576 |
. . . . . . 7
⊢ if(𝑛 = 0, 0 , if(0 < 𝑛, (seq1( + , (ℕ × {𝑥}))‘𝑛), (𝐼‘(seq1( + , (ℕ × {𝑥}))‘-𝑛)))) ∈ V |
| 122 | 117, 121 | fnmpoi 8095 |
. . . . . 6
⊢ (𝑛 ∈ ℤ, 𝑥 ∈ 𝐵 ↦ if(𝑛 = 0, 0 , if(0 < 𝑛, (seq1( + , (ℕ × {𝑥}))‘𝑛), (𝐼‘(seq1( + , (ℕ × {𝑥}))‘-𝑛))))) Fn (ℤ × 𝐵) |
| 123 | | fvprc 6898 |
. . . . . . . . . 10
⊢ (¬
𝐺 ∈ V →
(Base‘𝐺) =
∅) |
| 124 | 4, 123 | eqtrid 2789 |
. . . . . . . . 9
⊢ (¬
𝐺 ∈ V → 𝐵 = ∅) |
| 125 | 124 | xpeq2d 5715 |
. . . . . . . 8
⊢ (¬
𝐺 ∈ V → (ℤ
× 𝐵) = (ℤ
× ∅)) |
| 126 | | xp0 6178 |
. . . . . . . 8
⊢ (ℤ
× ∅) = ∅ |
| 127 | 125, 126 | eqtrdi 2793 |
. . . . . . 7
⊢ (¬
𝐺 ∈ V → (ℤ
× 𝐵) =
∅) |
| 128 | 127 | fneq2d 6662 |
. . . . . 6
⊢ (¬
𝐺 ∈ V → ((𝑛 ∈ ℤ, 𝑥 ∈ 𝐵 ↦ if(𝑛 = 0, 0 , if(0 < 𝑛, (seq1( + , (ℕ × {𝑥}))‘𝑛), (𝐼‘(seq1( + , (ℕ × {𝑥}))‘-𝑛))))) Fn (ℤ × 𝐵) ↔ (𝑛 ∈ ℤ, 𝑥 ∈ 𝐵 ↦ if(𝑛 = 0, 0 , if(0 < 𝑛, (seq1( + , (ℕ × {𝑥}))‘𝑛), (𝐼‘(seq1( + , (ℕ × {𝑥}))‘-𝑛))))) Fn ∅)) |
| 129 | 122, 128 | mpbii 233 |
. . . . 5
⊢ (¬
𝐺 ∈ V → (𝑛 ∈ ℤ, 𝑥 ∈ 𝐵 ↦ if(𝑛 = 0, 0 , if(0 < 𝑛, (seq1( + , (ℕ × {𝑥}))‘𝑛), (𝐼‘(seq1( + , (ℕ × {𝑥}))‘-𝑛))))) Fn ∅) |
| 130 | | fn0 6699 |
. . . . 5
⊢ ((𝑛 ∈ ℤ, 𝑥 ∈ 𝐵 ↦ if(𝑛 = 0, 0 , if(0 < 𝑛, (seq1( + , (ℕ × {𝑥}))‘𝑛), (𝐼‘(seq1( + , (ℕ × {𝑥}))‘-𝑛))))) Fn ∅ ↔ (𝑛 ∈ ℤ, 𝑥 ∈ 𝐵 ↦ if(𝑛 = 0, 0 , if(0 < 𝑛, (seq1( + , (ℕ × {𝑥}))‘𝑛), (𝐼‘(seq1( + , (ℕ × {𝑥}))‘-𝑛))))) = ∅) |
| 131 | 129, 130 | sylib 218 |
. . . 4
⊢ (¬
𝐺 ∈ V → (𝑛 ∈ ℤ, 𝑥 ∈ 𝐵 ↦ if(𝑛 = 0, 0 , if(0 < 𝑛, (seq1( + , (ℕ × {𝑥}))‘𝑛), (𝐼‘(seq1( + , (ℕ × {𝑥}))‘-𝑛))))) = ∅) |
| 132 | 116, 131 | eqtr4d 2780 |
. . 3
⊢ (¬
𝐺 ∈ V →
(.g‘𝐺) =
(𝑛 ∈ ℤ, 𝑥 ∈ 𝐵 ↦ if(𝑛 = 0, 0 , if(0 < 𝑛, (seq1( + , (ℕ × {𝑥}))‘𝑛), (𝐼‘(seq1( + , (ℕ × {𝑥}))‘-𝑛)))))) |
| 133 | 115, 132 | pm2.61i 182 |
. 2
⊢
(.g‘𝐺) = (𝑛 ∈ ℤ, 𝑥 ∈ 𝐵 ↦ if(𝑛 = 0, 0 , if(0 < 𝑛, (seq1( + , (ℕ × {𝑥}))‘𝑛), (𝐼‘(seq1( + , (ℕ × {𝑥}))‘-𝑛))))) |
| 134 | 1, 133 | eqtri 2765 |
1
⊢ · =
(𝑛 ∈ ℤ, 𝑥 ∈ 𝐵 ↦ if(𝑛 = 0, 0 , if(0 < 𝑛, (seq1( + , (ℕ × {𝑥}))‘𝑛), (𝐼‘(seq1( + , (ℕ × {𝑥}))‘-𝑛))))) |