Metamath Proof Explorer

Theorem cayleylem2

Description: Lemma for cayley . (Contributed by Paul Chapman, 3-Mar-2008) (Revised by Mario Carneiro, 13-Jan-2015)

Ref Expression
Hypotheses cayleylem1.x ⊢ 𝑋 = ( Base ‘ 𝐺 )
cayleylem1.p ⊢ + = ( +g ‘ 𝐺 )
cayleylem1.u ⊢ 0 = ( 0g ‘ 𝐺 )
cayleylem1.h ⊢ 𝐻 = ( SymGrp ‘ 𝑋 )
cayleylem1.s ⊢ 𝑆 = ( Base ‘ 𝐻 )
cayleylem1.f ⊢ 𝐹 = ( 𝑔 ∈ 𝑋 ↦ ( 𝑎 ∈ 𝑋 ↦ ( 𝑔 + 𝑎 ) ) )
Assertion cayleylem2 ( 𝐺 ∈ Grp → 𝐹 : 𝑋 –1-1→ 𝑆 )

Proof

Step Hyp Ref Expression
1 cayleylem1.x ⊢ 𝑋 = ( Base ‘ 𝐺 )
2 cayleylem1.p ⊢ + = ( +g ‘ 𝐺 )
3 cayleylem1.u ⊢ 0 = ( 0g ‘ 𝐺 )
4 cayleylem1.h ⊢ 𝐻 = ( SymGrp ‘ 𝑋 )
5 cayleylem1.s ⊢ 𝑆 = ( Base ‘ 𝐻 )
6 cayleylem1.f ⊢ 𝐹 = ( 𝑔 ∈ 𝑋 ↦ ( 𝑎 ∈ 𝑋 ↦ ( 𝑔 + 𝑎 ) ) )
7 fveq1 ⊢ ( ( 𝐹 ‘ 𝑥 ) = ( 0g ‘ 𝐻 ) → ( ( 𝐹 ‘ 𝑥 ) ‘ 0 ) = ( ( 0g ‘ 𝐻 ) ‘ 0 ) )
8 simpr ⊢ ( ( 𝐺 ∈ Grp ∧ 𝑥 ∈ 𝑋 ) → 𝑥 ∈ 𝑋 )
9 1 3 grpidcl ⊢ ( 𝐺 ∈ Grp → 0 ∈ 𝑋 )
10 9 adantr ⊢ ( ( 𝐺 ∈ Grp ∧ 𝑥 ∈ 𝑋 ) → 0 ∈ 𝑋 )
11 6 1 grplactval ⊢ ( ( 𝑥 ∈ 𝑋 ∧ 0 ∈ 𝑋 ) → ( ( 𝐹 ‘ 𝑥 ) ‘ 0 ) = ( 𝑥 + 0 ) )
12 8 10 11 syl2anc ⊢ ( ( 𝐺 ∈ Grp ∧ 𝑥 ∈ 𝑋 ) → ( ( 𝐹 ‘ 𝑥 ) ‘ 0 ) = ( 𝑥 + 0 ) )
13 1 2 3 grprid ⊢ ( ( 𝐺 ∈ Grp ∧ 𝑥 ∈ 𝑋 ) → ( 𝑥 + 0 ) = 𝑥 )
14 12 13 eqtrd ⊢ ( ( 𝐺 ∈ Grp ∧ 𝑥 ∈ 𝑋 ) → ( ( 𝐹 ‘ 𝑥 ) ‘ 0 ) = 𝑥 )
15 1 fvexi ⊢ 𝑋 ∈ V
16 4 symgid ⊢ ( 𝑋 ∈ V → ( I ↾ 𝑋 ) = ( 0g ‘ 𝐻 ) )
17 15 16 ax-mp ⊢ ( I ↾ 𝑋 ) = ( 0g ‘ 𝐻 )
18 17 fveq1i ⊢ ( ( I ↾ 𝑋 ) ‘ 0 ) = ( ( 0g ‘ 𝐻 ) ‘ 0 )
19 fvresi ⊢ ( 0 ∈ 𝑋 → ( ( I ↾ 𝑋 ) ‘ 0 ) = 0 )
20 10 19 syl ⊢ ( ( 𝐺 ∈ Grp ∧ 𝑥 ∈ 𝑋 ) → ( ( I ↾ 𝑋 ) ‘ 0 ) = 0 )
21 18 20 eqtr3id ⊢ ( ( 𝐺 ∈ Grp ∧ 𝑥 ∈ 𝑋 ) → ( ( 0g ‘ 𝐻 ) ‘ 0 ) = 0 )
22 14 21 eqeq12d ⊢ ( ( 𝐺 ∈ Grp ∧ 𝑥 ∈ 𝑋 ) → ( ( ( 𝐹 ‘ 𝑥 ) ‘ 0 ) = ( ( 0g ‘ 𝐻 ) ‘ 0 ) ↔ 𝑥 = 0 ) )
23 7 22 imbitrid ⊢ ( ( 𝐺 ∈ Grp ∧ 𝑥 ∈ 𝑋 ) → ( ( 𝐹 ‘ 𝑥 ) = ( 0g ‘ 𝐻 ) → 𝑥 = 0 ) )
24 23 ralrimiva ⊢ ( 𝐺 ∈ Grp → ∀ 𝑥 ∈ 𝑋 ( ( 𝐹 ‘ 𝑥 ) = ( 0g ‘ 𝐻 ) → 𝑥 = 0 ) )
25 1 2 3 4 5 6 cayleylem1 ⊢ ( 𝐺 ∈ Grp → 𝐹 ∈ ( 𝐺 GrpHom 𝐻 ) )
26 eqid ⊢ ( 0g ‘ 𝐻 ) = ( 0g ‘ 𝐻 )
27 1 5 3 26 ghmf1 ⊢ ( 𝐹 ∈ ( 𝐺 GrpHom 𝐻 ) → ( 𝐹 : 𝑋 –1-1→ 𝑆 ↔ ∀ 𝑥 ∈ 𝑋 ( ( 𝐹 ‘ 𝑥 ) = ( 0g ‘ 𝐻 ) → 𝑥 = 0 ) ) )
28 25 27 syl ⊢ ( 𝐺 ∈ Grp → ( 𝐹 : 𝑋 –1-1→ 𝑆 ↔ ∀ 𝑥 ∈ 𝑋 ( ( 𝐹 ‘ 𝑥 ) = ( 0g ‘ 𝐻 ) → 𝑥 = 0 ) ) )
29 24 28 mpbird ⊢ ( 𝐺 ∈ Grp → 𝐹 : 𝑋 –1-1→ 𝑆 )