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 = {Base}_{G}$
	issubg4.p	$⊢ \underset{˙}{-} = -_{G}$
Assertion	issubg4	$⊢ G \in Grp \to (S \in SubGrp (G) \leftrightarrow (S \subseteq B \land S \neq \emptyset \land \forall x \in S \forall y \in S x \underset{˙}{-} y \in S))$

Proof

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

Metamath Proof Explorer

Theorem issubg4

Proof