slesolex - Metamath Proof Explorer

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

Theorem slesolex 22567

Description: Every system of linear equations represented by a matrix with a unit as determinant has a solution. (Contributed by AV, 11-Feb-2019.) (Revised by AV, 28-Feb-2019.)

**Hypotheses**
Ref	Expression
slesolex.a	⊢ 𝐴 = (𝑁 Mat 𝑅)
slesolex.b	⊢ 𝐵 = (Base‘𝐴)
slesolex.v	⊢ 𝑉 = ((Base‘𝑅) ↑_m 𝑁)
slesolex.x	⊢ · = (𝑅 maVecMul ⟨𝑁, 𝑁⟩)
slesolex.d	⊢ 𝐷 = (𝑁 maDet 𝑅)

**Assertion**
Ref	Expression
slesolex	⊢ (((𝑁 ≠ ∅ ∧ 𝑅 ∈ CRing) ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝑉) ∧ (𝐷‘𝑋) ∈ (Unit‘𝑅)) → ∃𝑧 ∈ 𝑉 (𝑋 · 𝑧) = 𝑌)

Distinct variable groups: 𝑧,𝐴 𝑧,𝐵 𝑧,𝐷 𝑧,𝑁 𝑧,𝑅 𝑧,𝑉 𝑧,𝑋 𝑧,𝑌 𝑧, ·

