Theorem mpofrlmd

Description: Elements of the free module are mappings with two arguments defined by their operation values. (Contributed by AV, 20-Feb-2019) (Proof shortened by AV, 3-Jul-2022)

	Ref	Expression
Hypotheses	mpofrlmd.f	⊢ 𝐹 = ( 𝑅 freeLMod ( 𝑁 × 𝑀 ) )
	mpofrlmd.v	⊢ 𝑉 = ( Base ‘ 𝐹 )
	mpofrlmd.s	⊢ ( ( 𝑖 = 𝑎 ∧ 𝑗 = 𝑏 ) → 𝐴 = 𝐵 )
	mpofrlmd.a	⊢ ( ( 𝜑 ∧ 𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑀 ) → 𝐴 ∈ 𝑋 )
	mpofrlmd.b	⊢ ( ( 𝜑 ∧ 𝑎 ∈ 𝑁 ∧ 𝑏 ∈ 𝑀 ) → 𝐵 ∈ 𝑌 )
	mpofrlmd.e	⊢ ( 𝜑 → ( 𝑁 ∈ 𝑈 ∧ 𝑀 ∈ 𝑊 ∧ 𝑍 ∈ 𝑉 ) )
Assertion	mpofrlmd	⊢ ( 𝜑 → ( 𝑍 = ( 𝑎 ∈ 𝑁 , 𝑏 ∈ 𝑀 ↦ 𝐵 ) ↔ ∀ 𝑖 ∈ 𝑁 ∀ 𝑗 ∈ 𝑀 ( 𝑖 𝑍 𝑗 ) = 𝐴 ) )

Proof

Step	Hyp	Ref	Expression
1		mpofrlmd.f	⊢ 𝐹 = ( 𝑅 freeLMod ( 𝑁 × 𝑀 ) )
2		mpofrlmd.v	⊢ 𝑉 = ( Base ‘ 𝐹 )
3		mpofrlmd.s	⊢ ( ( 𝑖 = 𝑎 ∧ 𝑗 = 𝑏 ) → 𝐴 = 𝐵 )
4		mpofrlmd.a	⊢ ( ( 𝜑 ∧ 𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑀 ) → 𝐴 ∈ 𝑋 )
5		mpofrlmd.b	⊢ ( ( 𝜑 ∧ 𝑎 ∈ 𝑁 ∧ 𝑏 ∈ 𝑀 ) → 𝐵 ∈ 𝑌 )
6		mpofrlmd.e	⊢ ( 𝜑 → ( 𝑁 ∈ 𝑈 ∧ 𝑀 ∈ 𝑊 ∧ 𝑍 ∈ 𝑉 ) )
7		xpexg	⊢ ( ( 𝑁 ∈ 𝑈 ∧ 𝑀 ∈ 𝑊 ) → ( 𝑁 × 𝑀 ) ∈ V )
8	7	anim1i	⊢ ( ( ( 𝑁 ∈ 𝑈 ∧ 𝑀 ∈ 𝑊 ) ∧ 𝑍 ∈ 𝑉 ) → ( ( 𝑁 × 𝑀 ) ∈ V ∧ 𝑍 ∈ 𝑉 ) )
9	8	3impa	⊢ ( ( 𝑁 ∈ 𝑈 ∧ 𝑀 ∈ 𝑊 ∧ 𝑍 ∈ 𝑉 ) → ( ( 𝑁 × 𝑀 ) ∈ V ∧ 𝑍 ∈ 𝑉 ) )
10	6 9	syl	⊢ ( 𝜑 → ( ( 𝑁 × 𝑀 ) ∈ V ∧ 𝑍 ∈ 𝑉 ) )
11		eqid	⊢ ( Base ‘ 𝑅 ) = ( Base ‘ 𝑅 )
12	1 11 2	frlmbasf	⊢ ( ( ( 𝑁 × 𝑀 ) ∈ V ∧ 𝑍 ∈ 𝑉 ) → 𝑍 : ( 𝑁 × 𝑀 ) ⟶ ( Base ‘ 𝑅 ) )
13		ffn	⊢ ( 𝑍 : ( 𝑁 × 𝑀 ) ⟶ ( Base ‘ 𝑅 ) → 𝑍 Fn ( 𝑁 × 𝑀 ) )
14	10 12 13	3syl	⊢ ( 𝜑 → 𝑍 Fn ( 𝑁 × 𝑀 ) )
15	14 3 4 5	fnmpoovd	⊢ ( 𝜑 → ( 𝑍 = ( 𝑎 ∈ 𝑁 , 𝑏 ∈ 𝑀 ↦ 𝐵 ) ↔ ∀ 𝑖 ∈ 𝑁 ∀ 𝑗 ∈ 𝑀 ( 𝑖 𝑍 𝑗 ) = 𝐴 ) )