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

### Proof

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