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	fovrnd	⊢ ( ( ( 𝑅 ∈ 𝑊 ∧ 𝑋 ∈ 𝑉 ) ∧ ( 𝑁 ∈ Fin ∧ 𝑀 ∈ Fin ) ∧ ( 𝐼 ∈ 𝑁 ∧ 𝐽 ∈ 𝑀 ) ) → ( 𝐼 𝑋 𝐽 ) ∈ 𝐵 )