This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem frgpeccl

Description: Closure of the quotient map in a free group. (Contributed by Mario Carneiro, 1-Oct-2015)

Ref Expression
Hypotheses frgp0.m ⊢ 𝐺 = ( freeGrp ‘ 𝐼 )
frgp0.r ⊢ ∼ = ( ~FG ‘ 𝐼 )
frgpeccl.w ⊢ 𝑊 = ( I ‘ Word ( 𝐼 × 2o ) )
frgpeccl.b ⊢ 𝐵 = ( Base ‘ 𝐺 )
Assertion frgpeccl ( 𝑋 ∈ 𝑊 → [ 𝑋 ] ∼ ∈ 𝐵 )

Proof

Step Hyp Ref Expression
1 frgp0.m ⊢ 𝐺 = ( freeGrp ‘ 𝐼 )
2 frgp0.r ⊢ ∼ = ( ~FG ‘ 𝐼 )
3 frgpeccl.w ⊢ 𝑊 = ( I ‘ Word ( 𝐼 × 2o ) )
4 frgpeccl.b ⊢ 𝐵 = ( Base ‘ 𝐺 )
5 2 fvexi ⊢ ∼ ∈ V
6 5 ecelqsi ⊢ ( 𝑋 ∈ 𝑊 → [ 𝑋 ] ∼ ∈ ( 𝑊 / ∼ ) )
7 3 efgrcl ⊢ ( 𝑋 ∈ 𝑊 → ( 𝐼 ∈ V ∧ 𝑊 = Word ( 𝐼 × 2o ) ) )
8 7 simpld ⊢ ( 𝑋 ∈ 𝑊 → 𝐼 ∈ V )
9 eqid ⊢ ( freeMnd ‘ ( 𝐼 × 2o ) ) = ( freeMnd ‘ ( 𝐼 × 2o ) )
10 1 9 2 frgpval ⊢ ( 𝐼 ∈ V → 𝐺 = ( ( freeMnd ‘ ( 𝐼 × 2o ) ) /s ∼ ) )
11 8 10 syl ⊢ ( 𝑋 ∈ 𝑊 → 𝐺 = ( ( freeMnd ‘ ( 𝐼 × 2o ) ) /s ∼ ) )
12 7 simprd ⊢ ( 𝑋 ∈ 𝑊 → 𝑊 = Word ( 𝐼 × 2o ) )
13 2on ⊢ 2o ∈ On
14 xpexg ⊢ ( ( 𝐼 ∈ V ∧ 2o ∈ On ) → ( 𝐼 × 2o ) ∈ V )
15 8 13 14 sylancl ⊢ ( 𝑋 ∈ 𝑊 → ( 𝐼 × 2o ) ∈ V )
16 eqid ⊢ ( Base ‘ ( freeMnd ‘ ( 𝐼 × 2o ) ) ) = ( Base ‘ ( freeMnd ‘ ( 𝐼 × 2o ) ) )
17 9 16 frmdbas ⊢ ( ( 𝐼 × 2o ) ∈ V → ( Base ‘ ( freeMnd ‘ ( 𝐼 × 2o ) ) ) = Word ( 𝐼 × 2o ) )
18 15 17 syl ⊢ ( 𝑋 ∈ 𝑊 → ( Base ‘ ( freeMnd ‘ ( 𝐼 × 2o ) ) ) = Word ( 𝐼 × 2o ) )
19 12 18 eqtr4d ⊢ ( 𝑋 ∈ 𝑊 → 𝑊 = ( Base ‘ ( freeMnd ‘ ( 𝐼 × 2o ) ) ) )
20 5 a1i ⊢ ( 𝑋 ∈ 𝑊 → ∼ ∈ V )
21 fvexd ⊢ ( 𝑋 ∈ 𝑊 → ( freeMnd ‘ ( 𝐼 × 2o ) ) ∈ V )
22 11 19 20 21 qusbas ⊢ ( 𝑋 ∈ 𝑊 → ( 𝑊 / ∼ ) = ( Base ‘ 𝐺 ) )
23 22 4 eqtr4di ⊢ ( 𝑋 ∈ 𝑊 → ( 𝑊 / ∼ ) = 𝐵 )
24 6 23 eleqtrd ⊢ ( 𝑋 ∈ 𝑊 → [ 𝑋 ] ∼ ∈ 𝐵 )