Step | Hyp | Ref
| Expression |
1 | | mulgval.t |
. 2
⊢ · =
(.g‘𝐺) |
2 | | eqidd 2739 |
. . . . 5
⊢ (𝑤 = 𝐺 → ℤ = ℤ) |
3 | | fveq2 6766 |
. . . . . 6
⊢ (𝑤 = 𝐺 → (Base‘𝑤) = (Base‘𝐺)) |
4 | | mulgval.b |
. . . . . 6
⊢ 𝐵 = (Base‘𝐺) |
5 | 3, 4 | eqtr4di 2796 |
. . . . 5
⊢ (𝑤 = 𝐺 → (Base‘𝑤) = 𝐵) |
6 | | fveq2 6766 |
. . . . . . 7
⊢ (𝑤 = 𝐺 → (0g‘𝑤) = (0g‘𝐺)) |
7 | | mulgval.o |
. . . . . . 7
⊢ 0 =
(0g‘𝐺) |
8 | 6, 7 | eqtr4di 2796 |
. . . . . 6
⊢ (𝑤 = 𝐺 → (0g‘𝑤) = 0 ) |
9 | | fvex 6779 |
. . . . . . . . 9
⊢
(+g‘𝑤) ∈ V |
10 | | 1z 12360 |
. . . . . . . . 9
⊢ 1 ∈
ℤ |
11 | 9, 10 | seqexw 13747 |
. . . . . . . 8
⊢
seq1((+g‘𝑤), (ℕ × {𝑥})) ∈ V |
12 | 11 | a1i 11 |
. . . . . . 7
⊢ (𝑤 = 𝐺 → seq1((+g‘𝑤), (ℕ × {𝑥})) ∈ V) |
13 | | id 22 |
. . . . . . . . . 10
⊢ (𝑠 =
seq1((+g‘𝑤), (ℕ × {𝑥})) → 𝑠 = seq1((+g‘𝑤), (ℕ × {𝑥}))) |
14 | | fveq2 6766 |
. . . . . . . . . . . 12
⊢ (𝑤 = 𝐺 → (+g‘𝑤) = (+g‘𝐺)) |
15 | | mulgval.p |
. . . . . . . . . . . 12
⊢ + =
(+g‘𝐺) |
16 | 14, 15 | eqtr4di 2796 |
. . . . . . . . . . 11
⊢ (𝑤 = 𝐺 → (+g‘𝑤) = + ) |
17 | 16 | seqeq2d 13738 |
. . . . . . . . . 10
⊢ (𝑤 = 𝐺 → seq1((+g‘𝑤), (ℕ × {𝑥})) = seq1( + , (ℕ × {𝑥}))) |
18 | 13, 17 | sylan9eqr 2800 |
. . . . . . . . 9
⊢ ((𝑤 = 𝐺 ∧ 𝑠 = seq1((+g‘𝑤), (ℕ × {𝑥}))) → 𝑠 = seq1( + , (ℕ × {𝑥}))) |
19 | 18 | fveq1d 6768 |
. . . . . . . 8
⊢ ((𝑤 = 𝐺 ∧ 𝑠 = seq1((+g‘𝑤), (ℕ × {𝑥}))) → (𝑠‘𝑛) = (seq1( + , (ℕ × {𝑥}))‘𝑛)) |
20 | | simpl 483 |
. . . . . . . . . . 11
⊢ ((𝑤 = 𝐺 ∧ 𝑠 = seq1((+g‘𝑤), (ℕ × {𝑥}))) → 𝑤 = 𝐺) |
21 | 20 | fveq2d 6770 |
. . . . . . . . . 10
⊢ ((𝑤 = 𝐺 ∧ 𝑠 = seq1((+g‘𝑤), (ℕ × {𝑥}))) →
(invg‘𝑤) =
(invg‘𝐺)) |
22 | | mulgval.i |
. . . . . . . . . 10
⊢ 𝐼 = (invg‘𝐺) |
23 | 21, 22 | eqtr4di 2796 |
. . . . . . . . 9
⊢ ((𝑤 = 𝐺 ∧ 𝑠 = seq1((+g‘𝑤), (ℕ × {𝑥}))) →
(invg‘𝑤) =
𝐼) |
24 | 18 | fveq1d 6768 |
. . . . . . . . 9
⊢ ((𝑤 = 𝐺 ∧ 𝑠 = seq1((+g‘𝑤), (ℕ × {𝑥}))) → (𝑠‘-𝑛) = (seq1( + , (ℕ × {𝑥}))‘-𝑛)) |
25 | 23, 24 | fveq12d 6773 |
. . . . . . . 8
⊢ ((𝑤 = 𝐺 ∧ 𝑠 = seq1((+g‘𝑤), (ℕ × {𝑥}))) →
((invg‘𝑤)‘(𝑠‘-𝑛)) = (𝐼‘(seq1( + , (ℕ × {𝑥}))‘-𝑛))) |
26 | 19, 25 | ifeq12d 4480 |
. . . . . . 7
⊢ ((𝑤 = 𝐺 ∧ 𝑠 = seq1((+g‘𝑤), (ℕ × {𝑥}))) → if(0 < 𝑛, (𝑠‘𝑛), ((invg‘𝑤)‘(𝑠‘-𝑛))) = if(0 < 𝑛, (seq1( + , (ℕ × {𝑥}))‘𝑛), (𝐼‘(seq1( + , (ℕ × {𝑥}))‘-𝑛)))) |
27 | 12, 26 | csbied 3869 |
. . . . . 6
⊢ (𝑤 = 𝐺 →
⦋seq1((+g‘𝑤), (ℕ × {𝑥})) / 𝑠⦌if(0 < 𝑛, (𝑠‘𝑛), ((invg‘𝑤)‘(𝑠‘-𝑛))) = if(0 < 𝑛, (seq1( + , (ℕ × {𝑥}))‘𝑛), (𝐼‘(seq1( + , (ℕ × {𝑥}))‘-𝑛)))) |
28 | 8, 27 | ifeq12d 4480 |
. . . . 5
⊢ (𝑤 = 𝐺 → if(𝑛 = 0, (0g‘𝑤),
⦋seq1((+g‘𝑤), (ℕ × {𝑥})) / 𝑠⦌if(0 < 𝑛, (𝑠‘𝑛), ((invg‘𝑤)‘(𝑠‘-𝑛)))) = if(𝑛 = 0, 0 , if(0 < 𝑛, (seq1( + , (ℕ × {𝑥}))‘𝑛), (𝐼‘(seq1( + , (ℕ × {𝑥}))‘-𝑛))))) |
29 | 2, 5, 28 | mpoeq123dv 7340 |
. . . 4
⊢ (𝑤 = 𝐺 → (𝑛 ∈ ℤ, 𝑥 ∈ (Base‘𝑤) ↦ if(𝑛 = 0, (0g‘𝑤),
⦋seq1((+g‘𝑤), (ℕ × {𝑥})) / 𝑠⦌if(0 < 𝑛, (𝑠‘𝑛), ((invg‘𝑤)‘(𝑠‘-𝑛))))) = (𝑛 ∈ ℤ, 𝑥 ∈ 𝐵 ↦ if(𝑛 = 0, 0 , if(0 < 𝑛, (seq1( + , (ℕ × {𝑥}))‘𝑛), (𝐼‘(seq1( + , (ℕ × {𝑥}))‘-𝑛)))))) |
30 | | df-mulg 18711 |
. . . 4
⊢
.g = (𝑤
∈ V ↦ (𝑛 ∈
ℤ, 𝑥 ∈
(Base‘𝑤) ↦
if(𝑛 = 0,
(0g‘𝑤),
⦋seq1((+g‘𝑤), (ℕ × {𝑥})) / 𝑠⦌if(0 < 𝑛, (𝑠‘𝑛), ((invg‘𝑤)‘(𝑠‘-𝑛)))))) |
31 | | zex 12338 |
. . . . 5
⊢ ℤ
∈ V |
32 | 4 | fvexi 6780 |
. . . . 5
⊢ 𝐵 ∈ V |
33 | | snex 5352 |
. . . . . 6
⊢ { 0 } ∈
V |
34 | 15 | fvexi 6780 |
. . . . . . . . 9
⊢ + ∈
V |
35 | 34 | rnex 7749 |
. . . . . . . 8
⊢ ran + ∈
V |
36 | 35, 32 | unex 7586 |
. . . . . . 7
⊢ (ran
+ ∪
𝐵) ∈
V |
37 | 22 | fvexi 6780 |
. . . . . . . . 9
⊢ 𝐼 ∈ V |
38 | 37 | rnex 7749 |
. . . . . . . 8
⊢ ran 𝐼 ∈ V |
39 | | p0ex 5305 |
. . . . . . . 8
⊢ {∅}
∈ V |
40 | 38, 39 | unex 7586 |
. . . . . . 7
⊢ (ran
𝐼 ∪ {∅}) ∈
V |
41 | 36, 40 | unex 7586 |
. . . . . 6
⊢ ((ran
+ ∪
𝐵) ∪ (ran 𝐼 ∪ {∅})) ∈
V |
42 | 33, 41 | unex 7586 |
. . . . 5
⊢ ({ 0 } ∪ ((ran
+ ∪
𝐵) ∪ (ran 𝐼 ∪ {∅}))) ∈
V |
43 | | ssun1 4105 |
. . . . . . . . 9
⊢ { 0 } ⊆ ({
0 } ∪
((ran +
∪ 𝐵) ∪ (ran 𝐼 ∪
{∅}))) |
44 | 7 | fvexi 6780 |
. . . . . . . . . 10
⊢ 0 ∈
V |
45 | 44 | snid 4597 |
. . . . . . . . 9
⊢ 0 ∈ {
0
} |
46 | 43, 45 | sselii 3917 |
. . . . . . . 8
⊢ 0 ∈ ({
0 } ∪
((ran +
∪ 𝐵) ∪ (ran 𝐼 ∪
{∅}))) |
47 | 46 | a1i 11 |
. . . . . . 7
⊢ ((𝑛 ∈ ℤ ∧ 𝑥 ∈ 𝐵) → 0 ∈ ({ 0 } ∪ ((ran
+ ∪
𝐵) ∪ (ran 𝐼 ∪
{∅})))) |
48 | | ssun2 4106 |
. . . . . . . . . . . . . 14
⊢ 𝐵 ⊆ (ran + ∪ 𝐵) |
49 | | ssun1 4105 |
. . . . . . . . . . . . . 14
⊢ (ran
+ ∪
𝐵) ⊆ ((ran + ∪ 𝐵) ∪ (ran 𝐼 ∪ {∅})) |
50 | 48, 49 | sstri 3929 |
. . . . . . . . . . . . 13
⊢ 𝐵 ⊆ ((ran + ∪ 𝐵) ∪ (ran 𝐼 ∪ {∅})) |
51 | | ssun2 4106 |
. . . . . . . . . . . . 13
⊢ ((ran
+ ∪
𝐵) ∪ (ran 𝐼 ∪ {∅})) ⊆ ({
0 } ∪
((ran +
∪ 𝐵) ∪ (ran 𝐼 ∪
{∅}))) |
52 | 50, 51 | sstri 3929 |
. . . . . . . . . . . 12
⊢ 𝐵 ⊆ ({ 0 } ∪ ((ran + ∪ 𝐵) ∪ (ran 𝐼 ∪ {∅}))) |
53 | | fveq2 6766 |
. . . . . . . . . . . . . 14
⊢ (𝑛 = 1 → (seq1( + , (ℕ
× {𝑥}))‘𝑛) = (seq1( + , (ℕ × {𝑥}))‘1)) |
54 | 53 | adantl 482 |
. . . . . . . . . . . . 13
⊢ ((𝑥 ∈ 𝐵 ∧ 𝑛 = 1) → (seq1( + , (ℕ × {𝑥}))‘𝑛) = (seq1( + , (ℕ × {𝑥}))‘1)) |
55 | | seq1 13744 |
. . . . . . . . . . . . . . . 16
⊢ (1 ∈
ℤ → (seq1( + , (ℕ × {𝑥}))‘1) = ((ℕ ×
{𝑥})‘1)) |
56 | 10, 55 | ax-mp 5 |
. . . . . . . . . . . . . . 15
⊢ (seq1(
+ ,
(ℕ × {𝑥}))‘1) = ((ℕ × {𝑥})‘1) |
57 | | 1nn 11994 |
. . . . . . . . . . . . . . . . . 18
⊢ 1 ∈
ℕ |
58 | | vex 3433 |
. . . . . . . . . . . . . . . . . . 19
⊢ 𝑥 ∈ V |
59 | 58 | fvconst2 7071 |
. . . . . . . . . . . . . . . . . 18
⊢ (1 ∈
ℕ → ((ℕ × {𝑥})‘1) = 𝑥) |
60 | 57, 59 | ax-mp 5 |
. . . . . . . . . . . . . . . . 17
⊢ ((ℕ
× {𝑥})‘1) =
𝑥 |
61 | 60 | eleq1i 2829 |
. . . . . . . . . . . . . . . 16
⊢
(((ℕ × {𝑥})‘1) ∈ 𝐵 ↔ 𝑥 ∈ 𝐵) |
62 | 61 | biimpri 227 |
. . . . . . . . . . . . . . 15
⊢ (𝑥 ∈ 𝐵 → ((ℕ × {𝑥})‘1) ∈ 𝐵) |
63 | 56, 62 | eqeltrid 2843 |
. . . . . . . . . . . . . 14
⊢ (𝑥 ∈ 𝐵 → (seq1( + , (ℕ × {𝑥}))‘1) ∈ 𝐵) |
64 | 63 | adantr 481 |
. . . . . . . . . . . . 13
⊢ ((𝑥 ∈ 𝐵 ∧ 𝑛 = 1) → (seq1( + , (ℕ × {𝑥}))‘1) ∈ 𝐵) |
65 | 54, 64 | eqeltrd 2839 |
. . . . . . . . . . . 12
⊢ ((𝑥 ∈ 𝐵 ∧ 𝑛 = 1) → (seq1( + , (ℕ × {𝑥}))‘𝑛) ∈ 𝐵) |
66 | 52, 65 | sselid 3918 |
. . . . . . . . . . 11
⊢ ((𝑥 ∈ 𝐵 ∧ 𝑛 = 1) → (seq1( + , (ℕ × {𝑥}))‘𝑛) ∈ ({ 0 } ∪ ((ran + ∪ 𝐵) ∪ (ran 𝐼 ∪ {∅})))) |
67 | 66 | ad4ant24 751 |
. . . . . . . . . 10
⊢ ((((𝑛 ∈ ℤ ∧ 𝑥 ∈ 𝐵) ∧ 𝑛 ∈ (ℤ≥‘1))
∧ 𝑛 = 1) → (seq1(
+ ,
(ℕ × {𝑥}))‘𝑛) ∈ ({ 0 } ∪ ((ran + ∪ 𝐵) ∪ (ran 𝐼 ∪ {∅})))) |
68 | | zcn 12334 |
. . . . . . . . . . . . . . 15
⊢ (𝑛 ∈ ℤ → 𝑛 ∈
ℂ) |
69 | | npcan1 11410 |
. . . . . . . . . . . . . . 15
⊢ (𝑛 ∈ ℂ → ((𝑛 − 1) + 1) = 𝑛) |
70 | 68, 69 | syl 17 |
. . . . . . . . . . . . . 14
⊢ (𝑛 ∈ ℤ → ((𝑛 − 1) + 1) = 𝑛) |
71 | 70 | fveq2d 6770 |
. . . . . . . . . . . . 13
⊢ (𝑛 ∈ ℤ → (seq1(
+ ,
(ℕ × {𝑥}))‘((𝑛 − 1) + 1)) = (seq1( + , (ℕ × {𝑥}))‘𝑛)) |
72 | 71 | adantr 481 |
. . . . . . . . . . . 12
⊢ ((𝑛 ∈ ℤ ∧ (𝑛 − 1) ∈
(ℤ≥‘1)) → (seq1( + , (ℕ × {𝑥}))‘((𝑛 − 1) + 1)) = (seq1( + , (ℕ × {𝑥}))‘𝑛)) |
73 | | seqp1 13746 |
. . . . . . . . . . . . . 14
⊢ ((𝑛 − 1) ∈
(ℤ≥‘1) → (seq1( + , (ℕ × {𝑥}))‘((𝑛 − 1) + 1)) = ((seq1( + , (ℕ
× {𝑥}))‘(𝑛 − 1)) + ((ℕ × {𝑥})‘((𝑛 − 1) + 1)))) |
74 | | ssun1 4105 |
. . . . . . . . . . . . . . . . 17
⊢ ran + ⊆ (ran
+ ∪
𝐵) |
75 | | ssun2 4106 |
. . . . . . . . . . . . . . . . 17
⊢ {∅}
⊆ (ran 𝐼 ∪
{∅}) |
76 | | unss12 4115 |
. . . . . . . . . . . . . . . . 17
⊢ ((ran
+ ⊆
(ran +
∪ 𝐵) ∧ {∅}
⊆ (ran 𝐼 ∪
{∅})) → (ran + ∪ {∅}) ⊆
((ran +
∪ 𝐵) ∪ (ran 𝐼 ∪
{∅}))) |
77 | 74, 75, 76 | mp2an 689 |
. . . . . . . . . . . . . . . 16
⊢ (ran
+ ∪
{∅}) ⊆ ((ran + ∪ 𝐵) ∪ (ran 𝐼 ∪ {∅})) |
78 | 77, 51 | sstri 3929 |
. . . . . . . . . . . . . . 15
⊢ (ran
+ ∪
{∅}) ⊆ ({ 0 } ∪ ((ran + ∪ 𝐵) ∪ (ran 𝐼 ∪ {∅}))) |
79 | | df-ov 7270 |
. . . . . . . . . . . . . . . 16
⊢ ((seq1(
+ ,
(ℕ × {𝑥}))‘(𝑛 − 1)) + ((ℕ × {𝑥})‘((𝑛 − 1) + 1))) = ( + ‘〈(seq1( + , (ℕ
× {𝑥}))‘(𝑛 − 1)), ((ℕ ×
{𝑥})‘((𝑛 − 1) +
1))〉) |
80 | | fvrn0 6794 |
. . . . . . . . . . . . . . . 16
⊢ ( +
‘〈(seq1( + , (ℕ × {𝑥}))‘(𝑛 − 1)), ((ℕ × {𝑥})‘((𝑛 − 1) + 1))〉) ∈ (ran + ∪
{∅}) |
81 | 79, 80 | eqeltri 2835 |
. . . . . . . . . . . . . . 15
⊢ ((seq1(
+ ,
(ℕ × {𝑥}))‘(𝑛 − 1)) + ((ℕ × {𝑥})‘((𝑛 − 1) + 1))) ∈ (ran + ∪
{∅}) |
82 | 78, 81 | sselii 3917 |
. . . . . . . . . . . . . 14
⊢ ((seq1(
+ ,
(ℕ × {𝑥}))‘(𝑛 − 1)) + ((ℕ × {𝑥})‘((𝑛 − 1) + 1))) ∈ ({ 0 } ∪ ((ran
+ ∪
𝐵) ∪ (ran 𝐼 ∪
{∅}))) |
83 | 73, 82 | eqeltrdi 2847 |
. . . . . . . . . . . . 13
⊢ ((𝑛 − 1) ∈
(ℤ≥‘1) → (seq1( + , (ℕ × {𝑥}))‘((𝑛 − 1) + 1)) ∈ ({ 0 } ∪ ((ran
+ ∪
𝐵) ∪ (ran 𝐼 ∪
{∅})))) |
84 | 83 | adantl 482 |
. . . . . . . . . . . 12
⊢ ((𝑛 ∈ ℤ ∧ (𝑛 − 1) ∈
(ℤ≥‘1)) → (seq1( + , (ℕ × {𝑥}))‘((𝑛 − 1) + 1)) ∈ ({ 0 } ∪ ((ran
+ ∪
𝐵) ∪ (ran 𝐼 ∪
{∅})))) |
85 | 72, 84 | eqeltrrd 2840 |
. . . . . . . . . . 11
⊢ ((𝑛 ∈ ℤ ∧ (𝑛 − 1) ∈
(ℤ≥‘1)) → (seq1( + , (ℕ × {𝑥}))‘𝑛) ∈ ({ 0 } ∪ ((ran + ∪ 𝐵) ∪ (ran 𝐼 ∪ {∅})))) |
86 | 85 | ad4ant14 749 |
. . . . . . . . . 10
⊢ ((((𝑛 ∈ ℤ ∧ 𝑥 ∈ 𝐵) ∧ 𝑛 ∈ (ℤ≥‘1))
∧ (𝑛 − 1) ∈
(ℤ≥‘1)) → (seq1( + , (ℕ × {𝑥}))‘𝑛) ∈ ({ 0 } ∪ ((ran + ∪ 𝐵) ∪ (ran 𝐼 ∪ {∅})))) |
87 | | uzm1 12626 |
. . . . . . . . . . 11
⊢ (𝑛 ∈
(ℤ≥‘1) → (𝑛 = 1 ∨ (𝑛 − 1) ∈
(ℤ≥‘1))) |
88 | 87 | adantl 482 |
. . . . . . . . . 10
⊢ (((𝑛 ∈ ℤ ∧ 𝑥 ∈ 𝐵) ∧ 𝑛 ∈ (ℤ≥‘1))
→ (𝑛 = 1 ∨ (𝑛 − 1) ∈
(ℤ≥‘1))) |
89 | 67, 86, 88 | mpjaodan 956 |
. . . . . . . . 9
⊢ (((𝑛 ∈ ℤ ∧ 𝑥 ∈ 𝐵) ∧ 𝑛 ∈ (ℤ≥‘1))
→ (seq1( + , (ℕ × {𝑥}))‘𝑛) ∈ ({ 0 } ∪ ((ran + ∪ 𝐵) ∪ (ran 𝐼 ∪ {∅})))) |
90 | | simpr 485 |
. . . . . . . . . . . 12
⊢ (((𝑛 ∈ ℤ ∧ 𝑥 ∈ 𝐵) ∧ ¬ 𝑛 ∈ (ℤ≥‘1))
→ ¬ 𝑛 ∈
(ℤ≥‘1)) |
91 | | seqfn 13743 |
. . . . . . . . . . . . . . 15
⊢ (1 ∈
ℤ → seq1( + , (ℕ × {𝑥})) Fn
(ℤ≥‘1)) |
92 | 10, 91 | ax-mp 5 |
. . . . . . . . . . . . . 14
⊢ seq1(
+ ,
(ℕ × {𝑥})) Fn
(ℤ≥‘1) |
93 | 92 | fndmi 6529 |
. . . . . . . . . . . . 13
⊢ dom seq1(
+ ,
(ℕ × {𝑥})) =
(ℤ≥‘1) |
94 | 93 | eleq2i 2830 |
. . . . . . . . . . . 12
⊢ (𝑛 ∈ dom seq1( + , (ℕ
× {𝑥})) ↔ 𝑛 ∈
(ℤ≥‘1)) |
95 | 90, 94 | sylnibr 329 |
. . . . . . . . . . 11
⊢ (((𝑛 ∈ ℤ ∧ 𝑥 ∈ 𝐵) ∧ ¬ 𝑛 ∈ (ℤ≥‘1))
→ ¬ 𝑛 ∈ dom
seq1( + ,
(ℕ × {𝑥}))) |
96 | | ndmfv 6796 |
. . . . . . . . . . 11
⊢ (¬
𝑛 ∈ dom seq1( + , (ℕ
× {𝑥})) → (seq1(
+ ,
(ℕ × {𝑥}))‘𝑛) = ∅) |
97 | 95, 96 | syl 17 |
. . . . . . . . . 10
⊢ (((𝑛 ∈ ℤ ∧ 𝑥 ∈ 𝐵) ∧ ¬ 𝑛 ∈ (ℤ≥‘1))
→ (seq1( + , (ℕ × {𝑥}))‘𝑛) = ∅) |
98 | | ssun2 4106 |
. . . . . . . . . . . . . 14
⊢ (ran
𝐼 ∪ {∅}) ⊆
((ran +
∪ 𝐵) ∪ (ran 𝐼 ∪
{∅})) |
99 | 75, 98 | sstri 3929 |
. . . . . . . . . . . . 13
⊢ {∅}
⊆ ((ran + ∪ 𝐵) ∪ (ran 𝐼 ∪ {∅})) |
100 | 99, 51 | sstri 3929 |
. . . . . . . . . . . 12
⊢ {∅}
⊆ ({ 0 } ∪ ((ran + ∪ 𝐵) ∪ (ran 𝐼 ∪ {∅}))) |
101 | | 0ex 5229 |
. . . . . . . . . . . . 13
⊢ ∅
∈ V |
102 | 101 | snid 4597 |
. . . . . . . . . . . 12
⊢ ∅
∈ {∅} |
103 | 100, 102 | sselii 3917 |
. . . . . . . . . . 11
⊢ ∅
∈ ({ 0 } ∪ ((ran + ∪ 𝐵) ∪ (ran 𝐼 ∪ {∅}))) |
104 | 103 | a1i 11 |
. . . . . . . . . 10
⊢ (((𝑛 ∈ ℤ ∧ 𝑥 ∈ 𝐵) ∧ ¬ 𝑛 ∈ (ℤ≥‘1))
→ ∅ ∈ ({ 0 } ∪ ((ran + ∪ 𝐵) ∪ (ran 𝐼 ∪ {∅})))) |
105 | 97, 104 | eqeltrd 2839 |
. . . . . . . . 9
⊢ (((𝑛 ∈ ℤ ∧ 𝑥 ∈ 𝐵) ∧ ¬ 𝑛 ∈ (ℤ≥‘1))
→ (seq1( + , (ℕ × {𝑥}))‘𝑛) ∈ ({ 0 } ∪ ((ran + ∪ 𝐵) ∪ (ran 𝐼 ∪ {∅})))) |
106 | 89, 105 | pm2.61dan 810 |
. . . . . . . 8
⊢ ((𝑛 ∈ ℤ ∧ 𝑥 ∈ 𝐵) → (seq1( + , (ℕ × {𝑥}))‘𝑛) ∈ ({ 0 } ∪ ((ran + ∪ 𝐵) ∪ (ran 𝐼 ∪ {∅})))) |
107 | 98, 51 | sstri 3929 |
. . . . . . . . . 10
⊢ (ran
𝐼 ∪ {∅}) ⊆
({ 0 }
∪ ((ran + ∪ 𝐵) ∪ (ran 𝐼 ∪ {∅}))) |
108 | | fvrn0 6794 |
. . . . . . . . . 10
⊢ (𝐼‘(seq1( + , (ℕ × {𝑥}))‘-𝑛)) ∈ (ran 𝐼 ∪ {∅}) |
109 | 107, 108 | sselii 3917 |
. . . . . . . . 9
⊢ (𝐼‘(seq1( + , (ℕ × {𝑥}))‘-𝑛)) ∈ ({ 0 } ∪ ((ran + ∪ 𝐵) ∪ (ran 𝐼 ∪ {∅}))) |
110 | 109 | a1i 11 |
. . . . . . . 8
⊢ ((𝑛 ∈ ℤ ∧ 𝑥 ∈ 𝐵) → (𝐼‘(seq1( + , (ℕ × {𝑥}))‘-𝑛)) ∈ ({ 0 } ∪ ((ran + ∪ 𝐵) ∪ (ran 𝐼 ∪ {∅})))) |
111 | 106, 110 | ifcld 4505 |
. . . . . . 7
⊢ ((𝑛 ∈ ℤ ∧ 𝑥 ∈ 𝐵) → if(0 < 𝑛, (seq1( + , (ℕ × {𝑥}))‘𝑛), (𝐼‘(seq1( + , (ℕ × {𝑥}))‘-𝑛))) ∈ ({ 0 } ∪ ((ran + ∪ 𝐵) ∪ (ran 𝐼 ∪ {∅})))) |
112 | 47, 111 | ifcld 4505 |
. . . . . 6
⊢ ((𝑛 ∈ ℤ ∧ 𝑥 ∈ 𝐵) → if(𝑛 = 0, 0 , if(0 < 𝑛, (seq1( + , (ℕ × {𝑥}))‘𝑛), (𝐼‘(seq1( + , (ℕ × {𝑥}))‘-𝑛)))) ∈ ({ 0 } ∪ ((ran + ∪ 𝐵) ∪ (ran 𝐼 ∪ {∅})))) |
113 | 112 | rgen2 3127 |
. . . . 5
⊢
∀𝑛 ∈
ℤ ∀𝑥 ∈
𝐵 if(𝑛 = 0, 0 , if(0 < 𝑛, (seq1( + , (ℕ × {𝑥}))‘𝑛), (𝐼‘(seq1( + , (ℕ × {𝑥}))‘-𝑛)))) ∈ ({ 0 } ∪ ((ran + ∪ 𝐵) ∪ (ran 𝐼 ∪ {∅}))) |
114 | 31, 32, 42, 113 | mpoexw 7908 |
. . . 4
⊢ (𝑛 ∈ ℤ, 𝑥 ∈ 𝐵 ↦ if(𝑛 = 0, 0 , if(0 < 𝑛, (seq1( + , (ℕ × {𝑥}))‘𝑛), (𝐼‘(seq1( + , (ℕ × {𝑥}))‘-𝑛))))) ∈ V |
115 | 29, 30, 114 | fvmpt 6867 |
. . 3
⊢ (𝐺 ∈ V →
(.g‘𝐺) =
(𝑛 ∈ ℤ, 𝑥 ∈ 𝐵 ↦ if(𝑛 = 0, 0 , if(0 < 𝑛, (seq1( + , (ℕ × {𝑥}))‘𝑛), (𝐼‘(seq1( + , (ℕ × {𝑥}))‘-𝑛)))))) |
116 | | fvprc 6758 |
. . . 4
⊢ (¬
𝐺 ∈ V →
(.g‘𝐺) =
∅) |
117 | | eqid 2738 |
. . . . . . 7
⊢ (𝑛 ∈ ℤ, 𝑥 ∈ 𝐵 ↦ if(𝑛 = 0, 0 , if(0 < 𝑛, (seq1( + , (ℕ × {𝑥}))‘𝑛), (𝐼‘(seq1( + , (ℕ × {𝑥}))‘-𝑛))))) = (𝑛 ∈ ℤ, 𝑥 ∈ 𝐵 ↦ if(𝑛 = 0, 0 , if(0 < 𝑛, (seq1( + , (ℕ × {𝑥}))‘𝑛), (𝐼‘(seq1( + , (ℕ × {𝑥}))‘-𝑛))))) |
118 | | fvex 6779 |
. . . . . . . . 9
⊢ (seq1(
+ ,
(ℕ × {𝑥}))‘𝑛) ∈ V |
119 | | fvex 6779 |
. . . . . . . . 9
⊢ (𝐼‘(seq1( + , (ℕ × {𝑥}))‘-𝑛)) ∈ V |
120 | 118, 119 | ifex 4509 |
. . . . . . . 8
⊢ if(0 <
𝑛, (seq1( + , (ℕ
× {𝑥}))‘𝑛), (𝐼‘(seq1( + , (ℕ × {𝑥}))‘-𝑛))) ∈ V |
121 | 44, 120 | ifex 4509 |
. . . . . . 7
⊢ if(𝑛 = 0, 0 , if(0 < 𝑛, (seq1( + , (ℕ × {𝑥}))‘𝑛), (𝐼‘(seq1( + , (ℕ × {𝑥}))‘-𝑛)))) ∈ V |
122 | 117, 121 | fnmpoi 7899 |
. . . . . 6
⊢ (𝑛 ∈ ℤ, 𝑥 ∈ 𝐵 ↦ if(𝑛 = 0, 0 , if(0 < 𝑛, (seq1( + , (ℕ × {𝑥}))‘𝑛), (𝐼‘(seq1( + , (ℕ × {𝑥}))‘-𝑛))))) Fn (ℤ × 𝐵) |
123 | | fvprc 6758 |
. . . . . . . . . 10
⊢ (¬
𝐺 ∈ V →
(Base‘𝐺) =
∅) |
124 | 4, 123 | eqtrid 2790 |
. . . . . . . . 9
⊢ (¬
𝐺 ∈ V → 𝐵 = ∅) |
125 | 124 | xpeq2d 5614 |
. . . . . . . 8
⊢ (¬
𝐺 ∈ V → (ℤ
× 𝐵) = (ℤ
× ∅)) |
126 | | xp0 6054 |
. . . . . . . 8
⊢ (ℤ
× ∅) = ∅ |
127 | 125, 126 | eqtrdi 2794 |
. . . . . . 7
⊢ (¬
𝐺 ∈ V → (ℤ
× 𝐵) =
∅) |
128 | 127 | fneq2d 6519 |
. . . . . 6
⊢ (¬
𝐺 ∈ V → ((𝑛 ∈ ℤ, 𝑥 ∈ 𝐵 ↦ if(𝑛 = 0, 0 , if(0 < 𝑛, (seq1( + , (ℕ × {𝑥}))‘𝑛), (𝐼‘(seq1( + , (ℕ × {𝑥}))‘-𝑛))))) Fn (ℤ × 𝐵) ↔ (𝑛 ∈ ℤ, 𝑥 ∈ 𝐵 ↦ if(𝑛 = 0, 0 , if(0 < 𝑛, (seq1( + , (ℕ × {𝑥}))‘𝑛), (𝐼‘(seq1( + , (ℕ × {𝑥}))‘-𝑛))))) Fn ∅)) |
129 | 122, 128 | mpbii 232 |
. . . . 5
⊢ (¬
𝐺 ∈ V → (𝑛 ∈ ℤ, 𝑥 ∈ 𝐵 ↦ if(𝑛 = 0, 0 , if(0 < 𝑛, (seq1( + , (ℕ × {𝑥}))‘𝑛), (𝐼‘(seq1( + , (ℕ × {𝑥}))‘-𝑛))))) Fn ∅) |
130 | | fn0 6556 |
. . . . 5
⊢ ((𝑛 ∈ ℤ, 𝑥 ∈ 𝐵 ↦ if(𝑛 = 0, 0 , if(0 < 𝑛, (seq1( + , (ℕ × {𝑥}))‘𝑛), (𝐼‘(seq1( + , (ℕ × {𝑥}))‘-𝑛))))) Fn ∅ ↔ (𝑛 ∈ ℤ, 𝑥 ∈ 𝐵 ↦ if(𝑛 = 0, 0 , if(0 < 𝑛, (seq1( + , (ℕ × {𝑥}))‘𝑛), (𝐼‘(seq1( + , (ℕ × {𝑥}))‘-𝑛))))) = ∅) |
131 | 129, 130 | sylib 217 |
. . . 4
⊢ (¬
𝐺 ∈ V → (𝑛 ∈ ℤ, 𝑥 ∈ 𝐵 ↦ if(𝑛 = 0, 0 , if(0 < 𝑛, (seq1( + , (ℕ × {𝑥}))‘𝑛), (𝐼‘(seq1( + , (ℕ × {𝑥}))‘-𝑛))))) = ∅) |
132 | 116, 131 | eqtr4d 2781 |
. . 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 2766 |
1
⊢ · =
(𝑛 ∈ ℤ, 𝑥 ∈ 𝐵 ↦ if(𝑛 = 0, 0 , if(0 < 𝑛, (seq1( + , (ℕ × {𝑥}))‘𝑛), (𝐼‘(seq1( + , (ℕ × {𝑥}))‘-𝑛))))) |