issubg3

Description: A subgroup is a symmetric submonoid. (Contributed by Mario Carneiro, 7-Mar-2015)

		Ref	Expression
	Hypothesis	issubg3.i	$⊢ I = {inv}_{g} (G)$
	Assertion	issubg3	$⊢ G \in Grp \to (S \in SubGrp (G) \leftrightarrow (S \in SubMnd (G) \land \forall x \in S I (x) \in S))$

Proof

Step	Hyp	Ref	Expression
1		issubg3.i	$⊢ I = {inv}_{g} (G)$
2		eqid	$⊢ 0_{G} = 0_{G}$
3	2	subg0cl	$⊢ S \in SubGrp (G) \to 0_{G} \in S$
4	3	a1i	$⊢ G \in Grp \to (S \in SubGrp (G) \to 0_{G} \in S)$
5	2	subm0cl	$⊢ S \in SubMnd (G) \to 0_{G} \in S$
6	5	adantr	$⊢ (S \in SubMnd (G) \land \forall x \in S I (x) \in S) \to 0_{G} \in S$
7	6	a1i	$⊢ G \in Grp \to ((S \in SubMnd (G) \land \forall x \in S I (x) \in S) \to 0_{G} \in S)$
8		ne0i	$⊢ 0_{G} \in S \to S \neq \emptyset$
9		id	$⊢ 0_{G} \in S \to 0_{G} \in S$
10	8 9	2thd	$⊢ 0_{G} \in S \to (S \neq \emptyset \leftrightarrow 0_{G} \in S)$
11	10	adantl	$⊢ (G \in Grp \land 0_{G} \in S) \to (S \neq \emptyset \leftrightarrow 0_{G} \in S)$
12		r19.26	$⊢ \forall x \in S (\forall y \in S x +_{G} y \in S \land I (x) \in S) \leftrightarrow (\forall x \in S \forall y \in S x +_{G} y \in S \land \forall x \in S I (x) \in S)$
13	12	a1i	$⊢ (G \in Grp \land 0_{G} \in S) \to (\forall x \in S (\forall y \in S x +_{G} y \in S \land I (x) \in S) \leftrightarrow (\forall x \in S \forall y \in S x +_{G} y \in S \land \forall x \in S I (x) \in S))$
14	11 13	3anbi23d	$⊢ (G \in Grp \land 0_{G} \in S) \to ((S \subseteq {Base}_{G} \land S \neq \emptyset \land \forall x \in S (\forall y \in S x +_{G} y \in S \land I (x) \in S)) \leftrightarrow (S \subseteq {Base}_{G} \land 0_{G} \in S \land (\forall x \in S \forall y \in S x +_{G} y \in S \land \forall x \in S I (x) \in S)))$
15		anass	$⊢ (((S \subseteq {Base}_{G} \land 0_{G} \in S) \land \forall x \in S \forall y \in S x +_{G} y \in S) \land \forall x \in S I (x) \in S) \leftrightarrow ((S \subseteq {Base}_{G} \land 0_{G} \in S) \land (\forall x \in S \forall y \in S x +_{G} y \in S \land \forall x \in S I (x) \in S))$
16		df-3an	$⊢ (S \subseteq {Base}_{G} \land 0_{G} \in S \land \forall x \in S \forall y \in S x +_{G} y \in S) \leftrightarrow ((S \subseteq {Base}_{G} \land 0_{G} \in S) \land \forall x \in S \forall y \in S x +_{G} y \in S)$
17	16	anbi1i	$⊢ ((S \subseteq {Base}_{G} \land 0_{G} \in S \land \forall x \in S \forall y \in S x +_{G} y \in S) \land \forall x \in S I (x) \in S) \leftrightarrow (((S \subseteq {Base}_{G} \land 0_{G} \in S) \land \forall x \in S \forall y \in S x +_{G} y \in S) \land \forall x \in S I (x) \in S)$
18		df-3an	$⊢ (S \subseteq {Base}_{G} \land 0_{G} \in S \land (\forall x \in S \forall y \in S x +_{G} y \in S \land \forall x \in S I (x) \in S)) \leftrightarrow ((S \subseteq {Base}_{G} \land 0_{G} \in S) \land (\forall x \in S \forall y \in S x +_{G} y \in S \land \forall x \in S I (x) \in S))$
19	15 17 18	3bitr4ri	$⊢ (S \subseteq {Base}_{G} \land 0_{G} \in S \land (\forall x \in S \forall y \in S x +_{G} y \in S \land \forall x \in S I (x) \in S)) \leftrightarrow ((S \subseteq {Base}_{G} \land 0_{G} \in S \land \forall x \in S \forall y \in S x +_{G} y \in S) \land \forall x \in S I (x) \in S)$
20	14 19	bitrdi	$⊢ (G \in Grp \land 0_{G} \in S) \to ((S \subseteq {Base}_{G} \land S \neq \emptyset \land \forall x \in S (\forall y \in S x +_{G} y \in S \land I (x) \in S)) \leftrightarrow ((S \subseteq {Base}_{G} \land 0_{G} \in S \land \forall x \in S \forall y \in S x +_{G} y \in S) \land \forall x \in S I (x) \in S))$
21		eqid	$⊢ {Base}_{G} = {Base}_{G}$
22		eqid	$⊢ +_{G} = +_{G}$
23	21 22 1	issubg2	$⊢ G \in Grp \to (S \in SubGrp (G) \leftrightarrow (S \subseteq {Base}_{G} \land S \neq \emptyset \land \forall x \in S (\forall y \in S x +_{G} y \in S \land I (x) \in S)))$
24	23	adantr	$⊢ (G \in Grp \land 0_{G} \in S) \to (S \in SubGrp (G) \leftrightarrow (S \subseteq {Base}_{G} \land S \neq \emptyset \land \forall x \in S (\forall y \in S x +_{G} y \in S \land I (x) \in S)))$
25		grpmnd	$⊢ G \in Grp \to G \in Mnd$
26	21 2 22	issubm	$⊢ G \in Mnd \to (S \in SubMnd (G) \leftrightarrow (S \subseteq {Base}_{G} \land 0_{G} \in S \land \forall x \in S \forall y \in S x +_{G} y \in S))$
27	25 26	syl	$⊢ G \in Grp \to (S \in SubMnd (G) \leftrightarrow (S \subseteq {Base}_{G} \land 0_{G} \in S \land \forall x \in S \forall y \in S x +_{G} y \in S))$
28	27	anbi1d	$⊢ G \in Grp \to ((S \in SubMnd (G) \land \forall x \in S I (x) \in S) \leftrightarrow ((S \subseteq {Base}_{G} \land 0_{G} \in S \land \forall x \in S \forall y \in S x +_{G} y \in S) \land \forall x \in S I (x) \in S))$
29	28	adantr	$⊢ (G \in Grp \land 0_{G} \in S) \to ((S \in SubMnd (G) \land \forall x \in S I (x) \in S) \leftrightarrow ((S \subseteq {Base}_{G} \land 0_{G} \in S \land \forall x \in S \forall y \in S x +_{G} y \in S) \land \forall x \in S I (x) \in S))$
30	20 24 29	3bitr4d	$⊢ (G \in Grp \land 0_{G} \in S) \to (S \in SubGrp (G) \leftrightarrow (S \in SubMnd (G) \land \forall x \in S I (x) \in S))$
31	30	ex	$⊢ G \in Grp \to (0_{G} \in S \to (S \in SubGrp (G) \leftrightarrow (S \in SubMnd (G) \land \forall x \in S I (x) \in S)))$
32	4 7 31	pm5.21ndd	$⊢ G \in Grp \to (S \in SubGrp (G) \leftrightarrow (S \in SubMnd (G) \land \forall x \in S I (x) \in S))$

Metamath Proof Explorer

Theorem issubg3

Proof