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 syl5eq ( 𝐼𝑉𝑀 = { ⟨ ( Base ‘ ndx ) , 𝐵 ⟩ , ⟨ ( +g ‘ ndx ) , + ⟩ } )