Metamath Proof Explorer

Theorem slesolinvbi

Description: The solution of a system of linear equations represented by a matrix with a unit as determinant is the multiplication of the inverse of the matrix with the right-hand side vector. (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 𝑅 )
slesolinv.i ⊢ 𝐼 = ( invr ‘ 𝐴 )
Assertion slesolinvbi ( ( ( 𝑁 ≠ ∅ ∧ 𝑅 ∈ 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 slesolinv.i ⊢ 𝐼 = ( invr ‘ 𝐴 )
7 simpl1 ⊢ ( ( ( ( 𝑁 ≠ ∅ ∧ 𝑅 ∈ CRing ) ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝑉 ) ∧ ( 𝐷 ‘ 𝑋 ) ∈ ( Unit ‘ 𝑅 ) ) ∧ ( 𝑋 · 𝑍 ) = 𝑌 ) → ( 𝑁 ≠ ∅ ∧ 𝑅 ∈ CRing ) )
8 simpl2 ⊢ ( ( ( ( 𝑁 ≠ ∅ ∧ 𝑅 ∈ CRing ) ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝑉 ) ∧ ( 𝐷 ‘ 𝑋 ) ∈ ( Unit ‘ 𝑅 ) ) ∧ ( 𝑋 · 𝑍 ) = 𝑌 ) → ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝑉 ) )
9 simp3 ⊢ ( ( ( 𝑁 ≠ ∅ ∧ 𝑅 ∈ CRing ) ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝑉 ) ∧ ( 𝐷 ‘ 𝑋 ) ∈ ( Unit ‘ 𝑅 ) ) → ( 𝐷 ‘ 𝑋 ) ∈ ( Unit ‘ 𝑅 ) )
10 9 anim1i ⊢ ( ( ( ( 𝑁 ≠ ∅ ∧ 𝑅 ∈ CRing ) ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝑉 ) ∧ ( 𝐷 ‘ 𝑋 ) ∈ ( Unit ‘ 𝑅 ) ) ∧ ( 𝑋 · 𝑍 ) = 𝑌 ) → ( ( 𝐷 ‘ 𝑋 ) ∈ ( Unit ‘ 𝑅 ) ∧ ( 𝑋 · 𝑍 ) = 𝑌 ) )
11 1 2 3 4 5 6 slesolinv ⊢ ( ( ( 𝑁 ≠ ∅ ∧ 𝑅 ∈ CRing ) ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝑉 ) ∧ ( ( 𝐷 ‘ 𝑋 ) ∈ ( Unit ‘ 𝑅 ) ∧ ( 𝑋 · 𝑍 ) = 𝑌 ) ) → 𝑍 = ( ( 𝐼 ‘ 𝑋 ) · 𝑌 ) )
12 7 8 10 11 syl3anc ⊢ ( ( ( ( 𝑁 ≠ ∅ ∧ 𝑅 ∈ CRing ) ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝑉 ) ∧ ( 𝐷 ‘ 𝑋 ) ∈ ( Unit ‘ 𝑅 ) ) ∧ ( 𝑋 · 𝑍 ) = 𝑌 ) → 𝑍 = ( ( 𝐼 ‘ 𝑋 ) · 𝑌 ) )
13 oveq2 ⊢ ( 𝑍 = ( ( 𝐼 ‘ 𝑋 ) · 𝑌 ) → ( 𝑋 · 𝑍 ) = ( 𝑋 · ( ( 𝐼 ‘ 𝑋 ) · 𝑌 ) ) )
14 simpr ⊢ ( ( 𝑁 ≠ ∅ ∧ 𝑅 ∈ CRing ) → 𝑅 ∈ CRing )
15 1 2 matrcl ⊢ ( 𝑋 ∈ 𝐵 → ( 𝑁 ∈ Fin ∧ 𝑅 ∈ V ) )
16 15 simpld ⊢ ( 𝑋 ∈ 𝐵 → 𝑁 ∈ Fin )
17 16 adantr ⊢ ( ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝑉 ) → 𝑁 ∈ Fin )
18 14 17 anim12ci ⊢ ( ( ( 𝑁 ≠ ∅ ∧ 𝑅 ∈ CRing ) ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝑉 ) ) → ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ) )
19 18 3adant3 ⊢ ( ( ( 𝑁 ≠ ∅ ∧ 𝑅 ∈ CRing ) ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝑉 ) ∧ ( 𝐷 ‘ 𝑋 ) ∈ ( Unit ‘ 𝑅 ) ) → ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ) )
20 eqid ⊢ ( 𝑅 maMul ⟨ 𝑁 , 𝑁 , 𝑁 ⟩ ) = ( 𝑅 maMul ⟨ 𝑁 , 𝑁 , 𝑁 ⟩ )
21 1 20 matmulr ⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ) → ( 𝑅 maMul ⟨ 𝑁 , 𝑁 , 𝑁 ⟩ ) = ( .r ‘ 𝐴 ) )
22 19 21 syl ⊢ ( ( ( 𝑁 ≠ ∅ ∧ 𝑅 ∈ CRing ) ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝑉 ) ∧ ( 𝐷 ‘ 𝑋 ) ∈ ( Unit ‘ 𝑅 ) ) → ( 𝑅 maMul ⟨ 𝑁 , 𝑁 , 𝑁 ⟩ ) = ( .r ‘ 𝐴 ) )
23 22 oveqd ⊢ ( ( ( 𝑁 ≠ ∅ ∧ 𝑅 ∈ CRing ) ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝑉 ) ∧ ( 𝐷 ‘ 𝑋 ) ∈ ( Unit ‘ 𝑅 ) ) → ( 𝑋 ( 𝑅 maMul ⟨ 𝑁 , 𝑁 , 𝑁 ⟩ ) ( 𝐼 ‘ 𝑋 ) ) = ( 𝑋 ( .r ‘ 𝐴 ) ( 𝐼 ‘ 𝑋 ) ) )
24 crngring ⊢ ( 𝑅 ∈ CRing → 𝑅 ∈ Ring )
25 24 adantl ⊢ ( ( 𝑁 ≠ ∅ ∧ 𝑅 ∈ CRing ) → 𝑅 ∈ Ring )
26 25 17 anim12ci ⊢ ( ( ( 𝑁 ≠ ∅ ∧ 𝑅 ∈ CRing ) ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝑉 ) ) → ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) )
27 26 3adant3 ⊢ ( ( ( 𝑁 ≠ ∅ ∧ 𝑅 ∈ CRing ) ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝑉 ) ∧ ( 𝐷 ‘ 𝑋 ) ∈ ( Unit ‘ 𝑅 ) ) → ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) )
28 1 matring ⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) → 𝐴 ∈ Ring )
29 27 28 syl ⊢ ( ( ( 𝑁 ≠ ∅ ∧ 𝑅 ∈ CRing ) ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝑉 ) ∧ ( 𝐷 ‘ 𝑋 ) ∈ ( Unit ‘ 𝑅 ) ) → 𝐴 ∈ Ring )
30 eqid ⊢ ( Unit ‘ 𝐴 ) = ( Unit ‘ 𝐴 )
31 eqid ⊢ ( Unit ‘ 𝑅 ) = ( Unit ‘ 𝑅 )
32 1 5 2 30 31 matunit ⊢ ( ( 𝑅 ∈ CRing ∧ 𝑋 ∈ 𝐵 ) → ( 𝑋 ∈ ( Unit ‘ 𝐴 ) ↔ ( 𝐷 ‘ 𝑋 ) ∈ ( Unit ‘ 𝑅 ) ) )
33 32 ad2ant2lr ⊢ ( ( ( 𝑁 ≠ ∅ ∧ 𝑅 ∈ CRing ) ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝑉 ) ) → ( 𝑋 ∈ ( Unit ‘ 𝐴 ) ↔ ( 𝐷 ‘ 𝑋 ) ∈ ( Unit ‘ 𝑅 ) ) )
34 33 biimp3ar ⊢ ( ( ( 𝑁 ≠ ∅ ∧ 𝑅 ∈ CRing ) ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝑉 ) ∧ ( 𝐷 ‘ 𝑋 ) ∈ ( Unit ‘ 𝑅 ) ) → 𝑋 ∈ ( Unit ‘ 𝐴 ) )
35 eqid ⊢ ( .r ‘ 𝐴 ) = ( .r ‘ 𝐴 )
36 eqid ⊢ ( 1r ‘ 𝐴 ) = ( 1r ‘ 𝐴 )
37 30 6 35 36 unitrinv ⊢ ( ( 𝐴 ∈ Ring ∧ 𝑋 ∈ ( Unit ‘ 𝐴 ) ) → ( 𝑋 ( .r ‘ 𝐴 ) ( 𝐼 ‘ 𝑋 ) ) = ( 1r ‘ 𝐴 ) )
38 29 34 37 syl2anc ⊢ ( ( ( 𝑁 ≠ ∅ ∧ 𝑅 ∈ CRing ) ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝑉 ) ∧ ( 𝐷 ‘ 𝑋 ) ∈ ( Unit ‘ 𝑅 ) ) → ( 𝑋 ( .r ‘ 𝐴 ) ( 𝐼 ‘ 𝑋 ) ) = ( 1r ‘ 𝐴 ) )
39 23 38 eqtrd ⊢ ( ( ( 𝑁 ≠ ∅ ∧ 𝑅 ∈ CRing ) ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝑉 ) ∧ ( 𝐷 ‘ 𝑋 ) ∈ ( Unit ‘ 𝑅 ) ) → ( 𝑋 ( 𝑅 maMul ⟨ 𝑁 , 𝑁 , 𝑁 ⟩ ) ( 𝐼 ‘ 𝑋 ) ) = ( 1r ‘ 𝐴 ) )
40 39 oveq1d ⊢ ( ( ( 𝑁 ≠ ∅ ∧ 𝑅 ∈ CRing ) ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝑉 ) ∧ ( 𝐷 ‘ 𝑋 ) ∈ ( Unit ‘ 𝑅 ) ) → ( ( 𝑋 ( 𝑅 maMul ⟨ 𝑁 , 𝑁 , 𝑁 ⟩ ) ( 𝐼 ‘ 𝑋 ) ) · 𝑌 ) = ( ( 1r ‘ 𝐴 ) · 𝑌 ) )
41 eqid ⊢ ( Base ‘ 𝑅 ) = ( Base ‘ 𝑅 )
42 25 3ad2ant1 ⊢ ( ( ( 𝑁 ≠ ∅ ∧ 𝑅 ∈ CRing ) ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝑉 ) ∧ ( 𝐷 ‘ 𝑋 ) ∈ ( Unit ‘ 𝑅 ) ) → 𝑅 ∈ Ring )
43 17 3ad2ant2 ⊢ ( ( ( 𝑁 ≠ ∅ ∧ 𝑅 ∈ CRing ) ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝑉 ) ∧ ( 𝐷 ‘ 𝑋 ) ∈ ( Unit ‘ 𝑅 ) ) → 𝑁 ∈ Fin )
44 3 eleq2i ⊢ ( 𝑌 ∈ 𝑉 ↔ 𝑌 ∈ ( ( Base ‘ 𝑅 ) ↑m 𝑁 ) )
45 44 biimpi ⊢ ( 𝑌 ∈ 𝑉 → 𝑌 ∈ ( ( Base ‘ 𝑅 ) ↑m 𝑁 ) )
46 45 adantl ⊢ ( ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝑉 ) → 𝑌 ∈ ( ( Base ‘ 𝑅 ) ↑m 𝑁 ) )
47 46 3ad2ant2 ⊢ ( ( ( 𝑁 ≠ ∅ ∧ 𝑅 ∈ CRing ) ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝑉 ) ∧ ( 𝐷 ‘ 𝑋 ) ∈ ( Unit ‘ 𝑅 ) ) → 𝑌 ∈ ( ( Base ‘ 𝑅 ) ↑m 𝑁 ) )
48 2 eleq2i ⊢ ( 𝑋 ∈ 𝐵 ↔ 𝑋 ∈ ( Base ‘ 𝐴 ) )
49 48 biimpi ⊢ ( 𝑋 ∈ 𝐵 → 𝑋 ∈ ( Base ‘ 𝐴 ) )
50 49 adantr ⊢ ( ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝑉 ) → 𝑋 ∈ ( Base ‘ 𝐴 ) )
51 50 3ad2ant2 ⊢ ( ( ( 𝑁 ≠ ∅ ∧ 𝑅 ∈ CRing ) ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝑉 ) ∧ ( 𝐷 ‘ 𝑋 ) ∈ ( Unit ‘ 𝑅 ) ) → 𝑋 ∈ ( Base ‘ 𝐴 ) )
52 eqid ⊢ ( Base ‘ 𝐴 ) = ( Base ‘ 𝐴 )
53 30 6 52 ringinvcl ⊢ ( ( 𝐴 ∈ Ring ∧ 𝑋 ∈ ( Unit ‘ 𝐴 ) ) → ( 𝐼 ‘ 𝑋 ) ∈ ( Base ‘ 𝐴 ) )
54 29 34 53 syl2anc ⊢ ( ( ( 𝑁 ≠ ∅ ∧ 𝑅 ∈ CRing ) ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝑉 ) ∧ ( 𝐷 ‘ 𝑋 ) ∈ ( Unit ‘ 𝑅 ) ) → ( 𝐼 ‘ 𝑋 ) ∈ ( Base ‘ 𝐴 ) )
55 1 41 4 42 43 47 20 51 54 mavmulass ⊢ ( ( ( 𝑁 ≠ ∅ ∧ 𝑅 ∈ CRing ) ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝑉 ) ∧ ( 𝐷 ‘ 𝑋 ) ∈ ( Unit ‘ 𝑅 ) ) → ( ( 𝑋 ( 𝑅 maMul ⟨ 𝑁 , 𝑁 , 𝑁 ⟩ ) ( 𝐼 ‘ 𝑋 ) ) · 𝑌 ) = ( 𝑋 · ( ( 𝐼 ‘ 𝑋 ) · 𝑌 ) ) )
56 1 41 4 42 43 47 1mavmul ⊢ ( ( ( 𝑁 ≠ ∅ ∧ 𝑅 ∈ CRing ) ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝑉 ) ∧ ( 𝐷 ‘ 𝑋 ) ∈ ( Unit ‘ 𝑅 ) ) → ( ( 1r ‘ 𝐴 ) · 𝑌 ) = 𝑌 )
57 40 55 56 3eqtr3d ⊢ ( ( ( 𝑁 ≠ ∅ ∧ 𝑅 ∈ CRing ) ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝑉 ) ∧ ( 𝐷 ‘ 𝑋 ) ∈ ( Unit ‘ 𝑅 ) ) → ( 𝑋 · ( ( 𝐼 ‘ 𝑋 ) · 𝑌 ) ) = 𝑌 )
58 13 57 sylan9eqr ⊢ ( ( ( ( 𝑁 ≠ ∅ ∧ 𝑅 ∈ CRing ) ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝑉 ) ∧ ( 𝐷 ‘ 𝑋 ) ∈ ( Unit ‘ 𝑅 ) ) ∧ 𝑍 = ( ( 𝐼 ‘ 𝑋 ) · 𝑌 ) ) → ( 𝑋 · 𝑍 ) = 𝑌 )
59 12 58 impbida ⊢ ( ( ( 𝑁 ≠ ∅ ∧ 𝑅 ∈ CRing ) ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝑉 ) ∧ ( 𝐷 ‘ 𝑋 ) ∈ ( Unit ‘ 𝑅 ) ) → ( ( 𝑋 · 𝑍 ) = 𝑌 ↔ 𝑍 = ( ( 𝐼 ‘ 𝑋 ) · 𝑌 ) ) )