Theorem breprexplemb

Description: Lemma for breprexp (closure). (Contributed by Thierry Arnoux, 7-Dec-2021)

	Ref	Expression
Hypotheses	breprexp.n	|- ( ph -> N e. NN0 )
	breprexp.s	|- ( ph -> S e. NN0 )
	breprexp.z	|- ( ph -> Z e. CC )
	breprexp.h	|- ( ph -> L : ( 0 ..^ S ) --> ( CC ^m NN ) )
	breprexplemb.x	|- ( ph -> X e. ( 0 ..^ S ) )
	breprexplemb.y	|- ( ph -> Y e. NN )
Assertion	breprexplemb	|- ( ph -> ( ( L ` X ) ` Y ) e. CC )

Proof

Step	Hyp	Ref	Expression
1		breprexp.n	|- ( ph -> N e. NN0 )
2		breprexp.s	|- ( ph -> S e. NN0 )
3		breprexp.z	|- ( ph -> Z e. CC )
4		breprexp.h	|- ( ph -> L : ( 0 ..^ S ) --> ( CC ^m NN ) )
5		breprexplemb.x	|- ( ph -> X e. ( 0 ..^ S ) )
6		breprexplemb.y	|- ( ph -> Y e. NN )
7	4 5	ffvelrnd	|- ( ph -> ( L ` X ) e. ( CC ^m NN ) )
8		cnex	|- CC e. _V
9		nnex	|- NN e. _V
10	8 9	elmap	|- ( ( L ` X ) e. ( CC ^m NN ) <-> ( L ` X ) : NN --> CC )
11	7 10	sylib	|- ( ph -> ( L ` X ) : NN --> CC )
12	11 6	ffvelrnd	|- ( ph -> ( ( L ` X ) ` Y ) e. CC )