Theorem mpofrlmd

Description: Elements of the free module are mappings with two arguments defined by their operation values. (Contributed by AV, 20-Feb-2019) (Proof shortened by AV, 3-Jul-2022)

	Ref	Expression
Hypotheses	mpofrlmd.f	|- F = ( R freeLMod ( N X. M ) )
	mpofrlmd.v	|- V = ( Base ` F )
	mpofrlmd.s	|- ( ( i = a /\ j = b ) -> A = B )
	mpofrlmd.a	|- ( ( ph /\ i e. N /\ j e. M ) -> A e. X )
	mpofrlmd.b	|- ( ( ph /\ a e. N /\ b e. M ) -> B e. Y )
	mpofrlmd.e	|- ( ph -> ( N e. U /\ M e. W /\ Z e. V ) )
Assertion	mpofrlmd	|- ( ph -> ( Z = ( a e. N , b e. M |-> B ) <-> A. i e. N A. j e. M ( i Z j ) = A ) )

Proof

Step	Hyp	Ref	Expression
1		mpofrlmd.f	|- F = ( R freeLMod ( N X. M ) )
2		mpofrlmd.v	|- V = ( Base ` F )
3		mpofrlmd.s	|- ( ( i = a /\ j = b ) -> A = B )
4		mpofrlmd.a	|- ( ( ph /\ i e. N /\ j e. M ) -> A e. X )
5		mpofrlmd.b	|- ( ( ph /\ a e. N /\ b e. M ) -> B e. Y )
6		mpofrlmd.e	|- ( ph -> ( N e. U /\ M e. W /\ Z e. V ) )
7		xpexg	|- ( ( N e. U /\ M e. W ) -> ( N X. M ) e. _V )
8	7	anim1i	|- ( ( ( N e. U /\ M e. W ) /\ Z e. V ) -> ( ( N X. M ) e. _V /\ Z e. V ) )
9	8	3impa	|- ( ( N e. U /\ M e. W /\ Z e. V ) -> ( ( N X. M ) e. _V /\ Z e. V ) )
10	6 9	syl	|- ( ph -> ( ( N X. M ) e. _V /\ Z e. V ) )
11		eqid	|- ( Base ` R ) = ( Base ` R )
12	1 11 2	frlmbasf	|- ( ( ( N X. M ) e. _V /\ Z e. V ) -> Z : ( N X. M ) --> ( Base ` R ) )
13		ffn	|- ( Z : ( N X. M ) --> ( Base ` R ) -> Z Fn ( N X. M ) )
14	10 12 13	3syl	|- ( ph -> Z Fn ( N X. M ) )
15	14 3 4 5	fnmpoovd	|- ( ph -> ( Z = ( a e. N , b e. M |-> B ) <-> A. i e. N A. j e. M ( i Z j ) = A ) )