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 โ€˜ ๐‘… ) ) โ†’ ( ( ๐‘‹ ยท ๐‘ ) = ๐‘Œ โ†” ๐‘ = ( ( ๐ผ โ€˜ ๐‘‹ ) ยท ๐‘Œ ) ) )