Metamath Proof Explorer

Theorem cramerlem2

Description: Lemma 2 for cramer . (Contributed by AV, 21-Feb-2019) (Revised by AV, 1-Mar-2019)

Ref Expression
Hypotheses cramer.a โŠข ๐ด = ( ๐‘ Mat ๐‘… )
cramer.b โŠข ๐ต = ( Base โ€˜ ๐ด )
cramer.v โŠข ๐‘‰ = ( ( Base โ€˜ ๐‘… ) โ†‘m ๐‘ )
cramer.d โŠข ๐ท = ( ๐‘ maDet ๐‘… )
cramer.x โŠข ยท = ( ๐‘… maVecMul โŸจ ๐‘ , ๐‘ โŸฉ )
cramer.q โŠข / = ( /r โ€˜ ๐‘… )
Assertion cramerlem2 ( ( ๐‘… โˆˆ CRing โˆง ( ๐‘‹ โˆˆ ๐ต โˆง ๐‘Œ โˆˆ ๐‘‰ ) โˆง ( ๐ท โ€˜ ๐‘‹ ) โˆˆ ( Unit โ€˜ ๐‘… ) ) โ†’ โˆ€ ๐‘ง โˆˆ ๐‘‰ ( ( ๐‘‹ ยท ๐‘ง ) = ๐‘Œ โ†’ ๐‘ง = ( ๐‘– โˆˆ ๐‘ โ†ฆ ( ( ๐ท โ€˜ ( ( ๐‘‹ ( ๐‘ matRepV ๐‘… ) ๐‘Œ ) โ€˜ ๐‘– ) ) / ( ๐ท โ€˜ ๐‘‹ ) ) ) ) )

Proof

