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

Metamath Proof Explorer

Theorem mamufacex

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

Ref Expression
Hypotheses mamudm.e ⊢ 𝐸 = ( 𝑅 freeLMod ( 𝑀 × 𝑁 ) )
mamudm.b ⊢ 𝐵 = ( Base ‘ 𝐸 )
mamudm.f ⊢ 𝐹 = ( 𝑅 freeLMod ( 𝑁 × 𝑃 ) )
mamudm.c ⊢ 𝐶 = ( Base ‘ 𝐹 )
mamudm.m ⊢ × = ( 𝑅 maMul ⟨ 𝑀 , 𝑁 , 𝑃 ⟩ )
mamufacex.g ⊢ 𝐺 = ( 𝑅 freeLMod ( 𝑀 × 𝑃 ) )
mamufacex.d ⊢ 𝐷 = ( Base ‘ 𝐺 )
Assertion mamufacex ( ( ( 𝑀 ≠ ∅ ∧ 𝑃 ≠ ∅ ) ∧ ( 𝑅 ∈ 𝑉 ∧ 𝑌 ∈ 𝐷 ) ∧ ( 𝑀 ∈ Fin ∧ 𝑁 ∈ Fin ∧ 𝑃 ∈ Fin ) ) → ( ( 𝑋 × 𝑍 ) = 𝑌 → 𝑍 ∈ 𝐶 ) )

Proof

