Theorem slesolex

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)

	Ref	Expression
Hypotheses	slesolex.a	⊢ 𝐴 = ( 𝑁 Mat 𝑅 )
	slesolex.b	⊢ 𝐵 = ( Base ‘ 𝐴 )
	slesolex.v	⊢ 𝑉 = ( ( Base ‘ 𝑅 ) ↑m 𝑁 )
	slesolex.x	⊢ · = ( 𝑅 maVecMul ⟨ 𝑁 , 𝑁 ⟩ )
	slesolex.d	⊢ 𝐷 = ( 𝑁 maDet 𝑅 )
Assertion	slesolex	⊢ ( ( ( 𝑁 ≠ ∅ ∧ 𝑅 ∈ CRing ) ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝑉 ) ∧ ( 𝐷 ‘ 𝑋 ) ∈ ( Unit ‘ 𝑅 ) ) → ∃ 𝑧 ∈ 𝑉 ( 𝑋 · 𝑧 ) = 𝑌 )

Proof

Step	Hyp	Ref	Expression
1		slesolex.a	⊢ 𝐴 = ( 𝑁 Mat 𝑅 )
2		slesolex.b	⊢ 𝐵 = ( Base ‘ 𝐴 )
3		slesolex.v	⊢ 𝑉 = ( ( Base ‘ 𝑅 ) ↑m 𝑁 )
4		slesolex.x	⊢ · = ( 𝑅 maVecMul ⟨ 𝑁 , 𝑁 ⟩ )
5		slesolex.d	⊢ 𝐷 = ( 𝑁 maDet 𝑅 )
6		eqid	⊢ ( Base ‘ 𝑅 ) = ( Base ‘ 𝑅 )
7		eqid	⊢ ( .r ‘ 𝑅 ) = ( .r ‘ 𝑅 )
8		crngring	⊢ ( 𝑅 ∈ CRing → 𝑅 ∈ Ring )
9	8	adantl	⊢ ( ( 𝑁 ≠ ∅ ∧ 𝑅 ∈ CRing ) → 𝑅 ∈ Ring )
10	9	3ad2ant1	⊢ ( ( ( 𝑁 ≠ ∅ ∧ 𝑅 ∈ CRing ) ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝑉 ) ∧ ( 𝐷 ‘ 𝑋 ) ∈ ( Unit ‘ 𝑅 ) ) → 𝑅 ∈ Ring )
11	1 2	matrcl	⊢ ( 𝑋 ∈ 𝐵 → ( 𝑁 ∈ Fin ∧ 𝑅 ∈ V ) )
12	11	simpld	⊢ ( 𝑋 ∈ 𝐵 → 𝑁 ∈ Fin )
13	12	adantr	⊢ ( ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝑉 ) → 𝑁 ∈ Fin )
14	13	3ad2ant2	⊢ ( ( ( 𝑁 ≠ ∅ ∧ 𝑅 ∈ CRing ) ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝑉 ) ∧ ( 𝐷 ‘ 𝑋 ) ∈ ( Unit ‘ 𝑅 ) ) → 𝑁 ∈ Fin )
15	9 13	anim12ci	⊢ ( ( ( 𝑁 ≠ ∅ ∧ 𝑅 ∈ CRing ) ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝑉 ) ) → ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) )
16	15	3adant3	⊢ ( ( ( 𝑁 ≠ ∅ ∧ 𝑅 ∈ CRing ) ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝑉 ) ∧ ( 𝐷 ‘ 𝑋 ) ∈ ( Unit ‘ 𝑅 ) ) → ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) )
17	1	matring	⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) → 𝐴 ∈ Ring )
18	16 17	syl	⊢ ( ( ( 𝑁 ≠ ∅ ∧ 𝑅 ∈ CRing ) ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝑉 ) ∧ ( 𝐷 ‘ 𝑋 ) ∈ ( Unit ‘ 𝑅 ) ) → 𝐴 ∈ Ring )
19		eqid	⊢ ( Unit ‘ 𝐴 ) = ( Unit ‘ 𝐴 )
20		eqid	⊢ ( Unit ‘ 𝑅 ) = ( Unit ‘ 𝑅 )
21	1 5 2 19 20	matunit	⊢ ( ( 𝑅 ∈ CRing ∧ 𝑋 ∈ 𝐵 ) → ( 𝑋 ∈ ( Unit ‘ 𝐴 ) ↔ ( 𝐷 ‘ 𝑋 ) ∈ ( Unit ‘ 𝑅 ) ) )
22	21	bicomd	⊢ ( ( 𝑅 ∈ CRing ∧ 𝑋 ∈ 𝐵 ) → ( ( 𝐷 ‘ 𝑋 ) ∈ ( Unit ‘ 𝑅 ) ↔ 𝑋 ∈ ( Unit ‘ 𝐴 ) ) )
23	22	ad2ant2lr	⊢ ( ( ( 𝑁 ≠ ∅ ∧ 𝑅 ∈ CRing ) ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝑉 ) ) → ( ( 𝐷 ‘ 𝑋 ) ∈ ( Unit ‘ 𝑅 ) ↔ 𝑋 ∈ ( Unit ‘ 𝐴 ) ) )
24	23	biimp3a	⊢ ( ( ( 𝑁 ≠ ∅ ∧ 𝑅 ∈ CRing ) ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝑉 ) ∧ ( 𝐷 ‘ 𝑋 ) ∈ ( Unit ‘ 𝑅 ) ) → 𝑋 ∈ ( Unit ‘ 𝐴 ) )
25		eqid	⊢ ( invr ‘ 𝐴 ) = ( invr ‘ 𝐴 )
26		eqid	⊢ ( Base ‘ 𝐴 ) = ( Base ‘ 𝐴 )
27	19 25 26	ringinvcl	⊢ ( ( 𝐴 ∈ Ring ∧ 𝑋 ∈ ( Unit ‘ 𝐴 ) ) → ( ( invr ‘ 𝐴 ) ‘ 𝑋 ) ∈ ( Base ‘ 𝐴 ) )
28	18 24 27	syl2anc	⊢ ( ( ( 𝑁 ≠ ∅ ∧ 𝑅 ∈ CRing ) ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝑉 ) ∧ ( 𝐷 ‘ 𝑋 ) ∈ ( Unit ‘ 𝑅 ) ) → ( ( invr ‘ 𝐴 ) ‘ 𝑋 ) ∈ ( Base ‘ 𝐴 ) )
29	3	eleq2i	⊢ ( 𝑌 ∈ 𝑉 ↔ 𝑌 ∈ ( ( Base ‘ 𝑅 ) ↑m 𝑁 ) )
30	29	bilani	⊢ ( ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝑉 ) → 𝑌 ∈ ( ( Base ‘ 𝑅 ) ↑m 𝑁 ) )
31	30	3ad2ant2	⊢ ( ( ( 𝑁 ≠ ∅ ∧ 𝑅 ∈ CRing ) ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝑉 ) ∧ ( 𝐷 ‘ 𝑋 ) ∈ ( Unit ‘ 𝑅 ) ) → 𝑌 ∈ ( ( Base ‘ 𝑅 ) ↑m 𝑁 ) )
32	1 4 6 7 10 14 28 31	mavmulcl	⊢ ( ( ( 𝑁 ≠ ∅ ∧ 𝑅 ∈ CRing ) ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝑉 ) ∧ ( 𝐷 ‘ 𝑋 ) ∈ ( Unit ‘ 𝑅 ) ) → ( ( ( invr ‘ 𝐴 ) ‘ 𝑋 ) · 𝑌 ) ∈ ( ( Base ‘ 𝑅 ) ↑m 𝑁 ) )
33	32 3	eleqtrrdi	⊢ ( ( ( 𝑁 ≠ ∅ ∧ 𝑅 ∈ CRing ) ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝑉 ) ∧ ( 𝐷 ‘ 𝑋 ) ∈ ( Unit ‘ 𝑅 ) ) → ( ( ( invr ‘ 𝐴 ) ‘ 𝑋 ) · 𝑌 ) ∈ 𝑉 )
34	1 2 3 4 5 25	slesolinvbi	⊢ ( ( ( 𝑁 ≠ ∅ ∧ 𝑅 ∈ CRing ) ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝑉 ) ∧ ( 𝐷 ‘ 𝑋 ) ∈ ( Unit ‘ 𝑅 ) ) → ( ( 𝑋 · 𝑧 ) = 𝑌 ↔ 𝑧 = ( ( ( invr ‘ 𝐴 ) ‘ 𝑋 ) · 𝑌 ) ) )
35	34	adantr	⊢ ( ( ( ( 𝑁 ≠ ∅ ∧ 𝑅 ∈ CRing ) ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝑉 ) ∧ ( 𝐷 ‘ 𝑋 ) ∈ ( Unit ‘ 𝑅 ) ) ∧ ( ( 𝑁 ≠ ∅ ∧ 𝑅 ∈ CRing ) ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝑉 ) ∧ ( 𝐷 ‘ 𝑋 ) ∈ ( Unit ‘ 𝑅 ) ) ) → ( ( 𝑋 · 𝑧 ) = 𝑌 ↔ 𝑧 = ( ( ( invr ‘ 𝐴 ) ‘ 𝑋 ) · 𝑌 ) ) )
36	35	biimprd	⊢ ( ( ( ( 𝑁 ≠ ∅ ∧ 𝑅 ∈ CRing ) ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝑉 ) ∧ ( 𝐷 ‘ 𝑋 ) ∈ ( Unit ‘ 𝑅 ) ) ∧ ( ( 𝑁 ≠ ∅ ∧ 𝑅 ∈ CRing ) ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝑉 ) ∧ ( 𝐷 ‘ 𝑋 ) ∈ ( Unit ‘ 𝑅 ) ) ) → ( 𝑧 = ( ( ( invr ‘ 𝐴 ) ‘ 𝑋 ) · 𝑌 ) → ( 𝑋 · 𝑧 ) = 𝑌 ) )
37	36	impancom	⊢ ( ( ( ( 𝑁 ≠ ∅ ∧ 𝑅 ∈ CRing ) ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝑉 ) ∧ ( 𝐷 ‘ 𝑋 ) ∈ ( Unit ‘ 𝑅 ) ) ∧ 𝑧 = ( ( ( invr ‘ 𝐴 ) ‘ 𝑋 ) · 𝑌 ) ) → ( ( ( 𝑁 ≠ ∅ ∧ 𝑅 ∈ CRing ) ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝑉 ) ∧ ( 𝐷 ‘ 𝑋 ) ∈ ( Unit ‘ 𝑅 ) ) → ( 𝑋 · 𝑧 ) = 𝑌 ) )
38	33 37	rspcimedv	⊢ ( ( ( 𝑁 ≠ ∅ ∧ 𝑅 ∈ CRing ) ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝑉 ) ∧ ( 𝐷 ‘ 𝑋 ) ∈ ( Unit ‘ 𝑅 ) ) → ( ( ( 𝑁 ≠ ∅ ∧ 𝑅 ∈ CRing ) ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝑉 ) ∧ ( 𝐷 ‘ 𝑋 ) ∈ ( Unit ‘ 𝑅 ) ) → ∃ 𝑧 ∈ 𝑉 ( 𝑋 · 𝑧 ) = 𝑌 ) )
39	38	pm2.43i	⊢ ( ( ( 𝑁 ≠ ∅ ∧ 𝑅 ∈ CRing ) ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝑉 ) ∧ ( 𝐷 ‘ 𝑋 ) ∈ ( Unit ‘ 𝑅 ) ) → ∃ 𝑧 ∈ 𝑉 ( 𝑋 · 𝑧 ) = 𝑌 )