Metamath Proof Explorer


Theorem 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 SubGrp R SubGrp S

Proof

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