Metamath Proof Explorer


Theorem frgpval

Description: Value of the free group construction. (Contributed by Mario Carneiro, 1-Oct-2015)

Ref Expression
Hypotheses frgpval.m G = freeGrp I
frgpval.b M = freeMnd I × 2 𝑜
frgpval.r ˙ = ~ FG I
Assertion frgpval I V G = M / 𝑠 ˙

Proof

Step Hyp Ref Expression
1 frgpval.m G = freeGrp I
2 frgpval.b M = freeMnd I × 2 𝑜
3 frgpval.r ˙ = ~ FG I
4 elex I V I V
5 xpeq1 i = I i × 2 𝑜 = I × 2 𝑜
6 5 fveq2d i = I freeMnd i × 2 𝑜 = freeMnd I × 2 𝑜
7 6 2 eqtr4di i = I freeMnd i × 2 𝑜 = M
8 fveq2 i = I ~ FG i = ~ FG I
9 8 3 eqtr4di i = I ~ FG i = ˙
10 7 9 oveq12d i = I freeMnd i × 2 𝑜 / 𝑠 ~ FG i = M / 𝑠 ˙
11 df-frgp freeGrp = i V freeMnd i × 2 𝑜 / 𝑠 ~ FG i
12 ovex M / 𝑠 ˙ V
13 10 11 12 fvmpt I V freeGrp I = M / 𝑠 ˙
14 4 13 syl I V freeGrp I = M / 𝑠 ˙
15 1 14 syl5eq I V G = M / 𝑠 ˙