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 
|- B = ( Base ` R )
mavmuldm.c 
|- C = ( B ^m ( M X. N ) )
mavmuldm.d 
|- D = ( B ^m N )
mavmuldm.t 
|- .x. = ( R maVecMul <. M , N >. )
mavmulsolcl.e 
|- E = ( B ^m M )
Assertion mavmulsolcl 
|- ( ( ( M e. Fin /\ N e. Fin /\ M =/= (/) ) /\ ( R e. V /\ Y e. E ) ) -> ( ( A .x. X ) = Y -> X e. D ) )

Proof

Step Hyp Ref Expression
1 mavmuldm.b 
 |-  B = ( Base ` R )
2 mavmuldm.c 
 |-  C = ( B ^m ( M X. N ) )
3 mavmuldm.d 
 |-  D = ( B ^m N )
4 mavmuldm.t 
 |-  .x. = ( R maVecMul <. M , N >. )
5 mavmulsolcl.e 
 |-  E = ( B ^m M )
6 2a1 
 |-  ( X e. D -> ( ( ( M e. Fin /\ N e. Fin /\ M =/= (/) ) /\ ( R e. V /\ Y e. E ) ) -> ( ( A .x. X ) = Y -> X e. D ) ) )
7 simpl 
 |-  ( ( R e. V /\ Y e. E ) -> R e. V )
8 7 adantl 
 |-  ( ( ( M e. Fin /\ N e. Fin /\ M =/= (/) ) /\ ( R e. V /\ Y e. E ) ) -> R e. V )
9 simpl1 
 |-  ( ( ( M e. Fin /\ N e. Fin /\ M =/= (/) ) /\ ( R e. V /\ Y e. E ) ) -> M e. Fin )
10 simpl2 
 |-  ( ( ( M e. Fin /\ N e. Fin /\ M =/= (/) ) /\ ( R e. V /\ Y e. E ) ) -> N e. Fin )
11 8 9 10 3jca 
 |-  ( ( ( M e. Fin /\ N e. Fin /\ M =/= (/) ) /\ ( R e. V /\ Y e. E ) ) -> ( R e. V /\ M e. Fin /\ N e. Fin ) )
12 11 adantl 
 |-  ( ( -. X e. D /\ ( ( M e. Fin /\ N e. Fin /\ M =/= (/) ) /\ ( R e. V /\ Y e. E ) ) ) -> ( R e. V /\ M e. Fin /\ N e. Fin ) )
13 1 2 3 4 mavmuldm 
 |-  ( ( R e. V /\ M e. Fin /\ N e. Fin ) -> dom .x. = ( C X. D ) )
14 12 13 syl 
 |-  ( ( -. X e. D /\ ( ( M e. Fin /\ N e. Fin /\ M =/= (/) ) /\ ( R e. V /\ Y e. E ) ) ) -> dom .x. = ( C X. D ) )
15 simpl 
 |-  ( ( -. X e. D /\ ( ( M e. Fin /\ N e. Fin /\ M =/= (/) ) /\ ( R e. V /\ Y e. E ) ) ) -> -. X e. D )
16 15 intnand 
 |-  ( ( -. X e. D /\ ( ( M e. Fin /\ N e. Fin /\ M =/= (/) ) /\ ( R e. V /\ Y e. E ) ) ) -> -. ( A e. C /\ X e. D ) )
17 ndmovg 
 |-  ( ( dom .x. = ( C X. D ) /\ -. ( A e. C /\ X e. D ) ) -> ( A .x. X ) = (/) )
18 14 16 17 syl2anc 
 |-  ( ( -. X e. D /\ ( ( M e. Fin /\ N e. Fin /\ M =/= (/) ) /\ ( R e. V /\ Y e. E ) ) ) -> ( A .x. X ) = (/) )
19 eqeq1 
 |-  ( ( A .x. X ) = (/) -> ( ( A .x. X ) = Y <-> (/) = Y ) )
20 elmapi 
 |-  ( Y e. ( B ^m M ) -> Y : M --> B )
21 f0dom0 
 |-  ( Y : M --> B -> ( M = (/) <-> Y = (/) ) )
