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 𝐼 )