Theorem mavmulsolcl 18922

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 457	. . . . . . . . 9 |- ( ( R e. V /\ Y e. E ) -> R e. V )
4	3	adantl 466	. . . . . . . 8 |- ( ( ( M e. Fin /\ N e. Fin /\ M =/= (/) ) /\ ( R e. V /\ Y e. E ) ) -> R e. V )
5		simpl1 999	. . . . . . . 8 |- ( ( ( M e. Fin /\ N e. Fin /\ M =/= (/) ) /\ ( R e. V /\ Y e. E ) ) -> M e. Fin )
6		simpl2 1000	. . . . . . . 8 |- ( ( ( M e. Fin /\ N e. Fin /\ M =/= (/) ) /\ ( R e. V /\ Y e. E ) ) -> N e. Fin )
7	4, 5, 6	3jca 1176	. . . . . . 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 466	. . . . . 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 18921	. . . . . 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 457	. . . . . 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 6453	. . . . 5 |- ( ( dom .x. = ( C X. D ) /\ -. ( A e. C /\ X e. D ) ) -> ( A .x. X ) = (/) )
18	14, 16, 17	syl2anc 661	. . . 4 |- ( ( -. X e. D /\ ( ( M e. Fin /\ N e. Fin /\ M =/= (/) ) /\ ( R e. V /\ Y e. E ) ) ) -> ( A .x. X ) = (/) )
19		eqeq1 2471	. . . . . 6 |- ( ( A .x. X ) = (/) -> ( ( A .x. X ) = Y <-> (/) = Y ) )
20		elmapi 7452	. . . . . . . . . . . . . 14 |- ( Y e. ( B ^m M ) -> Y : M --> B )
21		f0dom0 5775	. . . . . . . . . . . . . . . . . . . 20 |- ( Y : M --> B -> ( M = (/) <-> Y = (/) ) )
22	21	biimprd 223	. . . . . . . . . . . . . . . . . . 19 |- ( Y : M --> B -> ( Y = (/) -> M = (/) ) )
23	22	necon3d 2691	. . . . . . . . . . . . . . . . . 18 |- ( Y : M --> B -> ( M =/= (/) -> Y =/= (/) ) )
24	23	com12 31	. . . . . . . . . . . . . . . . 17 |- ( M =/= (/) -> ( Y : M --> B -> Y =/= (/) ) )
25	24	3ad2ant3 1019	. . . . . . . . . . . . . . . 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 2575	. . . . . . . . . . . 12 |- ( Y e. E -> ( R e. V -> ( ( M e. Fin /\ N e. Fin /\ M =/= (/) ) -> Y =/= (/) ) ) )
31	30	impcom 430	. . . . . . . . . . 11 |- ( ( R e. V /\ Y e. E ) -> ( ( M e. Fin /\ N e. Fin /\ M =/= (/) ) -> Y =/= (/) ) )
32	31	impcom 430	. . . . . . . . . 10 |- ( ( ( M e. Fin /\ N e. Fin /\ M =/= (/) ) /\ ( R e. V /\ Y e. E ) ) -> Y =/= (/) )
33		eqneqall 2674	. . . . . . . . . 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 466	. . . . . . . 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 2479	. . . . . 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 434	. 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 369   /\ w3a 973   = wceq 1379   e. wcel 1767   =/= wne 2662   (/)c0 3790   <.cop 4039   X. cxp 5003   dom cdm 5005   -->wf 5590   ` cfv 5594  (class class class)co 6295   ^m cmap 7432   Fincfn 7528   Basecbs 14507   maVecMul cmvmul 18911

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1601  ax-4 1612  ax-5 1680  ax-6 1719  ax-7 1739  ax-8 1769  ax-9 1771  ax-10 1786  ax-11 1791  ax-12 1803  ax-13 1968  ax-ext 2445  ax-rep 4564  ax-sep 4574  ax-nul 4582  ax-pow 4631  ax-pr 4692  ax-un 6587

This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3an 975  df-tru 1382  df-ex 1597  df-nf 1600  df-sb 1712  df-eu 2279  df-mo 2280  df-clab 2453  df-cleq 2459  df-clel 2462  df-nfc 2617  df-ne 2664  df-ral 2822  df-rex 2823  df-reu 2824  df-rab 2826  df-v 3120  df-sbc 3337  df-csb 3441  df-dif 3484  df-un 3486  df-in 3488  df-ss 3495  df-nul 3791  df-if 3946  df-pw 4018  df-sn 4034  df-pr 4036  df-op 4040  df-uni 4252  df-iun 4333  df-br 4454  df-opab 4512  df-mpt 4513  df-id 4801  df-xp 5011  df-rel 5012  df-cnv 5013  df-co 5014  df-dm 5015  df-rn 5016  df-res 5017  df-ima 5018  df-iota 5557  df-fun 5596  df-fn 5597  df-f 5598  df-f1 5599  df-fo 5600  df-f1o 5601  df-fv 5602  df-ov 6298  df-oprab 6299  df-mpt2 6300  df-1st 6795  df-2nd 6796  df-map 7434  df-mvmul 18912

This theorem is referenced by:  slesolvec  19050  cramerimplem2  19055