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𝐻 ) )