Metamath Proof Explorer

Theorem conjsubg

Description: A conjugated subgroup is also a subgroup. (Contributed by Mario Carneiro, 13-Jan-2015)

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

Proof

Step Hyp Ref Expression
1 conjghm.x ⊢ 𝑋 = ( Base ‘ 𝐺 )
2 conjghm.p ⊢ + = ( +g ‘ 𝐺 )
3 conjghm.m ⊢ − = ( -g ‘ 𝐺 )
4 conjsubg.f ⊢ 𝐹 = ( 𝑥 ∈ 𝑆 ↦ ( ( 𝐴 + 𝑥 ) − 𝐴 ) )
5 1 subgss ⊢ ( 𝑆 ∈ ( SubGrp ‘ 𝐺 ) → 𝑆 ⊆ 𝑋 )
6 5 adantr ⊢ ( ( 𝑆 ∈ ( SubGrp ‘ 𝐺 ) ∧ 𝐴 ∈ 𝑋 ) → 𝑆 ⊆ 𝑋 )
7 df-ima ⊢ ( ( 𝑥 ∈ 𝑋 ↦ ( ( 𝐴 + 𝑥 ) − 𝐴 ) ) “ 𝑆 ) = ran ( ( 𝑥 ∈ 𝑋 ↦ ( ( 𝐴 + 𝑥 ) − 𝐴 ) ) ↾ 𝑆 )
8 resmpt ⊢ ( 𝑆 ⊆ 𝑋 → ( ( 𝑥 ∈ 𝑋 ↦ ( ( 𝐴 + 𝑥 ) − 𝐴 ) ) ↾ 𝑆 ) = ( 𝑥 ∈ 𝑆 ↦ ( ( 𝐴 + 𝑥 ) − 𝐴 ) ) )
9 8 4 eqtr4di ⊢ ( 𝑆 ⊆ 𝑋 → ( ( 𝑥 ∈ 𝑋 ↦ ( ( 𝐴 + 𝑥 ) − 𝐴 ) ) ↾ 𝑆 ) = 𝐹 )
10 9 rneqd ⊢ ( 𝑆 ⊆ 𝑋 → ran ( ( 𝑥 ∈ 𝑋 ↦ ( ( 𝐴 + 𝑥 ) − 𝐴 ) ) ↾ 𝑆 ) = ran 𝐹 )
11 7 10 eqtrid ⊢ ( 𝑆 ⊆ 𝑋 → ( ( 𝑥 ∈ 𝑋 ↦ ( ( 𝐴 + 𝑥 ) − 𝐴 ) ) “ 𝑆 ) = ran 𝐹 )
12 6 11 syl ⊢ ( ( 𝑆 ∈ ( SubGrp ‘ 𝐺 ) ∧ 𝐴 ∈ 𝑋 ) → ( ( 𝑥 ∈ 𝑋 ↦ ( ( 𝐴 + 𝑥 ) − 𝐴 ) ) “ 𝑆 ) = ran 𝐹 )
13 subgrcl ⊢ ( 𝑆 ∈ ( SubGrp ‘ 𝐺 ) → 𝐺 ∈ Grp )
14 eqid ⊢ ( 𝑥 ∈ 𝑋 ↦ ( ( 𝐴 + 𝑥 ) − 𝐴 ) ) = ( 𝑥 ∈ 𝑋 ↦ ( ( 𝐴 + 𝑥 ) − 𝐴 ) )
15 1 2 3 14 conjghm ⊢ ( ( 𝐺 ∈ Grp ∧ 𝐴 ∈ 𝑋 ) → ( ( 𝑥 ∈ 𝑋 ↦ ( ( 𝐴 + 𝑥 ) − 𝐴 ) ) ∈ ( 𝐺 GrpHom 𝐺 ) ∧ ( 𝑥 ∈ 𝑋 ↦ ( ( 𝐴 + 𝑥 ) − 𝐴 ) ) : 𝑋 –1-1-onto→ 𝑋 ) )
16 13 15 sylan ⊢ ( ( 𝑆 ∈ ( SubGrp ‘ 𝐺 ) ∧ 𝐴 ∈ 𝑋 ) → ( ( 𝑥 ∈ 𝑋 ↦ ( ( 𝐴 + 𝑥 ) − 𝐴 ) ) ∈ ( 𝐺 GrpHom 𝐺 ) ∧ ( 𝑥 ∈ 𝑋 ↦ ( ( 𝐴 + 𝑥 ) − 𝐴 ) ) : 𝑋 –1-1-onto→ 𝑋 ) )
17 16 simpld ⊢ ( ( 𝑆 ∈ ( SubGrp ‘ 𝐺 ) ∧ 𝐴 ∈ 𝑋 ) → ( 𝑥 ∈ 𝑋 ↦ ( ( 𝐴 + 𝑥 ) − 𝐴 ) ) ∈ ( 𝐺 GrpHom 𝐺 ) )
18 simpl ⊢ ( ( 𝑆 ∈ ( SubGrp ‘ 𝐺 ) ∧ 𝐴 ∈ 𝑋 ) → 𝑆 ∈ ( SubGrp ‘ 𝐺 ) )
19 ghmima ⊢ ( ( ( 𝑥 ∈ 𝑋 ↦ ( ( 𝐴 + 𝑥 ) − 𝐴 ) ) ∈ ( 𝐺 GrpHom 𝐺 ) ∧ 𝑆 ∈ ( SubGrp ‘ 𝐺 ) ) → ( ( 𝑥 ∈ 𝑋 ↦ ( ( 𝐴 + 𝑥 ) − 𝐴 ) ) “ 𝑆 ) ∈ ( SubGrp ‘ 𝐺 ) )
20 17 18 19 syl2anc ⊢ ( ( 𝑆 ∈ ( SubGrp ‘ 𝐺 ) ∧ 𝐴 ∈ 𝑋 ) → ( ( 𝑥 ∈ 𝑋 ↦ ( ( 𝐴 + 𝑥 ) − 𝐴 ) ) “ 𝑆 ) ∈ ( SubGrp ‘ 𝐺 ) )
21 12 20 eqeltrrd ⊢ ( ( 𝑆 ∈ ( SubGrp ‘ 𝐺 ) ∧ 𝐴 ∈ 𝑋 ) → ran 𝐹 ∈ ( SubGrp ‘ 𝐺 ) )