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 × M
frlmbas3.b ⊢ B = Base R
frlmbas3.v ⊢ V = Base F
Assertion frlmbas3 ⊢ R ∈ W ∧ X ∈ V ∧ N ∈ Fin ∧ M ∈ Fin ∧ I ∈ N ∧ J ∈ M → I X J ∈ B

Proof

Step Hyp Ref Expression
1 frlmbas3.f ⊢ F = R freeLMod N × M
2 frlmbas3.b ⊢ B = Base R
3 frlmbas3.v ⊢ V = Base F
4 3 eleq2i ⊢ X ∈ V ↔ X ∈ Base F
5 4 bilani ⊢ R ∈ W ∧ X ∈ V → X ∈ Base F
6 5 3ad2ant1 ⊢ R ∈ W ∧ X ∈ V ∧ N ∈ Fin ∧ M ∈ Fin ∧ I ∈ N ∧ J ∈ M → X ∈ Base F
7 simpl ⊢ R ∈ W ∧ X ∈ V → R ∈ W
8 xpfi ⊢ N ∈ Fin ∧ M ∈ Fin → N × M ∈ Fin
9 7 8 anim12i ⊢ R ∈ W ∧ X ∈ V ∧ N ∈ Fin ∧ M ∈ Fin → R ∈ W ∧ N × M ∈ Fin
10 9 3adant3 ⊢ R ∈ W ∧ X ∈ V ∧ N ∈ Fin ∧ M ∈ Fin ∧ I ∈ N ∧ J ∈ M → R ∈ W ∧ N × M ∈ Fin
11 1 2 frlmfibas ⊢ R ∈ W ∧ N × M ∈ Fin → B N × M = Base F
12 10 11 syl ⊢ R ∈ W ∧ X ∈ V ∧ N ∈ Fin ∧ M ∈ Fin ∧ I ∈ N ∧ J ∈ M → B N × M = Base F
13 6 12 eleqtrrd ⊢ R ∈ W ∧ X ∈ V ∧ N ∈ Fin ∧ M ∈ Fin ∧ I ∈ N ∧ J ∈ M → X ∈ B N × M
14 elmapi ⊢ X ∈ B N × M → X : N × M ⟶ B
15 13 14 syl ⊢ R ∈ W ∧ X ∈ V ∧ N ∈ Fin ∧ M ∈ Fin ∧ I ∈ N ∧ J ∈ M → X : N × M ⟶ B
16 simp3l ⊢ R ∈ W ∧ X ∈ V ∧ N ∈ Fin ∧ M ∈ Fin ∧ I ∈ N ∧ J ∈ M → I ∈ N
17 simp3r ⊢ R ∈ W ∧ X ∈ V ∧ N ∈ Fin ∧ M ∈ Fin ∧ I ∈ N ∧ J ∈ M → J ∈ M
18 15 16 17 fovcdmd ⊢ R ∈ W ∧ X ∈ V ∧ N ∈ Fin ∧ M ∈ Fin ∧ I ∈ N ∧ J ∈ M → I X J ∈ B