Step | Hyp | Ref
| Expression |
1 | | mulgpropd.b1 |
. . . . . . 7
⊢ (𝜑 → 𝐵 = (Base‘𝐺)) |
2 | | mulgpropd.b2 |
. . . . . . 7
⊢ (𝜑 → 𝐵 = (Base‘𝐻)) |
3 | | mulgpropdg.g |
. . . . . . 7
⊢ (𝜑 → 𝐺 ∈ 𝑉) |
4 | | mulgpropdg.h |
. . . . . . 7
⊢ (𝜑 → 𝐻 ∈ 𝑊) |
5 | | mulgpropd.i |
. . . . . . . . . 10
⊢ (𝜑 → 𝐵 ⊆ 𝐾) |
6 | | ssel 3149 |
. . . . . . . . . . 11
⊢ (𝐵 ⊆ 𝐾 → (𝑥 ∈ 𝐵 → 𝑥 ∈ 𝐾)) |
7 | | ssel 3149 |
. . . . . . . . . . 11
⊢ (𝐵 ⊆ 𝐾 → (𝑦 ∈ 𝐵 → 𝑦 ∈ 𝐾)) |
8 | 6, 7 | anim12d 335 |
. . . . . . . . . 10
⊢ (𝐵 ⊆ 𝐾 → ((𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵) → (𝑥 ∈ 𝐾 ∧ 𝑦 ∈ 𝐾))) |
9 | 5, 8 | syl 14 |
. . . . . . . . 9
⊢ (𝜑 → ((𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵) → (𝑥 ∈ 𝐾 ∧ 𝑦 ∈ 𝐾))) |
10 | 9 | imp 124 |
. . . . . . . 8
⊢ ((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) → (𝑥 ∈ 𝐾 ∧ 𝑦 ∈ 𝐾)) |
11 | | mulgpropd.e |
. . . . . . . 8
⊢ ((𝜑 ∧ (𝑥 ∈ 𝐾 ∧ 𝑦 ∈ 𝐾)) → (𝑥(+g‘𝐺)𝑦) = (𝑥(+g‘𝐻)𝑦)) |
12 | 10, 11 | syldan 282 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) → (𝑥(+g‘𝐺)𝑦) = (𝑥(+g‘𝐻)𝑦)) |
13 | 1, 2, 3, 4, 12 | grpidpropdg 12747 |
. . . . . 6
⊢ (𝜑 → (0g‘𝐺) = (0g‘𝐻)) |
14 | 13 | 3ad2ant1 1018 |
. . . . 5
⊢ ((𝜑 ∧ 𝑎 ∈ ℤ ∧ 𝑏 ∈ 𝐵) → (0g‘𝐺) = (0g‘𝐻)) |
15 | | 1zzd 9278 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑎 ∈ ℤ ∧ 𝑏 ∈ 𝐵) → 1 ∈ ℤ) |
16 | | nnuz 9561 |
. . . . . . . . 9
⊢ ℕ =
(ℤ≥‘1) |
17 | 5 | 3ad2ant1 1018 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑎 ∈ ℤ ∧ 𝑏 ∈ 𝐵) → 𝐵 ⊆ 𝐾) |
18 | | simp3 999 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑎 ∈ ℤ ∧ 𝑏 ∈ 𝐵) → 𝑏 ∈ 𝐵) |
19 | 17, 18 | sseldd 3156 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑎 ∈ ℤ ∧ 𝑏 ∈ 𝐵) → 𝑏 ∈ 𝐾) |
20 | 16, 19 | ialgrlemconst 12037 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑎 ∈ ℤ ∧ 𝑏 ∈ 𝐵) ∧ 𝑥 ∈ (ℤ≥‘1))
→ ((ℕ × {𝑏})‘𝑥) ∈ 𝐾) |
21 | | mulgpropd.k |
. . . . . . . . 9
⊢ ((𝜑 ∧ (𝑥 ∈ 𝐾 ∧ 𝑦 ∈ 𝐾)) → (𝑥(+g‘𝐺)𝑦) ∈ 𝐾) |
22 | 21 | 3ad2antl1 1159 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑎 ∈ ℤ ∧ 𝑏 ∈ 𝐵) ∧ (𝑥 ∈ 𝐾 ∧ 𝑦 ∈ 𝐾)) → (𝑥(+g‘𝐺)𝑦) ∈ 𝐾) |
23 | 11 | 3ad2antl1 1159 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑎 ∈ ℤ ∧ 𝑏 ∈ 𝐵) ∧ (𝑥 ∈ 𝐾 ∧ 𝑦 ∈ 𝐾)) → (𝑥(+g‘𝐺)𝑦) = (𝑥(+g‘𝐻)𝑦)) |
24 | 15, 20, 22, 23 | seqfeq3 10509 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑎 ∈ ℤ ∧ 𝑏 ∈ 𝐵) → seq1((+g‘𝐺), (ℕ × {𝑏})) =
seq1((+g‘𝐻), (ℕ × {𝑏}))) |
25 | 24 | fveq1d 5517 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑎 ∈ ℤ ∧ 𝑏 ∈ 𝐵) → (seq1((+g‘𝐺), (ℕ × {𝑏}))‘𝑎) = (seq1((+g‘𝐻), (ℕ × {𝑏}))‘𝑎)) |
26 | 1, 2, 3, 4, 12 | grpinvpropdg 12899 |
. . . . . . . 8
⊢ (𝜑 →
(invg‘𝐺) =
(invg‘𝐻)) |
27 | 26 | 3ad2ant1 1018 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑎 ∈ ℤ ∧ 𝑏 ∈ 𝐵) → (invg‘𝐺) = (invg‘𝐻)) |
28 | 24 | fveq1d 5517 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑎 ∈ ℤ ∧ 𝑏 ∈ 𝐵) → (seq1((+g‘𝐺), (ℕ × {𝑏}))‘-𝑎) = (seq1((+g‘𝐻), (ℕ × {𝑏}))‘-𝑎)) |
29 | 27, 28 | fveq12d 5522 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑎 ∈ ℤ ∧ 𝑏 ∈ 𝐵) → ((invg‘𝐺)‘(seq1((+g‘𝐺), (ℕ × {𝑏}))‘-𝑎)) = ((invg‘𝐻)‘(seq1((+g‘𝐻), (ℕ × {𝑏}))‘-𝑎))) |
30 | 25, 29 | ifeq12d 3553 |
. . . . 5
⊢ ((𝜑 ∧ 𝑎 ∈ ℤ ∧ 𝑏 ∈ 𝐵) → if(0 < 𝑎, (seq1((+g‘𝐺), (ℕ × {𝑏}))‘𝑎), ((invg‘𝐺)‘(seq1((+g‘𝐺), (ℕ × {𝑏}))‘-𝑎))) = if(0 < 𝑎, (seq1((+g‘𝐻), (ℕ × {𝑏}))‘𝑎), ((invg‘𝐻)‘(seq1((+g‘𝐻), (ℕ × {𝑏}))‘-𝑎)))) |
31 | 14, 30 | ifeq12d 3553 |
. . . 4
⊢ ((𝜑 ∧ 𝑎 ∈ ℤ ∧ 𝑏 ∈ 𝐵) → if(𝑎 = 0, (0g‘𝐺), if(0 < 𝑎, (seq1((+g‘𝐺), (ℕ × {𝑏}))‘𝑎), ((invg‘𝐺)‘(seq1((+g‘𝐺), (ℕ × {𝑏}))‘-𝑎)))) = if(𝑎 = 0, (0g‘𝐻), if(0 < 𝑎, (seq1((+g‘𝐻), (ℕ × {𝑏}))‘𝑎), ((invg‘𝐻)‘(seq1((+g‘𝐻), (ℕ × {𝑏}))‘-𝑎))))) |
32 | 31 | mpoeq3dva 5938 |
. . 3
⊢ (𝜑 → (𝑎 ∈ ℤ, 𝑏 ∈ 𝐵 ↦ if(𝑎 = 0, (0g‘𝐺), if(0 < 𝑎, (seq1((+g‘𝐺), (ℕ × {𝑏}))‘𝑎), ((invg‘𝐺)‘(seq1((+g‘𝐺), (ℕ × {𝑏}))‘-𝑎))))) = (𝑎 ∈ ℤ, 𝑏 ∈ 𝐵 ↦ if(𝑎 = 0, (0g‘𝐻), if(0 < 𝑎, (seq1((+g‘𝐻), (ℕ × {𝑏}))‘𝑎), ((invg‘𝐻)‘(seq1((+g‘𝐻), (ℕ × {𝑏}))‘-𝑎)))))) |
33 | | eqidd 2178 |
. . . 4
⊢ (𝜑 → ℤ =
ℤ) |
34 | | eqidd 2178 |
. . . 4
⊢ (𝜑 → if(𝑎 = 0, (0g‘𝐺), if(0 < 𝑎, (seq1((+g‘𝐺), (ℕ × {𝑏}))‘𝑎), ((invg‘𝐺)‘(seq1((+g‘𝐺), (ℕ × {𝑏}))‘-𝑎)))) = if(𝑎 = 0, (0g‘𝐺), if(0 < 𝑎, (seq1((+g‘𝐺), (ℕ × {𝑏}))‘𝑎), ((invg‘𝐺)‘(seq1((+g‘𝐺), (ℕ × {𝑏}))‘-𝑎))))) |
35 | 33, 1, 34 | mpoeq123dv 5936 |
. . 3
⊢ (𝜑 → (𝑎 ∈ ℤ, 𝑏 ∈ 𝐵 ↦ if(𝑎 = 0, (0g‘𝐺), if(0 < 𝑎, (seq1((+g‘𝐺), (ℕ × {𝑏}))‘𝑎), ((invg‘𝐺)‘(seq1((+g‘𝐺), (ℕ × {𝑏}))‘-𝑎))))) = (𝑎 ∈ ℤ, 𝑏 ∈ (Base‘𝐺) ↦ if(𝑎 = 0, (0g‘𝐺), if(0 < 𝑎, (seq1((+g‘𝐺), (ℕ × {𝑏}))‘𝑎), ((invg‘𝐺)‘(seq1((+g‘𝐺), (ℕ × {𝑏}))‘-𝑎)))))) |
36 | | eqidd 2178 |
. . . 4
⊢ (𝜑 → if(𝑎 = 0, (0g‘𝐻), if(0 < 𝑎, (seq1((+g‘𝐻), (ℕ × {𝑏}))‘𝑎), ((invg‘𝐻)‘(seq1((+g‘𝐻), (ℕ × {𝑏}))‘-𝑎)))) = if(𝑎 = 0, (0g‘𝐻), if(0 < 𝑎, (seq1((+g‘𝐻), (ℕ × {𝑏}))‘𝑎), ((invg‘𝐻)‘(seq1((+g‘𝐻), (ℕ × {𝑏}))‘-𝑎))))) |
37 | 33, 2, 36 | mpoeq123dv 5936 |
. . 3
⊢ (𝜑 → (𝑎 ∈ ℤ, 𝑏 ∈ 𝐵 ↦ if(𝑎 = 0, (0g‘𝐻), if(0 < 𝑎, (seq1((+g‘𝐻), (ℕ × {𝑏}))‘𝑎), ((invg‘𝐻)‘(seq1((+g‘𝐻), (ℕ × {𝑏}))‘-𝑎))))) = (𝑎 ∈ ℤ, 𝑏 ∈ (Base‘𝐻) ↦ if(𝑎 = 0, (0g‘𝐻), if(0 < 𝑎, (seq1((+g‘𝐻), (ℕ × {𝑏}))‘𝑎), ((invg‘𝐻)‘(seq1((+g‘𝐻), (ℕ × {𝑏}))‘-𝑎)))))) |
38 | 32, 35, 37 | 3eqtr3d 2218 |
. 2
⊢ (𝜑 → (𝑎 ∈ ℤ, 𝑏 ∈ (Base‘𝐺) ↦ if(𝑎 = 0, (0g‘𝐺), if(0 < 𝑎, (seq1((+g‘𝐺), (ℕ × {𝑏}))‘𝑎), ((invg‘𝐺)‘(seq1((+g‘𝐺), (ℕ × {𝑏}))‘-𝑎))))) = (𝑎 ∈ ℤ, 𝑏 ∈ (Base‘𝐻) ↦ if(𝑎 = 0, (0g‘𝐻), if(0 < 𝑎, (seq1((+g‘𝐻), (ℕ × {𝑏}))‘𝑎), ((invg‘𝐻)‘(seq1((+g‘𝐻), (ℕ × {𝑏}))‘-𝑎)))))) |
39 | | mulgpropdg.m |
. . 3
⊢ (𝜑 → · =
(.g‘𝐺)) |
40 | | eqid 2177 |
. . . . 5
⊢
(Base‘𝐺) =
(Base‘𝐺) |
41 | | eqid 2177 |
. . . . 5
⊢
(+g‘𝐺) = (+g‘𝐺) |
42 | | eqid 2177 |
. . . . 5
⊢
(0g‘𝐺) = (0g‘𝐺) |
43 | | eqid 2177 |
. . . . 5
⊢
(invg‘𝐺) = (invg‘𝐺) |
44 | | eqid 2177 |
. . . . 5
⊢
(.g‘𝐺) = (.g‘𝐺) |
45 | 40, 41, 42, 43, 44 | mulgfvalg 12939 |
. . . 4
⊢ (𝐺 ∈ 𝑉 → (.g‘𝐺) = (𝑎 ∈ ℤ, 𝑏 ∈ (Base‘𝐺) ↦ if(𝑎 = 0, (0g‘𝐺), if(0 < 𝑎, (seq1((+g‘𝐺), (ℕ × {𝑏}))‘𝑎), ((invg‘𝐺)‘(seq1((+g‘𝐺), (ℕ × {𝑏}))‘-𝑎)))))) |
46 | 3, 45 | syl 14 |
. . 3
⊢ (𝜑 → (.g‘𝐺) = (𝑎 ∈ ℤ, 𝑏 ∈ (Base‘𝐺) ↦ if(𝑎 = 0, (0g‘𝐺), if(0 < 𝑎, (seq1((+g‘𝐺), (ℕ × {𝑏}))‘𝑎), ((invg‘𝐺)‘(seq1((+g‘𝐺), (ℕ × {𝑏}))‘-𝑎)))))) |
47 | 39, 46 | eqtrd 2210 |
. 2
⊢ (𝜑 → · = (𝑎 ∈ ℤ, 𝑏 ∈ (Base‘𝐺) ↦ if(𝑎 = 0, (0g‘𝐺), if(0 < 𝑎, (seq1((+g‘𝐺), (ℕ × {𝑏}))‘𝑎), ((invg‘𝐺)‘(seq1((+g‘𝐺), (ℕ × {𝑏}))‘-𝑎)))))) |
48 | | mulgpropdg.n |
. . 3
⊢ (𝜑 → × =
(.g‘𝐻)) |
49 | | eqid 2177 |
. . . . 5
⊢
(Base‘𝐻) =
(Base‘𝐻) |
50 | | eqid 2177 |
. . . . 5
⊢
(+g‘𝐻) = (+g‘𝐻) |
51 | | eqid 2177 |
. . . . 5
⊢
(0g‘𝐻) = (0g‘𝐻) |
52 | | eqid 2177 |
. . . . 5
⊢
(invg‘𝐻) = (invg‘𝐻) |
53 | | eqid 2177 |
. . . . 5
⊢
(.g‘𝐻) = (.g‘𝐻) |
54 | 49, 50, 51, 52, 53 | mulgfvalg 12939 |
. . . 4
⊢ (𝐻 ∈ 𝑊 → (.g‘𝐻) = (𝑎 ∈ ℤ, 𝑏 ∈ (Base‘𝐻) ↦ if(𝑎 = 0, (0g‘𝐻), if(0 < 𝑎, (seq1((+g‘𝐻), (ℕ × {𝑏}))‘𝑎), ((invg‘𝐻)‘(seq1((+g‘𝐻), (ℕ × {𝑏}))‘-𝑎)))))) |
55 | 4, 54 | syl 14 |
. . 3
⊢ (𝜑 → (.g‘𝐻) = (𝑎 ∈ ℤ, 𝑏 ∈ (Base‘𝐻) ↦ if(𝑎 = 0, (0g‘𝐻), if(0 < 𝑎, (seq1((+g‘𝐻), (ℕ × {𝑏}))‘𝑎), ((invg‘𝐻)‘(seq1((+g‘𝐻), (ℕ × {𝑏}))‘-𝑎)))))) |
56 | 48, 55 | eqtrd 2210 |
. 2
⊢ (𝜑 → × = (𝑎 ∈ ℤ, 𝑏 ∈ (Base‘𝐻) ↦ if(𝑎 = 0, (0g‘𝐻), if(0 < 𝑎, (seq1((+g‘𝐻), (ℕ × {𝑏}))‘𝑎), ((invg‘𝐻)‘(seq1((+g‘𝐻), (ℕ × {𝑏}))‘-𝑎)))))) |
57 | 38, 47, 56 | 3eqtr4d 2220 |
1
⊢ (𝜑 → · = ×
) |