Metamath Proof Explorer


Theorem frgpval

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

Ref Expression
Hypotheses frgpval.m 𝐺 = ( freeGrp ‘ 𝐼 )
frgpval.b 𝑀 = ( freeMnd ‘ ( 𝐼 × 2o ) )
frgpval.r = ( ~FG𝐼 )
Assertion frgpval ( 𝐼𝑉𝐺 = ( 𝑀 /s ) )

Proof

Step Hyp Ref Expression
1 frgpval.m 𝐺 = ( freeGrp ‘ 𝐼 )
2 frgpval.b 𝑀 = ( freeMnd ‘ ( 𝐼 × 2o ) )
3 frgpval.r = ( ~FG𝐼 )
4 elex ( 𝐼𝑉𝐼 ∈ V )
5 xpeq1 ( 𝑖 = 𝐼 → ( 𝑖 × 2o ) = ( 𝐼 × 2o ) )
6 5 fveq2d ( 𝑖 = 𝐼 → ( freeMnd ‘ ( 𝑖 × 2o ) ) = ( freeMnd ‘ ( 𝐼 × 2o ) ) )
7 6 2 eqtr4di ( 𝑖 = 𝐼 → ( freeMnd ‘ ( 𝑖 × 2o ) ) = 𝑀 )
8 fveq2 ( 𝑖 = 𝐼 → ( ~FG𝑖 ) = ( ~FG𝐼 ) )
9 8 3 eqtr4di ( 𝑖 = 𝐼 → ( ~FG𝑖 ) = )
10 7 9 oveq12d ( 𝑖 = 𝐼 → ( ( freeMnd ‘ ( 𝑖 × 2o ) ) /s ( ~FG𝑖 ) ) = ( 𝑀 /s ) )
11 df-frgp freeGrp = ( 𝑖 ∈ V ↦ ( ( freeMnd ‘ ( 𝑖 × 2o ) ) /s ( ~FG𝑖 ) ) )
12 ovex ( 𝑀 /s ) ∈ V
13 10 11 12 fvmpt ( 𝐼 ∈ V → ( freeGrp ‘ 𝐼 ) = ( 𝑀 /s ) )
14 4 13 syl ( 𝐼𝑉 → ( freeGrp ‘ 𝐼 ) = ( 𝑀 /s ) )
15 1 14 syl5eq ( 𝐼𝑉𝐺 = ( 𝑀 /s ) )