**Proof of Theorem slesolex**
Step	Hyp	Ref	Expression
1		slesolex.a	. . . . 5 ⊢ 𝐴 = (𝑁 Mat 𝑅)
2		slesolex.x	. . . . 5 ⊢ · = (𝑅 maVecMul ⟨𝑁, 𝑁⟩)
3		eqid 2729	. . . . 5 ⊢ (Base‘𝑅) = (Base‘𝑅)
4		eqid 2729	. . . . 5 ⊢ (._r‘𝑅) = (._r‘𝑅)
5		crngring 20130	. . . . . . 7 ⊢ (𝑅 ∈ CRing → 𝑅 ∈ Ring)
6	5	adantl 481	. . . . . 6 ⊢ ((𝑁 ≠ ∅ ∧ 𝑅 ∈ CRing) → 𝑅 ∈ Ring)
7	6	3ad2ant1 1133	. . . . 5 ⊢ (((𝑁 ≠ ∅ ∧ 𝑅 ∈ CRing) ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝑉) ∧ (𝐷‘𝑋) ∈ (Unit‘𝑅)) → 𝑅 ∈ Ring)
8		slesolex.b	. . . . . . . . 9 ⊢ 𝐵 = (Base‘𝐴)
9	1, 8	matrcl 22297	. . . . . . . 8 ⊢ (𝑋 ∈ 𝐵 → (𝑁 ∈ Fin ∧ 𝑅 ∈ V))
10	9	simpld 494	. . . . . . 7 ⊢ (𝑋 ∈ 𝐵 → 𝑁 ∈ Fin)
11	10	adantr 480	. . . . . 6 ⊢ ((𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝑉) → 𝑁 ∈ Fin)
12	11	3ad2ant2 1134	. . . . 5 ⊢ (((𝑁 ≠ ∅ ∧ 𝑅 ∈ CRing) ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝑉) ∧ (𝐷‘𝑋) ∈ (Unit‘𝑅)) → 𝑁 ∈ Fin)
13	6, 11	anim12ci 614	. . . . . . . 8 ⊢ (((𝑁 ≠ ∅ ∧ 𝑅 ∈ CRing) ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝑉)) → (𝑁 ∈ Fin ∧ 𝑅 ∈ Ring))
14	13	3adant3 1132	. . . . . . 7 ⊢ (((𝑁 ≠ ∅ ∧ 𝑅 ∈ CRing) ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝑉) ∧ (𝐷‘𝑋) ∈ (Unit‘𝑅)) → (𝑁 ∈ Fin ∧ 𝑅 ∈ Ring))
15	1	matring 22328	. . . . . . 7 ⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) → 𝐴 ∈ Ring)
16	14, 15	syl 17	. . . . . 6 ⊢ (((𝑁 ≠ ∅ ∧ 𝑅 ∈ CRing) ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝑉) ∧ (𝐷‘𝑋) ∈ (Unit‘𝑅)) → 𝐴 ∈ Ring)
17		slesolex.d	. . . . . . . . . 10 ⊢ 𝐷 = (𝑁 maDet 𝑅)
18		eqid 2729	. . . . . . . . . 10 ⊢ (Unit‘𝐴) = (Unit‘𝐴)
19		eqid 2729	. . . . . . . . . 10 ⊢ (Unit‘𝑅) = (Unit‘𝑅)
20	1, 17, 8, 18, 19	matunit 22563	. . . . . . . . 9 ⊢ ((𝑅 ∈ CRing ∧ 𝑋 ∈ 𝐵) → (𝑋 ∈ (Unit‘𝐴) ↔ (𝐷‘𝑋) ∈ (Unit‘𝑅)))
21	20	bicomd 223	. . . . . . . 8 ⊢ ((𝑅 ∈ CRing ∧ 𝑋 ∈ 𝐵) → ((𝐷‘𝑋) ∈ (Unit‘𝑅) ↔ 𝑋 ∈ (Unit‘𝐴)))
22	21	ad2ant2lr 748	. . . . . . 7 ⊢ (((𝑁 ≠ ∅ ∧ 𝑅 ∈ CRing) ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝑉)) → ((𝐷‘𝑋) ∈ (Unit‘𝑅) ↔ 𝑋 ∈ (Unit‘𝐴)))
23	22	biimp3a 1471	. . . . . 6 ⊢ (((𝑁 ≠ ∅ ∧ 𝑅 ∈ CRing) ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝑉) ∧ (𝐷‘𝑋) ∈ (Unit‘𝑅)) → 𝑋 ∈ (Unit‘𝐴))
24		eqid 2729	. . . . . . 7 ⊢ (inv_r‘𝐴) = (inv_r‘𝐴)
25		eqid 2729	. . . . . . 7 ⊢ (Base‘𝐴) = (Base‘𝐴)
26	18, 24, 25	ringinvcl 20277	. . . . . 6 ⊢ ((𝐴 ∈ Ring ∧ 𝑋 ∈ (Unit‘𝐴)) → ((inv_r‘𝐴)‘𝑋) ∈ (Base‘𝐴))
27	16, 23, 26	syl2anc 584	. . . . 5 ⊢ (((𝑁 ≠ ∅ ∧ 𝑅 ∈ CRing) ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝑉) ∧ (𝐷‘𝑋) ∈ (Unit‘𝑅)) → ((inv_r‘𝐴)‘𝑋) ∈ (Base‘𝐴))
28		slesolex.v	. . . . . . . . 9 ⊢ 𝑉 = ((Base‘𝑅) ↑_m 𝑁)
29	28	eleq2i 2820	. . . . . . . 8 ⊢ (𝑌 ∈ 𝑉 ↔ 𝑌 ∈ ((Base‘𝑅) ↑_m 𝑁))
30	29	biimpi 216	. . . . . . 7 ⊢ (𝑌 ∈ 𝑉 → 𝑌 ∈ ((Base‘𝑅) ↑_m 𝑁))
31	30	adantl 481	. . . . . 6 ⊢ ((𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝑉) → 𝑌 ∈ ((Base‘𝑅) ↑_m 𝑁))
32	31	3ad2ant2 1134	. . . . 5 ⊢ (((𝑁 ≠ ∅ ∧ 𝑅 ∈ CRing) ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝑉) ∧ (𝐷‘𝑋) ∈ (Unit‘𝑅)) → 𝑌 ∈ ((Base‘𝑅) ↑_m 𝑁))
33	1, 2, 3, 4, 7, 12, 27, 32	mavmulcl 22432	. . . 4 ⊢ (((𝑁 ≠ ∅ ∧ 𝑅 ∈ CRing) ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝑉) ∧ (𝐷‘𝑋) ∈ (Unit‘𝑅)) → (((inv_r‘𝐴)‘𝑋) · 𝑌) ∈ ((Base‘𝑅) ↑_m 𝑁))
34	33, 28	eleqtrrdi 2839	. . 3 ⊢ (((𝑁 ≠ ∅ ∧ 𝑅 ∈ CRing) ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝑉) ∧ (𝐷‘𝑋) ∈ (Unit‘𝑅)) → (((inv_r‘𝐴)‘𝑋) · 𝑌) ∈ 𝑉)
35	1, 8, 28, 2, 17, 24	slesolinvbi 22566	. . . . . 6 ⊢ (((𝑁 ≠ ∅ ∧ 𝑅 ∈ CRing) ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝑉) ∧ (𝐷‘𝑋) ∈ (Unit‘𝑅)) → ((𝑋 · 𝑧) = 𝑌 ↔ 𝑧 = (((inv_r‘𝐴)‘𝑋) · 𝑌)))
36	35	adantr 480	. . . . 5 ⊢ ((((𝑁 ≠ ∅ ∧ 𝑅 ∈ CRing) ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝑉) ∧ (𝐷‘𝑋) ∈ (Unit‘𝑅)) ∧ ((𝑁 ≠ ∅ ∧ 𝑅 ∈ CRing) ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝑉) ∧ (𝐷‘𝑋) ∈ (Unit‘𝑅))) → ((𝑋 · 𝑧) = 𝑌 ↔ 𝑧 = (((inv_r‘𝐴)‘𝑋) · 𝑌)))
37	36	biimprd 248	. . . 4 ⊢ ((((𝑁 ≠ ∅ ∧ 𝑅 ∈ CRing) ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝑉) ∧ (𝐷‘𝑋) ∈ (Unit‘𝑅)) ∧ ((𝑁 ≠ ∅ ∧ 𝑅 ∈ CRing) ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝑉) ∧ (𝐷‘𝑋) ∈ (Unit‘𝑅))) → (𝑧 = (((inv_r‘𝐴)‘𝑋) · 𝑌) → (𝑋 · 𝑧) = 𝑌))
38	37	impancom 451	. . 3 ⊢ ((((𝑁 ≠ ∅ ∧ 𝑅 ∈ CRing) ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝑉) ∧ (𝐷‘𝑋) ∈ (Unit‘𝑅)) ∧ 𝑧 = (((inv_r‘𝐴)‘𝑋) · 𝑌)) → (((𝑁 ≠ ∅ ∧ 𝑅 ∈ CRing) ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝑉) ∧ (𝐷‘𝑋) ∈ (Unit‘𝑅)) → (𝑋 · 𝑧) = 𝑌))
39	34, 38	rspcimedv 3568	. 2 ⊢ (((𝑁 ≠ ∅ ∧ 𝑅 ∈ CRing) ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝑉) ∧ (𝐷‘𝑋) ∈ (Unit‘𝑅)) → (((𝑁 ≠ ∅ ∧ 𝑅 ∈ CRing) ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝑉) ∧ (𝐷‘𝑋) ∈ (Unit‘𝑅)) → ∃𝑧 ∈ 𝑉 (𝑋 · 𝑧) = 𝑌))
40	39	pm2.43i 52	1 ⊢ (((𝑁 ≠ ∅ ∧ 𝑅 ∈ CRing) ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝑉) ∧ (𝐷‘𝑋) ∈ (Unit‘𝑅)) → ∃𝑧 ∈ 𝑉 (𝑋 · 𝑧) = 𝑌)

