Metamath Proof Explorer


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 syl5eq
 |-  ( I e. V -> M = { <. ( Base ` ndx ) , B >. , <. ( +g ` ndx ) , .+ >. } )