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 \times M)$
		frlmbas3.b	$⊢ B = {Base}_{R}$
		frlmbas3.v	$⊢ V = {Base}_{F}$
	Assertion	frlmbas3	$⊢ ((R \in W \land X \in V) \land (N \in Fin \land M \in Fin) \land (I \in N \land J \in M)) \to I X J \in B$

Proof

Step	Hyp	Ref	Expression
1		frlmbas3.f	$⊢ F = R freeLMod (N \times M)$
2		frlmbas3.b	$⊢ B = {Base}_{R}$
3		frlmbas3.v	$⊢ V = {Base}_{F}$
4	3	eleq2i	$⊢ X \in V \leftrightarrow X \in {Base}_{F}$
5	4	biimpi	$⊢ X \in V \to X \in {Base}_{F}$
6	5	adantl	$⊢ (R \in W \land X \in V) \to X \in {Base}_{F}$
7	6	3ad2ant1	$⊢ ((R \in W \land X \in V) \land (N \in Fin \land M \in Fin) \land (I \in N \land J \in M)) \to X \in {Base}_{F}$
8		simpl	$⊢ (R \in W \land X \in V) \to R \in W$
9		xpfi	$⊢ (N \in Fin \land M \in Fin) \to N \times M \in Fin$
10	8 9	anim12i	$⊢ ((R \in W \land X \in V) \land (N \in Fin \land M \in Fin)) \to (R \in W \land N \times M \in Fin)$
11	10	3adant3	$⊢ ((R \in W \land X \in V) \land (N \in Fin \land M \in Fin) \land (I \in N \land J \in M)) \to (R \in W \land N \times M \in Fin)$
12	1 2	frlmfibas	$⊢ (R \in W \land N \times M \in Fin) \to B^{(N \times M)} = {Base}_{F}$
13	11 12	syl	$⊢ ((R \in W \land X \in V) \land (N \in Fin \land M \in Fin) \land (I \in N \land J \in M)) \to B^{(N \times M)} = {Base}_{F}$
14	7 13	eleqtrrd	$⊢ ((R \in W \land X \in V) \land (N \in Fin \land M \in Fin) \land (I \in N \land J \in M)) \to X \in (B^{(N \times M)})$
15		elmapi	$⊢ X \in (B^{(N \times M)}) \to X : N \times M ⟶ B$
16	14 15	syl	$⊢ ((R \in W \land X \in V) \land (N \in Fin \land M \in Fin) \land (I \in N \land J \in M)) \to X : N \times M ⟶ B$
17		simp3l	$⊢ ((R \in W \land X \in V) \land (N \in Fin \land M \in Fin) \land (I \in N \land J \in M)) \to I \in N$
18		simp3r	$⊢ ((R \in W \land X \in V) \land (N \in Fin \land M \in Fin) \land (I \in N \land J \in M)) \to J \in M$
19	16 17 18	fovcdmd	$⊢ ((R \in W \land X \in V) \land (N \in Fin \land M \in Fin) \land (I \in N \land J \in M)) \to I X J \in B$