Colors of variables: wff setvar class

Syntax hints: → wi 4 ↔ wb 206 ∧ wa 395 ∧ w3a 1086 = wceq 1540 ∈ wcel 2109 ≠ wne 2925 ∃wrex 3053 Vcvv 3436 ∅c0 4284 ⟨cop 4583 ‘cfv 6482 (class class class)co 7349 ↑_m cmap 8753 Fincfn 8872 Basecbs 17120 ._rcmulr 17162 Ringcrg 20118 CRingccrg 20119 Unitcui 20240 inv_rcinvr 20272 Mat cmat 22292 maVecMul cmvmul 22425 maDet cmdat 22469

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1795 ax-4 1809 ax-5 1910 ax-6 1967 ax-7 2008 ax-8 2111 ax-9 2119 ax-10 2142 ax-11 2158 ax-12 2178 ax-ext 2701 ax-rep 5218 ax-sep 5235 ax-nul 5245 ax-pow 5304 ax-pr 5371 ax-un 7671 ax-cnex 11065 ax-resscn 11066 ax-1cn 11067 ax-icn 11068 ax-addcl 11069 ax-addrcl 11070 ax-mulcl 11071 ax-mulrcl 11072 ax-mulcom 11073 ax-addass 11074 ax-mulass 11075 ax-distr 11076 ax-i2m1 11077 ax-1ne0 11078 ax-1rid 11079 ax-rnegex 11080 ax-rrecex 11081 ax-cnre 11082 ax-pre-lttri 11083 ax-pre-lttrn 11084 ax-pre-ltadd 11085 ax-pre-mulgt0 11086 ax-addf 11088 ax-mulf 11089

