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 biimpi 
 |-  ( X e. V -> X e. ( Base ` F ) )
6 5 adantl 
 |-  ( ( R e. W /\ X e. V ) -> X e. ( Base ` F ) )
7 6 3ad2ant1 
 |-  ( ( ( R e. W /\ X e. V ) /\ ( N e. Fin /\ M e. Fin ) /\ ( I e. N /\ J e. M ) ) -> X e. ( Base ` F ) )
8 simpl 
 |-  ( ( R e. W /\ X e. V ) -> R e. W )
9 xpfi 
 |-  ( ( N e. Fin /\ M e. Fin ) -> ( N X. M ) e. Fin )
10 8 9 anim12i 
 |-  ( ( ( R e. W /\ X e. V ) /\ ( N e. Fin /\ M e. Fin ) ) -> ( R e. W /\ ( N X. M ) e. Fin ) )
11 10 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 ) )
12 1 2 frlmfibas 
 |-  ( ( R e. W /\ ( N X. M ) e. Fin ) -> ( B ^m ( N X. M ) ) = ( Base ` F ) )
13 11 12 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 ) )
14 7 13 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 ) ) )
15 elmapi 
 |-  ( X e. ( B ^m ( N X. M ) ) -> X : ( N X. M ) --> B )
16 14 15 syl 
 |-  ( ( ( R e. W /\ X e. V ) /\ ( N e. Fin /\ M e. Fin ) /\ ( I e. N /\ J e. M ) ) -> X : ( N X. M ) --> B )
17 simp3l 
 |-  ( ( ( R e. W /\ X e. V ) /\ ( N e. Fin /\ M e. Fin ) /\ ( I e. N /\ J e. M ) ) -> I e. N )
18 simp3r 
 |-  ( ( ( R e. W /\ X e. V ) /\ ( N e. Fin /\ M e. Fin ) /\ ( I e. N /\ J e. M ) ) -> J e. M )
19 16 17 18 fovrnd 
 |-  ( ( ( R e. W /\ X e. V ) /\ ( N e. Fin /\ M e. Fin ) /\ ( I e. N /\ J e. M ) ) -> ( I X J ) e. B )