Theorem issubg2

Description: Characterize the subgroups of a group by closure properties. (Contributed by Mario Carneiro, 2-Dec-2014)

	Ref	Expression
Hypotheses	issubg2.b	$$⊢B={\mathrm{Base}}_G$$
	issubg2.p	$$⊢\underset{\dot{}}{+}={+}_G$$
	issubg2.i	$$⊢I={inv}_g\left(G\right)$$
Assertion	issubg2	$$⊢G\in \mathrm{Grp}\to \left(S\in \mathrm{SubGrp}\left(G\right)\leftrightarrow \left(S\subseteq B\wedge S\ne \varnothing \wedge \forall x\in S\left(\forall y\in Sx\underset{\dot{}}{+}y\in S\wedge I\left(x\right)\in S\right)\right)\right)$$

Proof

Step	Hyp	Ref	Expression
1		issubg2.b	$$⊢B={\mathrm{Base}}_G$$
2		issubg2.p	$$⊢\underset{\dot{}}{+}={+}_G$$
3		issubg2.i	$$⊢I={inv}_g\left(G\right)$$
4	1	subgss	$$⊢S\in \mathrm{SubGrp}\left(G\right)\to S\subseteq B$$
5		eqid	$$⊢G{\upharpoonright }_{𝑠}S=G{\upharpoonright }_{𝑠}S$$
6	5	subgbas	$$⊢S\in \mathrm{SubGrp}\left(G\right)\to S={\mathrm{Base}}_{\left(G{\upharpoonright }_{𝑠}S\right)}$$
7	5	subggrp	$$⊢S\in \mathrm{SubGrp}\left(G\right)\to G{\upharpoonright }_{𝑠}S\in \mathrm{Grp}$$
8		eqid	$$⊢{\mathrm{Base}}_{\left(G{\upharpoonright }_{𝑠}S\right)}={\mathrm{Base}}_{\left(G{\upharpoonright }_{𝑠}S\right)}$$
9	8	grpbn0	$$⊢G{\upharpoonright }_{𝑠}S\in \mathrm{Grp}\to {\mathrm{Base}}_{\left(G{\upharpoonright }_{𝑠}S\right)}\ne \varnothing$$
10	7 9	syl	$$⊢S\in \mathrm{SubGrp}\left(G\right)\to {\mathrm{Base}}_{\left(G{\upharpoonright }_{𝑠}S\right)}\ne \varnothing$$
11	6 10	eqnetrd	$$⊢S\in \mathrm{SubGrp}\left(G\right)\to S\ne \varnothing$$
12	2	subgcl	$$⊢\left(S\in \mathrm{SubGrp}\left(G\right)\wedge x\in S\wedge y\in S\right)\to x\underset{\dot{}}{+}y\in S$$
13	12	3expa	$$⊢\left(\left(S\in \mathrm{SubGrp}\left(G\right)\wedge x\in S\right)\wedge y\in S\right)\to x\underset{\dot{}}{+}y\in S$$
14	13	ralrimiva	$$⊢\left(S\in \mathrm{SubGrp}\left(G\right)\wedge x\in S\right)\to \forall y\in Sx\underset{\dot{}}{+}y\in S$$
15	3	subginvcl	$$⊢\left(S\in \mathrm{SubGrp}\left(G\right)\wedge x\in S\right)\to I\left(x\right)\in S$$
16	14 15	jca	$$⊢\left(S\in \mathrm{SubGrp}\left(G\right)\wedge x\in S\right)\to \left(\forall y\in Sx\underset{\dot{}}{+}y\in S\wedge I\left(x\right)\in S\right)$$
17	16	ralrimiva	$$⊢S\in \mathrm{SubGrp}\left(G\right)\to \forall x\in S\left(\forall y\in Sx\underset{\dot{}}{+}y\in S\wedge I\left(x\right)\in S\right)$$
18	4 11 17	3jca	$$⊢S\in \mathrm{SubGrp}\left(G\right)\to \left(S\subseteq B\wedge S\ne \varnothing \wedge \forall x\in S\left(\forall y\in Sx\underset{\dot{}}{+}y\in S\wedge I\left(x\right)\in S\right)\right)$$
19		simpl	$$⊢\left(G\in \mathrm{Grp}\wedge \left(S\subseteq B\wedge S\ne \varnothing \wedge \forall x\in S\left(\forall y\in Sx\underset{\dot{}}{+}y\in S\wedge I\left(x\right)\in S\right)\right)\right)\to G\in \mathrm{Grp}$$
20		simpr1	$$⊢\left(G\in \mathrm{Grp}\wedge \left(S\subseteq B\wedge S\ne \varnothing \wedge \forall x\in S\left(\forall y\in Sx\underset{\dot{}}{+}y\in S\wedge I\left(x\right)\in S\right)\right)\right)\to S\subseteq B$$
21	5 1	ressbas2	$$⊢S\subseteq B\to S={\mathrm{Base}}_{\left(G{\upharpoonright }_{𝑠}S\right)}$$
22	20 21	syl	$$⊢\left(G\in \mathrm{Grp}\wedge \left(S\subseteq B\wedge S\ne \varnothing \wedge \forall x\in S\left(\forall y\in Sx\underset{\dot{}}{+}y\in S\wedge I\left(x\right)\in S\right)\right)\right)\to S={\mathrm{Base}}_{\left(G{\upharpoonright }_{𝑠}S\right)}$$
23		fvex	$$⊢{\mathrm{Base}}_{\left(G{\upharpoonright }_{𝑠}S\right)}\in \mathrm{V}$$
24	22 23	eqeltrdi	$$⊢\left(G\in \mathrm{Grp}\wedge \left(S\subseteq B\wedge S\ne \varnothing \wedge \forall x\in S\left(\forall y\in Sx\underset{\dot{}}{+}y\in S\wedge I\left(x\right)\in S\right)\right)\right)\to S\in \mathrm{V}$$
25	5 2	ressplusg	$$⊢S\in \mathrm{V}\to \underset{\dot{}}{+}={+}_{\left(G{\upharpoonright }_{𝑠}S\right)}$$
26	24 25	syl	$$⊢\left(G\in \mathrm{Grp}\wedge \left(S\subseteq B\wedge S\ne \varnothing \wedge \forall x\in S\left(\forall y\in Sx\underset{\dot{}}{+}y\in S\wedge I\left(x\right)\in S\right)\right)\right)\to \underset{\dot{}}{+}={+}_{\left(G{\upharpoonright }_{𝑠}S\right)}$$
27		simpr3	$$⊢\left(G\in \mathrm{Grp}\wedge \left(S\subseteq B\wedge S\ne \varnothing \wedge \forall x\in S\left(\forall y\in Sx\underset{\dot{}}{+}y\in S\wedge I\left(x\right)\in S\right)\right)\right)\to \forall x\in S\left(\forall y\in Sx\underset{\dot{}}{+}y\in S\wedge I\left(x\right)\in S\right)$$
28		simpl	$$⊢\left(\forall y\in Sx\underset{\dot{}}{+}y\in S\wedge I\left(x\right)\in S\right)\to \forall y\in Sx\underset{\dot{}}{+}y\in S$$
29	28	ralimi	$$⊢\forall x\in S\left(\forall y\in Sx\underset{\dot{}}{+}y\in S\wedge I\left(x\right)\in S\right)\to \forall x\in S\forall y\in Sx\underset{\dot{}}{+}y\in S$$
30	27 29	syl	$$⊢\left(G\in \mathrm{Grp}\wedge \left(S\subseteq B\wedge S\ne \varnothing \wedge \forall x\in S\left(\forall y\in Sx\underset{\dot{}}{+}y\in S\wedge I\left(x\right)\in S\right)\right)\right)\to \forall x\in S\forall y\in Sx\underset{\dot{}}{+}y\in S$$
31		oveq1	$$⊢x=u\to x\underset{\dot{}}{+}y=u\underset{\dot{}}{+}y$$
32	31	eleq1d	$$⊢x=u\to \left(x\underset{\dot{}}{+}y\in S\leftrightarrow u\underset{\dot{}}{+}y\in S\right)$$
33		oveq2	$$⊢y=v\to u\underset{\dot{}}{+}y=u\underset{\dot{}}{+}v$$
34	33	eleq1d	$$⊢y=v\to \left(u\underset{\dot{}}{+}y\in S\leftrightarrow u\underset{\dot{}}{+}v\in S\right)$$
35	32 34	rspc2v	$$⊢\left(u\in S\wedge v\in S\right)\to \left(\forall x\in S\forall y\in Sx\underset{\dot{}}{+}y\in S\to u\underset{\dot{}}{+}v\in S\right)$$
36	30 35	syl5com	$$⊢\left(G\in \mathrm{Grp}\wedge \left(S\subseteq B\wedge S\ne \varnothing \wedge \forall x\in S\left(\forall y\in Sx\underset{\dot{}}{+}y\in S\wedge I\left(x\right)\in S\right)\right)\right)\to \left(\left(u\in S\wedge v\in S\right)\to u\underset{\dot{}}{+}v\in S\right)$$
37	36	3impib	$$⊢\left(\left(G\in \mathrm{Grp}\wedge \left(S\subseteq B\wedge S\ne \varnothing \wedge \forall x\in S\left(\forall y\in Sx\underset{\dot{}}{+}y\in S\wedge I\left(x\right)\in S\right)\right)\right)\wedge u\in S\wedge v\in S\right)\to u\underset{\dot{}}{+}v\in S$$
38	20	sseld	$$⊢\left(G\in \mathrm{Grp}\wedge \left(S\subseteq B\wedge S\ne \varnothing \wedge \forall x\in S\left(\forall y\in Sx\underset{\dot{}}{+}y\in S\wedge I\left(x\right)\in S\right)\right)\right)\to \left(u\in S\to u\in B\right)$$
39	20	sseld	$$⊢\left(G\in \mathrm{Grp}\wedge \left(S\subseteq B\wedge S\ne \varnothing \wedge \forall x\in S\left(\forall y\in Sx\underset{\dot{}}{+}y\in S\wedge I\left(x\right)\in S\right)\right)\right)\to \left(v\in S\to v\in B\right)$$
40	20	sseld	$$⊢\left(G\in \mathrm{Grp}\wedge \left(S\subseteq B\wedge S\ne \varnothing \wedge \forall x\in S\left(\forall y\in Sx\underset{\dot{}}{+}y\in S\wedge I\left(x\right)\in S\right)\right)\right)\to \left(w\in S\to w\in B\right)$$
41	38 39 40	3anim123d	$$⊢\left(G\in \mathrm{Grp}\wedge \left(S\subseteq B\wedge S\ne \varnothing \wedge \forall x\in S\left(\forall y\in Sx\underset{\dot{}}{+}y\in S\wedge I\left(x\right)\in S\right)\right)\right)\to \left(\left(u\in S\wedge v\in S\wedge w\in S\right)\to \left(u\in B\wedge v\in B\wedge w\in B\right)\right)$$
42	41	imp	$$⊢\left(\left(G\in \mathrm{Grp}\wedge \left(S\subseteq B\wedge S\ne \varnothing \wedge \forall x\in S\left(\forall y\in Sx\underset{\dot{}}{+}y\in S\wedge I\left(x\right)\in S\right)\right)\right)\wedge \left(u\in S\wedge v\in S\wedge w\in S\right)\right)\to \left(u\in B\wedge v\in B\wedge w\in B\right)$$
43	1 2	grpass	$$⊢\left(G\in \mathrm{Grp}\wedge \left(u\in B\wedge v\in B\wedge w\in B\right)\right)\to \left(u\underset{\dot{}}{+}v\right)\underset{\dot{}}{+}w=u\underset{\dot{}}{+}\left(v\underset{\dot{}}{+}w\right)$$
44	43	adantlr	$$⊢\left(\left(G\in \mathrm{Grp}\wedge \left(S\subseteq B\wedge S\ne \varnothing \wedge \forall x\in S\left(\forall y\in Sx\underset{\dot{}}{+}y\in S\wedge I\left(x\right)\in S\right)\right)\right)\wedge \left(u\in B\wedge v\in B\wedge w\in B\right)\right)\to \left(u\underset{\dot{}}{+}v\right)\underset{\dot{}}{+}w=u\underset{\dot{}}{+}\left(v\underset{\dot{}}{+}w\right)$$
45	42 44	syldan	$$⊢\left(\left(G\in \mathrm{Grp}\wedge \left(S\subseteq B\wedge S\ne \varnothing \wedge \forall x\in S\left(\forall y\in Sx\underset{\dot{}}{+}y\in S\wedge I\left(x\right)\in S\right)\right)\right)\wedge \left(u\in S\wedge v\in S\wedge w\in S\right)\right)\to \left(u\underset{\dot{}}{+}v\right)\underset{\dot{}}{+}w=u\underset{\dot{}}{+}\left(v\underset{\dot{}}{+}w\right)$$
46		simpr2	$$⊢\left(G\in \mathrm{Grp}\wedge \left(S\subseteq B\wedge S\ne \varnothing \wedge \forall x\in S\left(\forall y\in Sx\underset{\dot{}}{+}y\in S\wedge I\left(x\right)\in S\right)\right)\right)\to S\ne \varnothing$$
47		n0	$$⊢S\ne \varnothing \leftrightarrow \exists uu\in S$$
48	46 47	sylib	$$⊢\left(G\in \mathrm{Grp}\wedge \left(S\subseteq B\wedge S\ne \varnothing \wedge \forall x\in S\left(\forall y\in Sx\underset{\dot{}}{+}y\in S\wedge I\left(x\right)\in S\right)\right)\right)\to \exists uu\in S$$
49	20	sselda	$$⊢\left(\left(G\in \mathrm{Grp}\wedge \left(S\subseteq B\wedge S\ne \varnothing \wedge \forall x\in S\left(\forall y\in Sx\underset{\dot{}}{+}y\in S\wedge I\left(x\right)\in S\right)\right)\right)\wedge u\in S\right)\to u\in B$$
50		eqid	$$⊢0_G=0_G$$
51	1 2 50 3	grplinv	$$⊢\left(G\in \mathrm{Grp}\wedge u\in B\right)\to I\left(u\right)\underset{\dot{}}{+}u=0_G$$
52	51	adantlr	$$⊢\left(\left(G\in \mathrm{Grp}\wedge \left(S\subseteq B\wedge S\ne \varnothing \wedge \forall x\in S\left(\forall y\in Sx\underset{\dot{}}{+}y\in S\wedge I\left(x\right)\in S\right)\right)\right)\wedge u\in B\right)\to I\left(u\right)\underset{\dot{}}{+}u=0_G$$
53	49 52	syldan	$$⊢\left(\left(G\in \mathrm{Grp}\wedge \left(S\subseteq B\wedge S\ne \varnothing \wedge \forall x\in S\left(\forall y\in Sx\underset{\dot{}}{+}y\in S\wedge I\left(x\right)\in S\right)\right)\right)\wedge u\in S\right)\to I\left(u\right)\underset{\dot{}}{+}u=0_G$$
54		simpr	$$⊢\left(\forall y\in Sx\underset{\dot{}}{+}y\in S\wedge I\left(x\right)\in S\right)\to I\left(x\right)\in S$$
55	54	ralimi	$$⊢\forall x\in S\left(\forall y\in Sx\underset{\dot{}}{+}y\in S\wedge I\left(x\right)\in S\right)\to \forall x\in SI\left(x\right)\in S$$
56	27 55	syl	$$⊢\left(G\in \mathrm{Grp}\wedge \left(S\subseteq B\wedge S\ne \varnothing \wedge \forall x\in S\left(\forall y\in Sx\underset{\dot{}}{+}y\in S\wedge I\left(x\right)\in S\right)\right)\right)\to \forall x\in SI\left(x\right)\in S$$
57		fveq2	$$⊢x=u\to I\left(x\right)=I\left(u\right)$$
58	57	eleq1d	$$⊢x=u\to \left(I\left(x\right)\in S\leftrightarrow I\left(u\right)\in S\right)$$
59	58	rspccva	$$⊢\left(\forall x\in SI\left(x\right)\in S\wedge u\in S\right)\to I\left(u\right)\in S$$
60	56 59	sylan	$$⊢\left(\left(G\in \mathrm{Grp}\wedge \left(S\subseteq B\wedge S\ne \varnothing \wedge \forall x\in S\left(\forall y\in Sx\underset{\dot{}}{+}y\in S\wedge I\left(x\right)\in S\right)\right)\right)\wedge u\in S\right)\to I\left(u\right)\in S$$
61		simpr	$$⊢\left(\left(G\in \mathrm{Grp}\wedge \left(S\subseteq B\wedge S\ne \varnothing \wedge \forall x\in S\left(\forall y\in Sx\underset{\dot{}}{+}y\in S\wedge I\left(x\right)\in S\right)\right)\right)\wedge u\in S\right)\to u\in S$$
62	30	adantr	$$⊢\left(\left(G\in \mathrm{Grp}\wedge \left(S\subseteq B\wedge S\ne \varnothing \wedge \forall x\in S\left(\forall y\in Sx\underset{\dot{}}{+}y\in S\wedge I\left(x\right)\in S\right)\right)\right)\wedge u\in S\right)\to \forall x\in S\forall y\in Sx\underset{\dot{}}{+}y\in S$$
63		ovrspc2v	$$⊢\left(\left(I\left(u\right)\in S\wedge u\in S\right)\wedge \forall x\in S\forall y\in Sx\underset{\dot{}}{+}y\in S\right)\to I\left(u\right)\underset{\dot{}}{+}u\in S$$
64	60 61 62 63	syl21anc	$$⊢\left(\left(G\in \mathrm{Grp}\wedge \left(S\subseteq B\wedge S\ne \varnothing \wedge \forall x\in S\left(\forall y\in Sx\underset{\dot{}}{+}y\in S\wedge I\left(x\right)\in S\right)\right)\right)\wedge u\in S\right)\to I\left(u\right)\underset{\dot{}}{+}u\in S$$
65	53 64	eqeltrrd	$$⊢\left(\left(G\in \mathrm{Grp}\wedge \left(S\subseteq B\wedge S\ne \varnothing \wedge \forall x\in S\left(\forall y\in Sx\underset{\dot{}}{+}y\in S\wedge I\left(x\right)\in S\right)\right)\right)\wedge u\in S\right)\to 0_G\in S$$
66	48 65	exlimddv	$$⊢\left(G\in \mathrm{Grp}\wedge \left(S\subseteq B\wedge S\ne \varnothing \wedge \forall x\in S\left(\forall y\in Sx\underset{\dot{}}{+}y\in S\wedge I\left(x\right)\in S\right)\right)\right)\to 0_G\in S$$
67	1 2 50	grplid	$$⊢\left(G\in \mathrm{Grp}\wedge u\in B\right)\to 0_G\underset{\dot{}}{+}u=u$$
68	67	adantlr	$$⊢\left(\left(G\in \mathrm{Grp}\wedge \left(S\subseteq B\wedge S\ne \varnothing \wedge \forall x\in S\left(\forall y\in Sx\underset{\dot{}}{+}y\in S\wedge I\left(x\right)\in S\right)\right)\right)\wedge u\in B\right)\to 0_G\underset{\dot{}}{+}u=u$$
69	49 68	syldan	$$⊢\left(\left(G\in \mathrm{Grp}\wedge \left(S\subseteq B\wedge S\ne \varnothing \wedge \forall x\in S\left(\forall y\in Sx\underset{\dot{}}{+}y\in S\wedge I\left(x\right)\in S\right)\right)\right)\wedge u\in S\right)\to 0_G\underset{\dot{}}{+}u=u$$
70	22 26 37 45 66 69 60 53	isgrpd	$$⊢\left(G\in \mathrm{Grp}\wedge \left(S\subseteq B\wedge S\ne \varnothing \wedge \forall x\in S\left(\forall y\in Sx\underset{\dot{}}{+}y\in S\wedge I\left(x\right)\in S\right)\right)\right)\to G{\upharpoonright }_{𝑠}S\in \mathrm{Grp}$$
71	1	issubg	$$⊢S\in \mathrm{SubGrp}\left(G\right)\leftrightarrow \left(G\in \mathrm{Grp}\wedge S\subseteq B\wedge G{\upharpoonright }_{𝑠}S\in \mathrm{Grp}\right)$$
72	19 20 70 71	syl3anbrc	$$⊢\left(G\in \mathrm{Grp}\wedge \left(S\subseteq B\wedge S\ne \varnothing \wedge \forall x\in S\left(\forall y\in Sx\underset{\dot{}}{+}y\in S\wedge I\left(x\right)\in S\right)\right)\right)\to S\in \mathrm{SubGrp}\left(G\right)$$
73	72	ex	$$⊢G\in \mathrm{Grp}\to \left(\left(S\subseteq B\wedge S\ne \varnothing \wedge \forall x\in S\left(\forall y\in Sx\underset{\dot{}}{+}y\in S\wedge I\left(x\right)\in S\right)\right)\to S\in \mathrm{SubGrp}\left(G\right)\right)$$
74	18 73	impbid2	$$⊢G\in \mathrm{Grp}\to \left(S\in \mathrm{SubGrp}\left(G\right)\leftrightarrow \left(S\subseteq B\wedge S\ne \varnothing \wedge \forall x\in S\left(\forall y\in Sx\underset{\dot{}}{+}y\in S\wedge I\left(x\right)\in S\right)\right)\right)$$