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 ) )