Step | Hyp | Ref
| Expression |
1 | | mulgpropd.b1 |
. . . . . . 7
⊢ (𝜑 → 𝐵 = (Base‘𝐺)) |
2 | | mulgpropd.b2 |
. . . . . . 7
⊢ (𝜑 → 𝐵 = (Base‘𝐻)) |
3 | | mulgpropd.i |
. . . . . . . . . 10
⊢ (𝜑 → 𝐵 ⊆ 𝐾) |
4 | | ssel 3914 |
. . . . . . . . . . 11
⊢ (𝐵 ⊆ 𝐾 → (𝑥 ∈ 𝐵 → 𝑥 ∈ 𝐾)) |
5 | | ssel 3914 |
. . . . . . . . . . 11
⊢ (𝐵 ⊆ 𝐾 → (𝑦 ∈ 𝐵 → 𝑦 ∈ 𝐾)) |
6 | 4, 5 | anim12d 609 |
. . . . . . . . . 10
⊢ (𝐵 ⊆ 𝐾 → ((𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵) → (𝑥 ∈ 𝐾 ∧ 𝑦 ∈ 𝐾))) |
7 | 3, 6 | syl 17 |
. . . . . . . . 9
⊢ (𝜑 → ((𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵) → (𝑥 ∈ 𝐾 ∧ 𝑦 ∈ 𝐾))) |
8 | 7 | imp 407 |
. . . . . . . 8
⊢ ((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) → (𝑥 ∈ 𝐾 ∧ 𝑦 ∈ 𝐾)) |
9 | | mulgpropd.e |
. . . . . . . 8
⊢ ((𝜑 ∧ (𝑥 ∈ 𝐾 ∧ 𝑦 ∈ 𝐾)) → (𝑥(+g‘𝐺)𝑦) = (𝑥(+g‘𝐻)𝑦)) |
10 | 8, 9 | syldan 591 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) → (𝑥(+g‘𝐺)𝑦) = (𝑥(+g‘𝐻)𝑦)) |
11 | 1, 2, 10 | grpidpropd 18346 |
. . . . . 6
⊢ (𝜑 → (0g‘𝐺) = (0g‘𝐻)) |
12 | 11 | 3ad2ant1 1132 |
. . . . 5
⊢ ((𝜑 ∧ 𝑎 ∈ ℤ ∧ 𝑏 ∈ 𝐵) → (0g‘𝐺) = (0g‘𝐻)) |
13 | | 1zzd 12351 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑎 ∈ ℤ ∧ 𝑏 ∈ 𝐵) → 1 ∈ ℤ) |
14 | | vex 3436 |
. . . . . . . . . . . 12
⊢ 𝑏 ∈ V |
15 | 14 | fvconst2 7079 |
. . . . . . . . . . 11
⊢ (𝑥 ∈ ℕ → ((ℕ
× {𝑏})‘𝑥) = 𝑏) |
16 | | nnuz 12621 |
. . . . . . . . . . . 12
⊢ ℕ =
(ℤ≥‘1) |
17 | 16 | eqcomi 2747 |
. . . . . . . . . . 11
⊢
(ℤ≥‘1) = ℕ |
18 | 15, 17 | eleq2s 2857 |
. . . . . . . . . 10
⊢ (𝑥 ∈
(ℤ≥‘1) → ((ℕ × {𝑏})‘𝑥) = 𝑏) |
19 | 18 | adantl 482 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑎 ∈ ℤ ∧ 𝑏 ∈ 𝐵) ∧ 𝑥 ∈ (ℤ≥‘1))
→ ((ℕ × {𝑏})‘𝑥) = 𝑏) |
20 | 3 | 3ad2ant1 1132 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑎 ∈ ℤ ∧ 𝑏 ∈ 𝐵) → 𝐵 ⊆ 𝐾) |
21 | | simp3 1137 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑎 ∈ ℤ ∧ 𝑏 ∈ 𝐵) → 𝑏 ∈ 𝐵) |
22 | 20, 21 | sseldd 3922 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑎 ∈ ℤ ∧ 𝑏 ∈ 𝐵) → 𝑏 ∈ 𝐾) |
23 | 22 | adantr 481 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑎 ∈ ℤ ∧ 𝑏 ∈ 𝐵) ∧ 𝑥 ∈ (ℤ≥‘1))
→ 𝑏 ∈ 𝐾) |
24 | 19, 23 | eqeltrd 2839 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑎 ∈ ℤ ∧ 𝑏 ∈ 𝐵) ∧ 𝑥 ∈ (ℤ≥‘1))
→ ((ℕ × {𝑏})‘𝑥) ∈ 𝐾) |
25 | | mulgpropd.k |
. . . . . . . . 9
⊢ ((𝜑 ∧ (𝑥 ∈ 𝐾 ∧ 𝑦 ∈ 𝐾)) → (𝑥(+g‘𝐺)𝑦) ∈ 𝐾) |
26 | 25 | 3ad2antl1 1184 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑎 ∈ ℤ ∧ 𝑏 ∈ 𝐵) ∧ (𝑥 ∈ 𝐾 ∧ 𝑦 ∈ 𝐾)) → (𝑥(+g‘𝐺)𝑦) ∈ 𝐾) |
27 | 9 | 3ad2antl1 1184 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑎 ∈ ℤ ∧ 𝑏 ∈ 𝐵) ∧ (𝑥 ∈ 𝐾 ∧ 𝑦 ∈ 𝐾)) → (𝑥(+g‘𝐺)𝑦) = (𝑥(+g‘𝐻)𝑦)) |
28 | 13, 24, 26, 27 | seqfeq3 13773 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑎 ∈ ℤ ∧ 𝑏 ∈ 𝐵) → seq1((+g‘𝐺), (ℕ × {𝑏})) =
seq1((+g‘𝐻), (ℕ × {𝑏}))) |
29 | 28 | fveq1d 6776 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑎 ∈ ℤ ∧ 𝑏 ∈ 𝐵) → (seq1((+g‘𝐺), (ℕ × {𝑏}))‘𝑎) = (seq1((+g‘𝐻), (ℕ × {𝑏}))‘𝑎)) |
30 | 1, 2, 10 | grpinvpropd 18650 |
. . . . . . . 8
⊢ (𝜑 →
(invg‘𝐺) =
(invg‘𝐻)) |
31 | 30 | 3ad2ant1 1132 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑎 ∈ ℤ ∧ 𝑏 ∈ 𝐵) → (invg‘𝐺) = (invg‘𝐻)) |
32 | 28 | fveq1d 6776 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑎 ∈ ℤ ∧ 𝑏 ∈ 𝐵) → (seq1((+g‘𝐺), (ℕ × {𝑏}))‘-𝑎) = (seq1((+g‘𝐻), (ℕ × {𝑏}))‘-𝑎)) |
33 | 31, 32 | fveq12d 6781 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑎 ∈ ℤ ∧ 𝑏 ∈ 𝐵) → ((invg‘𝐺)‘(seq1((+g‘𝐺), (ℕ × {𝑏}))‘-𝑎)) = ((invg‘𝐻)‘(seq1((+g‘𝐻), (ℕ × {𝑏}))‘-𝑎))) |
34 | 29, 33 | ifeq12d 4480 |
. . . . 5
⊢ ((𝜑 ∧ 𝑎 ∈ ℤ ∧ 𝑏 ∈ 𝐵) → if(0 < 𝑎, (seq1((+g‘𝐺), (ℕ × {𝑏}))‘𝑎), ((invg‘𝐺)‘(seq1((+g‘𝐺), (ℕ × {𝑏}))‘-𝑎))) = if(0 < 𝑎, (seq1((+g‘𝐻), (ℕ × {𝑏}))‘𝑎), ((invg‘𝐻)‘(seq1((+g‘𝐻), (ℕ × {𝑏}))‘-𝑎)))) |
35 | 12, 34 | ifeq12d 4480 |
. . . 4
⊢ ((𝜑 ∧ 𝑎 ∈ ℤ ∧ 𝑏 ∈ 𝐵) → if(𝑎 = 0, (0g‘𝐺), if(0 < 𝑎, (seq1((+g‘𝐺), (ℕ × {𝑏}))‘𝑎), ((invg‘𝐺)‘(seq1((+g‘𝐺), (ℕ × {𝑏}))‘-𝑎)))) = if(𝑎 = 0, (0g‘𝐻), if(0 < 𝑎, (seq1((+g‘𝐻), (ℕ × {𝑏}))‘𝑎), ((invg‘𝐻)‘(seq1((+g‘𝐻), (ℕ × {𝑏}))‘-𝑎))))) |
36 | 35 | mpoeq3dva 7352 |
. . 3
⊢ (𝜑 → (𝑎 ∈ ℤ, 𝑏 ∈ 𝐵 ↦ if(𝑎 = 0, (0g‘𝐺), if(0 < 𝑎, (seq1((+g‘𝐺), (ℕ × {𝑏}))‘𝑎), ((invg‘𝐺)‘(seq1((+g‘𝐺), (ℕ × {𝑏}))‘-𝑎))))) = (𝑎 ∈ ℤ, 𝑏 ∈ 𝐵 ↦ if(𝑎 = 0, (0g‘𝐻), if(0 < 𝑎, (seq1((+g‘𝐻), (ℕ × {𝑏}))‘𝑎), ((invg‘𝐻)‘(seq1((+g‘𝐻), (ℕ × {𝑏}))‘-𝑎)))))) |
37 | | eqidd 2739 |
. . . 4
⊢ (𝜑 → ℤ =
ℤ) |
38 | | eqidd 2739 |
. . . 4
⊢ (𝜑 → if(𝑎 = 0, (0g‘𝐺), if(0 < 𝑎, (seq1((+g‘𝐺), (ℕ × {𝑏}))‘𝑎), ((invg‘𝐺)‘(seq1((+g‘𝐺), (ℕ × {𝑏}))‘-𝑎)))) = if(𝑎 = 0, (0g‘𝐺), if(0 < 𝑎, (seq1((+g‘𝐺), (ℕ × {𝑏}))‘𝑎), ((invg‘𝐺)‘(seq1((+g‘𝐺), (ℕ × {𝑏}))‘-𝑎))))) |
39 | 37, 1, 38 | mpoeq123dv 7350 |
. . 3
⊢ (𝜑 → (𝑎 ∈ ℤ, 𝑏 ∈ 𝐵 ↦ if(𝑎 = 0, (0g‘𝐺), if(0 < 𝑎, (seq1((+g‘𝐺), (ℕ × {𝑏}))‘𝑎), ((invg‘𝐺)‘(seq1((+g‘𝐺), (ℕ × {𝑏}))‘-𝑎))))) = (𝑎 ∈ ℤ, 𝑏 ∈ (Base‘𝐺) ↦ if(𝑎 = 0, (0g‘𝐺), if(0 < 𝑎, (seq1((+g‘𝐺), (ℕ × {𝑏}))‘𝑎), ((invg‘𝐺)‘(seq1((+g‘𝐺), (ℕ × {𝑏}))‘-𝑎)))))) |
40 | | eqidd 2739 |
. . . 4
⊢ (𝜑 → if(𝑎 = 0, (0g‘𝐻), if(0 < 𝑎, (seq1((+g‘𝐻), (ℕ × {𝑏}))‘𝑎), ((invg‘𝐻)‘(seq1((+g‘𝐻), (ℕ × {𝑏}))‘-𝑎)))) = if(𝑎 = 0, (0g‘𝐻), if(0 < 𝑎, (seq1((+g‘𝐻), (ℕ × {𝑏}))‘𝑎), ((invg‘𝐻)‘(seq1((+g‘𝐻), (ℕ × {𝑏}))‘-𝑎))))) |
41 | 37, 2, 40 | mpoeq123dv 7350 |
. . 3
⊢ (𝜑 → (𝑎 ∈ ℤ, 𝑏 ∈ 𝐵 ↦ if(𝑎 = 0, (0g‘𝐻), if(0 < 𝑎, (seq1((+g‘𝐻), (ℕ × {𝑏}))‘𝑎), ((invg‘𝐻)‘(seq1((+g‘𝐻), (ℕ × {𝑏}))‘-𝑎))))) = (𝑎 ∈ ℤ, 𝑏 ∈ (Base‘𝐻) ↦ if(𝑎 = 0, (0g‘𝐻), if(0 < 𝑎, (seq1((+g‘𝐻), (ℕ × {𝑏}))‘𝑎), ((invg‘𝐻)‘(seq1((+g‘𝐻), (ℕ × {𝑏}))‘-𝑎)))))) |
42 | 36, 39, 41 | 3eqtr3d 2786 |
. 2
⊢ (𝜑 → (𝑎 ∈ ℤ, 𝑏 ∈ (Base‘𝐺) ↦ if(𝑎 = 0, (0g‘𝐺), if(0 < 𝑎, (seq1((+g‘𝐺), (ℕ × {𝑏}))‘𝑎), ((invg‘𝐺)‘(seq1((+g‘𝐺), (ℕ × {𝑏}))‘-𝑎))))) = (𝑎 ∈ ℤ, 𝑏 ∈ (Base‘𝐻) ↦ if(𝑎 = 0, (0g‘𝐻), if(0 < 𝑎, (seq1((+g‘𝐻), (ℕ × {𝑏}))‘𝑎), ((invg‘𝐻)‘(seq1((+g‘𝐻), (ℕ × {𝑏}))‘-𝑎)))))) |
43 | | eqid 2738 |
. . 3
⊢
(Base‘𝐺) =
(Base‘𝐺) |
44 | | eqid 2738 |
. . 3
⊢
(+g‘𝐺) = (+g‘𝐺) |
45 | | eqid 2738 |
. . 3
⊢
(0g‘𝐺) = (0g‘𝐺) |
46 | | eqid 2738 |
. . 3
⊢
(invg‘𝐺) = (invg‘𝐺) |
47 | | mulgpropd.m |
. . 3
⊢ · =
(.g‘𝐺) |
48 | 43, 44, 45, 46, 47 | mulgfval 18702 |
. 2
⊢ · =
(𝑎 ∈ ℤ, 𝑏 ∈ (Base‘𝐺) ↦ if(𝑎 = 0, (0g‘𝐺), if(0 < 𝑎, (seq1((+g‘𝐺), (ℕ × {𝑏}))‘𝑎), ((invg‘𝐺)‘(seq1((+g‘𝐺), (ℕ × {𝑏}))‘-𝑎))))) |
49 | | eqid 2738 |
. . 3
⊢
(Base‘𝐻) =
(Base‘𝐻) |
50 | | eqid 2738 |
. . 3
⊢
(+g‘𝐻) = (+g‘𝐻) |
51 | | eqid 2738 |
. . 3
⊢
(0g‘𝐻) = (0g‘𝐻) |
52 | | eqid 2738 |
. . 3
⊢
(invg‘𝐻) = (invg‘𝐻) |
53 | | mulgpropd.n |
. . 3
⊢ × =
(.g‘𝐻) |
54 | 49, 50, 51, 52, 53 | mulgfval 18702 |
. 2
⊢ × =
(𝑎 ∈ ℤ, 𝑏 ∈ (Base‘𝐻) ↦ if(𝑎 = 0, (0g‘𝐻), if(0 < 𝑎, (seq1((+g‘𝐻), (ℕ × {𝑏}))‘𝑎), ((invg‘𝐻)‘(seq1((+g‘𝐻), (ℕ × {𝑏}))‘-𝑎))))) |
55 | 42, 48, 54 | 3eqtr4g 2803 |
1
⊢ (𝜑 → · = ×
) |