This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 ⊢ 𝐹 = ( 𝑅 freeLMod ( 𝑁 × 𝑀 ) )
frlmbas3.b ⊢ 𝐵 = ( Base ‘ 𝑅 )
frlmbas3.v ⊢ 𝑉 = ( Base ‘ 𝐹 )
Assertion frlmbas3 ( ( ( 𝑅 ∈ 𝑊 ∧ 𝑋 ∈ 𝑉 ) ∧ ( 𝑁 ∈ Fin ∧ 𝑀 ∈ Fin ) ∧ ( 𝐼 ∈ 𝑁 ∧ 𝐽 ∈ 𝑀 ) ) → ( 𝐼 𝑋 𝐽 ) ∈ 𝐵 )

Proof

Step Hyp Ref Expression
1 frlmbas3.f ⊢ 𝐹 = ( 𝑅 freeLMod ( 𝑁 × 𝑀 ) )
2 frlmbas3.b ⊢ 𝐵 = ( Base ‘ 𝑅 )
3 frlmbas3.v ⊢ 𝑉 = ( Base ‘ 𝐹 )
4 3 eleq2i ⊢ ( 𝑋 ∈ 𝑉 ↔ 𝑋 ∈ ( Base ‘ 𝐹 ) )
5 4 biimpi ⊢ ( 𝑋 ∈ 𝑉 → 𝑋 ∈ ( Base ‘ 𝐹 ) )
6 5 adantl ⊢ ( ( 𝑅 ∈ 𝑊 ∧ 𝑋 ∈ 𝑉 ) → 𝑋 ∈ ( Base ‘ 𝐹 ) )
7 6 3ad2ant1 ⊢ ( ( ( 𝑅 ∈ 𝑊 ∧ 𝑋 ∈ 𝑉 ) ∧ ( 𝑁 ∈ Fin ∧ 𝑀 ∈ Fin ) ∧ ( 𝐼 ∈ 𝑁 ∧ 𝐽 ∈ 𝑀 ) ) → 𝑋 ∈ ( Base ‘ 𝐹 ) )
8 simpl ⊢ ( ( 𝑅 ∈ 𝑊 ∧ 𝑋 ∈ 𝑉 ) → 𝑅 ∈ 𝑊 )
9 xpfi ⊢ ( ( 𝑁 ∈ Fin ∧ 𝑀 ∈ Fin ) → ( 𝑁 × 𝑀 ) ∈ Fin )
10 8 9 anim12i ⊢ ( ( ( 𝑅 ∈ 𝑊 ∧ 𝑋 ∈ 𝑉 ) ∧ ( 𝑁 ∈ Fin ∧ 𝑀 ∈ Fin ) ) → ( 𝑅 ∈ 𝑊 ∧ ( 𝑁 × 𝑀 ) ∈ Fin ) )
11 10 3adant3 ⊢ ( ( ( 𝑅 ∈ 𝑊 ∧ 𝑋 ∈ 𝑉 ) ∧ ( 𝑁 ∈ Fin ∧ 𝑀 ∈ Fin ) ∧ ( 𝐼 ∈ 𝑁 ∧ 𝐽 ∈ 𝑀 ) ) → ( 𝑅 ∈ 𝑊 ∧ ( 𝑁 × 𝑀 ) ∈ Fin ) )
12 1 2 frlmfibas ⊢ ( ( 𝑅 ∈ 𝑊 ∧ ( 𝑁 × 𝑀 ) ∈ Fin ) → ( 𝐵 ↑m ( 𝑁 × 𝑀 ) ) = ( Base ‘ 𝐹 ) )
13 11 12 syl ⊢ ( ( ( 𝑅 ∈ 𝑊 ∧ 𝑋 ∈ 𝑉 ) ∧ ( 𝑁 ∈ Fin ∧ 𝑀 ∈ Fin ) ∧ ( 𝐼 ∈ 𝑁 ∧ 𝐽 ∈ 𝑀 ) ) → ( 𝐵 ↑m ( 𝑁 × 𝑀 ) ) = ( Base ‘ 𝐹 ) )
14 7 13 eleqtrrd ⊢ ( ( ( 𝑅 ∈ 𝑊 ∧ 𝑋 ∈ 𝑉 ) ∧ ( 𝑁 ∈ Fin ∧ 𝑀 ∈ Fin ) ∧ ( 𝐼 ∈ 𝑁 ∧ 𝐽 ∈ 𝑀 ) ) → 𝑋 ∈ ( 𝐵 ↑m ( 𝑁 × 𝑀 ) ) )
15 elmapi ⊢ ( 𝑋 ∈ ( 𝐵 ↑m ( 𝑁 × 𝑀 ) ) → 𝑋 : ( 𝑁 × 𝑀 ) ⟶ 𝐵 )
16 14 15 syl ⊢ ( ( ( 𝑅 ∈ 𝑊 ∧ 𝑋 ∈ 𝑉 ) ∧ ( 𝑁 ∈ Fin ∧ 𝑀 ∈ Fin ) ∧ ( 𝐼 ∈ 𝑁 ∧ 𝐽 ∈ 𝑀 ) ) → 𝑋 : ( 𝑁 × 𝑀 ) ⟶ 𝐵 )
17 simp3l ⊢ ( ( ( 𝑅 ∈ 𝑊 ∧ 𝑋 ∈ 𝑉 ) ∧ ( 𝑁 ∈ Fin ∧ 𝑀 ∈ Fin ) ∧ ( 𝐼 ∈ 𝑁 ∧ 𝐽 ∈ 𝑀 ) ) → 𝐼 ∈ 𝑁 )
18 simp3r ⊢ ( ( ( 𝑅 ∈ 𝑊 ∧ 𝑋 ∈ 𝑉 ) ∧ ( 𝑁 ∈ Fin ∧ 𝑀 ∈ Fin ) ∧ ( 𝐼 ∈ 𝑁 ∧ 𝐽 ∈ 𝑀 ) ) → 𝐽 ∈ 𝑀 )
19 16 17 18 fovcdmd ⊢ ( ( ( 𝑅 ∈ 𝑊 ∧ 𝑋 ∈ 𝑉 ) ∧ ( 𝑁 ∈ Fin ∧ 𝑀 ∈ Fin ) ∧ ( 𝐼 ∈ 𝑁 ∧ 𝐽 ∈ 𝑀 ) ) → ( 𝐼 𝑋 𝐽 ) ∈ 𝐵 )