Theorem frmdval

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

	Ref	Expression
Hypotheses	frmdval.m	|- M = ( freeMnd ` I )
	frmdval.b	|- ( I e. V -> B = Word I )
	frmdval.p	|- .+ = ( ++ |` ( B X. B ) )
Assertion	frmdval	|- ( I e. V -> M = { <. ( Base ` ndx ) , B >. , <. ( +g ` ndx ) , .+ >. } )

Proof

Step	Hyp	Ref	Expression
1		frmdval.m	|- M = ( freeMnd ` I )
2		frmdval.b	|- ( I e. V -> B = Word I )
3		frmdval.p	|- .+ = ( ++ |` ( B X. B ) )
4		df-frmd	|- freeMnd = ( i e. _V |-> { <. ( Base ` ndx ) , Word i >. , <. ( +g ` ndx ) , ( ++ |` ( Word i X. Word i ) ) >. } )
5		wrdeq	|- ( i = I -> Word i = Word I )
6	2	eqcomd	|- ( I e. V -> Word I = B )
7	5 6	sylan9eqr	|- ( ( I e. V /\ i = I ) -> Word i = B )
8	7	opeq2d	|- ( ( I e. V /\ i = I ) -> <. ( Base ` ndx ) , Word i >. = <. ( Base ` ndx ) , B >. )
9	7	sqxpeqd	|- ( ( I e. V /\ i = I ) -> ( Word i X. Word i ) = ( B X. B ) )
10	9	reseq2d	|- ( ( I e. V /\ i = I ) -> ( ++ |` ( Word i X. Word i ) ) = ( ++ |` ( B X. B ) ) )
11	10 3	eqtr4di	|- ( ( I e. V /\ i = I ) -> ( ++ |` ( Word i X. Word i ) ) = .+ )
12	11	opeq2d	|- ( ( I e. V /\ i = I ) -> <. ( +g ` ndx ) , ( ++ |` ( Word i X. Word i ) ) >. = <. ( +g ` ndx ) , .+ >. )
13	8 12	preq12d	|- ( ( I e. V /\ i = I ) -> { <. ( Base ` ndx ) , Word i >. , <. ( +g ` ndx ) , ( ++ |` ( Word i X. Word i ) ) >. } = { <. ( Base ` ndx ) , B >. , <. ( +g ` ndx ) , .+ >. } )
14		elex	|- ( I e. V -> I e. _V )
15		prex	|- { <. ( Base ` ndx ) , B >. , <. ( +g ` ndx ) , .+ >. } e. _V
16	15	a1i	|- ( I e. V -> { <. ( Base ` ndx ) , B >. , <. ( +g ` ndx ) , .+ >. } e. _V )
17	4 13 14 16	fvmptd2	|- ( I e. V -> ( freeMnd ` I ) = { <. ( Base ` ndx ) , B >. , <. ( +g ` ndx ) , .+ >. } )
18	1 17	eqtrid	|- ( I e. V -> M = { <. ( Base ` ndx ) , B >. , <. ( +g ` ndx ) , .+ >. } )