Metamath Proof Explorer

Theorem pfxwrdsymb

Description: A prefix of a word is a word over the symbols it consists of. (Contributed by AV, 3-Dec-2022)

		Ref	Expression
	Assertion	pfxwrdsymb	\|- ( S e. Word A -> ( S prefix L ) e. Word ( S " ( 0 ..^ L ) ) )

Step	Hyp	Ref	Expression
1		pfxval0	\|- ( S e. Word A -> ( S prefix L ) = ( S substr <. 0 , L >. ) )
2		swrdwrdsymb	\|- ( S e. Word A -> ( S substr <. 0 , L >. ) e. Word ( S " ( 0 ..^ L ) ) )
3	1 2	eqeltrd	\|- ( S e. Word A -> ( S prefix L ) e. Word ( S " ( 0 ..^ L ) ) )

Step

Hyp

Ref

Expression

 |-  ( S e. Word A -> ( S prefix L ) = ( S substr <. 0 , L >. ) )

 |-  ( S e. Word A -> ( S substr <. 0 , L >. ) e. Word ( S " ( 0 ..^ L ) ) )

1 2

 |-  ( S e. Word A -> ( S prefix L ) e. Word ( S " ( 0 ..^ L ) ) )