# Metamath Proof Explorer

## Theorem issubg4

Description: A subgroup is a nonempty subset of the group closed under subtraction. (Contributed by Mario Carneiro, 17-Sep-2015)

Ref Expression
Hypotheses issubg4.b ${⊢}{B}={\mathrm{Base}}_{{G}}$
issubg4.p
Assertion issubg4

### Proof

Step Hyp Ref Expression
1 issubg4.b ${⊢}{B}={\mathrm{Base}}_{{G}}$
2 issubg4.p
3 1 subgss ${⊢}{S}\in \mathrm{SubGrp}\left({G}\right)\to {S}\subseteq {B}$
4 eqid ${⊢}{0}_{{G}}={0}_{{G}}$
5 4 subg0cl ${⊢}{S}\in \mathrm{SubGrp}\left({G}\right)\to {0}_{{G}}\in {S}$
6 5 ne0d ${⊢}{S}\in \mathrm{SubGrp}\left({G}\right)\to {S}\ne \varnothing$
7 2 subgsubcl
8 7 3expb
9 8 ralrimivva
10 3 6 9 3jca
11 simplrl
12 simplrr
13 oveq1
14 13 eleq1d
15 14 ralbidv
16 simpr
17 simprr ${⊢}\left({G}\in \mathrm{Grp}\wedge \left({S}\subseteq {B}\wedge {S}\ne \varnothing \right)\right)\to {S}\ne \varnothing$
18 r19.2z
19 17 18 sylan
20 oveq2
21 20 eleq1d
22 21 rspcv
24 simprl ${⊢}\left({G}\in \mathrm{Grp}\wedge \left({S}\subseteq {B}\wedge {S}\ne \varnothing \right)\right)\to {S}\subseteq {B}$
25 24 sselda ${⊢}\left(\left({G}\in \mathrm{Grp}\wedge \left({S}\subseteq {B}\wedge {S}\ne \varnothing \right)\right)\wedge {x}\in {S}\right)\to {x}\in {B}$
26 1 4 2 grpsubid
28 25 27 syldan
29 28 eleq1d
30 23 29 sylibd
31 30 rexlimdva
32 31 imp
33 19 32 syldan
34 15 16 33 rspcdva
35 1 4 grpidcl ${⊢}{G}\in \mathrm{Grp}\to {0}_{{G}}\in {B}$
36 35 ad2antrr ${⊢}\left(\left({G}\in \mathrm{Grp}\wedge \left({S}\subseteq {B}\wedge {S}\ne \varnothing \right)\right)\wedge {y}\in {S}\right)\to {0}_{{G}}\in {B}$
37 24 sselda ${⊢}\left(\left({G}\in \mathrm{Grp}\wedge \left({S}\subseteq {B}\wedge {S}\ne \varnothing \right)\right)\wedge {y}\in {S}\right)\to {y}\in {B}$
38 eqid ${⊢}{+}_{{G}}={+}_{{G}}$
39 eqid ${⊢}{inv}_{g}\left({G}\right)={inv}_{g}\left({G}\right)$
40 1 38 39 2 grpsubval
41 36 37 40 syl2anc
42 simpll ${⊢}\left(\left({G}\in \mathrm{Grp}\wedge \left({S}\subseteq {B}\wedge {S}\ne \varnothing \right)\right)\wedge {y}\in {S}\right)\to {G}\in \mathrm{Grp}$
43 1 39 grpinvcl ${⊢}\left({G}\in \mathrm{Grp}\wedge {y}\in {B}\right)\to {inv}_{g}\left({G}\right)\left({y}\right)\in {B}$
44 42 37 43 syl2anc ${⊢}\left(\left({G}\in \mathrm{Grp}\wedge \left({S}\subseteq {B}\wedge {S}\ne \varnothing \right)\right)\wedge {y}\in {S}\right)\to {inv}_{g}\left({G}\right)\left({y}\right)\in {B}$
45 1 38 4 grplid ${⊢}\left({G}\in \mathrm{Grp}\wedge {inv}_{g}\left({G}\right)\left({y}\right)\in {B}\right)\to {0}_{{G}}{+}_{{G}}{inv}_{g}\left({G}\right)\left({y}\right)={inv}_{g}\left({G}\right)\left({y}\right)$
46 42 44 45 syl2anc ${⊢}\left(\left({G}\in \mathrm{Grp}\wedge \left({S}\subseteq {B}\wedge {S}\ne \varnothing \right)\right)\wedge {y}\in {S}\right)\to {0}_{{G}}{+}_{{G}}{inv}_{g}\left({G}\right)\left({y}\right)={inv}_{g}\left({G}\right)\left({y}\right)$
47 41 46 eqtrd
48 47 eleq1d
49 48 ralbidva
51 34 50 mpbid
52 fveq2 ${⊢}{y}={z}\to {inv}_{g}\left({G}\right)\left({y}\right)={inv}_{g}\left({G}\right)\left({z}\right)$
53 52 eleq1d ${⊢}{y}={z}\to \left({inv}_{g}\left({G}\right)\left({y}\right)\in {S}↔{inv}_{g}\left({G}\right)\left({z}\right)\in {S}\right)$
54 53 rspccva ${⊢}\left(\forall {y}\in {S}\phantom{\rule{.4em}{0ex}}{inv}_{g}\left({G}\right)\left({y}\right)\in {S}\wedge {z}\in {S}\right)\to {inv}_{g}\left({G}\right)\left({z}\right)\in {S}$
55 54 ad2ant2l ${⊢}\left(\left(\left({G}\in \mathrm{Grp}\wedge \left({S}\subseteq {B}\wedge {S}\ne \varnothing \right)\right)\wedge \forall {y}\in {S}\phantom{\rule{.4em}{0ex}}{inv}_{g}\left({G}\right)\left({y}\right)\in {S}\right)\wedge \left({x}\in {S}\wedge {z}\in {S}\right)\right)\to {inv}_{g}\left({G}\right)\left({z}\right)\in {S}$
56 oveq2
57 56 eleq1d
58 57 rspcv
59 55 58 syl
60 simplll ${⊢}\left(\left(\left({G}\in \mathrm{Grp}\wedge \left({S}\subseteq {B}\wedge {S}\ne \varnothing \right)\right)\wedge \forall {y}\in {S}\phantom{\rule{.4em}{0ex}}{inv}_{g}\left({G}\right)\left({y}\right)\in {S}\right)\wedge \left({x}\in {S}\wedge {z}\in {S}\right)\right)\to {G}\in \mathrm{Grp}$
61 simplrl ${⊢}\left(\left({G}\in \mathrm{Grp}\wedge \left({S}\subseteq {B}\wedge {S}\ne \varnothing \right)\right)\wedge \forall {y}\in {S}\phantom{\rule{.4em}{0ex}}{inv}_{g}\left({G}\right)\left({y}\right)\in {S}\right)\to {S}\subseteq {B}$
62 61 adantr ${⊢}\left(\left(\left({G}\in \mathrm{Grp}\wedge \left({S}\subseteq {B}\wedge {S}\ne \varnothing \right)\right)\wedge \forall {y}\in {S}\phantom{\rule{.4em}{0ex}}{inv}_{g}\left({G}\right)\left({y}\right)\in {S}\right)\wedge \left({x}\in {S}\wedge {z}\in {S}\right)\right)\to {S}\subseteq {B}$
63 simprl ${⊢}\left(\left(\left({G}\in \mathrm{Grp}\wedge \left({S}\subseteq {B}\wedge {S}\ne \varnothing \right)\right)\wedge \forall {y}\in {S}\phantom{\rule{.4em}{0ex}}{inv}_{g}\left({G}\right)\left({y}\right)\in {S}\right)\wedge \left({x}\in {S}\wedge {z}\in {S}\right)\right)\to {x}\in {S}$
64 62 63 sseldd ${⊢}\left(\left(\left({G}\in \mathrm{Grp}\wedge \left({S}\subseteq {B}\wedge {S}\ne \varnothing \right)\right)\wedge \forall {y}\in {S}\phantom{\rule{.4em}{0ex}}{inv}_{g}\left({G}\right)\left({y}\right)\in {S}\right)\wedge \left({x}\in {S}\wedge {z}\in {S}\right)\right)\to {x}\in {B}$
65 simprr ${⊢}\left(\left(\left({G}\in \mathrm{Grp}\wedge \left({S}\subseteq {B}\wedge {S}\ne \varnothing \right)\right)\wedge \forall {y}\in {S}\phantom{\rule{.4em}{0ex}}{inv}_{g}\left({G}\right)\left({y}\right)\in {S}\right)\wedge \left({x}\in {S}\wedge {z}\in {S}\right)\right)\to {z}\in {S}$
66 62 65 sseldd ${⊢}\left(\left(\left({G}\in \mathrm{Grp}\wedge \left({S}\subseteq {B}\wedge {S}\ne \varnothing \right)\right)\wedge \forall {y}\in {S}\phantom{\rule{.4em}{0ex}}{inv}_{g}\left({G}\right)\left({y}\right)\in {S}\right)\wedge \left({x}\in {S}\wedge {z}\in {S}\right)\right)\to {z}\in {B}$
67 1 38 2 39 60 64 66 grpsubinv
68 67 eleq1d
69 59 68 sylibd
70 69 anassrs
71 70 ralrimdva
72 71 ralimdva
73 72 impancom
74 51 73 mpd
75 oveq1 ${⊢}{x}={y}\to {x}{+}_{{G}}{z}={y}{+}_{{G}}{z}$
76 75 eleq1d ${⊢}{x}={y}\to \left({x}{+}_{{G}}{z}\in {S}↔{y}{+}_{{G}}{z}\in {S}\right)$
77 76 ralbidv ${⊢}{x}={y}\to \left(\forall {z}\in {S}\phantom{\rule{.4em}{0ex}}{x}{+}_{{G}}{z}\in {S}↔\forall {z}\in {S}\phantom{\rule{.4em}{0ex}}{y}{+}_{{G}}{z}\in {S}\right)$
78 77 cbvralvw ${⊢}\forall {x}\in {S}\phantom{\rule{.4em}{0ex}}\forall {z}\in {S}\phantom{\rule{.4em}{0ex}}{x}{+}_{{G}}{z}\in {S}↔\forall {y}\in {S}\phantom{\rule{.4em}{0ex}}\forall {z}\in {S}\phantom{\rule{.4em}{0ex}}{y}{+}_{{G}}{z}\in {S}$
79 74 78 sylib
80 r19.26 ${⊢}\forall {y}\in {S}\phantom{\rule{.4em}{0ex}}\left(\forall {z}\in {S}\phantom{\rule{.4em}{0ex}}{y}{+}_{{G}}{z}\in {S}\wedge {inv}_{g}\left({G}\right)\left({y}\right)\in {S}\right)↔\left(\forall {y}\in {S}\phantom{\rule{.4em}{0ex}}\forall {z}\in {S}\phantom{\rule{.4em}{0ex}}{y}{+}_{{G}}{z}\in {S}\wedge \forall {y}\in {S}\phantom{\rule{.4em}{0ex}}{inv}_{g}\left({G}\right)\left({y}\right)\in {S}\right)$
81 79 51 80 sylanbrc
82 11 12 81 3jca
83 82 exp42
84 83 3impd
85 1 38 39 issubg2 ${⊢}{G}\in \mathrm{Grp}\to \left({S}\in \mathrm{SubGrp}\left({G}\right)↔\left({S}\subseteq {B}\wedge {S}\ne \varnothing \wedge \forall {y}\in {S}\phantom{\rule{.4em}{0ex}}\left(\forall {z}\in {S}\phantom{\rule{.4em}{0ex}}{y}{+}_{{G}}{z}\in {S}\wedge {inv}_{g}\left({G}\right)\left({y}\right)\in {S}\right)\right)\right)$
86 84 85 sylibrd
87 10 86 impbid2