Metamath Proof Explorer

Theorem grpsubpropd2

Description: Strong property deduction for the group subtraction operation. (Contributed by Mario Carneiro, 4-Oct-2015)

Ref Expression
Hypotheses grpsubpropd2.1 ⊢ ( 𝜑 → 𝐵 = ( Base ‘ 𝐺 ) )
grpsubpropd2.2 ⊢ ( 𝜑 → 𝐵 = ( Base ‘ 𝐻 ) )
grpsubpropd2.3 ⊢ ( 𝜑 → 𝐺 ∈ Grp )
grpsubpropd2.4 ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) ) → ( 𝑥 ( +g ‘ 𝐺 ) 𝑦 ) = ( 𝑥 ( +g ‘ 𝐻 ) 𝑦 ) )
Assertion grpsubpropd2 ( 𝜑 → ( -g ‘ 𝐺 ) = ( -g ‘ 𝐻 ) )

Proof

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