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 ( 𝜑 → ( 𝑋𝑈 ∧ ( 𝐼𝑋 ) = 𝑌 ) )