This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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