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 ~=g S -> ( SubGrp ` R ) ~~ ( SubGrp ` S ) )

Proof

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