mavmulsolcl - Metamath Proof Explorer

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

Theorem mavmulsolcl 19576

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		2a1 28	. 2 $/\$ $/\$ $/\$ $/\$
2		simpl 459	. . . . . . . . 9 $/\$
3	2	adantl 468	. . . . . . . 8 $/\$ $/\$ $/\$ $/\$
4		simpl1 1011	. . . . . . . 8 $/\$ $/\$ $/\$ $/\$
5		simpl2 1012	. . . . . . . 8 $/\$ $/\$ $/\$ $/\$
6	3, 4, 5	3jca 1188	. . . . . . 7 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
7	6	adantl 468	. . . . . 6 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
8		mavmuldm.b	. . . . . . 7
9		mavmuldm.c	. . . . . . 7
10		mavmuldm.d	. . . . . . 7
11		mavmuldm.t	. . . . . . 7 maVecMul
12	8, 9, 10, 11	mavmuldm 19575	. . . . . 6 $/\$ $/\$
13	7, 12	syl 17	. . . . 5 $/\$ $/\$ $/\$ $/\$ $/\$
14		simpl 459	. . . . . 6 $/\$ $/\$ $/\$ $/\$ $/\$
15	14	intnand 927	. . . . 5 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
16		ndmovg 6452	. . . . 5 $/\$ $/\$
17	13, 15, 16	syl2anc 667	. . . 4 $/\$ $/\$ $/\$ $/\$ $/\$
18		eqeq1 2455	. . . . . 6
19		elmapi 7493	. . . . . . . . . . . . . 14
20		f0dom0 5767	. . . . . . . . . . . . . . . . . . . 20
21	20	biimprd 227	. . . . . . . . . . . . . . . . . . 19
22	21	necon3d 2645	. . . . . . . . . . . . . . . . . 18
23	22	com12 32	. . . . . . . . . . . . . . . . 17
24	23	3ad2ant3 1031	. . . . . . . . . . . . . . . 16 $/\$ $/\$
25	24	com12 32	. . . . . . . . . . . . . . 15 $/\$ $/\$
26	25	a1d 26	. . . . . . . . . . . . . 14 $/\$ $/\$
27	19, 26	syl 17	. . . . . . . . . . . . 13 $/\$ $/\$
28		mavmulsolcl.e	. . . . . . . . . . . . 13
29	27, 28	eleq2s 2547	. . . . . . . . . . . 12 $/\$ $/\$
30	29	impcom 432	. . . . . . . . . . 11 $/\$ $/\$ $/\$
31	30	impcom 432	. . . . . . . . . 10 $/\$ $/\$ $/\$ $/\$
32		eqneqall 2634	. . . . . . . . . 10
33	31, 32	syl5com 31	. . . . . . . . 9 $/\$ $/\$ $/\$ $/\$
34	33	adantl 468	. . . . . . . 8 $/\$ $/\$ $/\$ $/\$ $/\$
35	34	com12 32	. . . . . . 7 $/\$ $/\$ $/\$ $/\$ $/\$
36	35	eqcoms 2459	. . . . . 6 $/\$ $/\$ $/\$ $/\$ $/\$
37	18, 36	syl6bi 232	. . . . 5 $/\$ $/\$ $/\$ $/\$ $/\$
38	37	com23 81	. . . 4 $/\$ $/\$ $/\$ $/\$ $/\$
39	17, 38	mpcom 37	. . 3 $/\$ $/\$ $/\$ $/\$ $/\$
40	39	ex 436	. 2 $/\$ $/\$ $/\$ $/\$
41	1, 40	pm2.61i 168	1 $/\$ $/\$ $/\$ $/\$

Colors of variables: wff setvar class

Syntax hints:

wn 3

wi 4 $/\$ wa 371 $/\$ w3a 985

wceq 1444

wcel 1887

wne 2622

c0 3731

cop 3974

cxp 4832

cdm 4834

wf 5578

cfv 5582 (class class class)co 6290

cmap 7472

cfn 7569

cbs 15121 maVecMul cmvmul 19565

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1669 ax-4 1682 ax-5 1758 ax-6 1805 ax-7 1851 ax-8 1889 ax-9 1896 ax-10 1915 ax-11 1920 ax-12 1933 ax-13 2091 ax-ext 2431 ax-rep 4515 ax-sep 4525 ax-nul 4534 ax-pow 4581 ax-pr 4639 ax-un 6583

This theorem depends on definitions: df-bi 189 df-or 372 df-an 373 df-3an 987 df-tru 1447 df-ex 1664 df-nf 1668 df-sb 1798 df-eu 2303 df-mo 2304 df-clab 2438 df-cleq 2444 df-clel 2447 df-nfc 2581 df-ne 2624 df-ral 2742 df-rex 2743 df-reu 2744 df-rab 2746 df-v 3047 df-sbc 3268 df-csb 3364 df-dif 3407 df-un 3409 df-in 3411 df-ss 3418 df-nul 3732 df-if 3882 df-pw 3953 df-sn 3969 df-pr 3971 df-op 3975 df-uni 4199 df-iun 4280 df-br 4403 df-opab 4462 df-mpt 4463 df-id 4749 df-xp 4840 df-rel 4841 df-cnv 4842 df-co 4843 df-dm 4844 df-rn 4845 df-res 4846 df-ima 4847 df-iota 5546 df-fun 5584 df-fn 5585 df-f 5586 df-f1 5587 df-fo 5588 df-f1o 5589 df-fv 5590 df-ov 6293 df-oprab 6294 df-mpt2 6295 df-1st 6793 df-2nd 6794 df-map 7474 df-mvmul 19566

This theorem is referenced by: slesolvec 19704 cramerimplem2 19709

W3C validator