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