# 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 syl5eq ( 𝐼𝑉𝐵 = Word 𝐼 )