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 ( 𝑅 ≃𝑔 𝑆 → ( SubGrp ‘ 𝑅 ) ≈ ( SubGrp ‘ 𝑆 ) )

Proof

Step Hyp Ref Expression
1 brgic ⊢ ( 𝑅 ≃𝑔 𝑆 ↔ ( 𝑅 GrpIso 𝑆 ) ≠ ∅ )
2 n0 ⊢ ( ( 𝑅 GrpIso 𝑆 ) ≠ ∅ ↔ ∃ 𝑎 𝑎 ∈ ( 𝑅 GrpIso 𝑆 ) )
3 1 2 bitri ⊢ ( 𝑅 ≃𝑔 𝑆 ↔ ∃ 𝑎 𝑎 ∈ ( 𝑅 GrpIso 𝑆 ) )
4 fvexd ⊢ ( 𝑎 ∈ ( 𝑅 GrpIso 𝑆 ) → ( SubGrp ‘ 𝑅 ) ∈ V )
5 fvexd ⊢ ( 𝑎 ∈ ( 𝑅 GrpIso 𝑆 ) → ( SubGrp ‘ 𝑆 ) ∈ V )
6 vex ⊢ 𝑎 ∈ V
7 6 imaex ⊢ ( 𝑎 “ 𝑏 ) ∈ V
8 7 2a1i ⊢ ( 𝑎 ∈ ( 𝑅 GrpIso 𝑆 ) → ( 𝑏 ∈ ( SubGrp ‘ 𝑅 ) → ( 𝑎 “ 𝑏 ) ∈ V ) )
9 6 cnvex ⊢ ◡ 𝑎 ∈ V
10 9 imaex ⊢ ( ◡ 𝑎 “ 𝑐 ) ∈ V
11 10 2a1i ⊢ ( 𝑎 ∈ ( 𝑅 GrpIso 𝑆 ) → ( 𝑐 ∈ ( SubGrp ‘ 𝑆 ) → ( ◡ 𝑎 “ 𝑐 ) ∈ V ) )
12 gimghm ⊢ ( 𝑎 ∈ ( 𝑅 GrpIso 𝑆 ) → 𝑎 ∈ ( 𝑅 GrpHom 𝑆 ) )
13 ghmima ⊢ ( ( 𝑎 ∈ ( 𝑅 GrpHom 𝑆 ) ∧ 𝑏 ∈ ( SubGrp ‘ 𝑅 ) ) → ( 𝑎 “ 𝑏 ) ∈ ( SubGrp ‘ 𝑆 ) )
14 12 13 sylan ⊢ ( ( 𝑎 ∈ ( 𝑅 GrpIso 𝑆 ) ∧ 𝑏 ∈ ( SubGrp ‘ 𝑅 ) ) → ( 𝑎 “ 𝑏 ) ∈ ( SubGrp ‘ 𝑆 ) )
15 eqid ⊢ ( Base ‘ 𝑅 ) = ( Base ‘ 𝑅 )
16 eqid ⊢ ( Base ‘ 𝑆 ) = ( Base ‘ 𝑆 )
17 15 16 gimf1o ⊢ ( 𝑎 ∈ ( 𝑅 GrpIso 𝑆 ) → 𝑎 : ( Base ‘ 𝑅 ) –1-1-onto→ ( Base ‘ 𝑆 ) )
18 f1of1 ⊢ ( 𝑎 : ( Base ‘ 𝑅 ) –1-1-onto→ ( Base ‘ 𝑆 ) → 𝑎 : ( Base ‘ 𝑅 ) –1-1→ ( Base ‘ 𝑆 ) )
19 17 18 syl ⊢ ( 𝑎 ∈ ( 𝑅 GrpIso 𝑆 ) → 𝑎 : ( Base ‘ 𝑅 ) –1-1→ ( Base ‘ 𝑆 ) )
20 15 subgss ⊢ ( 𝑏 ∈ ( SubGrp ‘ 𝑅 ) → 𝑏 ⊆ ( Base ‘ 𝑅 ) )
21 f1imacnv ⊢ ( ( 𝑎 : ( Base ‘ 𝑅 ) –1-1→ ( Base ‘ 𝑆 ) ∧ 𝑏 ⊆ ( Base ‘ 𝑅 ) ) → ( ◡ 𝑎 “ ( 𝑎 “ 𝑏 ) ) = 𝑏 )
22 19 20 21 syl2an ⊢ ( ( 𝑎 ∈ ( 𝑅 GrpIso 𝑆 ) ∧ 𝑏 ∈ ( SubGrp ‘ 𝑅 ) ) → ( ◡ 𝑎 “ ( 𝑎 “ 𝑏 ) ) = 𝑏 )
23 22 eqcomd ⊢ ( ( 𝑎 ∈ ( 𝑅 GrpIso 𝑆 ) ∧ 𝑏 ∈ ( SubGrp ‘ 𝑅 ) ) → 𝑏 = ( ◡ 𝑎 “ ( 𝑎 “ 𝑏 ) ) )
24 14 23 jca ⊢ ( ( 𝑎 ∈ ( 𝑅 GrpIso 𝑆 ) ∧ 𝑏 ∈ ( SubGrp ‘ 𝑅 ) ) → ( ( 𝑎 “ 𝑏 ) ∈ ( SubGrp ‘ 𝑆 ) ∧ 𝑏 = ( ◡ 𝑎 “ ( 𝑎 “ 𝑏 ) ) ) )
25 eleq1 ⊢ ( 𝑐 = ( 𝑎 “ 𝑏 ) → ( 𝑐 ∈ ( SubGrp ‘ 𝑆 ) ↔ ( 𝑎 “ 𝑏 ) ∈ ( SubGrp ‘ 𝑆 ) ) )
26 imaeq2 ⊢ ( 𝑐 = ( 𝑎 “ 𝑏 ) → ( ◡ 𝑎 “ 𝑐 ) = ( ◡ 𝑎 “ ( 𝑎 “ 𝑏 ) ) )
27 26 eqeq2d ⊢ ( 𝑐 = ( 𝑎 “ 𝑏 ) → ( 𝑏 = ( ◡ 𝑎 “ 𝑐 ) ↔ 𝑏 = ( ◡ 𝑎 “ ( 𝑎 “ 𝑏 ) ) ) )
28 25 27 anbi12d ⊢ ( 𝑐 = ( 𝑎 “ 𝑏 ) → ( ( 𝑐 ∈ ( SubGrp ‘ 𝑆 ) ∧ 𝑏 = ( ◡ 𝑎 “ 𝑐 ) ) ↔ ( ( 𝑎 “ 𝑏 ) ∈ ( SubGrp ‘ 𝑆 ) ∧ 𝑏 = ( ◡ 𝑎 “ ( 𝑎 “ 𝑏 ) ) ) ) )
29 24 28 syl5ibrcom ⊢ ( ( 𝑎 ∈ ( 𝑅 GrpIso 𝑆 ) ∧ 𝑏 ∈ ( SubGrp ‘ 𝑅 ) ) → ( 𝑐 = ( 𝑎 “ 𝑏 ) → ( 𝑐 ∈ ( SubGrp ‘ 𝑆 ) ∧ 𝑏 = ( ◡ 𝑎 “ 𝑐 ) ) ) )
30 29 impr ⊢ ( ( 𝑎 ∈ ( 𝑅 GrpIso 𝑆 ) ∧ ( 𝑏 ∈ ( SubGrp ‘ 𝑅 ) ∧ 𝑐 = ( 𝑎 “ 𝑏 ) ) ) → ( 𝑐 ∈ ( SubGrp ‘ 𝑆 ) ∧ 𝑏 = ( ◡ 𝑎 “ 𝑐 ) ) )
31 ghmpreima ⊢ ( ( 𝑎 ∈ ( 𝑅 GrpHom 𝑆 ) ∧ 𝑐 ∈ ( SubGrp ‘ 𝑆 ) ) → ( ◡ 𝑎 “ 𝑐 ) ∈ ( SubGrp ‘ 𝑅 ) )
32 12 31 sylan ⊢ ( ( 𝑎 ∈ ( 𝑅 GrpIso 𝑆 ) ∧ 𝑐 ∈ ( SubGrp ‘ 𝑆 ) ) → ( ◡ 𝑎 “ 𝑐 ) ∈ ( SubGrp ‘ 𝑅 ) )
33 f1ofo ⊢ ( 𝑎 : ( Base ‘ 𝑅 ) –1-1-onto→ ( Base ‘ 𝑆 ) → 𝑎 : ( Base ‘ 𝑅 ) –onto→ ( Base ‘ 𝑆 ) )
34 17 33 syl ⊢ ( 𝑎 ∈ ( 𝑅 GrpIso 𝑆 ) → 𝑎 : ( Base ‘ 𝑅 ) –onto→ ( Base ‘ 𝑆 ) )
35 16 subgss ⊢ ( 𝑐 ∈ ( SubGrp ‘ 𝑆 ) → 𝑐 ⊆ ( Base ‘ 𝑆 ) )
36 foimacnv ⊢ ( ( 𝑎 : ( Base ‘ 𝑅 ) –onto→ ( Base ‘ 𝑆 ) ∧ 𝑐 ⊆ ( Base ‘ 𝑆 ) ) → ( 𝑎 “ ( ◡ 𝑎 “ 𝑐 ) ) = 𝑐 )
37 34 35 36 syl2an ⊢ ( ( 𝑎 ∈ ( 𝑅 GrpIso 𝑆 ) ∧ 𝑐 ∈ ( SubGrp ‘ 𝑆 ) ) → ( 𝑎 “ ( ◡ 𝑎 “ 𝑐 ) ) = 𝑐 )
38 37 eqcomd ⊢ ( ( 𝑎 ∈ ( 𝑅 GrpIso 𝑆 ) ∧ 𝑐 ∈ ( SubGrp ‘ 𝑆 ) ) → 𝑐 = ( 𝑎 “ ( ◡ 𝑎 “ 𝑐 ) ) )
39 32 38 jca ⊢ ( ( 𝑎 ∈ ( 𝑅 GrpIso 𝑆 ) ∧ 𝑐 ∈ ( SubGrp ‘ 𝑆 ) ) → ( ( ◡ 𝑎 “ 𝑐 ) ∈ ( SubGrp ‘ 𝑅 ) ∧ 𝑐 = ( 𝑎 “ ( ◡ 𝑎 “ 𝑐 ) ) ) )
40 eleq1 ⊢ ( 𝑏 = ( ◡ 𝑎 “ 𝑐 ) → ( 𝑏 ∈ ( SubGrp ‘ 𝑅 ) ↔ ( ◡ 𝑎 “ 𝑐 ) ∈ ( SubGrp ‘ 𝑅 ) ) )
41 imaeq2 ⊢ ( 𝑏 = ( ◡ 𝑎 “ 𝑐 ) → ( 𝑎 “ 𝑏 ) = ( 𝑎 “ ( ◡ 𝑎 “ 𝑐 ) ) )
42 41 eqeq2d ⊢ ( 𝑏 = ( ◡ 𝑎 “ 𝑐 ) → ( 𝑐 = ( 𝑎 “ 𝑏 ) ↔ 𝑐 = ( 𝑎 “ ( ◡ 𝑎 “ 𝑐 ) ) ) )
43 40 42 anbi12d ⊢ ( 𝑏 = ( ◡ 𝑎 “ 𝑐 ) → ( ( 𝑏 ∈ ( SubGrp ‘ 𝑅 ) ∧ 𝑐 = ( 𝑎 “ 𝑏 ) ) ↔ ( ( ◡ 𝑎 “ 𝑐 ) ∈ ( SubGrp ‘ 𝑅 ) ∧ 𝑐 = ( 𝑎 “ ( ◡ 𝑎 “ 𝑐 ) ) ) ) )
44 39 43 syl5ibrcom ⊢ ( ( 𝑎 ∈ ( 𝑅 GrpIso 𝑆 ) ∧ 𝑐 ∈ ( SubGrp ‘ 𝑆 ) ) → ( 𝑏 = ( ◡ 𝑎 “ 𝑐 ) → ( 𝑏 ∈ ( SubGrp ‘ 𝑅 ) ∧ 𝑐 = ( 𝑎 “ 𝑏 ) ) ) )
45 44 impr ⊢ ( ( 𝑎 ∈ ( 𝑅 GrpIso 𝑆 ) ∧ ( 𝑐 ∈ ( SubGrp ‘ 𝑆 ) ∧ 𝑏 = ( ◡ 𝑎 “ 𝑐 ) ) ) → ( 𝑏 ∈ ( SubGrp ‘ 𝑅 ) ∧ 𝑐 = ( 𝑎 “ 𝑏 ) ) )
46 30 45 impbida ⊢ ( 𝑎 ∈ ( 𝑅 GrpIso 𝑆 ) → ( ( 𝑏 ∈ ( SubGrp ‘ 𝑅 ) ∧ 𝑐 = ( 𝑎 “ 𝑏 ) ) ↔ ( 𝑐 ∈ ( SubGrp ‘ 𝑆 ) ∧ 𝑏 = ( ◡ 𝑎 “ 𝑐 ) ) ) )
47 4 5 8 11 46 en2d ⊢ ( 𝑎 ∈ ( 𝑅 GrpIso 𝑆 ) → ( SubGrp ‘ 𝑅 ) ≈ ( SubGrp ‘ 𝑆 ) )
48 47 exlimiv ⊢ ( ∃ 𝑎 𝑎 ∈ ( 𝑅 GrpIso 𝑆 ) → ( SubGrp ‘ 𝑅 ) ≈ ( SubGrp ‘ 𝑆 ) )
49 3 48 sylbi ⊢ ( 𝑅 ≃𝑔 𝑆 → ( SubGrp ‘ 𝑅 ) ≈ ( SubGrp ‘ 𝑆 ) )