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

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 eqtrid ⊢ ( 𝐼 ∈ 𝑉 → 𝐺 = ( 𝑀 /s ∼ ) )