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	bilani	⊢ ( ( 𝑅 ∈ 𝑊 ∧ 𝑋 ∈ 𝑉 ) → 𝑋 ∈ ( Base ‘ 𝐹 ) )
6	5	3ad2ant1	⊢ ( ( ( 𝑅 ∈ 𝑊 ∧ 𝑋 ∈ 𝑉 ) ∧ ( 𝑁 ∈ Fin ∧ 𝑀 ∈ Fin ) ∧ ( 𝐼 ∈ 𝑁 ∧ 𝐽 ∈ 𝑀 ) ) → 𝑋 ∈ ( Base ‘ 𝐹 ) )
7		simpl	⊢ ( ( 𝑅 ∈ 𝑊 ∧ 𝑋 ∈ 𝑉 ) → 𝑅 ∈ 𝑊 )
8		xpfi	⊢ ( ( 𝑁 ∈ Fin ∧ 𝑀 ∈ Fin ) → ( 𝑁 × 𝑀 ) ∈ Fin )
9	7 8	anim12i	⊢ ( ( ( 𝑅 ∈ 𝑊 ∧ 𝑋 ∈ 𝑉 ) ∧ ( 𝑁 ∈ Fin ∧ 𝑀 ∈ Fin ) ) → ( 𝑅 ∈ 𝑊 ∧ ( 𝑁 × 𝑀 ) ∈ Fin ) )
10	9	3adant3	⊢ ( ( ( 𝑅 ∈ 𝑊 ∧ 𝑋 ∈ 𝑉 ) ∧ ( 𝑁 ∈ Fin ∧ 𝑀 ∈ Fin ) ∧ ( 𝐼 ∈ 𝑁 ∧ 𝐽 ∈ 𝑀 ) ) → ( 𝑅 ∈ 𝑊 ∧ ( 𝑁 × 𝑀 ) ∈ Fin ) )
11	1 2	frlmfibas	⊢ ( ( 𝑅 ∈ 𝑊 ∧ ( 𝑁 × 𝑀 ) ∈ Fin ) → ( 𝐵 ↑m ( 𝑁 × 𝑀 ) ) = ( Base ‘ 𝐹 ) )
12	10 11	syl	⊢ ( ( ( 𝑅 ∈ 𝑊 ∧ 𝑋 ∈ 𝑉 ) ∧ ( 𝑁 ∈ Fin ∧ 𝑀 ∈ Fin ) ∧ ( 𝐼 ∈ 𝑁 ∧ 𝐽 ∈ 𝑀 ) ) → ( 𝐵 ↑m ( 𝑁 × 𝑀 ) ) = ( Base ‘ 𝐹 ) )
13	6 12	eleqtrrd	⊢ ( ( ( 𝑅 ∈ 𝑊 ∧ 𝑋 ∈ 𝑉 ) ∧ ( 𝑁 ∈ Fin ∧ 𝑀 ∈ Fin ) ∧ ( 𝐼 ∈ 𝑁 ∧ 𝐽 ∈ 𝑀 ) ) → 𝑋 ∈ ( 𝐵 ↑m ( 𝑁 × 𝑀 ) ) )
14		elmapi	⊢ ( 𝑋 ∈ ( 𝐵 ↑m ( 𝑁 × 𝑀 ) ) → 𝑋 : ( 𝑁 × 𝑀 ) ⟶ 𝐵 )
15	13 14	syl	⊢ ( ( ( 𝑅 ∈ 𝑊 ∧ 𝑋 ∈ 𝑉 ) ∧ ( 𝑁 ∈ Fin ∧ 𝑀 ∈ Fin ) ∧ ( 𝐼 ∈ 𝑁 ∧ 𝐽 ∈ 𝑀 ) ) → 𝑋 : ( 𝑁 × 𝑀 ) ⟶ 𝐵 )
16		simp3l	⊢ ( ( ( 𝑅 ∈ 𝑊 ∧ 𝑋 ∈ 𝑉 ) ∧ ( 𝑁 ∈ Fin ∧ 𝑀 ∈ Fin ) ∧ ( 𝐼 ∈ 𝑁 ∧ 𝐽 ∈ 𝑀 ) ) → 𝐼 ∈ 𝑁 )
17		simp3r	⊢ ( ( ( 𝑅 ∈ 𝑊 ∧ 𝑋 ∈ 𝑉 ) ∧ ( 𝑁 ∈ Fin ∧ 𝑀 ∈ Fin ) ∧ ( 𝐼 ∈ 𝑁 ∧ 𝐽 ∈ 𝑀 ) ) → 𝐽 ∈ 𝑀 )
18	15 16 17	fovcdmd	⊢ ( ( ( 𝑅 ∈ 𝑊 ∧ 𝑋 ∈ 𝑉 ) ∧ ( 𝑁 ∈ Fin ∧ 𝑀 ∈ Fin ) ∧ ( 𝐼 ∈ 𝑁 ∧ 𝐽 ∈ 𝑀 ) ) → ( 𝐼 𝑋 𝐽 ) ∈ 𝐵 )