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	fovcdmd	\|- ( ( ( R e. W /\ X e. V ) /\ ( N e. Fin /\ M e. Fin ) /\ ( I e. N /\ J e. M ) ) -> ( I X J ) e. B )