This theorem depends on definitions: df-bi 207 df-an 396 df-or 848 df-3or 1087 df-3an 1088 df-xor 1512 df-tru 1543 df-fal 1553 df-ex 1780 df-nf 1784 df-sb 2066 df-mo 2533 df-eu 2562 df-clab 2708 df-cleq 2721 df-clel 2803 df-nfc 2878 df-ne 2926 df-nel 3030 df-ral 3045 df-rex 3054 df-rmo 3343 df-reu 3344 df-rab 3395 df-v 3438 df-sbc 3743 df-csb 3852 df-dif 3906 df-un 3908 df-in 3910 df-ss 3920 df-pss 3923 df-nul 4285 df-if 4477 df-pw 4553 df-sn 4578 df-pr 4580 df-tp 4582 df-op 4584 df-ot 4586 df-uni 4859 df-int 4897 df-iun 4943 df-iin 4944 df-br 5093 df-opab 5155 df-mpt 5174 df-tr 5200 df-id 5514 df-eprel 5519 df-po 5527 df-so 5528 df-fr 5572 df-se 5573 df-we 5574 df-xp 5625 df-rel 5626 df-cnv 5627 df-co 5628 df-dm 5629 df-rn 5630 df-res 5631 df-ima 5632 df-pred 6249 df-ord 6310 df-on 6311 df-lim 6312 df-suc 6313 df-iota 6438 df-fun 6484 df-fn 6485 df-f 6486 df-f1 6487 df-fo 6488 df-f1o 6489 df-fv 6490 df-isom 6491 df-riota 7306 df-ov 7352 df-oprab 7353 df-mpo 7354 df-of 7613 df-om 7800 df-1st 7924 df-2nd 7925 df-supp 8094 df-tpos 8159 df-frecs 8214 df-wrecs 8245 df-recs 8294 df-rdg 8332 df-1o 8388 df-2o 8389 df-er 8625 df-map 8755 df-pm 8756 df-ixp 8825 df-en 8873 df-dom 8874 df-sdom 8875 df-fin 8876 df-fsupp 9252 df-sup 9332 df-oi 9402 df-card 9835 df-pnf 11151 df-mnf 11152 df-xr 11153 df-ltxr 11154 df-le 11155 df-sub 11349 df-neg 11350 df-div 11778 df-nn 12129 df-2 12191 df-3 12192 df-4 12193 df-5 12194 df-6 12195 df-7 12196 df-8 12197 df-9 12198 df-n0 12385 df-xnn0 12458 df-z 12472 df-dec 12592 df-uz 12736 df-rp 12894 df-fz 13411 df-fzo 13558 df-seq 13909 df-exp 13969 df-hash 14238 df-word 14421 df-lsw 14470 df-concat 14478 df-s1 14503 df-substr 14548 df-pfx 14578 df-splice 14656 df-reverse 14665 df-s2 14755 df-struct 17058 df-sets 17075 df-slot 17093 df-ndx 17105 df-base 17121 df-ress 17142 df-plusg 17174 df-mulr 17175 df-starv 17176 df-sca 17177 df-vsca 17178 df-ip 17179 df-tset 17180 df-ple 17181 df-ds 17183 df-unif 17184 df-hom 17185 df-cco 17186 df-0g 17345 df-gsum 17346 df-prds 17351 df-pws 17353 df-mre 17488 df-mrc 17489 df-acs 17491 df-mgm 18514 df-sgrp 18593 df-mnd 18609 df-mhm 18657 df-submnd 18658 df-efmnd 18743 df-grp 18815 df-minusg 18816 df-sbg 18817 df-mulg 18947 df-subg 19002 df-ghm 19092 df-gim 19138 df-cntz 19196 df-oppg 19225 df-symg 19249 df-pmtr 19321 df-psgn 19370 df-evpm 19371 df-cmn 19661 df-abl 19662 df-mgp 20026 df-rng 20038 df-ur 20067 df-srg 20072 df-ring 20120 df-cring 20121 df-oppr 20222 df-dvdsr 20242 df-unit 20243 df-invr 20273 df-dvr 20286 df-rhm 20357 df-subrng 20431 df-subrg 20455 df-drng 20616 df-lmod 20765 df-lss 20835 df-sra 21077 df-rgmod 21078 df-cnfld 21262 df-zring 21354 df-zrh 21410 df-dsmm 21639 df-frlm 21654 df-assa 21760 df-mamu 22276 df-mat 22293 df-mvmul 22426 df-mdet 22470 df-madu 22519

This theorem is referenced by: cramerlem3 22574

W3C validator