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 G = freeGrp I
frgp0.r ˙ = ~ FG I
frgpeccl.w W = I Word I × 2 𝑜
frgpeccl.b B = Base G
Assertion frgpeccl X W X ˙ B

Proof

Step Hyp Ref Expression
1 frgp0.m G = freeGrp I
2 frgp0.r ˙ = ~ FG I
3 frgpeccl.w W = I Word I × 2 𝑜
4 frgpeccl.b B = Base G
5 2 fvexi ˙ V
6 5 ecelqsi X W X ˙ W / ˙
7 3 efgrcl X W I V W = Word I × 2 𝑜
8 7 simpld X W I V
9 eqid freeMnd I × 2 𝑜 = freeMnd I × 2 𝑜
10 1 9 2 frgpval I V G = freeMnd I × 2 𝑜 / 𝑠 ˙
11 8 10 syl X W G = freeMnd I × 2 𝑜 / 𝑠 ˙
12 7 simprd X W W = Word I × 2 𝑜
13 2on 2 𝑜 On
14 xpexg I V 2 𝑜 On I × 2 𝑜 V
15 8 13 14 sylancl X W I × 2 𝑜 V
16 eqid Base freeMnd I × 2 𝑜 = Base freeMnd I × 2 𝑜
17 9 16 frmdbas I × 2 𝑜 V Base freeMnd I × 2 𝑜 = Word I × 2 𝑜
18 15 17 syl X W Base freeMnd I × 2 𝑜 = Word I × 2 𝑜
19 12 18 eqtr4d X W W = Base freeMnd I × 2 𝑜
20 5 a1i X W ˙ V
21 fvexd X W freeMnd I × 2 𝑜 V
22 11 19 20 21 qusbas X W W / ˙ = Base G
23 22 4 syl6eqr X W W / ˙ = B
24 6 23 eleqtrd X W X ˙ B