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 
|- E = ( R freeLMod ( M X. N ) )
mamudm.b 
|- B = ( Base ` E )
mamudm.f 
|- F = ( R freeLMod ( N X. P ) )
mamudm.c 
|- C = ( Base ` F )
mamudm.m 
|- .X. = ( R maMul <. M , N , P >. )
mamufacex.g 
|- G = ( R freeLMod ( M X. P ) )
mamufacex.d 
|- D = ( Base ` G )
Assertion mamufacex 
|- ( ( ( M =/= (/) /\ P =/= (/) ) /\ ( R e. V /\ Y e. D ) /\ ( M e. Fin /\ N e. Fin /\ P e. Fin ) ) -> ( ( X .X. Z ) = Y -> Z e. C ) )

Proof

Step Hyp Ref Expression
1 mamudm.e 
 |-  E = ( R freeLMod ( M X. N ) )
2 mamudm.b 
 |-  B = ( Base ` E )
3 mamudm.f 
 |-  F = ( R freeLMod ( N X. P ) )
4 mamudm.c 
 |-  C = ( Base ` F )
5 mamudm.m 
 |-  .X. = ( R maMul <. M , N , P >. )
6 mamufacex.g 
 |-  G = ( R freeLMod ( M X. P ) )
7 mamufacex.d 
 |-  D = ( Base ` G )
8 2a1 
 |-  ( Z e. C -> ( ( ( M =/= (/) /\ P =/= (/) ) /\ ( R e. V /\ Y e. D ) /\ ( M e. Fin /\ N e. Fin /\ P e. Fin ) ) -> ( ( X .X. Z ) = Y -> Z e. C ) ) )
9 1 2 3 4 5 mamudm 
 |-  ( ( R e. V /\ ( M e. Fin /\ N e. Fin /\ P e. Fin ) ) -> dom .X. = ( B X. C ) )
10 9 adantlr 
 |-  ( ( ( R e. V /\ Y e. D ) /\ ( M e. Fin /\ N e. Fin /\ P e. Fin ) ) -> dom .X. = ( B X. C ) )
11 10 3adant1 
 |-  ( ( ( M =/= (/) /\ P =/= (/) ) /\ ( R e. V /\ Y e. D ) /\ ( M e. Fin /\ N e. Fin /\ P e. Fin ) ) -> dom .X. = ( B X. C ) )
12 simpl 
 |-  ( ( -. Z e. C /\ ( ( M =/= (/) /\ P =/= (/) ) /\ ( R e. V /\ Y e. D ) /\ ( M e. Fin /\ N e. Fin /\ P e. Fin ) ) ) -> -. Z e. C )
13 12 intnand 
 |-  ( ( -. Z e. C /\ ( ( M =/= (/) /\ P =/= (/) ) /\ ( R e. V /\ Y e. D ) /\ ( M e. Fin /\ N e. Fin /\ P e. Fin ) ) ) -> -. ( X e. B /\ Z e. C ) )
14 ndmovg 
 |-  ( ( dom .X. = ( B X. C ) /\ -. ( X e. B /\ Z e. C ) ) -> ( X .X. Z ) = (/) )
15 11 13 14 syl2an2 
 |-  ( ( -. Z e. C /\ ( ( M =/= (/) /\ P =/= (/) ) /\ ( R e. V /\ Y e. D ) /\ ( M e. Fin /\ N e. Fin /\ P e. Fin ) ) ) -> ( X .X. Z ) = (/) )
16 eqeq1 
 |-  ( ( X .X. Z ) = (/) -> ( ( X .X. Z ) = Y <-> (/) = Y ) )
17 xpfi 
 |-  ( ( M e. Fin /\ P e. Fin ) -> ( M X. P ) e. Fin )
18 17 3adant2 
 |-  ( ( M e. Fin /\ N e. Fin /\ P e. Fin ) -> ( M X. P ) e. Fin )
19 xpnz 
 |-  ( ( M =/= (/) /\ P =/= (/) ) <-> ( M X. P ) =/= (/) )
20 19 biimpi 
 |-  ( ( M =/= (/) /\ P =/= (/) ) -> ( M X. P ) =/= (/) )
21 eqid 
 |-  ( Base ` R ) = ( Base ` R )
22 6 21 7 elfrlmbasn0 
 |-  ( ( ( M X. P ) e. Fin /\ ( M X. P ) =/= (/) ) -> ( Y e. D -> Y =/= (/) ) )
