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 syl5eq ⊢ ( 𝜑 → ( 𝑌 ( .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 syl5eq ⊢ ( 𝜑 → ( 𝑋 ( .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 ⊢ ( 𝜑 → ( 𝑋 ∈ 𝑈 ∧ ( 𝐼 ‘ 𝑋 ) = 𝑌 ) )