Metamath Proof Explorer


Theorem mavmulsolcl

Description: Every solution of the equation A * X = Y for a matrix A and a vector B is a vector. (Contributed by AV, 27-Feb-2019)

Ref Expression
Hypotheses mavmuldm.b 𝐵 = ( Base ‘ 𝑅 )
mavmuldm.c 𝐶 = ( 𝐵m ( 𝑀 × 𝑁 ) )
mavmuldm.d 𝐷 = ( 𝐵m 𝑁 )
mavmuldm.t · = ( 𝑅 maVecMul ⟨ 𝑀 , 𝑁 ⟩ )
mavmulsolcl.e 𝐸 = ( 𝐵m 𝑀 )
Assertion mavmulsolcl ( ( ( 𝑀 ∈ Fin ∧ 𝑁 ∈ Fin ∧ 𝑀 ≠ ∅ ) ∧ ( 𝑅𝑉𝑌𝐸 ) ) → ( ( 𝐴 · 𝑋 ) = 𝑌𝑋𝐷 ) )

Proof

Step Hyp Ref Expression
1 mavmuldm.b 𝐵 = ( Base ‘ 𝑅 )
2 mavmuldm.c 𝐶 = ( 𝐵m ( 𝑀 × 𝑁 ) )
3 mavmuldm.d 𝐷 = ( 𝐵m 𝑁 )
4 mavmuldm.t · = ( 𝑅 maVecMul ⟨ 𝑀 , 𝑁 ⟩ )
5 mavmulsolcl.e 𝐸 = ( 𝐵m 𝑀 )
6 2a1 ( 𝑋𝐷 → ( ( ( 𝑀 ∈ Fin ∧ 𝑁 ∈ Fin ∧ 𝑀 ≠ ∅ ) ∧ ( 𝑅𝑉𝑌𝐸 ) ) → ( ( 𝐴 · 𝑋 ) = 𝑌𝑋𝐷 ) ) )
7 simpl ( ( 𝑅𝑉𝑌𝐸 ) → 𝑅𝑉 )
8 7 adantl ( ( ( 𝑀 ∈ Fin ∧ 𝑁 ∈ Fin ∧ 𝑀 ≠ ∅ ) ∧ ( 𝑅𝑉𝑌𝐸 ) ) → 𝑅𝑉 )
9 simpl1 ( ( ( 𝑀 ∈ Fin ∧ 𝑁 ∈ Fin ∧ 𝑀 ≠ ∅ ) ∧ ( 𝑅𝑉𝑌𝐸 ) ) → 𝑀 ∈ Fin )
10 simpl2 ( ( ( 𝑀 ∈ Fin ∧ 𝑁 ∈ Fin ∧ 𝑀 ≠ ∅ ) ∧ ( 𝑅𝑉𝑌𝐸 ) ) → 𝑁 ∈ Fin )
11 8 9 10 3jca ( ( ( 𝑀 ∈ Fin ∧ 𝑁 ∈ Fin ∧ 𝑀 ≠ ∅ ) ∧ ( 𝑅𝑉𝑌𝐸 ) ) → ( 𝑅𝑉𝑀 ∈ Fin ∧ 𝑁 ∈ Fin ) )
12 11 adantl ( ( ¬ 𝑋𝐷 ∧ ( ( 𝑀 ∈ Fin ∧ 𝑁 ∈ Fin ∧ 𝑀 ≠ ∅ ) ∧ ( 𝑅𝑉𝑌𝐸 ) ) ) → ( 𝑅𝑉𝑀 ∈ Fin ∧ 𝑁 ∈ Fin ) )
13 1 2 3 4 mavmuldm ( ( 𝑅𝑉𝑀 ∈ Fin ∧ 𝑁 ∈ Fin ) → dom · = ( 𝐶 × 𝐷 ) )
14 12 13 syl ( ( ¬ 𝑋𝐷 ∧ ( ( 𝑀 ∈ Fin ∧ 𝑁 ∈ Fin ∧ 𝑀 ≠ ∅ ) ∧ ( 𝑅𝑉𝑌𝐸 ) ) ) → dom · = ( 𝐶 × 𝐷 ) )
15 simpl ( ( ¬ 𝑋𝐷 ∧ ( ( 𝑀 ∈ Fin ∧ 𝑁 ∈ Fin ∧ 𝑀 ≠ ∅ ) ∧ ( 𝑅𝑉𝑌𝐸 ) ) ) → ¬ 𝑋𝐷 )
16 15 intnand ( ( ¬ 𝑋𝐷 ∧ ( ( 𝑀 ∈ Fin ∧ 𝑁 ∈ Fin ∧ 𝑀 ≠ ∅ ) ∧ ( 𝑅𝑉𝑌𝐸 ) ) ) → ¬ ( 𝐴𝐶𝑋𝐷 ) )
17 ndmovg ( ( dom · = ( 𝐶 × 𝐷 ) ∧ ¬ ( 𝐴𝐶𝑋𝐷 ) ) → ( 𝐴 · 𝑋 ) = ∅ )
18 14 16 17 syl2anc ( ( ¬ 𝑋𝐷 ∧ ( ( 𝑀 ∈ Fin ∧ 𝑁 ∈ Fin ∧ 𝑀 ≠ ∅ ) ∧ ( 𝑅𝑉𝑌𝐸 ) ) ) → ( 𝐴 · 𝑋 ) = ∅ )
19 eqeq1 ( ( 𝐴 · 𝑋 ) = ∅ → ( ( 𝐴 · 𝑋 ) = 𝑌 ↔ ∅ = 𝑌 ) )
20 elmapi ( 𝑌 ∈ ( 𝐵m 𝑀 ) → 𝑌 : 𝑀𝐵 )
21 f0dom0 ( 𝑌 : 𝑀𝐵 → ( 𝑀 = ∅ ↔ 𝑌 = ∅ ) )
22 21 biimprd ( 𝑌 : 𝑀𝐵 → ( 𝑌 = ∅ → 𝑀 = ∅ ) )
23 22 necon3d ( 𝑌 : 𝑀𝐵 → ( 𝑀 ≠ ∅ → 𝑌 ≠ ∅ ) )
24 23 com12 ( 𝑀 ≠ ∅ → ( 𝑌 : 𝑀𝐵𝑌 ≠ ∅ ) )
25 24 3ad2ant3 ( ( 𝑀 ∈ Fin ∧ 𝑁 ∈ Fin ∧ 𝑀 ≠ ∅ ) → ( 𝑌 : 𝑀𝐵𝑌 ≠ ∅ ) )
26 25 com12 ( 𝑌 : 𝑀𝐵 → ( ( 𝑀 ∈ Fin ∧ 𝑁 ∈ Fin ∧ 𝑀 ≠ ∅ ) → 𝑌 ≠ ∅ ) )
27 26 a1d ( 𝑌 : 𝑀𝐵 → ( 𝑅𝑉 → ( ( 𝑀 ∈ Fin ∧ 𝑁 ∈ Fin ∧ 𝑀 ≠ ∅ ) → 𝑌 ≠ ∅ ) ) )
28 20 27 syl ( 𝑌 ∈ ( 𝐵m 𝑀 ) → ( 𝑅𝑉 → ( ( 𝑀 ∈ Fin ∧ 𝑁 ∈ Fin ∧ 𝑀 ≠ ∅ ) → 𝑌 ≠ ∅ ) ) )
29 28 5 eleq2s ( 𝑌𝐸 → ( 𝑅𝑉 → ( ( 𝑀 ∈ Fin ∧ 𝑁 ∈ Fin ∧ 𝑀 ≠ ∅ ) → 𝑌 ≠ ∅ ) ) )
30 29 impcom ( ( 𝑅𝑉𝑌𝐸 ) → ( ( 𝑀 ∈ Fin ∧ 𝑁 ∈ Fin ∧ 𝑀 ≠ ∅ ) → 𝑌 ≠ ∅ ) )
31 30 impcom ( ( ( 𝑀 ∈ Fin ∧ 𝑁 ∈ Fin ∧ 𝑀 ≠ ∅ ) ∧ ( 𝑅𝑉𝑌𝐸 ) ) → 𝑌 ≠ ∅ )
32 eqneqall ( 𝑌 = ∅ → ( 𝑌 ≠ ∅ → 𝑋𝐷 ) )
33 31 32 syl5com ( ( ( 𝑀 ∈ Fin ∧ 𝑁 ∈ Fin ∧ 𝑀 ≠ ∅ ) ∧ ( 𝑅𝑉𝑌𝐸 ) ) → ( 𝑌 = ∅ → 𝑋𝐷 ) )
34 33 adantl ( ( ¬ 𝑋𝐷 ∧ ( ( 𝑀 ∈ Fin ∧ 𝑁 ∈ Fin ∧ 𝑀 ≠ ∅ ) ∧ ( 𝑅𝑉𝑌𝐸 ) ) ) → ( 𝑌 = ∅ → 𝑋𝐷 ) )
35 34 com12 ( 𝑌 = ∅ → ( ( ¬ 𝑋𝐷 ∧ ( ( 𝑀 ∈ Fin ∧ 𝑁 ∈ Fin ∧ 𝑀 ≠ ∅ ) ∧ ( 𝑅𝑉𝑌𝐸 ) ) ) → 𝑋𝐷 ) )
36 35 eqcoms ( ∅ = 𝑌 → ( ( ¬ 𝑋𝐷 ∧ ( ( 𝑀 ∈ Fin ∧ 𝑁 ∈ Fin ∧ 𝑀 ≠ ∅ ) ∧ ( 𝑅𝑉𝑌𝐸 ) ) ) → 𝑋𝐷 ) )
37 19 36 syl6bi ( ( 𝐴 · 𝑋 ) = ∅ → ( ( 𝐴 · 𝑋 ) = 𝑌 → ( ( ¬ 𝑋𝐷 ∧ ( ( 𝑀 ∈ Fin ∧ 𝑁 ∈ Fin ∧ 𝑀 ≠ ∅ ) ∧ ( 𝑅𝑉𝑌𝐸 ) ) ) → 𝑋𝐷 ) ) )
38 37 com23 ( ( 𝐴 · 𝑋 ) = ∅ → ( ( ¬ 𝑋𝐷 ∧ ( ( 𝑀 ∈ Fin ∧ 𝑁 ∈ Fin ∧ 𝑀 ≠ ∅ ) ∧ ( 𝑅𝑉𝑌𝐸 ) ) ) → ( ( 𝐴 · 𝑋 ) = 𝑌𝑋𝐷 ) ) )
39 18 38 mpcom ( ( ¬ 𝑋𝐷 ∧ ( ( 𝑀 ∈ Fin ∧ 𝑁 ∈ Fin ∧ 𝑀 ≠ ∅ ) ∧ ( 𝑅𝑉𝑌𝐸 ) ) ) → ( ( 𝐴 · 𝑋 ) = 𝑌𝑋𝐷 ) )
40 39 ex ( ¬ 𝑋𝐷 → ( ( ( 𝑀 ∈ Fin ∧ 𝑁 ∈ Fin ∧ 𝑀 ≠ ∅ ) ∧ ( 𝑅𝑉𝑌𝐸 ) ) → ( ( 𝐴 · 𝑋 ) = 𝑌𝑋𝐷 ) ) )
41 6 40 pm2.61i ( ( ( 𝑀 ∈ Fin ∧ 𝑁 ∈ Fin ∧ 𝑀 ≠ ∅ ) ∧ ( 𝑅𝑉𝑌𝐸 ) ) → ( ( 𝐴 · 𝑋 ) = 𝑌𝑋𝐷 ) )