subgint

Description: The intersection of a nonempty collection of subgroups is a subgroup. (Contributed by Mario Carneiro, 7-Dec-2014)

		Ref	Expression
	Assertion	subgint	$⊢ (S \subseteq SubGrp (G) \land S \neq \emptyset) \to ⋂ S \in SubGrp (G)$

Proof

Step	Hyp	Ref	Expression
1		intssuni	$⊢ S \neq \emptyset \to ⋂ S \subseteq ⋃ S$
2	1	adantl	$⊢ (S \subseteq SubGrp (G) \land S \neq \emptyset) \to ⋂ S \subseteq ⋃ S$
3		ssel2	$⊢ (S \subseteq SubGrp (G) \land g \in S) \to g \in SubGrp (G)$
4	3	adantlr	$⊢ ((S \subseteq SubGrp (G) \land S \neq \emptyset) \land g \in S) \to g \in SubGrp (G)$
5		eqid	$⊢ {Base}_{G} = {Base}_{G}$
6	5	subgss	$⊢ g \in SubGrp (G) \to g \subseteq {Base}_{G}$
7	4 6	syl	$⊢ ((S \subseteq SubGrp (G) \land S \neq \emptyset) \land g \in S) \to g \subseteq {Base}_{G}$
8	7	ralrimiva	$⊢ (S \subseteq SubGrp (G) \land S \neq \emptyset) \to \forall g \in S g \subseteq {Base}_{G}$
9		unissb	$⊢ ⋃ S \subseteq {Base}_{G} \leftrightarrow \forall g \in S g \subseteq {Base}_{G}$
10	8 9	sylibr	$⊢ (S \subseteq SubGrp (G) \land S \neq \emptyset) \to ⋃ S \subseteq {Base}_{G}$
11	2 10	sstrd	$⊢ (S \subseteq SubGrp (G) \land S \neq \emptyset) \to ⋂ S \subseteq {Base}_{G}$
12		eqid	$⊢ 0_{G} = 0_{G}$
13	12	subg0cl	$⊢ g \in SubGrp (G) \to 0_{G} \in g$
14	4 13	syl	$⊢ ((S \subseteq SubGrp (G) \land S \neq \emptyset) \land g \in S) \to 0_{G} \in g$
15	14	ralrimiva	$⊢ (S \subseteq SubGrp (G) \land S \neq \emptyset) \to \forall g \in S 0_{G} \in g$
16		fvex	$⊢ 0_{G} \in V$
17	16	elint2	$⊢ 0_{G} \in ⋂ S \leftrightarrow \forall g \in S 0_{G} \in g$
18	15 17	sylibr	$⊢ (S \subseteq SubGrp (G) \land S \neq \emptyset) \to 0_{G} \in ⋂ S$
19	18	ne0d	$⊢ (S \subseteq SubGrp (G) \land S \neq \emptyset) \to ⋂ S \neq \emptyset$
20	4	adantlr	$⊢ (((S \subseteq SubGrp (G) \land S \neq \emptyset) \land (x \in ⋂ S \land y \in ⋂ S)) \land g \in S) \to g \in SubGrp (G)$
21		simprl	$⊢ ((S \subseteq SubGrp (G) \land S \neq \emptyset) \land (x \in ⋂ S \land y \in ⋂ S)) \to x \in ⋂ S$
22		elinti	$⊢ x \in ⋂ S \to (g \in S \to x \in g)$
23	22	imp	$⊢ (x \in ⋂ S \land g \in S) \to x \in g$
24	21 23	sylan	$⊢ (((S \subseteq SubGrp (G) \land S \neq \emptyset) \land (x \in ⋂ S \land y \in ⋂ S)) \land g \in S) \to x \in g$
25		simprr	$⊢ ((S \subseteq SubGrp (G) \land S \neq \emptyset) \land (x \in ⋂ S \land y \in ⋂ S)) \to y \in ⋂ S$
26		elinti	$⊢ y \in ⋂ S \to (g \in S \to y \in g)$
27	26	imp	$⊢ (y \in ⋂ S \land g \in S) \to y \in g$
28	25 27	sylan	$⊢ (((S \subseteq SubGrp (G) \land S \neq \emptyset) \land (x \in ⋂ S \land y \in ⋂ S)) \land g \in S) \to y \in g$
29		eqid	$⊢ +_{G} = +_{G}$
30	29	subgcl	$⊢ (g \in SubGrp (G) \land x \in g \land y \in g) \to x +_{G} y \in g$
31	20 24 28 30	syl3anc	$⊢ (((S \subseteq SubGrp (G) \land S \neq \emptyset) \land (x \in ⋂ S \land y \in ⋂ S)) \land g \in S) \to x +_{G} y \in g$
32	31	ralrimiva	$⊢ ((S \subseteq SubGrp (G) \land S \neq \emptyset) \land (x \in ⋂ S \land y \in ⋂ S)) \to \forall g \in S x +_{G} y \in g$
33		ovex	$⊢ x +_{G} y \in V$
34	33	elint2	$⊢ x +_{G} y \in ⋂ S \leftrightarrow \forall g \in S x +_{G} y \in g$
35	32 34	sylibr	$⊢ ((S \subseteq SubGrp (G) \land S \neq \emptyset) \land (x \in ⋂ S \land y \in ⋂ S)) \to x +_{G} y \in ⋂ S$
36	35	anassrs	$⊢ (((S \subseteq SubGrp (G) \land S \neq \emptyset) \land x \in ⋂ S) \land y \in ⋂ S) \to x +_{G} y \in ⋂ S$
37	36	ralrimiva	$⊢ ((S \subseteq SubGrp (G) \land S \neq \emptyset) \land x \in ⋂ S) \to \forall y \in ⋂ S x +_{G} y \in ⋂ S$
38	4	adantlr	$⊢ (((S \subseteq SubGrp (G) \land S \neq \emptyset) \land x \in ⋂ S) \land g \in S) \to g \in SubGrp (G)$
39	23	adantll	$⊢ (((S \subseteq SubGrp (G) \land S \neq \emptyset) \land x \in ⋂ S) \land g \in S) \to x \in g$
40		eqid	$⊢ {inv}_{g} (G) = {inv}_{g} (G)$
41	40	subginvcl	$⊢ (g \in SubGrp (G) \land x \in g) \to {inv}_{g} (G) (x) \in g$
42	38 39 41	syl2anc	$⊢ (((S \subseteq SubGrp (G) \land S \neq \emptyset) \land x \in ⋂ S) \land g \in S) \to {inv}_{g} (G) (x) \in g$
43	42	ralrimiva	$⊢ ((S \subseteq SubGrp (G) \land S \neq \emptyset) \land x \in ⋂ S) \to \forall g \in S {inv}_{g} (G) (x) \in g$
44		fvex	$⊢ {inv}_{g} (G) (x) \in V$
45	44	elint2	$⊢ {inv}_{g} (G) (x) \in ⋂ S \leftrightarrow \forall g \in S {inv}_{g} (G) (x) \in g$
46	43 45	sylibr	$⊢ ((S \subseteq SubGrp (G) \land S \neq \emptyset) \land x \in ⋂ S) \to {inv}_{g} (G) (x) \in ⋂ S$
47	37 46	jca	$⊢ ((S \subseteq SubGrp (G) \land S \neq \emptyset) \land x \in ⋂ S) \to (\forall y \in ⋂ S x +_{G} y \in ⋂ S \land {inv}_{g} (G) (x) \in ⋂ S)$
48	47	ralrimiva	$⊢ (S \subseteq SubGrp (G) \land S \neq \emptyset) \to \forall x \in ⋂ S (\forall y \in ⋂ S x +_{G} y \in ⋂ S \land {inv}_{g} (G) (x) \in ⋂ S)$
49		ssn0	$⊢ (S \subseteq SubGrp (G) \land S \neq \emptyset) \to SubGrp (G) \neq \emptyset$
50		n0	$⊢ SubGrp (G) \neq \emptyset \leftrightarrow \exists g g \in SubGrp (G)$
51		subgrcl	$⊢ g \in SubGrp (G) \to G \in Grp$
52	51	exlimiv	$⊢ \exists g g \in SubGrp (G) \to G \in Grp$
53	50 52	sylbi	$⊢ SubGrp (G) \neq \emptyset \to G \in Grp$
54	5 29 40	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 {inv}_{g} (G) (x) \in ⋂ S)))$
55	49 53 54	3syl	$⊢ (S \subseteq SubGrp (G) \land S \neq \emptyset) \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 {inv}_{g} (G) (x) \in ⋂ S)))$
56	11 19 48 55	mpbir3and	$⊢ (S \subseteq SubGrp (G) \land S \neq \emptyset) \to ⋂ S \in SubGrp (G)$

Metamath Proof Explorer

Theorem subgint

Proof