| Step | Hyp | Ref | Expression | 
|---|
| 1 |  | simp1 1137 | . . . . . 6
⊢ ((𝜑 ∧ 𝑎 ∈ (Base‘𝐺) ∧ 𝑏 ∈ (Base‘𝐺)) → 𝜑) | 
| 2 |  | simp2 1138 | . . . . . . 7
⊢ ((𝜑 ∧ 𝑎 ∈ (Base‘𝐺) ∧ 𝑏 ∈ (Base‘𝐺)) → 𝑎 ∈ (Base‘𝐺)) | 
| 3 |  | grpsubpropd2.1 | . . . . . . . 8
⊢ (𝜑 → 𝐵 = (Base‘𝐺)) | 
| 4 | 3 | 3ad2ant1 1134 | . . . . . . 7
⊢ ((𝜑 ∧ 𝑎 ∈ (Base‘𝐺) ∧ 𝑏 ∈ (Base‘𝐺)) → 𝐵 = (Base‘𝐺)) | 
| 5 | 2, 4 | eleqtrrd 2844 | . . . . . 6
⊢ ((𝜑 ∧ 𝑎 ∈ (Base‘𝐺) ∧ 𝑏 ∈ (Base‘𝐺)) → 𝑎 ∈ 𝐵) | 
| 6 |  | grpsubpropd2.3 | . . . . . . . . 9
⊢ (𝜑 → 𝐺 ∈ Grp) | 
| 7 | 6 | 3ad2ant1 1134 | . . . . . . . 8
⊢ ((𝜑 ∧ 𝑎 ∈ (Base‘𝐺) ∧ 𝑏 ∈ (Base‘𝐺)) → 𝐺 ∈ Grp) | 
| 8 |  | simp3 1139 | . . . . . . . 8
⊢ ((𝜑 ∧ 𝑎 ∈ (Base‘𝐺) ∧ 𝑏 ∈ (Base‘𝐺)) → 𝑏 ∈ (Base‘𝐺)) | 
| 9 |  | eqid 2737 | . . . . . . . . 9
⊢
(Base‘𝐺) =
(Base‘𝐺) | 
| 10 |  | eqid 2737 | . . . . . . . . 9
⊢
(invg‘𝐺) = (invg‘𝐺) | 
| 11 | 9, 10 | grpinvcl 19005 | . . . . . . . 8
⊢ ((𝐺 ∈ Grp ∧ 𝑏 ∈ (Base‘𝐺)) →
((invg‘𝐺)‘𝑏) ∈ (Base‘𝐺)) | 
| 12 | 7, 8, 11 | syl2anc 584 | . . . . . . 7
⊢ ((𝜑 ∧ 𝑎 ∈ (Base‘𝐺) ∧ 𝑏 ∈ (Base‘𝐺)) → ((invg‘𝐺)‘𝑏) ∈ (Base‘𝐺)) | 
| 13 | 12, 4 | eleqtrrd 2844 | . . . . . 6
⊢ ((𝜑 ∧ 𝑎 ∈ (Base‘𝐺) ∧ 𝑏 ∈ (Base‘𝐺)) → ((invg‘𝐺)‘𝑏) ∈ 𝐵) | 
| 14 |  | grpsubpropd2.4 | . . . . . . 7
⊢ ((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) → (𝑥(+g‘𝐺)𝑦) = (𝑥(+g‘𝐻)𝑦)) | 
| 15 | 14 | oveqrspc2v 7458 | . . . . . 6
⊢ ((𝜑 ∧ (𝑎 ∈ 𝐵 ∧ ((invg‘𝐺)‘𝑏) ∈ 𝐵)) → (𝑎(+g‘𝐺)((invg‘𝐺)‘𝑏)) = (𝑎(+g‘𝐻)((invg‘𝐺)‘𝑏))) | 
| 16 | 1, 5, 13, 15 | syl12anc 837 | . . . . 5
⊢ ((𝜑 ∧ 𝑎 ∈ (Base‘𝐺) ∧ 𝑏 ∈ (Base‘𝐺)) → (𝑎(+g‘𝐺)((invg‘𝐺)‘𝑏)) = (𝑎(+g‘𝐻)((invg‘𝐺)‘𝑏))) | 
| 17 |  | grpsubpropd2.2 | . . . . . . . . 9
⊢ (𝜑 → 𝐵 = (Base‘𝐻)) | 
| 18 | 3, 17, 14 | grpinvpropd 19033 | . . . . . . . 8
⊢ (𝜑 →
(invg‘𝐺) =
(invg‘𝐻)) | 
| 19 | 18 | fveq1d 6908 | . . . . . . 7
⊢ (𝜑 →
((invg‘𝐺)‘𝑏) = ((invg‘𝐻)‘𝑏)) | 
| 20 | 19 | oveq2d 7447 | . . . . . 6
⊢ (𝜑 → (𝑎(+g‘𝐻)((invg‘𝐺)‘𝑏)) = (𝑎(+g‘𝐻)((invg‘𝐻)‘𝑏))) | 
| 21 | 20 | 3ad2ant1 1134 | . . . . 5
⊢ ((𝜑 ∧ 𝑎 ∈ (Base‘𝐺) ∧ 𝑏 ∈ (Base‘𝐺)) → (𝑎(+g‘𝐻)((invg‘𝐺)‘𝑏)) = (𝑎(+g‘𝐻)((invg‘𝐻)‘𝑏))) | 
| 22 | 16, 21 | eqtrd 2777 | . . . 4
⊢ ((𝜑 ∧ 𝑎 ∈ (Base‘𝐺) ∧ 𝑏 ∈ (Base‘𝐺)) → (𝑎(+g‘𝐺)((invg‘𝐺)‘𝑏)) = (𝑎(+g‘𝐻)((invg‘𝐻)‘𝑏))) | 
| 23 | 22 | mpoeq3dva 7510 | . . 3
⊢ (𝜑 → (𝑎 ∈ (Base‘𝐺), 𝑏 ∈ (Base‘𝐺) ↦ (𝑎(+g‘𝐺)((invg‘𝐺)‘𝑏))) = (𝑎 ∈ (Base‘𝐺), 𝑏 ∈ (Base‘𝐺) ↦ (𝑎(+g‘𝐻)((invg‘𝐻)‘𝑏)))) | 
| 24 | 3, 17 | eqtr3d 2779 | . . . 4
⊢ (𝜑 → (Base‘𝐺) = (Base‘𝐻)) | 
| 25 |  | mpoeq12 7506 | . . . 4
⊢
(((Base‘𝐺) =
(Base‘𝐻) ∧
(Base‘𝐺) =
(Base‘𝐻)) →
(𝑎 ∈ (Base‘𝐺), 𝑏 ∈ (Base‘𝐺) ↦ (𝑎(+g‘𝐻)((invg‘𝐻)‘𝑏))) = (𝑎 ∈ (Base‘𝐻), 𝑏 ∈ (Base‘𝐻) ↦ (𝑎(+g‘𝐻)((invg‘𝐻)‘𝑏)))) | 
| 26 | 24, 24, 25 | syl2anc 584 | . . 3
⊢ (𝜑 → (𝑎 ∈ (Base‘𝐺), 𝑏 ∈ (Base‘𝐺) ↦ (𝑎(+g‘𝐻)((invg‘𝐻)‘𝑏))) = (𝑎 ∈ (Base‘𝐻), 𝑏 ∈ (Base‘𝐻) ↦ (𝑎(+g‘𝐻)((invg‘𝐻)‘𝑏)))) | 
| 27 | 23, 26 | eqtrd 2777 | . 2
⊢ (𝜑 → (𝑎 ∈ (Base‘𝐺), 𝑏 ∈ (Base‘𝐺) ↦ (𝑎(+g‘𝐺)((invg‘𝐺)‘𝑏))) = (𝑎 ∈ (Base‘𝐻), 𝑏 ∈ (Base‘𝐻) ↦ (𝑎(+g‘𝐻)((invg‘𝐻)‘𝑏)))) | 
| 28 |  | eqid 2737 | . . 3
⊢
(+g‘𝐺) = (+g‘𝐺) | 
| 29 |  | eqid 2737 | . . 3
⊢
(-g‘𝐺) = (-g‘𝐺) | 
| 30 | 9, 28, 10, 29 | grpsubfval 19001 | . 2
⊢
(-g‘𝐺) = (𝑎 ∈ (Base‘𝐺), 𝑏 ∈ (Base‘𝐺) ↦ (𝑎(+g‘𝐺)((invg‘𝐺)‘𝑏))) | 
| 31 |  | eqid 2737 | . . 3
⊢
(Base‘𝐻) =
(Base‘𝐻) | 
| 32 |  | eqid 2737 | . . 3
⊢
(+g‘𝐻) = (+g‘𝐻) | 
| 33 |  | eqid 2737 | . . 3
⊢
(invg‘𝐻) = (invg‘𝐻) | 
| 34 |  | eqid 2737 | . . 3
⊢
(-g‘𝐻) = (-g‘𝐻) | 
| 35 | 31, 32, 33, 34 | grpsubfval 19001 | . 2
⊢
(-g‘𝐻) = (𝑎 ∈ (Base‘𝐻), 𝑏 ∈ (Base‘𝐻) ↦ (𝑎(+g‘𝐻)((invg‘𝐻)‘𝑏))) | 
| 36 | 27, 30, 35 | 3eqtr4g 2802 | 1
⊢ (𝜑 → (-g‘𝐺) = (-g‘𝐻)) |