Metamath Proof Explorer


Theorem conjsubgen

Description: A conjugated subgroup is equinumerous to the original subgroup. (Contributed by Mario Carneiro, 18-Jan-2015)

Ref Expression
Hypotheses conjghm.x 𝑋 = ( Base ‘ 𝐺 )
conjghm.p + = ( +g𝐺 )
conjghm.m = ( -g𝐺 )
conjsubg.f 𝐹 = ( 𝑥𝑆 ↦ ( ( 𝐴 + 𝑥 ) 𝐴 ) )
Assertion conjsubgen ( ( 𝑆 ∈ ( SubGrp ‘ 𝐺 ) ∧ 𝐴𝑋 ) → 𝑆 ≈ ran 𝐹 )

Proof

Step Hyp Ref Expression
1 conjghm.x 𝑋 = ( Base ‘ 𝐺 )
2 conjghm.p + = ( +g𝐺 )
3 conjghm.m = ( -g𝐺 )
4 conjsubg.f 𝐹 = ( 𝑥𝑆 ↦ ( ( 𝐴 + 𝑥 ) 𝐴 ) )
5 subgrcl ( 𝑆 ∈ ( SubGrp ‘ 𝐺 ) → 𝐺 ∈ Grp )
6 eqid ( 𝑥𝑋 ↦ ( ( 𝐴 + 𝑥 ) 𝐴 ) ) = ( 𝑥𝑋 ↦ ( ( 𝐴 + 𝑥 ) 𝐴 ) )
7 1 2 3 6 conjghm ( ( 𝐺 ∈ Grp ∧ 𝐴𝑋 ) → ( ( 𝑥𝑋 ↦ ( ( 𝐴 + 𝑥 ) 𝐴 ) ) ∈ ( 𝐺 GrpHom 𝐺 ) ∧ ( 𝑥𝑋 ↦ ( ( 𝐴 + 𝑥 ) 𝐴 ) ) : 𝑋1-1-onto𝑋 ) )
8 5 7 sylan ( ( 𝑆 ∈ ( SubGrp ‘ 𝐺 ) ∧ 𝐴𝑋 ) → ( ( 𝑥𝑋 ↦ ( ( 𝐴 + 𝑥 ) 𝐴 ) ) ∈ ( 𝐺 GrpHom 𝐺 ) ∧ ( 𝑥𝑋 ↦ ( ( 𝐴 + 𝑥 ) 𝐴 ) ) : 𝑋1-1-onto𝑋 ) )
9 f1of1 ( ( 𝑥𝑋 ↦ ( ( 𝐴 + 𝑥 ) 𝐴 ) ) : 𝑋1-1-onto𝑋 → ( 𝑥𝑋 ↦ ( ( 𝐴 + 𝑥 ) 𝐴 ) ) : 𝑋1-1𝑋 )
10 8 9 simpl2im ( ( 𝑆 ∈ ( SubGrp ‘ 𝐺 ) ∧ 𝐴𝑋 ) → ( 𝑥𝑋 ↦ ( ( 𝐴 + 𝑥 ) 𝐴 ) ) : 𝑋1-1𝑋 )
11 1 subgss ( 𝑆 ∈ ( SubGrp ‘ 𝐺 ) → 𝑆𝑋 )
12 11 adantr ( ( 𝑆 ∈ ( SubGrp ‘ 𝐺 ) ∧ 𝐴𝑋 ) → 𝑆𝑋 )
13 f1ssres ( ( ( 𝑥𝑋 ↦ ( ( 𝐴 + 𝑥 ) 𝐴 ) ) : 𝑋1-1𝑋𝑆𝑋 ) → ( ( 𝑥𝑋 ↦ ( ( 𝐴 + 𝑥 ) 𝐴 ) ) ↾ 𝑆 ) : 𝑆1-1𝑋 )
14 10 12 13 syl2anc ( ( 𝑆 ∈ ( SubGrp ‘ 𝐺 ) ∧ 𝐴𝑋 ) → ( ( 𝑥𝑋 ↦ ( ( 𝐴 + 𝑥 ) 𝐴 ) ) ↾ 𝑆 ) : 𝑆1-1𝑋 )
15 12 resmptd ( ( 𝑆 ∈ ( SubGrp ‘ 𝐺 ) ∧ 𝐴𝑋 ) → ( ( 𝑥𝑋 ↦ ( ( 𝐴 + 𝑥 ) 𝐴 ) ) ↾ 𝑆 ) = ( 𝑥𝑆 ↦ ( ( 𝐴 + 𝑥 ) 𝐴 ) ) )
16 15 4 eqtr4di ( ( 𝑆 ∈ ( SubGrp ‘ 𝐺 ) ∧ 𝐴𝑋 ) → ( ( 𝑥𝑋 ↦ ( ( 𝐴 + 𝑥 ) 𝐴 ) ) ↾ 𝑆 ) = 𝐹 )
17 f1eq1 ( ( ( 𝑥𝑋 ↦ ( ( 𝐴 + 𝑥 ) 𝐴 ) ) ↾ 𝑆 ) = 𝐹 → ( ( ( 𝑥𝑋 ↦ ( ( 𝐴 + 𝑥 ) 𝐴 ) ) ↾ 𝑆 ) : 𝑆1-1𝑋𝐹 : 𝑆1-1𝑋 ) )
18 16 17 syl ( ( 𝑆 ∈ ( SubGrp ‘ 𝐺 ) ∧ 𝐴𝑋 ) → ( ( ( 𝑥𝑋 ↦ ( ( 𝐴 + 𝑥 ) 𝐴 ) ) ↾ 𝑆 ) : 𝑆1-1𝑋𝐹 : 𝑆1-1𝑋 ) )
19 14 18 mpbid ( ( 𝑆 ∈ ( SubGrp ‘ 𝐺 ) ∧ 𝐴𝑋 ) → 𝐹 : 𝑆1-1𝑋 )
20 f1f1orn ( 𝐹 : 𝑆1-1𝑋𝐹 : 𝑆1-1-onto→ ran 𝐹 )
21 19 20 syl ( ( 𝑆 ∈ ( SubGrp ‘ 𝐺 ) ∧ 𝐴𝑋 ) → 𝐹 : 𝑆1-1-onto→ ran 𝐹 )
22 f1oeng ( ( 𝑆 ∈ ( SubGrp ‘ 𝐺 ) ∧ 𝐹 : 𝑆1-1-onto→ ran 𝐹 ) → 𝑆 ≈ ran 𝐹 )
23 21 22 syldan ( ( 𝑆 ∈ ( SubGrp ‘ 𝐺 ) ∧ 𝐴𝑋 ) → 𝑆 ≈ ran 𝐹 )