mavmulsolcl - Metamath Proof Explorer

	Metamath Proof Explorer	< Previous Next > Nearby theorems
Mirrors > Home > MPE Home > Th. List > mavmulsolcl		Structured version Unicode version

Theorem mavmulsolcl 18492

Description: Every solution of the equation

for a matrix

and a vector

is a vector. (Contributed by AV, 27-Feb-2019.)

**Hypotheses**
Ref	Expression
mavmuldm.b
mavmuldm.c
mavmuldm.d
mavmuldm.t	maVecMul
mavmulsolcl.e

**Assertion**
Ref	Expression
mavmulsolcl	$/\$ $/\$ $/\$ $/\$

**Proof of Theorem mavmulsolcl**
Step	Hyp	Ref	Expression
1		ax-1 6	. . 3
2	1	a1d 25	. 2 $/\$ $/\$ $/\$ $/\$
3		simpl 457	. . . . . . . . 9 $/\$
4	3	adantl 466	. . . . . . . 8 $/\$ $/\$ $/\$ $/\$
5		simpl1 991	. . . . . . . 8 $/\$ $/\$ $/\$ $/\$
6		simpl2 992	. . . . . . . 8 $/\$ $/\$ $/\$ $/\$
7	4, 5, 6	3jca 1168	. . . . . . 7 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
8	7	adantl 466	. . . . . 6 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
9		mavmuldm.b	. . . . . . 7
10		mavmuldm.c	. . . . . . 7
11		mavmuldm.d	. . . . . . 7
12		mavmuldm.t	. . . . . . 7 maVecMul
13	9, 10, 11, 12	mavmuldm 18491	. . . . . 6 $/\$ $/\$
14	8, 13	syl 16	. . . . 5 $/\$ $/\$ $/\$ $/\$ $/\$
15		simpl 457	. . . . . 6 $/\$ $/\$ $/\$ $/\$ $/\$
16	15	intnand 907	. . . . 5 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
17		ndmovg 6359	. . . . 5 $/\$ $/\$
18	14, 16, 17	syl2anc 661	. . . 4 $/\$ $/\$ $/\$ $/\$ $/\$
19		eqeq1 2458	. . . . . 6
20		elmapi 7347	. . . . . . . . . . . . . 14
21		f0dom0 5706	. . . . . . . . . . . . . . . . . . . 20
22	21	biimprd 223	. . . . . . . . . . . . . . . . . . 19
23	22	necon3d 2676	. . . . . . . . . . . . . . . . . 18
24	23	com12 31	. . . . . . . . . . . . . . . . 17
25	24	3ad2ant3 1011	. . . . . . . . . . . . . . . 16 $/\$ $/\$
26	25	com12 31	. . . . . . . . . . . . . . 15 $/\$ $/\$
27	26	a1d 25	. . . . . . . . . . . . . 14 $/\$ $/\$
28	20, 27	syl 16	. . . . . . . . . . . . 13 $/\$ $/\$
29		mavmulsolcl.e	. . . . . . . . . . . . 13
30	28, 29	eleq2s 2562	. . . . . . . . . . . 12 $/\$ $/\$
31	30	impcom 430	. . . . . . . . . . 11 $/\$ $/\$ $/\$
32	31	impcom 430	. . . . . . . . . 10 $/\$ $/\$ $/\$ $/\$
33		eqneqall 2661	. . . . . . . . . 10
34	32, 33	syl5com 30	. . . . . . . . 9 $/\$ $/\$ $/\$ $/\$
35	34	adantl 466	. . . . . . . 8 $/\$ $/\$ $/\$ $/\$ $/\$
36	35	com12 31	. . . . . . 7 $/\$ $/\$ $/\$ $/\$ $/\$
37	36	eqcoms 2466	. . . . . 6 $/\$ $/\$ $/\$ $/\$ $/\$
38	19, 37	syl6bi 228	. . . . 5 $/\$ $/\$ $/\$ $/\$ $/\$
39	38	com23 78	. . . 4 $/\$ $/\$ $/\$ $/\$ $/\$
40	18, 39	mpcom 36	. . 3 $/\$ $/\$ $/\$ $/\$ $/\$
41	40	ex 434	. 2 $/\$ $/\$ $/\$ $/\$
42	2, 41	pm2.61i 164	1 $/\$ $/\$ $/\$ $/\$

Colors of variables: wff setvar class

Syntax hints:

wn 3

wi 4 $/\$ wa 369 $/\$ w3a 965

wceq 1370

wcel 1758

wne 2648

c0 3748

cop 3994

cxp 4949

cdm 4951

wf 5525

cfv 5529 (class class class)co 6203

cmap 7327

cfn 7423

cbs 14295 maVecMul cmvmul 18481

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1592 ax-4 1603 ax-5 1671 ax-6 1710 ax-7 1730 ax-8 1760 ax-9 1762 ax-10 1777 ax-11 1782 ax-12 1794 ax-13 1955 ax-ext 2432 ax-rep 4514 ax-sep 4524 ax-nul 4532 ax-pow 4581 ax-pr 4642 ax-un 6485

This theorem depends on definitions: df-bi 185 df-or 370 df-an 371 df-3an 967 df-tru 1373 df-ex 1588 df-nf 1591 df-sb 1703 df-eu 2266 df-mo 2267 df-clab 2440 df-cleq 2446 df-clel 2449 df-nfc 2604 df-ne 2650 df-ral 2804 df-rex 2805 df-reu 2806 df-rab 2808 df-v 3080 df-sbc 3295 df-csb 3399 df-dif 3442 df-un 3444 df-in 3446 df-ss 3453 df-nul 3749 df-if 3903 df-pw 3973 df-sn 3989 df-pr 3991 df-op 3995 df-uni 4203 df-iun 4284 df-br 4404 df-opab 4462 df-mpt 4463 df-id 4747 df-xp 4957 df-rel 4958 df-cnv 4959 df-co 4960 df-dm 4961 df-rn 4962 df-res 4963 df-ima 4964 df-iota 5492 df-fun 5531 df-fn 5532 df-f 5533 df-f1 5534 df-fo 5535 df-f1o 5536 df-fv 5537 df-ov 6206 df-oprab 6207 df-mpt2 6208 df-1st 6690 df-2nd 6691 df-map 7329 df-mvmul 18482

This theorem is referenced by: slesolvec 18620 cramerimplem2 18625

W3C validator