Theorem grpsubpropd2 12831

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

Hypotheses

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

Assertion

Ref	Expression
grpsubpropd2	⊢ (𝜑 → (-g‘𝐺) = (-g‘𝐻))

Distinct variable groups:   𝑥,𝑦,𝐵   𝑥,𝐺,𝑦   𝑥,𝐻,𝑦   𝜑,𝑥,𝑦

Proof of Theorem grpsubpropd2

Dummy variables 𝑎 𝑏 are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		simp1 995	. . . . . 6 ⊢ ((𝜑 ∧ 𝑎 ∈ (Base‘𝐺) ∧ 𝑏 ∈ (Base‘𝐺)) → 𝜑)
2		simp2 996	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑎 ∈ (Base‘𝐺) ∧ 𝑏 ∈ (Base‘𝐺)) → 𝑎 ∈ (Base‘𝐺))
3		grpsubpropd2.1	. . . . . . . 8 ⊢ (𝜑 → 𝐵 = (Base‘𝐺))
4	3	3ad2ant1 1016	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑎 ∈ (Base‘𝐺) ∧ 𝑏 ∈ (Base‘𝐺)) → 𝐵 = (Base‘𝐺))
5	2, 4	eleqtrrd 2253	. . . . . 6 ⊢ ((𝜑 ∧ 𝑎 ∈ (Base‘𝐺) ∧ 𝑏 ∈ (Base‘𝐺)) → 𝑎 ∈ 𝐵)
6		grpsubpropd2.3	. . . . . . . . 9 ⊢ (𝜑 → 𝐺 ∈ Grp)
7	6	3ad2ant1 1016	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑎 ∈ (Base‘𝐺) ∧ 𝑏 ∈ (Base‘𝐺)) → 𝐺 ∈ Grp)
8		simp3 997	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑎 ∈ (Base‘𝐺) ∧ 𝑏 ∈ (Base‘𝐺)) → 𝑏 ∈ (Base‘𝐺))
9		eqid 2173	. . . . . . . . 9 ⊢ (Base‘𝐺) = (Base‘𝐺)
10		eqid 2173	. . . . . . . . 9 ⊢ (invg‘𝐺) = (invg‘𝐺)
11	9, 10	grpinvcl 12778	. . . . . . . 8 ⊢ ((𝐺 ∈ Grp ∧ 𝑏 ∈ (Base‘𝐺)) → ((invg‘𝐺)‘𝑏) ∈ (Base‘𝐺))
12	7, 8, 11	syl2anc 411	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑎 ∈ (Base‘𝐺) ∧ 𝑏 ∈ (Base‘𝐺)) → ((invg‘𝐺)‘𝑏) ∈ (Base‘𝐺))
13	12, 4	eleqtrrd 2253	. . . . . 6 ⊢ ((𝜑 ∧ 𝑎 ∈ (Base‘𝐺) ∧ 𝑏 ∈ (Base‘𝐺)) → ((invg‘𝐺)‘𝑏) ∈ 𝐵)
14		grpsubpropd2.4	. . . . . . 7 ⊢ ((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) → (𝑥(+g‘𝐺)𝑦) = (𝑥(+g‘𝐻)𝑦))
15	14	oveqrspc2v 5889	. . . . . 6 ⊢ ((𝜑 ∧ (𝑎 ∈ 𝐵 ∧ ((invg‘𝐺)‘𝑏) ∈ 𝐵)) → (𝑎(+g‘𝐺)((invg‘𝐺)‘𝑏)) = (𝑎(+g‘𝐻)((invg‘𝐺)‘𝑏)))
16	1, 5, 13, 15	syl12anc 1234	. . . . 5 ⊢ ((𝜑 ∧ 𝑎 ∈ (Base‘𝐺) ∧ 𝑏 ∈ (Base‘𝐺)) → (𝑎(+g‘𝐺)((invg‘𝐺)‘𝑏)) = (𝑎(+g‘𝐻)((invg‘𝐺)‘𝑏)))
17		grpsubpropd2.2	. . . . . . . . 9 ⊢ (𝜑 → 𝐵 = (Base‘𝐻))
18		eqid 2173	. . . . . . . . . . . . 13 ⊢ (0g‘𝐺) = (0g‘𝐺)
19	9, 18	grpidcl 12761	. . . . . . . . . . . 12 ⊢ (𝐺 ∈ Grp → (0g‘𝐺) ∈ (Base‘𝐺))
20	6, 19	syl 14	. . . . . . . . . . 11 ⊢ (𝜑 → (0g‘𝐺) ∈ (Base‘𝐺))
21	20, 3	eleqtrrd 2253	. . . . . . . . . 10 ⊢ (𝜑 → (0g‘𝐺) ∈ 𝐵)
22	17, 21	basmexd 12484	. . . . . . . . 9 ⊢ (𝜑 → 𝐻 ∈ V)
23	3, 17, 6, 22, 14	grpinvpropdg 12801	. . . . . . . 8 ⊢ (𝜑 → (invg‘𝐺) = (invg‘𝐻))
24	23	fveq1d 5506	. . . . . . 7 ⊢ (𝜑 → ((invg‘𝐺)‘𝑏) = ((invg‘𝐻)‘𝑏))
25	24	oveq2d 5878	. . . . . 6 ⊢ (𝜑 → (𝑎(+g‘𝐻)((invg‘𝐺)‘𝑏)) = (𝑎(+g‘𝐻)((invg‘𝐻)‘𝑏)))
26	25	3ad2ant1 1016	. . . . 5 ⊢ ((𝜑 ∧ 𝑎 ∈ (Base‘𝐺) ∧ 𝑏 ∈ (Base‘𝐺)) → (𝑎(+g‘𝐻)((invg‘𝐺)‘𝑏)) = (𝑎(+g‘𝐻)((invg‘𝐻)‘𝑏)))
27	16, 26	eqtrd 2206	. . . 4 ⊢ ((𝜑 ∧ 𝑎 ∈ (Base‘𝐺) ∧ 𝑏 ∈ (Base‘𝐺)) → (𝑎(+g‘𝐺)((invg‘𝐺)‘𝑏)) = (𝑎(+g‘𝐻)((invg‘𝐻)‘𝑏)))
28	27	mpoeq3dva 5926	. . 3 ⊢ (𝜑 → (𝑎 ∈ (Base‘𝐺), 𝑏 ∈ (Base‘𝐺) ↦ (𝑎(+g‘𝐺)((invg‘𝐺)‘𝑏))) = (𝑎 ∈ (Base‘𝐺), 𝑏 ∈ (Base‘𝐺) ↦ (𝑎(+g‘𝐻)((invg‘𝐻)‘𝑏))))
29	3, 17	eqtr3d 2208	. . . 4 ⊢ (𝜑 → (Base‘𝐺) = (Base‘𝐻))
30		mpoeq12 5922	. . . 4 ⊢ (((Base‘𝐺) = (Base‘𝐻) ∧ (Base‘𝐺) = (Base‘𝐻)) → (𝑎 ∈ (Base‘𝐺), 𝑏 ∈ (Base‘𝐺) ↦ (𝑎(+g‘𝐻)((invg‘𝐻)‘𝑏))) = (𝑎 ∈ (Base‘𝐻), 𝑏 ∈ (Base‘𝐻) ↦ (𝑎(+g‘𝐻)((invg‘𝐻)‘𝑏))))
31	29, 29, 30	syl2anc 411	. . 3 ⊢ (𝜑 → (𝑎 ∈ (Base‘𝐺), 𝑏 ∈ (Base‘𝐺) ↦ (𝑎(+g‘𝐻)((invg‘𝐻)‘𝑏))) = (𝑎 ∈ (Base‘𝐻), 𝑏 ∈ (Base‘𝐻) ↦ (𝑎(+g‘𝐻)((invg‘𝐻)‘𝑏))))
32	28, 31	eqtrd 2206	. 2 ⊢ (𝜑 → (𝑎 ∈ (Base‘𝐺), 𝑏 ∈ (Base‘𝐺) ↦ (𝑎(+g‘𝐺)((invg‘𝐺)‘𝑏))) = (𝑎 ∈ (Base‘𝐻), 𝑏 ∈ (Base‘𝐻) ↦ (𝑎(+g‘𝐻)((invg‘𝐻)‘𝑏))))
33		eqid 2173	. . . 4 ⊢ (+g‘𝐺) = (+g‘𝐺)
34		eqid 2173	. . . 4 ⊢ (-g‘𝐺) = (-g‘𝐺)
35	9, 33, 10, 34	grpsubfvalg 12775	. . 3 ⊢ (𝐺 ∈ Grp → (-g‘𝐺) = (𝑎 ∈ (Base‘𝐺), 𝑏 ∈ (Base‘𝐺) ↦ (𝑎(+g‘𝐺)((invg‘𝐺)‘𝑏))))
36	6, 35	syl 14	. 2 ⊢ (𝜑 → (-g‘𝐺) = (𝑎 ∈ (Base‘𝐺), 𝑏 ∈ (Base‘𝐺) ↦ (𝑎(+g‘𝐺)((invg‘𝐺)‘𝑏))))
37		eqid 2173	. . . 4 ⊢ (Base‘𝐻) = (Base‘𝐻)
38		eqid 2173	. . . 4 ⊢ (+g‘𝐻) = (+g‘𝐻)
39		eqid 2173	. . . 4 ⊢ (invg‘𝐻) = (invg‘𝐻)
40		eqid 2173	. . . 4 ⊢ (-g‘𝐻) = (-g‘𝐻)
41	37, 38, 39, 40	grpsubfvalg 12775	. . 3 ⊢ (𝐻 ∈ V → (-g‘𝐻) = (𝑎 ∈ (Base‘𝐻), 𝑏 ∈ (Base‘𝐻) ↦ (𝑎(+g‘𝐻)((invg‘𝐻)‘𝑏))))
42	22, 41	syl 14	. 2 ⊢ (𝜑 → (-g‘𝐻) = (𝑎 ∈ (Base‘𝐻), 𝑏 ∈ (Base‘𝐻) ↦ (𝑎(+g‘𝐻)((invg‘𝐻)‘𝑏))))
43	32, 36, 42	3eqtr4d 2216	1 ⊢ (𝜑 → (-g‘𝐺) = (-g‘𝐻))

