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

Metamath Proof Explorer

Theorem frmdbas

Description: The base set of a free monoid. (Contributed by Mario Carneiro, 27-Sep-2015) (Revised by Mario Carneiro, 27-Feb-2016)

Ref Expression
Hypotheses frmdbas.m ⊢ 𝑀 = ( freeMnd ‘ 𝐼 )
frmdbas.b ⊢ 𝐵 = ( Base ‘ 𝑀 )
Assertion frmdbas ( 𝐼 ∈ 𝑉 → 𝐵 = Word 𝐼 )

Proof

Step Hyp Ref Expression
1 frmdbas.m ⊢ 𝑀 = ( freeMnd ‘ 𝐼 )
2 frmdbas.b ⊢ 𝐵 = ( Base ‘ 𝑀 )
3 eqidd ⊢ ( 𝐼 ∈ 𝑉 → Word 𝐼 = Word 𝐼 )
4 eqid ⊢ ( ++ ↾ ( Word 𝐼 × Word 𝐼 ) ) = ( ++ ↾ ( Word 𝐼 × Word 𝐼 ) )
5 1 3 4 frmdval ⊢ ( 𝐼 ∈ 𝑉 → 𝑀 = { ⟨ ( Base ‘ ndx ) , Word 𝐼 ⟩ , ⟨ ( +g ‘ ndx ) , ( ++ ↾ ( Word 𝐼 × Word 𝐼 ) ) ⟩ } )
6 5 fveq2d ⊢ ( 𝐼 ∈ 𝑉 → ( Base ‘ 𝑀 ) = ( Base ‘ { ⟨ ( Base ‘ ndx ) , Word 𝐼 ⟩ , ⟨ ( +g ‘ ndx ) , ( ++ ↾ ( Word 𝐼 × Word 𝐼 ) ) ⟩ } ) )
7 wrdexg ⊢ ( 𝐼 ∈ 𝑉 → Word 𝐼 ∈ V )
8 eqid ⊢ { ⟨ ( Base ‘ ndx ) , Word 𝐼 ⟩ , ⟨ ( +g ‘ ndx ) , ( ++ ↾ ( Word 𝐼 × Word 𝐼 ) ) ⟩ } = { ⟨ ( Base ‘ ndx ) , Word 𝐼 ⟩ , ⟨ ( +g ‘ ndx ) , ( ++ ↾ ( Word 𝐼 × Word 𝐼 ) ) ⟩ }
9 8 grpbase ⊢ ( Word 𝐼 ∈ V → Word 𝐼 = ( Base ‘ { ⟨ ( Base ‘ ndx ) , Word 𝐼 ⟩ , ⟨ ( +g ‘ ndx ) , ( ++ ↾ ( Word 𝐼 × Word 𝐼 ) ) ⟩ } ) )
10 7 9 syl ⊢ ( 𝐼 ∈ 𝑉 → Word 𝐼 = ( Base ‘ { ⟨ ( Base ‘ ndx ) , Word 𝐼 ⟩ , ⟨ ( +g ‘ ndx ) , ( ++ ↾ ( Word 𝐼 × Word 𝐼 ) ) ⟩ } ) )
11 6 10 eqtr4d ⊢ ( 𝐼 ∈ 𝑉 → ( Base ‘ 𝑀 ) = Word 𝐼 )
12 2 11 eqtrid ⊢ ( 𝐼 ∈ 𝑉 → 𝐵 = Word 𝐼 )