Step Hyp Ref Expression
1 cramer.a โŠข ๐ด = ( ๐‘ Mat ๐‘… )
2 cramer.b โŠข ๐ต = ( Base โ€˜ ๐ด )
3 cramer.v โŠข ๐‘‰ = ( ( Base โ€˜ ๐‘… ) โ†‘m ๐‘ )
4 cramer.d โŠข ๐ท = ( ๐‘ maDet ๐‘… )
5 cramer.x โŠข ยท = ( ๐‘… maVecMul โŸจ ๐‘ , ๐‘ โŸฉ )
6 cramer.q โŠข / = ( /r โ€˜ ๐‘… )
7 simpll1 โŠข ( ( ( ( ๐‘… โˆˆ CRing โˆง ( ๐‘‹ โˆˆ ๐ต โˆง ๐‘Œ โˆˆ ๐‘‰ ) โˆง ( ๐ท โ€˜ ๐‘‹ ) โˆˆ ( Unit โ€˜ ๐‘… ) ) โˆง ๐‘ง โˆˆ ๐‘‰ ) โˆง ( ๐‘‹ ยท ๐‘ง ) = ๐‘Œ ) โ†’ ๐‘… โˆˆ CRing )
8 simpll2 โŠข ( ( ( ( ๐‘… โˆˆ CRing โˆง ( ๐‘‹ โˆˆ ๐ต โˆง ๐‘Œ โˆˆ ๐‘‰ ) โˆง ( ๐ท โ€˜ ๐‘‹ ) โˆˆ ( Unit โ€˜ ๐‘… ) ) โˆง ๐‘ง โˆˆ ๐‘‰ ) โˆง ( ๐‘‹ ยท ๐‘ง ) = ๐‘Œ ) โ†’ ( ๐‘‹ โˆˆ ๐ต โˆง ๐‘Œ โˆˆ ๐‘‰ ) )
9 simpll3 โŠข ( ( ( ( ๐‘… โˆˆ CRing โˆง ( ๐‘‹ โˆˆ ๐ต โˆง ๐‘Œ โˆˆ ๐‘‰ ) โˆง ( ๐ท โ€˜ ๐‘‹ ) โˆˆ ( Unit โ€˜ ๐‘… ) ) โˆง ๐‘ง โˆˆ ๐‘‰ ) โˆง ( ๐‘‹ ยท ๐‘ง ) = ๐‘Œ ) โ†’ ( ๐ท โ€˜ ๐‘‹ ) โˆˆ ( Unit โ€˜ ๐‘… ) )
10 simplr โŠข ( ( ( ( ๐‘… โˆˆ CRing โˆง ( ๐‘‹ โˆˆ ๐ต โˆง ๐‘Œ โˆˆ ๐‘‰ ) โˆง ( ๐ท โ€˜ ๐‘‹ ) โˆˆ ( Unit โ€˜ ๐‘… ) ) โˆง ๐‘ง โˆˆ ๐‘‰ ) โˆง ( ๐‘‹ ยท ๐‘ง ) = ๐‘Œ ) โ†’ ๐‘ง โˆˆ ๐‘‰ )
11 simpr โŠข ( ( ( ( ๐‘… โˆˆ CRing โˆง ( ๐‘‹ โˆˆ ๐ต โˆง ๐‘Œ โˆˆ ๐‘‰ ) โˆง ( ๐ท โ€˜ ๐‘‹ ) โˆˆ ( Unit โ€˜ ๐‘… ) ) โˆง ๐‘ง โˆˆ ๐‘‰ ) โˆง ( ๐‘‹ ยท ๐‘ง ) = ๐‘Œ ) โ†’ ( ๐‘‹ ยท ๐‘ง ) = ๐‘Œ )
12 1 2 3 4 5 6 cramerlem1 โŠข ( ( ๐‘… โˆˆ CRing โˆง ( ๐‘‹ โˆˆ ๐ต โˆง ๐‘Œ โˆˆ ๐‘‰ ) โˆง ( ( ๐ท โ€˜ ๐‘‹ ) โˆˆ ( Unit โ€˜ ๐‘… ) โˆง ๐‘ง โˆˆ ๐‘‰ โˆง ( ๐‘‹ ยท ๐‘ง ) = ๐‘Œ ) ) โ†’ ๐‘ง = ( ๐‘– โˆˆ ๐‘ โ†ฆ ( ( ๐ท โ€˜ ( ( ๐‘‹ ( ๐‘ matRepV ๐‘… ) ๐‘Œ ) โ€˜ ๐‘– ) ) / ( ๐ท โ€˜ ๐‘‹ ) ) ) )
13 7 8 9 10 11 12 syl113anc โŠข ( ( ( ( ๐‘… โˆˆ CRing โˆง ( ๐‘‹ โˆˆ ๐ต โˆง ๐‘Œ โˆˆ ๐‘‰ ) โˆง ( ๐ท โ€˜ ๐‘‹ ) โˆˆ ( Unit โ€˜ ๐‘… ) ) โˆง ๐‘ง โˆˆ ๐‘‰ ) โˆง ( ๐‘‹ ยท ๐‘ง ) = ๐‘Œ ) โ†’ ๐‘ง = ( ๐‘– โˆˆ ๐‘ โ†ฆ ( ( ๐ท โ€˜ ( ( ๐‘‹ ( ๐‘ matRepV ๐‘… ) ๐‘Œ ) โ€˜ ๐‘– ) ) / ( ๐ท โ€˜ ๐‘‹ ) ) ) )
14 13 ex โŠข ( ( ( ๐‘… โˆˆ CRing โˆง ( ๐‘‹ โˆˆ ๐ต โˆง ๐‘Œ โˆˆ ๐‘‰ ) โˆง ( ๐ท โ€˜ ๐‘‹ ) โˆˆ ( Unit โ€˜ ๐‘… ) ) โˆง ๐‘ง โˆˆ ๐‘‰ ) โ†’ ( ( ๐‘‹ ยท ๐‘ง ) = ๐‘Œ โ†’ ๐‘ง = ( ๐‘– โˆˆ ๐‘ โ†ฆ ( ( ๐ท โ€˜ ( ( ๐‘‹ ( ๐‘ matRepV ๐‘… ) ๐‘Œ ) โ€˜ ๐‘– ) ) / ( ๐ท โ€˜ ๐‘‹ ) ) ) ) )
15 14 ralrimiva โŠข ( ( ๐‘… โˆˆ CRing โˆง ( ๐‘‹ โˆˆ ๐ต โˆง ๐‘Œ โˆˆ ๐‘‰ ) โˆง ( ๐ท โ€˜ ๐‘‹ ) โˆˆ ( Unit โ€˜ ๐‘… ) ) โ†’ โˆ€ ๐‘ง โˆˆ ๐‘‰ ( ( ๐‘‹ ยท ๐‘ง ) = ๐‘Œ โ†’ ๐‘ง = ( ๐‘– โˆˆ ๐‘ โ†ฆ ( ( ๐ท โ€˜ ( ( ๐‘‹ ( ๐‘ matRepV ๐‘… ) ๐‘Œ ) โ€˜ ๐‘– ) ) / ( ๐ท โ€˜ ๐‘‹ ) ) ) ) )