gicsubgen

Description: A less trivial example of a group invariant: cardinality of the subgroup lattice. (Contributed by Stefan O'Rear, 25-Jan-2015)

		Ref	Expression
	Assertion	gicsubgen	$⊢ R ≃_{𝑔} S \to SubGrp (R) \approx SubGrp (S)$

Proof

Step	Hyp	Ref	Expression
1		brgic	$⊢ R ≃_{𝑔} S \leftrightarrow R GrpIso S \neq \emptyset$
2		n0	$⊢ R GrpIso S \neq \emptyset \leftrightarrow \exists a a \in (R GrpIso S)$
3	1 2	bitri	$⊢ R ≃_{𝑔} S \leftrightarrow \exists a a \in (R GrpIso S)$
4		fvexd	$⊢ a \in (R GrpIso S) \to SubGrp (R) \in V$
5		fvexd	$⊢ a \in (R GrpIso S) \to SubGrp (S) \in V$
6		vex	$⊢ a \in V$
7	6	imaex	$⊢ a [b] \in V$
8	7	2a1i	$⊢ a \in (R GrpIso S) \to (b \in SubGrp (R) \to a [b] \in V)$
9	6	cnvex	$⊢ a^{-1} \in V$
10	9	imaex	$⊢ a^{-1} [c] \in V$
11	10	2a1i	$⊢ a \in (R GrpIso S) \to (c \in SubGrp (S) \to a^{-1} [c] \in V)$
12		gimghm	$⊢ a \in (R GrpIso S) \to a \in (R GrpHom S)$
13		ghmima	$⊢ (a \in (R GrpHom S) \land b \in SubGrp (R)) \to a [b] \in SubGrp (S)$
14	12 13	sylan	$⊢ (a \in (R GrpIso S) \land b \in SubGrp (R)) \to a [b] \in SubGrp (S)$
15		eqid	$⊢ {Base}_{R} = {Base}_{R}$
16		eqid	$⊢ {Base}_{S} = {Base}_{S}$
17	15 16	gimf1o	$⊢ a \in (R GrpIso S) \to a : {Base}_{R} \underset{1-1 onto}{⟶} {Base}_{S}$
18		f1of1	$⊢ a : {Base}_{R} \underset{1-1 onto}{⟶} {Base}_{S} \to a : {Base}_{R} \underset{1-1}{⟶} {Base}_{S}$
19	17 18	syl	$⊢ a \in (R GrpIso S) \to a : {Base}_{R} \underset{1-1}{⟶} {Base}_{S}$
20	15	subgss	$⊢ b \in SubGrp (R) \to b \subseteq {Base}_{R}$
21		f1imacnv	$⊢ (a : {Base}_{R} \underset{1-1}{⟶} {Base}_{S} \land b \subseteq {Base}_{R}) \to a^{-1} [a [b]] = b$
22	19 20 21	syl2an	$⊢ (a \in (R GrpIso S) \land b \in SubGrp (R)) \to a^{-1} [a [b]] = b$
23	22	eqcomd	$⊢ (a \in (R GrpIso S) \land b \in SubGrp (R)) \to b = a^{-1} [a [b]]$
24	14 23	jca	$⊢ (a \in (R GrpIso S) \land b \in SubGrp (R)) \to (a [b] \in SubGrp (S) \land b = a^{-1} [a [b]])$
25		eleq1	$⊢ c = a [b] \to (c \in SubGrp (S) \leftrightarrow a [b] \in SubGrp (S))$
26		imaeq2	$⊢ c = a [b] \to a^{-1} [c] = a^{-1} [a [b]]$
27	26	eqeq2d	$⊢ c = a [b] \to (b = a^{-1} [c] \leftrightarrow b = a^{-1} [a [b]])$
28	25 27	anbi12d	$⊢ c = a [b] \to ((c \in SubGrp (S) \land b = a^{-1} [c]) \leftrightarrow (a [b] \in SubGrp (S) \land b = a^{-1} [a [b]]))$
29	24 28	syl5ibrcom	$⊢ (a \in (R GrpIso S) \land b \in SubGrp (R)) \to (c = a [b] \to (c \in SubGrp (S) \land b = a^{-1} [c]))$
30	29	impr	$⊢ (a \in (R GrpIso S) \land (b \in SubGrp (R) \land c = a [b])) \to (c \in SubGrp (S) \land b = a^{-1} [c])$
31		ghmpreima	$⊢ (a \in (R GrpHom S) \land c \in SubGrp (S)) \to a^{-1} [c] \in SubGrp (R)$
32	12 31	sylan	$⊢ (a \in (R GrpIso S) \land c \in SubGrp (S)) \to a^{-1} [c] \in SubGrp (R)$
33		f1ofo	$⊢ a : {Base}_{R} \underset{1-1 onto}{⟶} {Base}_{S} \to a : {Base}_{R} \underset{onto}{⟶} {Base}_{S}$
34	17 33	syl	$⊢ a \in (R GrpIso S) \to a : {Base}_{R} \underset{onto}{⟶} {Base}_{S}$
35	16	subgss	$⊢ c \in SubGrp (S) \to c \subseteq {Base}_{S}$
36		foimacnv	$⊢ (a : {Base}_{R} \underset{onto}{⟶} {Base}_{S} \land c \subseteq {Base}_{S}) \to a [a^{-1} [c]] = c$
37	34 35 36	syl2an	$⊢ (a \in (R GrpIso S) \land c \in SubGrp (S)) \to a [a^{-1} [c]] = c$
38	37	eqcomd	$⊢ (a \in (R GrpIso S) \land c \in SubGrp (S)) \to c = a [a^{-1} [c]]$
39	32 38	jca	$⊢ (a \in (R GrpIso S) \land c \in SubGrp (S)) \to (a^{-1} [c] \in SubGrp (R) \land c = a [a^{-1} [c]])$
40		eleq1	$⊢ b = a^{-1} [c] \to (b \in SubGrp (R) \leftrightarrow a^{-1} [c] \in SubGrp (R))$
41		imaeq2	$⊢ b = a^{-1} [c] \to a [b] = a [a^{-1} [c]]$
42	41	eqeq2d	$⊢ b = a^{-1} [c] \to (c = a [b] \leftrightarrow c = a [a^{-1} [c]])$
43	40 42	anbi12d	$⊢ b = a^{-1} [c] \to ((b \in SubGrp (R) \land c = a [b]) \leftrightarrow (a^{-1} [c] \in SubGrp (R) \land c = a [a^{-1} [c]]))$
44	39 43	syl5ibrcom	$⊢ (a \in (R GrpIso S) \land c \in SubGrp (S)) \to (b = a^{-1} [c] \to (b \in SubGrp (R) \land c = a [b]))$
45	44	impr	$⊢ (a \in (R GrpIso S) \land (c \in SubGrp (S) \land b = a^{-1} [c])) \to (b \in SubGrp (R) \land c = a [b])$
46	30 45	impbida	$⊢ a \in (R GrpIso S) \to ((b \in SubGrp (R) \land c = a [b]) \leftrightarrow (c \in SubGrp (S) \land b = a^{-1} [c]))$
47	4 5 8 11 46	en2d	$⊢ a \in (R GrpIso S) \to SubGrp (R) \approx SubGrp (S)$
48	47	exlimiv	$⊢ \exists a a \in (R GrpIso S) \to SubGrp (R) \approx SubGrp (S)$
49	3 48	sylbi	$⊢ R ≃_{𝑔} S \to SubGrp (R) \approx SubGrp (S)$

Metamath Proof Explorer

Theorem gicsubgen

Proof