Syntax hints:   → wi 4   ∧ wa 104   ∧ w3a 976   = wceq 1351   ∈ wcel 2144  Vcvv 2733  ‘cfv 5205  (class class class)co 5862   ∈ cmpo 5864  Basecbs 12425  +_gcplusg 12489  0_gc0g 12623  Grpcgrp 12735  inv_gcminusg 12736  -_gcsg 12737

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-io 707  ax-5 1443  ax-7 1444  ax-gen 1445  ax-ie1 1489  ax-ie2 1490  ax-8 1500  ax-10 1501  ax-11 1502  ax-i12 1503  ax-bndl 1505  ax-4 1506  ax-17 1522  ax-i9 1526  ax-ial 1530  ax-i5r 1531  ax-13 2146  ax-14 2147  ax-ext 2155  ax-coll 4110  ax-sep 4113  ax-pow 4166  ax-pr 4200  ax-un 4424  ax-cnex 7874  ax-resscn 7875  ax-1re 7877  ax-addrcl 7880

This theorem depends on definitions:  df-bi 117  df-3an 978  df-tru 1354  df-nf 1457  df-sb 1759  df-eu 2025  df-mo 2026  df-clab 2160  df-cleq 2166  df-clel 2169  df-nfc 2304  df-ral 2456  df-rex 2457  df-reu 2458  df-rmo 2459  df-rab 2460  df-v 2735  df-sbc 2959  df-csb 3053  df-un 3128  df-in 3130  df-ss 3137  df-pw 3571  df-sn 3592  df-pr 3593  df-op 3595  df-uni 3803  df-int 3838  df-iun 3881  df-br 3996  df-opab 4057  df-mpt 4058  df-id 4284  df-xp 4623  df-rel 4624  df-cnv 4625  df-co 4626  df-dm 4627  df-rn 4628  df-res 4629  df-ima 4630  df-iota 5167  df-fun 5207  df-fn 5208  df-f 5209  df-f1 5210  df-fo 5211  df-f1o 5212  df-fv 5213  df-riota 5818  df-ov 5865  df-oprab 5866  df-mpo 5867  df-1st 6128  df-2nd 6129  df-inn 8888  df-2 8946  df-ndx 12428  df-slot 12429  df-base 12431  df-plusg 12502  df-0g 12625  df-mgm 12637  df-sgrp 12670  df-mnd 12680  df-grp 12738  df-minusg 12739  df-sbg 12740

This theorem is referenced by: (None)