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