Metamath Proof Explorer

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	$⊢ F = R freeLMod (N \times M)$
		mpofrlmd.v	$⊢ V = {Base}_{F}$
		mpofrlmd.s	$⊢ (i = a \land j = b) \to A = B$
		mpofrlmd.a	$⊢ (φ \land i \in N \land j \in M) \to A \in X$
		mpofrlmd.b	$⊢ (φ \land a \in N \land b \in M) \to B \in Y$
		mpofrlmd.e	$⊢ φ \to (N \in U \land M \in W \land Z \in V)$
	Assertion	mpofrlmd	$⊢ φ \to (Z = (a \in N, b \in M ⟼ B) \leftrightarrow \forall i \in N \forall j \in M i Z j = A)$

Proof

Step	Hyp	Ref	Expression
1		mpofrlmd.f	$⊢ F = R freeLMod (N \times M)$
2		mpofrlmd.v	$⊢ V = {Base}_{F}$
3		mpofrlmd.s	$⊢ (i = a \land j = b) \to A = B$
4		mpofrlmd.a	$⊢ (φ \land i \in N \land j \in M) \to A \in X$
5		mpofrlmd.b	$⊢ (φ \land a \in N \land b \in M) \to B \in Y$
6		mpofrlmd.e	$⊢ φ \to (N \in U \land M \in W \land Z \in V)$
7		xpexg	$⊢ (N \in U \land M \in W) \to N \times M \in V$
8	7	anim1i	$⊢ ((N \in U \land M \in W) \land Z \in V) \to (N \times M \in V \land Z \in V)$
9	8	3impa	$⊢ (N \in U \land M \in W \land Z \in V) \to (N \times M \in V \land Z \in V)$
10	6 9	syl	$⊢ φ \to (N \times M \in V \land Z \in V)$
11		eqid	$⊢ {Base}_{R} = {Base}_{R}$
12	1 11 2	frlmbasf	$⊢ (N \times M \in V \land Z \in V) \to Z : N \times M ⟶ {Base}_{R}$
13		ffn	$⊢ Z : N \times M ⟶ {Base}_{R} \to Z Fn (N \times M)$
14	10 12 13	3syl	$⊢ φ \to Z Fn (N \times M)$
15	14 3 4 5	fnmpoovd	$⊢ φ \to (Z = (a \in N, b \in M ⟼ B) \leftrightarrow \forall i \in N \forall j \in M i Z j = A)$