Metamath Proof Explorer

Theorem cramerlem3

Description: Lemma 3 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 cramerlem3 ( ( ( ๐‘ โ‰  โˆ… โˆง ๐‘… โˆˆ 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 1 2 3 5 4 slesolex โŠข ( ( ( ๐‘ โ‰  โˆ… โˆง ๐‘… โˆˆ CRing ) โˆง ( ๐‘‹ โˆˆ ๐ต โˆง ๐‘Œ โˆˆ ๐‘‰ ) โˆง ( ๐ท โ€˜ ๐‘‹ ) โˆˆ ( Unit โ€˜ ๐‘… ) ) โ†’ โˆƒ ๐‘ฃ โˆˆ ๐‘‰ ( ๐‘‹ ยท ๐‘ฃ ) = ๐‘Œ )
8 1 2 3 4 5 6 cramerlem2 โŠข ( ( ๐‘… โˆˆ CRing โˆง ( ๐‘‹ โˆˆ ๐ต โˆง ๐‘Œ โˆˆ ๐‘‰ ) โˆง ( ๐ท โ€˜ ๐‘‹ ) โˆˆ ( Unit โ€˜ ๐‘… ) ) โ†’ โˆ€ ๐‘ง โˆˆ ๐‘‰ ( ( ๐‘‹ ยท ๐‘ง ) = ๐‘Œ โ†’ ๐‘ง = ( ๐‘– โˆˆ ๐‘ โ†ฆ ( ( ๐ท โ€˜ ( ( ๐‘‹ ( ๐‘ matRepV ๐‘… ) ๐‘Œ ) โ€˜ ๐‘– ) ) / ( ๐ท โ€˜ ๐‘‹ ) ) ) ) )
9 8 3adant1l โŠข ( ( ( ๐‘ โ‰  โˆ… โˆง ๐‘… โˆˆ CRing ) โˆง ( ๐‘‹ โˆˆ ๐ต โˆง ๐‘Œ โˆˆ ๐‘‰ ) โˆง ( ๐ท โ€˜ ๐‘‹ ) โˆˆ ( Unit โ€˜ ๐‘… ) ) โ†’ โˆ€ ๐‘ง โˆˆ ๐‘‰ ( ( ๐‘‹ ยท ๐‘ง ) = ๐‘Œ โ†’ ๐‘ง = ( ๐‘– โˆˆ ๐‘ โ†ฆ ( ( ๐ท โ€˜ ( ( ๐‘‹ ( ๐‘ matRepV ๐‘… ) ๐‘Œ ) โ€˜ ๐‘– ) ) / ( ๐ท โ€˜ ๐‘‹ ) ) ) ) )
10 oveq2 โŠข ( ๐‘ง = ๐‘ฃ โ†’ ( ๐‘‹ ยท ๐‘ง ) = ( ๐‘‹ ยท ๐‘ฃ ) )
11 10 eqeq1d โŠข ( ๐‘ง = ๐‘ฃ โ†’ ( ( ๐‘‹ ยท ๐‘ง ) = ๐‘Œ โ†” ( ๐‘‹ ยท ๐‘ฃ ) = ๐‘Œ ) )
12 oveq2 โŠข ( ๐‘ฃ = ( ๐‘– โˆˆ ๐‘ โ†ฆ ( ( ๐ท โ€˜ ( ( ๐‘‹ ( ๐‘ matRepV ๐‘… ) ๐‘Œ ) โ€˜ ๐‘– ) ) / ( ๐ท โ€˜ ๐‘‹ ) ) ) โ†’ ( ๐‘‹ ยท ๐‘ฃ ) = ( ๐‘‹ ยท ( ๐‘– โˆˆ ๐‘ โ†ฆ ( ( ๐ท โ€˜ ( ( ๐‘‹ ( ๐‘ matRepV ๐‘… ) ๐‘Œ ) โ€˜ ๐‘– ) ) / ( ๐ท โ€˜ ๐‘‹ ) ) ) ) )
13 12 eqeq1d โŠข ( ๐‘ฃ = ( ๐‘– โˆˆ ๐‘ โ†ฆ ( ( ๐ท โ€˜ ( ( ๐‘‹ ( ๐‘ matRepV ๐‘… ) ๐‘Œ ) โ€˜ ๐‘– ) ) / ( ๐ท โ€˜ ๐‘‹ ) ) ) โ†’ ( ( ๐‘‹ ยท ๐‘ฃ ) = ๐‘Œ โ†” ( ๐‘‹ ยท ( ๐‘– โˆˆ ๐‘ โ†ฆ ( ( ๐ท โ€˜ ( ( ๐‘‹ ( ๐‘ matRepV ๐‘… ) ๐‘Œ ) โ€˜ ๐‘– ) ) / ( ๐ท โ€˜ ๐‘‹ ) ) ) ) = ๐‘Œ ) )
14 11 13 rexraleqim โŠข ( ( โˆƒ ๐‘ฃ โˆˆ ๐‘‰ ( ๐‘‹ ยท ๐‘ฃ ) = ๐‘Œ โˆง โˆ€ ๐‘ง โˆˆ ๐‘‰ ( ( ๐‘‹ ยท ๐‘ง ) = ๐‘Œ โ†’ ๐‘ง = ( ๐‘– โˆˆ ๐‘ โ†ฆ ( ( ๐ท โ€˜ ( ( ๐‘‹ ( ๐‘ matRepV ๐‘… ) ๐‘Œ ) โ€˜ ๐‘– ) ) / ( ๐ท โ€˜ ๐‘‹ ) ) ) ) ) โ†’ ( ๐‘‹ ยท ( ๐‘– โˆˆ ๐‘ โ†ฆ ( ( ๐ท โ€˜ ( ( ๐‘‹ ( ๐‘ matRepV ๐‘… ) ๐‘Œ ) โ€˜ ๐‘– ) ) / ( ๐ท โ€˜ ๐‘‹ ) ) ) ) = ๐‘Œ )
15 oveq2 โŠข ( ๐‘ = ( ๐‘– โˆˆ ๐‘ โ†ฆ ( ( ๐ท โ€˜ ( ( ๐‘‹ ( ๐‘ matRepV ๐‘… ) ๐‘Œ ) โ€˜ ๐‘– ) ) / ( ๐ท โ€˜ ๐‘‹ ) ) ) โ†’ ( ๐‘‹ ยท ๐‘ ) = ( ๐‘‹ ยท ( ๐‘– โˆˆ ๐‘ โ†ฆ ( ( ๐ท โ€˜ ( ( ๐‘‹ ( ๐‘ matRepV ๐‘… ) ๐‘Œ ) โ€˜ ๐‘– ) ) / ( ๐ท โ€˜ ๐‘‹ ) ) ) ) )
16 15 adantl โŠข ( ( ( ๐‘‹ ยท ( ๐‘– โˆˆ ๐‘ โ†ฆ ( ( ๐ท โ€˜ ( ( ๐‘‹ ( ๐‘ matRepV ๐‘… ) ๐‘Œ ) โ€˜ ๐‘– ) ) / ( ๐ท โ€˜ ๐‘‹ ) ) ) ) = ๐‘Œ โˆง ๐‘ = ( ๐‘– โˆˆ ๐‘ โ†ฆ ( ( ๐ท โ€˜ ( ( ๐‘‹ ( ๐‘ matRepV ๐‘… ) ๐‘Œ ) โ€˜ ๐‘– ) ) / ( ๐ท โ€˜ ๐‘‹ ) ) ) ) โ†’ ( ๐‘‹ ยท ๐‘ ) = ( ๐‘‹ ยท ( ๐‘– โˆˆ ๐‘ โ†ฆ ( ( ๐ท โ€˜ ( ( ๐‘‹ ( ๐‘ matRepV ๐‘… ) ๐‘Œ ) โ€˜ ๐‘– ) ) / ( ๐ท โ€˜ ๐‘‹ ) ) ) ) )
17 simpl โŠข ( ( ( ๐‘‹ ยท ( ๐‘– โˆˆ ๐‘ โ†ฆ ( ( ๐ท โ€˜ ( ( ๐‘‹ ( ๐‘ matRepV ๐‘… ) ๐‘Œ ) โ€˜ ๐‘– ) ) / ( ๐ท โ€˜ ๐‘‹ ) ) ) ) = ๐‘Œ โˆง ๐‘ = ( ๐‘– โˆˆ ๐‘ โ†ฆ ( ( ๐ท โ€˜ ( ( ๐‘‹ ( ๐‘ matRepV ๐‘… ) ๐‘Œ ) โ€˜ ๐‘– ) ) / ( ๐ท โ€˜ ๐‘‹ ) ) ) ) โ†’ ( ๐‘‹ ยท ( ๐‘– โˆˆ ๐‘ โ†ฆ ( ( ๐ท โ€˜ ( ( ๐‘‹ ( ๐‘ matRepV ๐‘… ) ๐‘Œ ) โ€˜ ๐‘– ) ) / ( ๐ท โ€˜ ๐‘‹ ) ) ) ) = ๐‘Œ )
18 16 17 eqtrd โŠข ( ( ( ๐‘‹ ยท ( ๐‘– โˆˆ ๐‘ โ†ฆ ( ( ๐ท โ€˜ ( ( ๐‘‹ ( ๐‘ matRepV ๐‘… ) ๐‘Œ ) โ€˜ ๐‘– ) ) / ( ๐ท โ€˜ ๐‘‹ ) ) ) ) = ๐‘Œ โˆง ๐‘ = ( ๐‘– โˆˆ ๐‘ โ†ฆ ( ( ๐ท โ€˜ ( ( ๐‘‹ ( ๐‘ matRepV ๐‘… ) ๐‘Œ ) โ€˜ ๐‘– ) ) / ( ๐ท โ€˜ ๐‘‹ ) ) ) ) โ†’ ( ๐‘‹ ยท ๐‘ ) = ๐‘Œ )
19 18 ex โŠข ( ( ๐‘‹ ยท ( ๐‘– โˆˆ ๐‘ โ†ฆ ( ( ๐ท โ€˜ ( ( ๐‘‹ ( ๐‘ matRepV ๐‘… ) ๐‘Œ ) โ€˜ ๐‘– ) ) / ( ๐ท โ€˜ ๐‘‹ ) ) ) ) = ๐‘Œ โ†’ ( ๐‘ = ( ๐‘– โˆˆ ๐‘ โ†ฆ ( ( ๐ท โ€˜ ( ( ๐‘‹ ( ๐‘ matRepV ๐‘… ) ๐‘Œ ) โ€˜ ๐‘– ) ) / ( ๐ท โ€˜ ๐‘‹ ) ) ) โ†’ ( ๐‘‹ ยท ๐‘ ) = ๐‘Œ ) )
20 19 a1d โŠข ( ( ๐‘‹ ยท ( ๐‘– โˆˆ ๐‘ โ†ฆ ( ( ๐ท โ€˜ ( ( ๐‘‹ ( ๐‘ matRepV ๐‘… ) ๐‘Œ ) โ€˜ ๐‘– ) ) / ( ๐ท โ€˜ ๐‘‹ ) ) ) ) = ๐‘Œ โ†’ ( ( ( ๐‘ โ‰  โˆ… โˆง ๐‘… โˆˆ CRing ) โˆง ( ๐‘‹ โˆˆ ๐ต โˆง ๐‘Œ โˆˆ ๐‘‰ ) โˆง ( ๐ท โ€˜ ๐‘‹ ) โˆˆ ( Unit โ€˜ ๐‘… ) ) โ†’ ( ๐‘ = ( ๐‘– โˆˆ ๐‘ โ†ฆ ( ( ๐ท โ€˜ ( ( ๐‘‹ ( ๐‘ matRepV ๐‘… ) ๐‘Œ ) โ€˜ ๐‘– ) ) / ( ๐ท โ€˜ ๐‘‹ ) ) ) โ†’ ( ๐‘‹ ยท ๐‘ ) = ๐‘Œ ) ) )
21 14 20 syl โŠข ( ( โˆƒ ๐‘ฃ โˆˆ ๐‘‰ ( ๐‘‹ ยท ๐‘ฃ ) = ๐‘Œ โˆง โˆ€ ๐‘ง โˆˆ ๐‘‰ ( ( ๐‘‹ ยท ๐‘ง ) = ๐‘Œ โ†’ ๐‘ง = ( ๐‘– โˆˆ ๐‘ โ†ฆ ( ( ๐ท โ€˜ ( ( ๐‘‹ ( ๐‘ matRepV ๐‘… ) ๐‘Œ ) โ€˜ ๐‘– ) ) / ( ๐ท โ€˜ ๐‘‹ ) ) ) ) ) โ†’ ( ( ( ๐‘ โ‰  โˆ… โˆง ๐‘… โˆˆ CRing ) โˆง ( ๐‘‹ โˆˆ ๐ต โˆง ๐‘Œ โˆˆ ๐‘‰ ) โˆง ( ๐ท โ€˜ ๐‘‹ ) โˆˆ ( Unit โ€˜ ๐‘… ) ) โ†’ ( ๐‘ = ( ๐‘– โˆˆ ๐‘ โ†ฆ ( ( ๐ท โ€˜ ( ( ๐‘‹ ( ๐‘ matRepV ๐‘… ) ๐‘Œ ) โ€˜ ๐‘– ) ) / ( ๐ท โ€˜ ๐‘‹ ) ) ) โ†’ ( ๐‘‹ ยท ๐‘ ) = ๐‘Œ ) ) )
22 21 expcom โŠข ( โˆ€ ๐‘ง โˆˆ ๐‘‰ ( ( ๐‘‹ ยท ๐‘ง ) = ๐‘Œ โ†’ ๐‘ง = ( ๐‘– โˆˆ ๐‘ โ†ฆ ( ( ๐ท โ€˜ ( ( ๐‘‹ ( ๐‘ matRepV ๐‘… ) ๐‘Œ ) โ€˜ ๐‘– ) ) / ( ๐ท โ€˜ ๐‘‹ ) ) ) ) โ†’ ( โˆƒ ๐‘ฃ โˆˆ ๐‘‰ ( ๐‘‹ ยท ๐‘ฃ ) = ๐‘Œ โ†’ ( ( ( ๐‘ โ‰  โˆ… โˆง ๐‘… โˆˆ CRing ) โˆง ( ๐‘‹ โˆˆ ๐ต โˆง ๐‘Œ โˆˆ ๐‘‰ ) โˆง ( ๐ท โ€˜ ๐‘‹ ) โˆˆ ( Unit โ€˜ ๐‘… ) ) โ†’ ( ๐‘ = ( ๐‘– โˆˆ ๐‘ โ†ฆ ( ( ๐ท โ€˜ ( ( ๐‘‹ ( ๐‘ matRepV ๐‘… ) ๐‘Œ ) โ€˜ ๐‘– ) ) / ( ๐ท โ€˜ ๐‘‹ ) ) ) โ†’ ( ๐‘‹ ยท ๐‘ ) = ๐‘Œ ) ) ) )
23 22 com23 โŠข ( โˆ€ ๐‘ง โˆˆ ๐‘‰ ( ( ๐‘‹ ยท ๐‘ง ) = ๐‘Œ โ†’ ๐‘ง = ( ๐‘– โˆˆ ๐‘ โ†ฆ ( ( ๐ท โ€˜ ( ( ๐‘‹ ( ๐‘ matRepV ๐‘… ) ๐‘Œ ) โ€˜ ๐‘– ) ) / ( ๐ท โ€˜ ๐‘‹ ) ) ) ) โ†’ ( ( ( ๐‘ โ‰  โˆ… โˆง ๐‘… โˆˆ CRing ) โˆง ( ๐‘‹ โˆˆ ๐ต โˆง ๐‘Œ โˆˆ ๐‘‰ ) โˆง ( ๐ท โ€˜ ๐‘‹ ) โˆˆ ( Unit โ€˜ ๐‘… ) ) โ†’ ( โˆƒ ๐‘ฃ โˆˆ ๐‘‰ ( ๐‘‹ ยท ๐‘ฃ ) = ๐‘Œ โ†’ ( ๐‘ = ( ๐‘– โˆˆ ๐‘ โ†ฆ ( ( ๐ท โ€˜ ( ( ๐‘‹ ( ๐‘ matRepV ๐‘… ) ๐‘Œ ) โ€˜ ๐‘– ) ) / ( ๐ท โ€˜ ๐‘‹ ) ) ) โ†’ ( ๐‘‹ ยท ๐‘ ) = ๐‘Œ ) ) ) )
24 9 23 mpcom โŠข ( ( ( ๐‘ โ‰  โˆ… โˆง ๐‘… โˆˆ CRing ) โˆง ( ๐‘‹ โˆˆ ๐ต โˆง ๐‘Œ โˆˆ ๐‘‰ ) โˆง ( ๐ท โ€˜ ๐‘‹ ) โˆˆ ( Unit โ€˜ ๐‘… ) ) โ†’ ( โˆƒ ๐‘ฃ โˆˆ ๐‘‰ ( ๐‘‹ ยท ๐‘ฃ ) = ๐‘Œ โ†’ ( ๐‘ = ( ๐‘– โˆˆ ๐‘ โ†ฆ ( ( ๐ท โ€˜ ( ( ๐‘‹ ( ๐‘ matRepV ๐‘… ) ๐‘Œ ) โ€˜ ๐‘– ) ) / ( ๐ท โ€˜ ๐‘‹ ) ) ) โ†’ ( ๐‘‹ ยท ๐‘ ) = ๐‘Œ ) ) )
25 7 24 mpd โŠข ( ( ( ๐‘ โ‰  โˆ… โˆง ๐‘… โˆˆ CRing ) โˆง ( ๐‘‹ โˆˆ ๐ต โˆง ๐‘Œ โˆˆ ๐‘‰ ) โˆง ( ๐ท โ€˜ ๐‘‹ ) โˆˆ ( Unit โ€˜ ๐‘… ) ) โ†’ ( ๐‘ = ( ๐‘– โˆˆ ๐‘ โ†ฆ ( ( ๐ท โ€˜ ( ( ๐‘‹ ( ๐‘ matRepV ๐‘… ) ๐‘Œ ) โ€˜ ๐‘– ) ) / ( ๐ท โ€˜ ๐‘‹ ) ) ) โ†’ ( ๐‘‹ ยท ๐‘ ) = ๐‘Œ ) )