22 21 biimprd 
 |-  ( Y : M --> B -> ( Y = (/) -> M = (/) ) )
23 22 necon3d 
 |-  ( Y : M --> B -> ( M =/= (/) -> Y =/= (/) ) )
24 23 com12 
 |-  ( M =/= (/) -> ( Y : M --> B -> Y =/= (/) ) )
25 24 3ad2ant3 
 |-  ( ( M e. Fin /\ N e. Fin /\ M =/= (/) ) -> ( Y : M --> B -> Y =/= (/) ) )
26 25 com12 
 |-  ( Y : M --> B -> ( ( M e. Fin /\ N e. Fin /\ M =/= (/) ) -> Y =/= (/) ) )
27 26 a1d 
 |-  ( Y : M --> B -> ( R e. V -> ( ( M e. Fin /\ N e. Fin /\ M =/= (/) ) -> Y =/= (/) ) ) )
28 20 27 syl 
 |-  ( Y e. ( B ^m M ) -> ( R e. V -> ( ( M e. Fin /\ N e. Fin /\ M =/= (/) ) -> Y =/= (/) ) ) )
29 28 5 eleq2s 
 |-  ( Y e. E -> ( R e. V -> ( ( M e. Fin /\ N e. Fin /\ M =/= (/) ) -> Y =/= (/) ) ) )
30 29 impcom 
 |-  ( ( R e. V /\ Y e. E ) -> ( ( M e. Fin /\ N e. Fin /\ M =/= (/) ) -> Y =/= (/) ) )
31 30 impcom 
 |-  ( ( ( M e. Fin /\ N e. Fin /\ M =/= (/) ) /\ ( R e. V /\ Y e. E ) ) -> Y =/= (/) )
32 eqneqall 
 |-  ( Y = (/) -> ( Y =/= (/) -> X e. D ) )
33 31 32 syl5com 
 |-  ( ( ( M e. Fin /\ N e. Fin /\ M =/= (/) ) /\ ( R e. V /\ Y e. E ) ) -> ( Y = (/) -> X e. D ) )
34 33 adantl 
 |-  ( ( -. X e. D /\ ( ( M e. Fin /\ N e. Fin /\ M =/= (/) ) /\ ( R e. V /\ Y e. E ) ) ) -> ( Y = (/) -> X e. D ) )
35 34 com12 
 |-  ( Y = (/) -> ( ( -. X e. D /\ ( ( M e. Fin /\ N e. Fin /\ M =/= (/) ) /\ ( R e. V /\ Y e. E ) ) ) -> X e. D ) )
36 35 eqcoms 
 |-  ( (/) = Y -> ( ( -. X e. D /\ ( ( M e. Fin /\ N e. Fin /\ M =/= (/) ) /\ ( R e. V /\ Y e. E ) ) ) -> X e. D ) )
37 19 36 syl6bi 
 |-  ( ( A .x. X ) = (/) -> ( ( A .x. X ) = Y -> ( ( -. X e. D /\ ( ( M e. Fin /\ N e. Fin /\ M =/= (/) ) /\ ( R e. V /\ Y e. E ) ) ) -> X e. D ) ) )
38 37 com23 
 |-  ( ( A .x. X ) = (/) -> ( ( -. X e. D /\ ( ( M e. Fin /\ N e. Fin /\ M =/= (/) ) /\ ( R e. V /\ Y e. E ) ) ) -> ( ( A .x. X ) = Y -> X e. D ) ) )
39 18 38 mpcom 
 |-  ( ( -. X e. D /\ ( ( M e. Fin /\ N e. Fin /\ M =/= (/) ) /\ ( R e. V /\ Y e. E ) ) ) -> ( ( A .x. X ) = Y -> X e. D ) )
40 39 ex 
 |-  ( -. X e. D -> ( ( ( M e. Fin /\ N e. Fin /\ M =/= (/) ) /\ ( R e. V /\ Y e. E ) ) -> ( ( A .x. X ) = Y -> X e. D ) ) )
41 6 40 pm2.61i 
 |-  ( ( ( M e. Fin /\ N e. Fin /\ M =/= (/) ) /\ ( R e. V /\ Y e. E ) ) -> ( ( A .x. X ) = Y -> X e. D ) )