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

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 × M
mpofrlmd.v ⊢ V = Base F
mpofrlmd.s ⊢ i = a ∧ j = b → A = B
mpofrlmd.a ⊢ φ ∧ i ∈ N ∧ j ∈ M → A ∈ X
mpofrlmd.b ⊢ φ ∧ a ∈ N ∧ b ∈ M → B ∈ Y
mpofrlmd.e ⊢ φ → N ∈ U ∧ M ∈ W ∧ Z ∈ V
Assertion mpofrlmd ⊢ φ → Z = a ∈ N , b ∈ M ⟼ B ↔ ∀ i ∈ N ∀ j ∈ M i Z j = A

Proof

Step Hyp Ref Expression
1 mpofrlmd.f ⊢ F = R freeLMod N × M
2 mpofrlmd.v ⊢ V = Base F
3 mpofrlmd.s ⊢ i = a ∧ j = b → A = B
4 mpofrlmd.a ⊢ φ ∧ i ∈ N ∧ j ∈ M → A ∈ X
5 mpofrlmd.b ⊢ φ ∧ a ∈ N ∧ b ∈ M → B ∈ Y
6 mpofrlmd.e ⊢ φ → N ∈ U ∧ M ∈ W ∧ Z ∈ V
7 xpexg ⊢ N ∈ U ∧ M ∈ W → N × M ∈ V
8 7 anim1i ⊢ N ∈ U ∧ M ∈ W ∧ Z ∈ V → N × M ∈ V ∧ Z ∈ V
9 8 3impa ⊢ N ∈ U ∧ M ∈ W ∧ Z ∈ V → N × M ∈ V ∧ Z ∈ V
10 eqid ⊢ Base R = Base R
11 1 10 2 frlmbasf ⊢ N × M ∈ V ∧ Z ∈ V → Z : N × M ⟶ Base R
12 ffn ⊢ Z : N × M ⟶ Base R → Z Fn N × M
13 6 9 11 12 4syl ⊢ φ → Z Fn N × M
14 13 3 4 5 fnmpoovd ⊢ φ → Z = a ∈ N , b ∈ M ⟼ B ↔ ∀ i ∈ N ∀ j ∈ M i Z j = A