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

Metamath Proof Explorer

Theorem frlmbas3

Description: An element of the base set of a finite free module with a Cartesian product as index set as operation value. (Contributed by AV, 14-Feb-2019)

Ref Expression
Hypotheses frlmbas3.f 
|- F = ( R freeLMod ( N X. M ) )
frlmbas3.b 
|- B = ( Base ` R )
frlmbas3.v 
|- V = ( Base ` F )
Assertion frlmbas3 
|- ( ( ( R e. W /\ X e. V ) /\ ( N e. Fin /\ M e. Fin ) /\ ( I e. N /\ J e. M ) ) -> ( I X J ) e. B )

Proof

Step Hyp Ref Expression
1 frlmbas3.f 
 |-  F = ( R freeLMod ( N X. M ) )
2 frlmbas3.b 
 |-  B = ( Base ` R )
3 frlmbas3.v 
 |-  V = ( Base ` F )
4 3 eleq2i 
 |-  ( X e. V <-> X e. ( Base ` F ) )
5 4 bilani 
 |-  ( ( R e. W /\ X e. V ) -> X e. ( Base ` F ) )
6 5 3ad2ant1 
 |-  ( ( ( R e. W /\ X e. V ) /\ ( N e. Fin /\ M e. Fin ) /\ ( I e. N /\ J e. M ) ) -> X e. ( Base ` F ) )
7 simpl 
 |-  ( ( R e. W /\ X e. V ) -> R e. W )
8 xpfi 
 |-  ( ( N e. Fin /\ M e. Fin ) -> ( N X. M ) e. Fin )
9 7 8 anim12i 
 |-  ( ( ( R e. W /\ X e. V ) /\ ( N e. Fin /\ M e. Fin ) ) -> ( R e. W /\ ( N X. M ) e. Fin ) )
10 9 3adant3 
 |-  ( ( ( R e. W /\ X e. V ) /\ ( N e. Fin /\ M e. Fin ) /\ ( I e. N /\ J e. M ) ) -> ( R e. W /\ ( N X. M ) e. Fin ) )
11 1 2 frlmfibas 
 |-  ( ( R e. W /\ ( N X. M ) e. Fin ) -> ( B ^m ( N X. M ) ) = ( Base ` F ) )
12 10 11 syl 
 |-  ( ( ( R e. W /\ X e. V ) /\ ( N e. Fin /\ M e. Fin ) /\ ( I e. N /\ J e. M ) ) -> ( B ^m ( N X. M ) ) = ( Base ` F ) )
13 6 12 eleqtrrd 
 |-  ( ( ( R e. W /\ X e. V ) /\ ( N e. Fin /\ M e. Fin ) /\ ( I e. N /\ J e. M ) ) -> X e. ( B ^m ( N X. M ) ) )
14 elmapi 
 |-  ( X e. ( B ^m ( N X. M ) ) -> X : ( N X. M ) --> B )
15 13 14 syl 
 |-  ( ( ( R e. W /\ X e. V ) /\ ( N e. Fin /\ M e. Fin ) /\ ( I e. N /\ J e. M ) ) -> X : ( N X. M ) --> B )
16 simp3l 
 |-  ( ( ( R e. W /\ X e. V ) /\ ( N e. Fin /\ M e. Fin ) /\ ( I e. N /\ J e. M ) ) -> I e. N )
17 simp3r 
 |-  ( ( ( R e. W /\ X e. V ) /\ ( N e. Fin /\ M e. Fin ) /\ ( I e. N /\ J e. M ) ) -> J e. M )
18 15 16 17 fovcdmd 
 |-  ( ( ( R e. W /\ X e. V ) /\ ( N e. Fin /\ M e. Fin ) /\ ( I e. N /\ J e. M ) ) -> ( I X J ) e. B )