Step Hyp Ref Expression
1 mamudm.e ⊢ 𝐸 = ( 𝑅 freeLMod ( 𝑀 × 𝑁 ) )
2 mamudm.b ⊢ 𝐵 = ( Base ‘ 𝐸 )
3 mamudm.f ⊢ 𝐹 = ( 𝑅 freeLMod ( 𝑁 × 𝑃 ) )
4 mamudm.c ⊢ 𝐶 = ( Base ‘ 𝐹 )
5 mamudm.m ⊢ × = ( 𝑅 maMul ⟨ 𝑀 , 𝑁 , 𝑃 ⟩ )
6 mamufacex.g ⊢ 𝐺 = ( 𝑅 freeLMod ( 𝑀 × 𝑃 ) )
7 mamufacex.d ⊢ 𝐷 = ( Base ‘ 𝐺 )
8 2a1 ⊢ ( 𝑍 ∈ 𝐶 → ( ( ( 𝑀 ≠ ∅ ∧ 𝑃 ≠ ∅ ) ∧ ( 𝑅 ∈ 𝑉 ∧ 𝑌 ∈ 𝐷 ) ∧ ( 𝑀 ∈ Fin ∧ 𝑁 ∈ Fin ∧ 𝑃 ∈ Fin ) ) → ( ( 𝑋 × 𝑍 ) = 𝑌 → 𝑍 ∈ 𝐶 ) ) )
9 1 2 3 4 5 mamudm ⊢ ( ( 𝑅 ∈ 𝑉 ∧ ( 𝑀 ∈ Fin ∧ 𝑁 ∈ Fin ∧ 𝑃 ∈ Fin ) ) → dom × = ( 𝐵 × 𝐶 ) )
10 9 adantlr ⊢ ( ( ( 𝑅 ∈ 𝑉 ∧ 𝑌 ∈ 𝐷 ) ∧ ( 𝑀 ∈ Fin ∧ 𝑁 ∈ Fin ∧ 𝑃 ∈ Fin ) ) → dom × = ( 𝐵 × 𝐶 ) )
11 10 3adant1 ⊢ ( ( ( 𝑀 ≠ ∅ ∧ 𝑃 ≠ ∅ ) ∧ ( 𝑅 ∈ 𝑉 ∧ 𝑌 ∈ 𝐷 ) ∧ ( 𝑀 ∈ Fin ∧ 𝑁 ∈ Fin ∧ 𝑃 ∈ Fin ) ) → dom × = ( 𝐵 × 𝐶 ) )
12 simpl ⊢ ( ( ¬ 𝑍 ∈ 𝐶 ∧ ( ( 𝑀 ≠ ∅ ∧ 𝑃 ≠ ∅ ) ∧ ( 𝑅 ∈ 𝑉 ∧ 𝑌 ∈ 𝐷 ) ∧ ( 𝑀 ∈ Fin ∧ 𝑁 ∈ Fin ∧ 𝑃 ∈ Fin ) ) ) → ¬ 𝑍 ∈ 𝐶 )
13 12 intnand ⊢ ( ( ¬ 𝑍 ∈ 𝐶 ∧ ( ( 𝑀 ≠ ∅ ∧ 𝑃 ≠ ∅ ) ∧ ( 𝑅 ∈ 𝑉 ∧ 𝑌 ∈ 𝐷 ) ∧ ( 𝑀 ∈ Fin ∧ 𝑁 ∈ Fin ∧ 𝑃 ∈ Fin ) ) ) → ¬ ( 𝑋 ∈ 𝐵 ∧ 𝑍 ∈ 𝐶 ) )
14 ndmovg ⊢ ( ( dom × = ( 𝐵 × 𝐶 ) ∧ ¬ ( 𝑋 ∈ 𝐵 ∧ 𝑍 ∈ 𝐶 ) ) → ( 𝑋 × 𝑍 ) = ∅ )
15 11 13 14 syl2an2 ⊢ ( ( ¬ 𝑍 ∈ 𝐶 ∧ ( ( 𝑀 ≠ ∅ ∧ 𝑃 ≠ ∅ ) ∧ ( 𝑅 ∈ 𝑉 ∧ 𝑌 ∈ 𝐷 ) ∧ ( 𝑀 ∈ Fin ∧ 𝑁 ∈ Fin ∧ 𝑃 ∈ Fin ) ) ) → ( 𝑋 × 𝑍 ) = ∅ )
16 eqeq1 ⊢ ( ( 𝑋 × 𝑍 ) = ∅ → ( ( 𝑋 × 𝑍 ) = 𝑌 ↔ ∅ = 𝑌 ) )
17 xpfi ⊢ ( ( 𝑀 ∈ Fin ∧ 𝑃 ∈ Fin ) → ( 𝑀 × 𝑃 ) ∈ Fin )
18 17 3adant2 ⊢ ( ( 𝑀 ∈ Fin ∧ 𝑁 ∈ Fin ∧ 𝑃 ∈ Fin ) → ( 𝑀 × 𝑃 ) ∈ Fin )
19 xpnz ⊢ ( ( 𝑀 ≠ ∅ ∧ 𝑃 ≠ ∅ ) ↔ ( 𝑀 × 𝑃 ) ≠ ∅ )
20 19 biimpi ⊢ ( ( 𝑀 ≠ ∅ ∧ 𝑃 ≠ ∅ ) → ( 𝑀 × 𝑃 ) ≠ ∅ )
21 eqid ⊢ ( Base ‘ 𝑅 ) = ( Base ‘ 𝑅 )
22 6 21 7 elfrlmbasn0 ⊢ ( ( ( 𝑀 × 𝑃 ) ∈ Fin ∧ ( 𝑀 × 𝑃 ) ≠ ∅ ) → ( 𝑌 ∈ 𝐷 → 𝑌 ≠ ∅ ) )
23 18 20 22 syl2an ⊢ ( ( ( 𝑀 ∈ Fin ∧ 𝑁 ∈ Fin ∧ 𝑃 ∈ Fin ) ∧ ( 𝑀 ≠ ∅ ∧ 𝑃 ≠ ∅ ) ) → ( 𝑌 ∈ 𝐷 → 𝑌 ≠ ∅ ) )
24 23 ex ⊢ ( ( 𝑀 ∈ Fin ∧ 𝑁 ∈ Fin ∧ 𝑃 ∈ Fin ) → ( ( 𝑀 ≠ ∅ ∧ 𝑃 ≠ ∅ ) → ( 𝑌 ∈ 𝐷 → 𝑌 ≠ ∅ ) ) )
25 24 com13 ⊢ ( 𝑌 ∈ 𝐷 → ( ( 𝑀 ≠ ∅ ∧ 𝑃 ≠ ∅ ) → ( ( 𝑀 ∈ Fin ∧ 𝑁 ∈ Fin ∧ 𝑃 ∈ Fin ) → 𝑌 ≠ ∅ ) ) )
26 25 adantl ⊢ ( ( 𝑅 ∈ 𝑉 ∧ 𝑌 ∈ 𝐷 ) → ( ( 𝑀 ≠ ∅ ∧ 𝑃 ≠ ∅ ) → ( ( 𝑀 ∈ Fin ∧ 𝑁 ∈ Fin ∧ 𝑃 ∈ Fin ) → 𝑌 ≠ ∅ ) ) )
27 26 3imp21 ⊢ ( ( ( 𝑀 ≠ ∅ ∧ 𝑃 ≠ ∅ ) ∧ ( 𝑅 ∈ 𝑉 ∧ 𝑌 ∈ 𝐷 ) ∧ ( 𝑀 ∈ Fin ∧ 𝑁 ∈ Fin ∧ 𝑃 ∈ Fin ) ) → 𝑌 ≠ ∅ )
28 eqneqall ⊢ ( 𝑌 = ∅ → ( 𝑌 ≠ ∅ → 𝑍 ∈ 𝐶 ) )
29 27 28 syl5com ⊢ ( ( ( 𝑀 ≠ ∅ ∧ 𝑃 ≠ ∅ ) ∧ ( 𝑅 ∈ 𝑉 ∧ 𝑌 ∈ 𝐷 ) ∧ ( 𝑀 ∈ Fin ∧ 𝑁 ∈ Fin ∧ 𝑃 ∈ Fin ) ) → ( 𝑌 = ∅ → 𝑍 ∈ 𝐶 ) )
30 29 adantl ⊢ ( ( ¬ 𝑍 ∈ 𝐶 ∧ ( ( 𝑀 ≠ ∅ ∧ 𝑃 ≠ ∅ ) ∧ ( 𝑅 ∈ 𝑉 ∧ 𝑌 ∈ 𝐷 ) ∧ ( 𝑀 ∈ Fin ∧ 𝑁 ∈ Fin ∧ 𝑃 ∈ Fin ) ) ) → ( 𝑌 = ∅ → 𝑍 ∈ 𝐶 ) )
31 30 com12 ⊢ ( 𝑌 = ∅ → ( ( ¬ 𝑍 ∈ 𝐶 ∧ ( ( 𝑀 ≠ ∅ ∧ 𝑃 ≠ ∅ ) ∧ ( 𝑅 ∈ 𝑉 ∧ 𝑌 ∈ 𝐷 ) ∧ ( 𝑀 ∈ Fin ∧ 𝑁 ∈ Fin ∧ 𝑃 ∈ Fin ) ) ) → 𝑍 ∈ 𝐶 ) )
32 31 eqcoms ⊢ ( ∅ = 𝑌 → ( ( ¬ 𝑍 ∈ 𝐶 ∧ ( ( 𝑀 ≠ ∅ ∧ 𝑃 ≠ ∅ ) ∧ ( 𝑅 ∈ 𝑉 ∧ 𝑌 ∈ 𝐷 ) ∧ ( 𝑀 ∈ Fin ∧ 𝑁 ∈ Fin ∧ 𝑃 ∈ Fin ) ) ) → 𝑍 ∈ 𝐶 ) )
33 16 32 biimtrdi ⊢ ( ( 𝑋 × 𝑍 ) = ∅ → ( ( 𝑋 × 𝑍 ) = 𝑌 → ( ( ¬ 𝑍 ∈ 𝐶 ∧ ( ( 𝑀 ≠ ∅ ∧ 𝑃 ≠ ∅ ) ∧ ( 𝑅 ∈ 𝑉 ∧ 𝑌 ∈ 𝐷 ) ∧ ( 𝑀 ∈ Fin ∧ 𝑁 ∈ Fin ∧ 𝑃 ∈ Fin ) ) ) → 𝑍 ∈ 𝐶 ) ) )
34 33 com23 ⊢ ( ( 𝑋 × 𝑍 ) = ∅ → ( ( ¬ 𝑍 ∈ 𝐶 ∧ ( ( 𝑀 ≠ ∅ ∧ 𝑃 ≠ ∅ ) ∧ ( 𝑅 ∈ 𝑉 ∧ 𝑌 ∈ 𝐷 ) ∧ ( 𝑀 ∈ Fin ∧ 𝑁 ∈ Fin ∧ 𝑃 ∈ Fin ) ) ) → ( ( 𝑋 × 𝑍 ) = 𝑌 → 𝑍 ∈ 𝐶 ) ) )
35 15 34 mpcom ⊢ ( ( ¬ 𝑍 ∈ 𝐶 ∧ ( ( 𝑀 ≠ ∅ ∧ 𝑃 ≠ ∅ ) ∧ ( 𝑅 ∈ 𝑉 ∧ 𝑌 ∈ 𝐷 ) ∧ ( 𝑀 ∈ Fin ∧ 𝑁 ∈ Fin ∧ 𝑃 ∈ Fin ) ) ) → ( ( 𝑋 × 𝑍 ) = 𝑌 → 𝑍 ∈ 𝐶 ) )
36 35 ex ⊢ ( ¬ 𝑍 ∈ 𝐶 → ( ( ( 𝑀 ≠ ∅ ∧ 𝑃 ≠ ∅ ) ∧ ( 𝑅 ∈ 𝑉 ∧ 𝑌 ∈ 𝐷 ) ∧ ( 𝑀 ∈ Fin ∧ 𝑁 ∈ Fin ∧ 𝑃 ∈ Fin ) ) → ( ( 𝑋 × 𝑍 ) = 𝑌 → 𝑍 ∈ 𝐶 ) ) )
37 8 36 pm2.61i ⊢ ( ( ( 𝑀 ≠ ∅ ∧ 𝑃 ≠ ∅ ) ∧ ( 𝑅 ∈ 𝑉 ∧ 𝑌 ∈ 𝐷 ) ∧ ( 𝑀 ∈ Fin ∧ 𝑁 ∈ Fin ∧ 𝑃 ∈ Fin ) ) → ( ( 𝑋 × 𝑍 ) = 𝑌 → 𝑍 ∈ 𝐶 ) )