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 ⊢ 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 eqtrid ⊢ I ∈ V → G = M / 𝑠 ∼ ˙