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