This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 eqid 
 |-  ( Base ` R ) = ( Base ` R )
11 1 10 2 frlmbasf 
 |-  ( ( ( N X. M ) e. _V /\ Z e. V ) -> Z : ( N X. M ) --> ( Base ` R ) )
12 ffn 
 |-  ( Z : ( N X. M ) --> ( Base ` R ) -> Z Fn ( N X. M ) )
13 6 9 11 12 4syl 
 |-  ( ph -> Z Fn ( N X. M ) )
14 13 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 ) )