Metamath Proof Explorer


Theorem invrvald

Description: If a matrix multiplied with a given matrix (from the left as well as from the right) results in the identity matrix, this matrix is the inverse (matrix) of the given matrix. (Contributed by Stefan O'Rear, 17-Jul-2018)

Ref Expression
Hypotheses invrvald.b โŠข ๐ต = ( Base โ€˜ ๐‘… )
invrvald.t โŠข ยท = ( .r โ€˜ ๐‘… )
invrvald.o โŠข 1 = ( 1r โ€˜ ๐‘… )
invrvald.u โŠข ๐‘ˆ = ( Unit โ€˜ ๐‘… )
invrvald.i โŠข ๐ผ = ( invr โ€˜ ๐‘… )
invrvald.r โŠข ( ๐œ‘ โ†’ ๐‘… โˆˆ Ring )
invrvald.x โŠข ( ๐œ‘ โ†’ ๐‘‹ โˆˆ ๐ต )
invrvald.y โŠข ( ๐œ‘ โ†’ ๐‘Œ โˆˆ ๐ต )
invrvald.xy โŠข ( ๐œ‘ โ†’ ( ๐‘‹ ยท ๐‘Œ ) = 1 )
invrvald.yx โŠข ( ๐œ‘ โ†’ ( ๐‘Œ ยท ๐‘‹ ) = 1 )
Assertion invrvald ( ๐œ‘ โ†’ ( ๐‘‹ โˆˆ ๐‘ˆ โˆง ( ๐ผ โ€˜ ๐‘‹ ) = ๐‘Œ ) )

Proof

Step Hyp Ref Expression
1 invrvald.b โŠข ๐ต = ( Base โ€˜ ๐‘… )
2 invrvald.t โŠข ยท = ( .r โ€˜ ๐‘… )
3 invrvald.o โŠข 1 = ( 1r โ€˜ ๐‘… )
4 invrvald.u โŠข ๐‘ˆ = ( Unit โ€˜ ๐‘… )
5 invrvald.i โŠข ๐ผ = ( invr โ€˜ ๐‘… )
6 invrvald.r โŠข ( ๐œ‘ โ†’ ๐‘… โˆˆ Ring )
7 invrvald.x โŠข ( ๐œ‘ โ†’ ๐‘‹ โˆˆ ๐ต )
8 invrvald.y โŠข ( ๐œ‘ โ†’ ๐‘Œ โˆˆ ๐ต )
9 invrvald.xy โŠข ( ๐œ‘ โ†’ ( ๐‘‹ ยท ๐‘Œ ) = 1 )
10 invrvald.yx โŠข ( ๐œ‘ โ†’ ( ๐‘Œ ยท ๐‘‹ ) = 1 )
11 eqid โŠข ( โˆฅr โ€˜ ๐‘… ) = ( โˆฅr โ€˜ ๐‘… )
12 1 11 2 dvdsrmul โŠข ( ( ๐‘‹ โˆˆ ๐ต โˆง ๐‘Œ โˆˆ ๐ต ) โ†’ ๐‘‹ ( โˆฅr โ€˜ ๐‘… ) ( ๐‘Œ ยท ๐‘‹ ) )
13 7 8 12 syl2anc โŠข ( ๐œ‘ โ†’ ๐‘‹ ( โˆฅr โ€˜ ๐‘… ) ( ๐‘Œ ยท ๐‘‹ ) )
14 13 10 breqtrd โŠข ( ๐œ‘ โ†’ ๐‘‹ ( โˆฅr โ€˜ ๐‘… ) 1 )
15 eqid โŠข ( oppr โ€˜ ๐‘… ) = ( oppr โ€˜ ๐‘… )
16 15 1 opprbas โŠข ๐ต = ( Base โ€˜ ( oppr โ€˜ ๐‘… ) )
17 eqid โŠข ( โˆฅr โ€˜ ( oppr โ€˜ ๐‘… ) ) = ( โˆฅr โ€˜ ( oppr โ€˜ ๐‘… ) )
18 eqid โŠข ( .r โ€˜ ( oppr โ€˜ ๐‘… ) ) = ( .r โ€˜ ( oppr โ€˜ ๐‘… ) )
19 16 17 18 dvdsrmul โŠข ( ( ๐‘‹ โˆˆ ๐ต โˆง ๐‘Œ โˆˆ ๐ต ) โ†’ ๐‘‹ ( โˆฅr โ€˜ ( oppr โ€˜ ๐‘… ) ) ( ๐‘Œ ( .r โ€˜ ( oppr โ€˜ ๐‘… ) ) ๐‘‹ ) )
20 7 8 19 syl2anc โŠข ( ๐œ‘ โ†’ ๐‘‹ ( โˆฅr โ€˜ ( oppr โ€˜ ๐‘… ) ) ( ๐‘Œ ( .r โ€˜ ( oppr โ€˜ ๐‘… ) ) ๐‘‹ ) )
21 1 2 15 18 opprmul โŠข ( ๐‘Œ ( .r โ€˜ ( oppr โ€˜ ๐‘… ) ) ๐‘‹ ) = ( ๐‘‹ ยท ๐‘Œ )
22 21 9 eqtrid โŠข ( ๐œ‘ โ†’ ( ๐‘Œ ( .r โ€˜ ( oppr โ€˜ ๐‘… ) ) ๐‘‹ ) = 1 )
23 20 22 breqtrd โŠข ( ๐œ‘ โ†’ ๐‘‹ ( โˆฅr โ€˜ ( oppr โ€˜ ๐‘… ) ) 1 )
24 4 3 11 15 17 isunit โŠข ( ๐‘‹ โˆˆ ๐‘ˆ โ†” ( ๐‘‹ ( โˆฅr โ€˜ ๐‘… ) 1 โˆง ๐‘‹ ( โˆฅr โ€˜ ( oppr โ€˜ ๐‘… ) ) 1 ) )
25 14 23 24 sylanbrc โŠข ( ๐œ‘ โ†’ ๐‘‹ โˆˆ ๐‘ˆ )
26 eqid โŠข ( ( mulGrp โ€˜ ๐‘… ) โ†พs ๐‘ˆ ) = ( ( mulGrp โ€˜ ๐‘… ) โ†พs ๐‘ˆ )
27 4 26 3 unitgrpid โŠข ( ๐‘… โˆˆ Ring โ†’ 1 = ( 0g โ€˜ ( ( mulGrp โ€˜ ๐‘… ) โ†พs ๐‘ˆ ) ) )
28 6 27 syl โŠข ( ๐œ‘ โ†’ 1 = ( 0g โ€˜ ( ( mulGrp โ€˜ ๐‘… ) โ†พs ๐‘ˆ ) ) )
29 9 28 eqtrd โŠข ( ๐œ‘ โ†’ ( ๐‘‹ ยท ๐‘Œ ) = ( 0g โ€˜ ( ( mulGrp โ€˜ ๐‘… ) โ†พs ๐‘ˆ ) ) )
30 4 26 unitgrp โŠข ( ๐‘… โˆˆ Ring โ†’ ( ( mulGrp โ€˜ ๐‘… ) โ†พs ๐‘ˆ ) โˆˆ Grp )
31 6 30 syl โŠข ( ๐œ‘ โ†’ ( ( mulGrp โ€˜ ๐‘… ) โ†พs ๐‘ˆ ) โˆˆ Grp )
32 1 11 2 dvdsrmul โŠข ( ( ๐‘Œ โˆˆ ๐ต โˆง ๐‘‹ โˆˆ ๐ต ) โ†’ ๐‘Œ ( โˆฅr โ€˜ ๐‘… ) ( ๐‘‹ ยท ๐‘Œ ) )
33 8 7 32 syl2anc โŠข ( ๐œ‘ โ†’ ๐‘Œ ( โˆฅr โ€˜ ๐‘… ) ( ๐‘‹ ยท ๐‘Œ ) )
34 33 9 breqtrd โŠข ( ๐œ‘ โ†’ ๐‘Œ ( โˆฅr โ€˜ ๐‘… ) 1 )
35 16 17 18 dvdsrmul โŠข ( ( ๐‘Œ โˆˆ ๐ต โˆง ๐‘‹ โˆˆ ๐ต ) โ†’ ๐‘Œ ( โˆฅr โ€˜ ( oppr โ€˜ ๐‘… ) ) ( ๐‘‹ ( .r โ€˜ ( oppr โ€˜ ๐‘… ) ) ๐‘Œ ) )
36 8 7 35 syl2anc โŠข ( ๐œ‘ โ†’ ๐‘Œ ( โˆฅr โ€˜ ( oppr โ€˜ ๐‘… ) ) ( ๐‘‹ ( .r โ€˜ ( oppr โ€˜ ๐‘… ) ) ๐‘Œ ) )
37 1 2 15 18 opprmul โŠข ( ๐‘‹ ( .r โ€˜ ( oppr โ€˜ ๐‘… ) ) ๐‘Œ ) = ( ๐‘Œ ยท ๐‘‹ )
38 37 10 eqtrid โŠข ( ๐œ‘ โ†’ ( ๐‘‹ ( .r โ€˜ ( oppr โ€˜ ๐‘… ) ) ๐‘Œ ) = 1 )
39 36 38 breqtrd โŠข ( ๐œ‘ โ†’ ๐‘Œ ( โˆฅr โ€˜ ( oppr โ€˜ ๐‘… ) ) 1 )
40 4 3 11 15 17 isunit โŠข ( ๐‘Œ โˆˆ ๐‘ˆ โ†” ( ๐‘Œ ( โˆฅr โ€˜ ๐‘… ) 1 โˆง ๐‘Œ ( โˆฅr โ€˜ ( oppr โ€˜ ๐‘… ) ) 1 ) )
41 34 39 40 sylanbrc โŠข ( ๐œ‘ โ†’ ๐‘Œ โˆˆ ๐‘ˆ )
42 4 26 unitgrpbas โŠข ๐‘ˆ = ( Base โ€˜ ( ( mulGrp โ€˜ ๐‘… ) โ†พs ๐‘ˆ ) )
43 4 fvexi โŠข ๐‘ˆ โˆˆ V
44 eqid โŠข ( mulGrp โ€˜ ๐‘… ) = ( mulGrp โ€˜ ๐‘… )
45 44 2 mgpplusg โŠข ยท = ( +g โ€˜ ( mulGrp โ€˜ ๐‘… ) )
46 26 45 ressplusg โŠข ( ๐‘ˆ โˆˆ V โ†’ ยท = ( +g โ€˜ ( ( mulGrp โ€˜ ๐‘… ) โ†พs ๐‘ˆ ) ) )
47 43 46 ax-mp โŠข ยท = ( +g โ€˜ ( ( mulGrp โ€˜ ๐‘… ) โ†พs ๐‘ˆ ) )
48 eqid โŠข ( 0g โ€˜ ( ( mulGrp โ€˜ ๐‘… ) โ†พs ๐‘ˆ ) ) = ( 0g โ€˜ ( ( mulGrp โ€˜ ๐‘… ) โ†พs ๐‘ˆ ) )
49 4 26 5 invrfval โŠข ๐ผ = ( invg โ€˜ ( ( mulGrp โ€˜ ๐‘… ) โ†พs ๐‘ˆ ) )
50 42 47 48 49 grpinvid1 โŠข ( ( ( ( mulGrp โ€˜ ๐‘… ) โ†พs ๐‘ˆ ) โˆˆ Grp โˆง ๐‘‹ โˆˆ ๐‘ˆ โˆง ๐‘Œ โˆˆ ๐‘ˆ ) โ†’ ( ( ๐ผ โ€˜ ๐‘‹ ) = ๐‘Œ โ†” ( ๐‘‹ ยท ๐‘Œ ) = ( 0g โ€˜ ( ( mulGrp โ€˜ ๐‘… ) โ†พs ๐‘ˆ ) ) ) )
51 31 25 41 50 syl3anc โŠข ( ๐œ‘ โ†’ ( ( ๐ผ โ€˜ ๐‘‹ ) = ๐‘Œ โ†” ( ๐‘‹ ยท ๐‘Œ ) = ( 0g โ€˜ ( ( mulGrp โ€˜ ๐‘… ) โ†พs ๐‘ˆ ) ) ) )
52 29 51 mpbird โŠข ( ๐œ‘ โ†’ ( ๐ผ โ€˜ ๐‘‹ ) = ๐‘Œ )
53 25 52 jca โŠข ( ๐œ‘ โ†’ ( ๐‘‹ โˆˆ ๐‘ˆ โˆง ( ๐ผ โ€˜ ๐‘‹ ) = ๐‘Œ ) )