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

Metamath Proof Explorer

Theorem frmdval

Description: Value of the free monoid construction. (Contributed by Mario Carneiro, 27-Sep-2015)

Ref Expression
Hypotheses frmdval.m ⊢ 𝑀 = ( freeMnd ‘ 𝐼 )
frmdval.b ⊢ ( 𝐼 ∈ 𝑉 → 𝐵 = Word 𝐼 )
frmdval.p ⊢ + = ( ++ ↾ ( 𝐵 × 𝐵 ) )
Assertion frmdval ( 𝐼 ∈ 𝑉 → 𝑀 = { ⟨ ( Base ‘ ndx ) , 𝐵 ⟩ , ⟨ ( +g ‘ ndx ) , + ⟩ } )

Proof

Step Hyp Ref Expression
1 frmdval.m ⊢ 𝑀 = ( freeMnd ‘ 𝐼 )
2 frmdval.b ⊢ ( 𝐼 ∈ 𝑉 → 𝐵 = Word 𝐼 )
3 frmdval.p ⊢ + = ( ++ ↾ ( 𝐵 × 𝐵 ) )
4 df-frmd ⊢ freeMnd = ( 𝑖 ∈ V ↦ { ⟨ ( Base ‘ ndx ) , Word 𝑖 ⟩ , ⟨ ( +g ‘ ndx ) , ( ++ ↾ ( Word 𝑖 × Word 𝑖 ) ) ⟩ } )
5 wrdeq ⊢ ( 𝑖 = 𝐼 → Word 𝑖 = Word 𝐼 )
6 2 eqcomd ⊢ ( 𝐼 ∈ 𝑉 → Word 𝐼 = 𝐵 )
7 5 6 sylan9eqr ⊢ ( ( 𝐼 ∈ 𝑉 ∧ 𝑖 = 𝐼 ) → Word 𝑖 = 𝐵 )
8 7 opeq2d ⊢ ( ( 𝐼 ∈ 𝑉 ∧ 𝑖 = 𝐼 ) → ⟨ ( Base ‘ ndx ) , Word 𝑖 ⟩ = ⟨ ( Base ‘ ndx ) , 𝐵 ⟩ )
9 7 sqxpeqd ⊢ ( ( 𝐼 ∈ 𝑉 ∧ 𝑖 = 𝐼 ) → ( Word 𝑖 × Word 𝑖 ) = ( 𝐵 × 𝐵 ) )
10 9 reseq2d ⊢ ( ( 𝐼 ∈ 𝑉 ∧ 𝑖 = 𝐼 ) → ( ++ ↾ ( Word 𝑖 × Word 𝑖 ) ) = ( ++ ↾ ( 𝐵 × 𝐵 ) ) )
11 10 3 eqtr4di ⊢ ( ( 𝐼 ∈ 𝑉 ∧ 𝑖 = 𝐼 ) → ( ++ ↾ ( Word 𝑖 × Word 𝑖 ) ) = + )
12 11 opeq2d ⊢ ( ( 𝐼 ∈ 𝑉 ∧ 𝑖 = 𝐼 ) → ⟨ ( +g ‘ ndx ) , ( ++ ↾ ( Word 𝑖 × Word 𝑖 ) ) ⟩ = ⟨ ( +g ‘ ndx ) , + ⟩ )
13 8 12 preq12d ⊢ ( ( 𝐼 ∈ 𝑉 ∧ 𝑖 = 𝐼 ) → { ⟨ ( Base ‘ ndx ) , Word 𝑖 ⟩ , ⟨ ( +g ‘ ndx ) , ( ++ ↾ ( Word 𝑖 × Word 𝑖 ) ) ⟩ } = { ⟨ ( Base ‘ ndx ) , 𝐵 ⟩ , ⟨ ( +g ‘ ndx ) , + ⟩ } )
14 elex ⊢ ( 𝐼 ∈ 𝑉 → 𝐼 ∈ V )
15 prex ⊢ { ⟨ ( Base ‘ ndx ) , 𝐵 ⟩ , ⟨ ( +g ‘ ndx ) , + ⟩ } ∈ V
16 15 a1i ⊢ ( 𝐼 ∈ 𝑉 → { ⟨ ( Base ‘ ndx ) , 𝐵 ⟩ , ⟨ ( +g ‘ ndx ) , + ⟩ } ∈ V )
17 4 13 14 16 fvmptd2 ⊢ ( 𝐼 ∈ 𝑉 → ( freeMnd ‘ 𝐼 ) = { ⟨ ( Base ‘ ndx ) , 𝐵 ⟩ , ⟨ ( +g ‘ ndx ) , + ⟩ } )
18 1 17 eqtrid ⊢ ( 𝐼 ∈ 𝑉 → 𝑀 = { ⟨ ( Base ‘ ndx ) , 𝐵 ⟩ , ⟨ ( +g ‘ ndx ) , + ⟩ } )