| 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 | | seqex 14044 |
. . . . . . . 8
⊢
seq1((+g‘𝑤), (ℕ × {𝑥})) ∈ V |
| 10 | 9 | a1i 11 |
. . . . . . 7
⊢ (𝑤 = 𝐺 → seq1((+g‘𝑤), (ℕ × {𝑥})) ∈ V) |
| 11 | | id 22 |
. . . . . . . . . 10
⊢ (𝑠 =
seq1((+g‘𝑤), (ℕ × {𝑥})) → 𝑠 = seq1((+g‘𝑤), (ℕ × {𝑥}))) |
| 12 | | fveq2 6906 |
. . . . . . . . . . . 12
⊢ (𝑤 = 𝐺 → (+g‘𝑤) = (+g‘𝐺)) |
| 13 | | mulgval.p |
. . . . . . . . . . . 12
⊢ + =
(+g‘𝐺) |
| 14 | 12, 13 | eqtr4di 2795 |
. . . . . . . . . . 11
⊢ (𝑤 = 𝐺 → (+g‘𝑤) = + ) |
| 15 | 14 | seqeq2d 14049 |
. . . . . . . . . 10
⊢ (𝑤 = 𝐺 → seq1((+g‘𝑤), (ℕ × {𝑥})) = seq1( + , (ℕ × {𝑥}))) |
| 16 | 11, 15 | sylan9eqr 2799 |
. . . . . . . . 9
⊢ ((𝑤 = 𝐺 ∧ 𝑠 = seq1((+g‘𝑤), (ℕ × {𝑥}))) → 𝑠 = seq1( + , (ℕ × {𝑥}))) |
| 17 | 16 | fveq1d 6908 |
. . . . . . . 8
⊢ ((𝑤 = 𝐺 ∧ 𝑠 = seq1((+g‘𝑤), (ℕ × {𝑥}))) → (𝑠‘𝑛) = (seq1( + , (ℕ × {𝑥}))‘𝑛)) |
| 18 | | simpl 482 |
. . . . . . . . . . 11
⊢ ((𝑤 = 𝐺 ∧ 𝑠 = seq1((+g‘𝑤), (ℕ × {𝑥}))) → 𝑤 = 𝐺) |
| 19 | 18 | fveq2d 6910 |
. . . . . . . . . 10
⊢ ((𝑤 = 𝐺 ∧ 𝑠 = seq1((+g‘𝑤), (ℕ × {𝑥}))) →
(invg‘𝑤) =
(invg‘𝐺)) |
| 20 | | mulgval.i |
. . . . . . . . . 10
⊢ 𝐼 = (invg‘𝐺) |
| 21 | 19, 20 | eqtr4di 2795 |
. . . . . . . . 9
⊢ ((𝑤 = 𝐺 ∧ 𝑠 = seq1((+g‘𝑤), (ℕ × {𝑥}))) →
(invg‘𝑤) =
𝐼) |
| 22 | 16 | fveq1d 6908 |
. . . . . . . . 9
⊢ ((𝑤 = 𝐺 ∧ 𝑠 = seq1((+g‘𝑤), (ℕ × {𝑥}))) → (𝑠‘-𝑛) = (seq1( + , (ℕ × {𝑥}))‘-𝑛)) |
| 23 | 21, 22 | fveq12d 6913 |
. . . . . . . 8
⊢ ((𝑤 = 𝐺 ∧ 𝑠 = seq1((+g‘𝑤), (ℕ × {𝑥}))) →
((invg‘𝑤)‘(𝑠‘-𝑛)) = (𝐼‘(seq1( + , (ℕ × {𝑥}))‘-𝑛))) |
| 24 | 17, 23 | ifeq12d 4547 |
. . . . . . 7
⊢ ((𝑤 = 𝐺 ∧ 𝑠 = seq1((+g‘𝑤), (ℕ × {𝑥}))) → if(0 < 𝑛, (𝑠‘𝑛), ((invg‘𝑤)‘(𝑠‘-𝑛))) = if(0 < 𝑛, (seq1( + , (ℕ × {𝑥}))‘𝑛), (𝐼‘(seq1( + , (ℕ × {𝑥}))‘-𝑛)))) |
| 25 | 10, 24 | csbied 3935 |
. . . . . 6
⊢ (𝑤 = 𝐺 →
⦋seq1((+g‘𝑤), (ℕ × {𝑥})) / 𝑠⦌if(0 < 𝑛, (𝑠‘𝑛), ((invg‘𝑤)‘(𝑠‘-𝑛))) = if(0 < 𝑛, (seq1( + , (ℕ × {𝑥}))‘𝑛), (𝐼‘(seq1( + , (ℕ × {𝑥}))‘-𝑛)))) |
| 26 | 8, 25 | ifeq12d 4547 |
. . . . 5
⊢ (𝑤 = 𝐺 → if(𝑛 = 0, (0g‘𝑤),
⦋seq1((+g‘𝑤), (ℕ × {𝑥})) / 𝑠⦌if(0 < 𝑛, (𝑠‘𝑛), ((invg‘𝑤)‘(𝑠‘-𝑛)))) = if(𝑛 = 0, 0 , if(0 < 𝑛, (seq1( + , (ℕ × {𝑥}))‘𝑛), (𝐼‘(seq1( + , (ℕ × {𝑥}))‘-𝑛))))) |
| 27 | 2, 5, 26 | mpoeq123dv 7508 |
. . . 4
⊢ (𝑤 = 𝐺 → (𝑛 ∈ ℤ, 𝑥 ∈ (Base‘𝑤) ↦ if(𝑛 = 0, (0g‘𝑤),
⦋seq1((+g‘𝑤), (ℕ × {𝑥})) / 𝑠⦌if(0 < 𝑛, (𝑠‘𝑛), ((invg‘𝑤)‘(𝑠‘-𝑛))))) = (𝑛 ∈ ℤ, 𝑥 ∈ 𝐵 ↦ if(𝑛 = 0, 0 , if(0 < 𝑛, (seq1( + , (ℕ × {𝑥}))‘𝑛), (𝐼‘(seq1( + , (ℕ × {𝑥}))‘-𝑛)))))) |
| 28 | | df-mulg 19086 |
. . . 4
⊢
.g = (𝑤
∈ V ↦ (𝑛 ∈
ℤ, 𝑥 ∈
(Base‘𝑤) ↦
if(𝑛 = 0,
(0g‘𝑤),
⦋seq1((+g‘𝑤), (ℕ × {𝑥})) / 𝑠⦌if(0 < 𝑛, (𝑠‘𝑛), ((invg‘𝑤)‘(𝑠‘-𝑛)))))) |
| 29 | | zex 12622 |
. . . . 5
⊢ ℤ
∈ V |
| 30 | 4 | fvexi 6920 |
. . . . 5
⊢ 𝐵 ∈ V |
| 31 | 29, 30 | mpoex 8104 |
. . . 4
⊢ (𝑛 ∈ ℤ, 𝑥 ∈ 𝐵 ↦ if(𝑛 = 0, 0 , if(0 < 𝑛, (seq1( + , (ℕ × {𝑥}))‘𝑛), (𝐼‘(seq1( + , (ℕ × {𝑥}))‘-𝑛))))) ∈ V |
| 32 | 27, 28, 31 | fvmpt 7016 |
. . 3
⊢ (𝐺 ∈ V →
(.g‘𝐺) =
(𝑛 ∈ ℤ, 𝑥 ∈ 𝐵 ↦ if(𝑛 = 0, 0 , if(0 < 𝑛, (seq1( + , (ℕ × {𝑥}))‘𝑛), (𝐼‘(seq1( + , (ℕ × {𝑥}))‘-𝑛)))))) |
| 33 | | fvprc 6898 |
. . . 4
⊢ (¬
𝐺 ∈ V →
(.g‘𝐺) =
∅) |
| 34 | | eqid 2737 |
. . . . . . 7
⊢ (𝑛 ∈ ℤ, 𝑥 ∈ 𝐵 ↦ if(𝑛 = 0, 0 , if(0 < 𝑛, (seq1( + , (ℕ × {𝑥}))‘𝑛), (𝐼‘(seq1( + , (ℕ × {𝑥}))‘-𝑛))))) = (𝑛 ∈ ℤ, 𝑥 ∈ 𝐵 ↦ if(𝑛 = 0, 0 , if(0 < 𝑛, (seq1( + , (ℕ × {𝑥}))‘𝑛), (𝐼‘(seq1( + , (ℕ × {𝑥}))‘-𝑛))))) |
| 35 | 7 | fvexi 6920 |
. . . . . . . 8
⊢ 0 ∈
V |
| 36 | | fvex 6919 |
. . . . . . . . 9
⊢ (seq1(
+ ,
(ℕ × {𝑥}))‘𝑛) ∈ V |
| 37 | | fvex 6919 |
. . . . . . . . 9
⊢ (𝐼‘(seq1( + , (ℕ × {𝑥}))‘-𝑛)) ∈ V |
| 38 | 36, 37 | ifex 4576 |
. . . . . . . 8
⊢ if(0 <
𝑛, (seq1( + , (ℕ
× {𝑥}))‘𝑛), (𝐼‘(seq1( + , (ℕ × {𝑥}))‘-𝑛))) ∈ V |
| 39 | 35, 38 | ifex 4576 |
. . . . . . 7
⊢ if(𝑛 = 0, 0 , if(0 < 𝑛, (seq1( + , (ℕ × {𝑥}))‘𝑛), (𝐼‘(seq1( + , (ℕ × {𝑥}))‘-𝑛)))) ∈ V |
| 40 | 34, 39 | fnmpoi 8095 |
. . . . . 6
⊢ (𝑛 ∈ ℤ, 𝑥 ∈ 𝐵 ↦ if(𝑛 = 0, 0 , if(0 < 𝑛, (seq1( + , (ℕ × {𝑥}))‘𝑛), (𝐼‘(seq1( + , (ℕ × {𝑥}))‘-𝑛))))) Fn (ℤ × 𝐵) |
| 41 | | fvprc 6898 |
. . . . . . . . . 10
⊢ (¬
𝐺 ∈ V →
(Base‘𝐺) =
∅) |
| 42 | 4, 41 | eqtrid 2789 |
. . . . . . . . 9
⊢ (¬
𝐺 ∈ V → 𝐵 = ∅) |
| 43 | 42 | xpeq2d 5715 |
. . . . . . . 8
⊢ (¬
𝐺 ∈ V → (ℤ
× 𝐵) = (ℤ
× ∅)) |
| 44 | | xp0 6178 |
. . . . . . . 8
⊢ (ℤ
× ∅) = ∅ |
| 45 | 43, 44 | eqtrdi 2793 |
. . . . . . 7
⊢ (¬
𝐺 ∈ V → (ℤ
× 𝐵) =
∅) |
| 46 | 45 | fneq2d 6662 |
. . . . . 6
⊢ (¬
𝐺 ∈ V → ((𝑛 ∈ ℤ, 𝑥 ∈ 𝐵 ↦ if(𝑛 = 0, 0 , if(0 < 𝑛, (seq1( + , (ℕ × {𝑥}))‘𝑛), (𝐼‘(seq1( + , (ℕ × {𝑥}))‘-𝑛))))) Fn (ℤ × 𝐵) ↔ (𝑛 ∈ ℤ, 𝑥 ∈ 𝐵 ↦ if(𝑛 = 0, 0 , if(0 < 𝑛, (seq1( + , (ℕ × {𝑥}))‘𝑛), (𝐼‘(seq1( + , (ℕ × {𝑥}))‘-𝑛))))) Fn ∅)) |
| 47 | 40, 46 | mpbii 233 |
. . . . 5
⊢ (¬
𝐺 ∈ V → (𝑛 ∈ ℤ, 𝑥 ∈ 𝐵 ↦ if(𝑛 = 0, 0 , if(0 < 𝑛, (seq1( + , (ℕ × {𝑥}))‘𝑛), (𝐼‘(seq1( + , (ℕ × {𝑥}))‘-𝑛))))) Fn ∅) |
| 48 | | fn0 6699 |
. . . . 5
⊢ ((𝑛 ∈ ℤ, 𝑥 ∈ 𝐵 ↦ if(𝑛 = 0, 0 , if(0 < 𝑛, (seq1( + , (ℕ × {𝑥}))‘𝑛), (𝐼‘(seq1( + , (ℕ × {𝑥}))‘-𝑛))))) Fn ∅ ↔ (𝑛 ∈ ℤ, 𝑥 ∈ 𝐵 ↦ if(𝑛 = 0, 0 , if(0 < 𝑛, (seq1( + , (ℕ × {𝑥}))‘𝑛), (𝐼‘(seq1( + , (ℕ × {𝑥}))‘-𝑛))))) = ∅) |
| 49 | 47, 48 | sylib 218 |
. . . 4
⊢ (¬
𝐺 ∈ V → (𝑛 ∈ ℤ, 𝑥 ∈ 𝐵 ↦ if(𝑛 = 0, 0 , if(0 < 𝑛, (seq1( + , (ℕ × {𝑥}))‘𝑛), (𝐼‘(seq1( + , (ℕ × {𝑥}))‘-𝑛))))) = ∅) |
| 50 | 33, 49 | eqtr4d 2780 |
. . 3
⊢ (¬
𝐺 ∈ V →
(.g‘𝐺) =
(𝑛 ∈ ℤ, 𝑥 ∈ 𝐵 ↦ if(𝑛 = 0, 0 , if(0 < 𝑛, (seq1( + , (ℕ × {𝑥}))‘𝑛), (𝐼‘(seq1( + , (ℕ × {𝑥}))‘-𝑛)))))) |
| 51 | 32, 50 | pm2.61i 182 |
. 2
⊢
(.g‘𝐺) = (𝑛 ∈ ℤ, 𝑥 ∈ 𝐵 ↦ if(𝑛 = 0, 0 , if(0 < 𝑛, (seq1( + , (ℕ × {𝑥}))‘𝑛), (𝐼‘(seq1( + , (ℕ × {𝑥}))‘-𝑛))))) |
| 52 | 1, 51 | eqtri 2765 |
1
⊢ · =
(𝑛 ∈ ℤ, 𝑥 ∈ 𝐵 ↦ if(𝑛 = 0, 0 , if(0 < 𝑛, (seq1( + , (ℕ × {𝑥}))‘𝑛), (𝐼‘(seq1( + , (ℕ × {𝑥}))‘-𝑛))))) |