Theorem mavmulsolcl 19220

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.)

Hypotheses

Ref	Expression
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

Ref	Expression
mavmulsolcl	|- ( ( ( M e. Fin /\ N e. Fin /\ M =/= (/) ) /\ ( R e. V /\ Y e. E ) ) -> ( ( A .x. X ) = Y -> X e. D ) )

Proof of Theorem mavmulsolcl

Step	Hyp	Ref	Expression
1		ax-1 6	. . 3 |- ( X e. D -> ( ( A .x. X ) = Y -> X e. D ) )
2	1	a1d 25	. 2 |- ( X e. D -> ( ( ( M e. Fin /\ N e. Fin /\ M =/= (/) ) /\ ( R e. V /\ Y e. E ) ) -> ( ( A .x. X ) = Y -> X e. D ) ) )
3		simpl 455	. . . . . . . . 9 |- ( ( R e. V /\ Y e. E ) -> R e. V )
4	3	adantl 464	. . . . . . . 8 |- ( ( ( M e. Fin /\ N e. Fin /\ M =/= (/) ) /\ ( R e. V /\ Y e. E ) ) -> R e. V )
5		simpl1 997	. . . . . . . 8 |- ( ( ( M e. Fin /\ N e. Fin /\ M =/= (/) ) /\ ( R e. V /\ Y e. E ) ) -> M e. Fin )
6		simpl2 998	. . . . . . . 8 |- ( ( ( M e. Fin /\ N e. Fin /\ M =/= (/) ) /\ ( R e. V /\ Y e. E ) ) -> N e. Fin )
7	4, 5, 6	3jca 1174	. . . . . . 7 |- ( ( ( M e. Fin /\ N e. Fin /\ M =/= (/) ) /\ ( R e. V /\ Y e. E ) ) -> ( R e. V /\ M e. Fin /\ N e. Fin ) )
8	7	adantl 464	. . . . . 6 |- ( ( -. 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 ) )
9		mavmuldm.b	. . . . . . 7 |- B = ( Base ` R )
10		mavmuldm.c	. . . . . . 7 |- C = ( B ^m ( M X. N ) )
11		mavmuldm.d	. . . . . . 7 |- D = ( B ^m N )
12		mavmuldm.t	. . . . . . 7 |- .x. = ( R maVecMul <. M , N >. )
13	9, 10, 11, 12	mavmuldm 19219	. . . . . 6 |- ( ( R e. V /\ M e. Fin /\ N e. Fin ) -> dom .x. = ( C X. D ) )
14	8, 13	syl 16	. . . . 5 |- ( ( -. X e. D /\ ( ( M e. Fin /\ N e. Fin /\ M =/= (/) ) /\ ( R e. V /\ Y e. E ) ) ) -> dom .x. = ( C X. D ) )
15		simpl 455	. . . . . 6 |- ( ( -. X e. D /\ ( ( M e. Fin /\ N e. Fin /\ M =/= (/) ) /\ ( R e. V /\ Y e. E ) ) ) -> -. X e. D )
16	15	intnand 914	. . . . 5 |- ( ( -. X e. D /\ ( ( M e. Fin /\ N e. Fin /\ M =/= (/) ) /\ ( R e. V /\ Y e. E ) ) ) -> -. ( A e. C /\ X e. D ) )
17		ndmovg 6431	. . . . 5 |- ( ( dom .x. = ( C X. D ) /\ -. ( A e. C /\ X e. D ) ) -> ( A .x. X ) = (/) )
18	14, 16, 17	syl2anc 659	. . . 4 |- ( ( -. X e. D /\ ( ( M e. Fin /\ N e. Fin /\ M =/= (/) ) /\ ( R e. V /\ Y e. E ) ) ) -> ( A .x. X ) = (/) )
19		eqeq1 2458	. . . . . 6 |- ( ( A .x. X ) = (/) -> ( ( A .x. X ) = Y <-> (/) = Y ) )
20		elmapi 7433	. . . . . . . . . . . . . 14 |- ( Y e. ( B ^m M ) -> Y : M --> B )
21		f0dom0 5751	. . . . . . . . . . . . . . . . . . . 20 |- ( Y : M --> B -> ( M = (/) <-> Y = (/) ) )
22	21	biimprd 223	. . . . . . . . . . . . . . . . . . 19 |- ( Y : M --> B -> ( Y = (/) -> M = (/) ) )
23	22	necon3d 2678	. . . . . . . . . . . . . . . . . 18 |- ( Y : M --> B -> ( M =/= (/) -> Y =/= (/) ) )
24	23	com12 31	. . . . . . . . . . . . . . . . 17 |- ( M =/= (/) -> ( Y : M --> B -> Y =/= (/) ) )
25	24	3ad2ant3 1017	. . . . . . . . . . . . . . . 16 |- ( ( M e. Fin /\ N e. Fin /\ M =/= (/) ) -> ( Y : M --> B -> Y =/= (/) ) )
26	25	com12 31	. . . . . . . . . . . . . . 15 |- ( Y : M --> B -> ( ( M e. Fin /\ N e. Fin /\ M =/= (/) ) -> Y =/= (/) ) )
27	26	a1d 25	. . . . . . . . . . . . . 14 |- ( Y : M --> B -> ( R e. V -> ( ( M e. Fin /\ N e. Fin /\ M =/= (/) ) -> Y =/= (/) ) ) )
28	20, 27	syl 16	. . . . . . . . . . . . 13 |- ( Y e. ( B ^m M ) -> ( R e. V -> ( ( M e. Fin /\ N e. Fin /\ M =/= (/) ) -> Y =/= (/) ) ) )
29		mavmulsolcl.e	. . . . . . . . . . . . 13 |- E = ( B ^m M )
30	28, 29	eleq2s 2562	. . . . . . . . . . . 12 |- ( Y e. E -> ( R e. V -> ( ( M e. Fin /\ N e. Fin /\ M =/= (/) ) -> Y =/= (/) ) ) )
31	30	impcom 428	. . . . . . . . . . 11 |- ( ( R e. V /\ Y e. E ) -> ( ( M e. Fin /\ N e. Fin /\ M =/= (/) ) -> Y =/= (/) ) )
32	31	impcom 428	. . . . . . . . . 10 |- ( ( ( M e. Fin /\ N e. Fin /\ M =/= (/) ) /\ ( R e. V /\ Y e. E ) ) -> Y =/= (/) )
33		eqneqall 2661	. . . . . . . . . 10 |- ( Y = (/) -> ( Y =/= (/) -> X e. D ) )
34	32, 33	syl5com 30	. . . . . . . . 9 |- ( ( ( M e. Fin /\ N e. Fin /\ M =/= (/) ) /\ ( R e. V /\ Y e. E ) ) -> ( Y = (/) -> X e. D ) )
35	34	adantl 464	. . . . . . . 8 |- ( ( -. X e. D /\ ( ( M e. Fin /\ N e. Fin /\ M =/= (/) ) /\ ( R e. V /\ Y e. E ) ) ) -> ( Y = (/) -> X e. D ) )
36	35	com12 31	. . . . . . 7 |- ( Y = (/) -> ( ( -. X e. D /\ ( ( M e. Fin /\ N e. Fin /\ M =/= (/) ) /\ ( R e. V /\ Y e. E ) ) ) -> X e. D ) )
37	36	eqcoms 2466	. . . . . 6 |- ( (/) = Y -> ( ( -. X e. D /\ ( ( M e. Fin /\ N e. Fin /\ M =/= (/) ) /\ ( R e. V /\ Y e. E ) ) ) -> X e. D ) )
38	19, 37	syl6bi 228	. . . . 5 |- ( ( 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 ) ) )
39	38	com23 78	. . . 4 |- ( ( 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 ) ) )
40	18, 39	mpcom 36	. . 3 |- ( ( -. X e. D /\ ( ( M e. Fin /\ N e. Fin /\ M =/= (/) ) /\ ( R e. V /\ Y e. E ) ) ) -> ( ( A .x. X ) = Y -> X e. D ) )
41	40	ex 432	. 2 |- ( -. X e. D -> ( ( ( M e. Fin /\ N e. Fin /\ M =/= (/) ) /\ ( R e. V /\ Y e. E ) ) -> ( ( A .x. X ) = Y -> X e. D ) ) )
42	2, 41	pm2.61i 164	1 |- ( ( ( M e. Fin /\ N e. Fin /\ M =/= (/) ) /\ ( R e. V /\ Y e. E ) ) -> ( ( A .x. X ) = Y -> X e. D ) )

Syntax hints:   -. wn 3   -> wi 4   /\ wa 367   /\ w3a 971   = wceq 1398   e. wcel 1823   =/= wne 2649   (/)c0 3783   <.cop 4022   X. cxp 4986   dom cdm 4988   -->wf 5566   ` cfv 5570  (class class class)co 6270   ^m cmap 7412   Fincfn 7509   Basecbs 14716   maVecMul cmvmul 19209

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1623  ax-4 1636  ax-5 1709  ax-6 1752  ax-7 1795  ax-8 1825  ax-9 1827  ax-10 1842  ax-11 1847  ax-12 1859  ax-13 2004  ax-ext 2432  ax-rep 4550  ax-sep 4560  ax-nul 4568  ax-pow 4615  ax-pr 4676  ax-un 6565

This theorem depends on definitions:  df-bi 185  df-or 368  df-an 369  df-3an 973  df-tru 1401  df-ex 1618  df-nf 1622  df-sb 1745  df-eu 2288  df-mo 2289  df-clab 2440  df-cleq 2446  df-clel 2449  df-nfc 2604  df-ne 2651  df-ral 2809  df-rex 2810  df-reu 2811  df-rab 2813  df-v 3108  df-sbc 3325  df-csb 3421  df-dif 3464  df-un 3466  df-in 3468  df-ss 3475  df-nul 3784  df-if 3930  df-pw 4001  df-sn 4017  df-pr 4019  df-op 4023  df-uni 4236  df-iun 4317  df-br 4440  df-opab 4498  df-mpt 4499  df-id 4784  df-xp 4994  df-rel 4995  df-cnv 4996  df-co 4997  df-dm 4998  df-rn 4999  df-res 5000  df-ima 5001  df-iota 5534  df-fun 5572  df-fn 5573  df-f 5574  df-f1 5575  df-fo 5576  df-f1o 5577  df-fv 5578  df-ov 6273  df-oprab 6274  df-mpt2 6275  df-1st 6773  df-2nd 6774  df-map 7414  df-mvmul 19210

This theorem is referenced by:  slesolvec  19348  cramerimplem2  19353