23 18 20 22 syl2an 
 |-  ( ( ( M e. Fin /\ N e. Fin /\ P e. Fin ) /\ ( M =/= (/) /\ P =/= (/) ) ) -> ( Y e. D -> Y =/= (/) ) )
24 23 ex 
 |-  ( ( M e. Fin /\ N e. Fin /\ P e. Fin ) -> ( ( M =/= (/) /\ P =/= (/) ) -> ( Y e. D -> Y =/= (/) ) ) )
25 24 com13 
 |-  ( Y e. D -> ( ( M =/= (/) /\ P =/= (/) ) -> ( ( M e. Fin /\ N e. Fin /\ P e. Fin ) -> Y =/= (/) ) ) )
26 25 adantl 
 |-  ( ( R e. V /\ Y e. D ) -> ( ( M =/= (/) /\ P =/= (/) ) -> ( ( M e. Fin /\ N e. Fin /\ P e. Fin ) -> Y =/= (/) ) ) )
27 26 3imp21 
 |-  ( ( ( M =/= (/) /\ P =/= (/) ) /\ ( R e. V /\ Y e. D ) /\ ( M e. Fin /\ N e. Fin /\ P e. Fin ) ) -> Y =/= (/) )
28 eqneqall 
 |-  ( Y = (/) -> ( Y =/= (/) -> Z e. C ) )
29 27 28 syl5com 
 |-  ( ( ( M =/= (/) /\ P =/= (/) ) /\ ( R e. V /\ Y e. D ) /\ ( M e. Fin /\ N e. Fin /\ P e. Fin ) ) -> ( Y = (/) -> Z e. C ) )
30 29 adantl 
 |-  ( ( -. Z e. C /\ ( ( M =/= (/) /\ P =/= (/) ) /\ ( R e. V /\ Y e. D ) /\ ( M e. Fin /\ N e. Fin /\ P e. Fin ) ) ) -> ( Y = (/) -> Z e. C ) )
31 30 com12 
 |-  ( Y = (/) -> ( ( -. Z e. C /\ ( ( M =/= (/) /\ P =/= (/) ) /\ ( R e. V /\ Y e. D ) /\ ( M e. Fin /\ N e. Fin /\ P e. Fin ) ) ) -> Z e. C ) )
32 31 eqcoms 
 |-  ( (/) = Y -> ( ( -. Z e. C /\ ( ( M =/= (/) /\ P =/= (/) ) /\ ( R e. V /\ Y e. D ) /\ ( M e. Fin /\ N e. Fin /\ P e. Fin ) ) ) -> Z e. C ) )
33 16 32 syl6bi 
 |-  ( ( X .X. Z ) = (/) -> ( ( X .X. Z ) = Y -> ( ( -. Z e. C /\ ( ( M =/= (/) /\ P =/= (/) ) /\ ( R e. V /\ Y e. D ) /\ ( M e. Fin /\ N e. Fin /\ P e. Fin ) ) ) -> Z e. C ) ) )
34 33 com23 
 |-  ( ( X .X. Z ) = (/) -> ( ( -. Z e. C /\ ( ( M =/= (/) /\ P =/= (/) ) /\ ( R e. V /\ Y e. D ) /\ ( M e. Fin /\ N e. Fin /\ P e. Fin ) ) ) -> ( ( X .X. Z ) = Y -> Z e. C ) ) )
35 15 34 mpcom 
 |-  ( ( -. Z e. C /\ ( ( M =/= (/) /\ P =/= (/) ) /\ ( R e. V /\ Y e. D ) /\ ( M e. Fin /\ N e. Fin /\ P e. Fin ) ) ) -> ( ( X .X. Z ) = Y -> Z e. C ) )
36 35 ex 
 |-  ( -. Z e. C -> ( ( ( M =/= (/) /\ P =/= (/) ) /\ ( R e. V /\ Y e. D ) /\ ( M e. Fin /\ N e. Fin /\ P e. Fin ) ) -> ( ( X .X. Z ) = Y -> Z e. C ) ) )
37 8 36 pm2.61i 
 |-  ( ( ( M =/= (/) /\ P =/= (/) ) /\ ( R e. V /\ Y e. D ) /\ ( M e. Fin /\ N e. Fin /\ P e. Fin ) ) -> ( ( X .X. Z ) = Y -> Z e. C ) )