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	$$⊢B={\mathrm{Base}}_R$$
	invrvald.t	$$⊢\underset{\dot{}}{·}={\cdot }_R$$
	invrvald.o	$$⊢\underset{\dot{}}{1}=1_R$$
	invrvald.u	$$⊢U=\mathrm{Unit}\left(R\right)$$
	invrvald.i	$$⊢I={inv}_r\left(R\right)$$
	invrvald.r	$$⊢\phi \to R\in \mathrm{Ring}$$
	invrvald.x	$$⊢\phi \to X\in B$$
	invrvald.y	$$⊢\phi \to Y\in B$$
	invrvald.xy	$$⊢\phi \to X\underset{\dot{}}{·}Y=\underset{\dot{}}{1}$$
	invrvald.yx	$$⊢\phi \to Y\underset{\dot{}}{·}X=\underset{\dot{}}{1}$$
Assertion	invrvald	$$⊢\phi \to \left(X\in U\wedge I\left(X\right)=Y\right)$$

Proof

Step	Hyp	Ref	Expression
1		invrvald.b	$$⊢B={\mathrm{Base}}_R$$
2		invrvald.t	$$⊢\underset{\dot{}}{·}={\cdot }_R$$
3		invrvald.o	$$⊢\underset{\dot{}}{1}=1_R$$
4		invrvald.u	$$⊢U=\mathrm{Unit}\left(R\right)$$
5		invrvald.i	$$⊢I={inv}_r\left(R\right)$$
6		invrvald.r	$$⊢\phi \to R\in \mathrm{Ring}$$
7		invrvald.x	$$⊢\phi \to X\in B$$
8		invrvald.y	$$⊢\phi \to Y\in B$$
9		invrvald.xy	$$⊢\phi \to X\underset{\dot{}}{·}Y=\underset{\dot{}}{1}$$
10		invrvald.yx	$$⊢\phi \to Y\underset{\dot{}}{·}X=\underset{\dot{}}{1}$$
11		eqid	$$⊢{\parallel }_r\left(R\right)={\parallel }_r\left(R\right)$$
12	1 11 2	dvdsrmul	$$⊢\left(X\in B\wedge Y\in B\right)\to X{\parallel }_r\left(R\right)\left(Y\underset{\dot{}}{·}X\right)$$
13	7 8 12	syl2anc	$$⊢\phi \to X{\parallel }_r\left(R\right)\left(Y\underset{\dot{}}{·}X\right)$$
14	13 10	breqtrd	$$⊢\phi \to X{\parallel }_r\left(R\right)\underset{\dot{}}{1}$$
15		eqid	$$⊢{opp}_r\left(R\right)={opp}_r\left(R\right)$$
16	15 1	opprbas	$$⊢B={\mathrm{Base}}_{{opp}_r\left(R\right)}$$
17		eqid	$$⊢{\parallel }_r\left({opp}_r\left(R\right)\right)={\parallel }_r\left({opp}_r\left(R\right)\right)$$
18		eqid	$$⊢{\cdot }_{{opp}_r\left(R\right)}={\cdot }_{{opp}_r\left(R\right)}$$
19	16 17 18	dvdsrmul	$$⊢\left(X\in B\wedge Y\in B\right)\to X{\parallel }_r\left({opp}_r\left(R\right)\right)\left(Y{\cdot }_{{opp}_r\left(R\right)}X\right)$$
20	7 8 19	syl2anc	$$⊢\phi \to X{\parallel }_r\left({opp}_r\left(R\right)\right)\left(Y{\cdot }_{{opp}_r\left(R\right)}X\right)$$
21	1 2 15 18	opprmul	$$⊢Y{\cdot }_{{opp}_r\left(R\right)}X=X\underset{\dot{}}{·}Y$$
22	21 9	syl5eq	$$⊢\phi \to Y{\cdot }_{{opp}_r\left(R\right)}X=\underset{\dot{}}{1}$$
23	20 22	breqtrd	$$⊢\phi \to X{\parallel }_r\left({opp}_r\left(R\right)\right)\underset{\dot{}}{1}$$
24	4 3 11 15 17	isunit	$$⊢X\in U\leftrightarrow \left(X{\parallel }_r\left(R\right)\underset{\dot{}}{1}\wedge X{\parallel }_r\left({opp}_r\left(R\right)\right)\underset{\dot{}}{1}\right)$$
25	14 23 24	sylanbrc	$$⊢\phi \to X\in U$$
26		eqid	$$⊢{\mathrm{mulGrp}}_R{\upharpoonright }_{𝑠}U={\mathrm{mulGrp}}_R{\upharpoonright }_{𝑠}U$$
27	4 26 3	unitgrpid	$$⊢R\in \mathrm{Ring}\to \underset{\dot{}}{1}=0_{\left({\mathrm{mulGrp}}_R{\upharpoonright }_{𝑠}U\right)}$$
28	6 27	syl	$$⊢\phi \to \underset{\dot{}}{1}=0_{\left({\mathrm{mulGrp}}_R{\upharpoonright }_{𝑠}U\right)}$$
29	9 28	eqtrd	$$⊢\phi \to X\underset{\dot{}}{·}Y=0_{\left({\mathrm{mulGrp}}_R{\upharpoonright }_{𝑠}U\right)}$$
30	4 26	unitgrp	$$⊢R\in \mathrm{Ring}\to {\mathrm{mulGrp}}_R{\upharpoonright }_{𝑠}U\in \mathrm{Grp}$$
31	6 30	syl	$$⊢\phi \to {\mathrm{mulGrp}}_R{\upharpoonright }_{𝑠}U\in \mathrm{Grp}$$
32	1 11 2	dvdsrmul	$$⊢\left(Y\in B\wedge X\in B\right)\to Y{\parallel }_r\left(R\right)\left(X\underset{\dot{}}{·}Y\right)$$
33	8 7 32	syl2anc	$$⊢\phi \to Y{\parallel }_r\left(R\right)\left(X\underset{\dot{}}{·}Y\right)$$
34	33 9	breqtrd	$$⊢\phi \to Y{\parallel }_r\left(R\right)\underset{\dot{}}{1}$$
35	16 17 18	dvdsrmul	$$⊢\left(Y\in B\wedge X\in B\right)\to Y{\parallel }_r\left({opp}_r\left(R\right)\right)\left(X{\cdot }_{{opp}_r\left(R\right)}Y\right)$$
36	8 7 35	syl2anc	$$⊢\phi \to Y{\parallel }_r\left({opp}_r\left(R\right)\right)\left(X{\cdot }_{{opp}_r\left(R\right)}Y\right)$$
37	1 2 15 18	opprmul	$$⊢X{\cdot }_{{opp}_r\left(R\right)}Y=Y\underset{\dot{}}{·}X$$
38	37 10	syl5eq	$$⊢\phi \to X{\cdot }_{{opp}_r\left(R\right)}Y=\underset{\dot{}}{1}$$
39	36 38	breqtrd	$$⊢\phi \to Y{\parallel }_r\left({opp}_r\left(R\right)\right)\underset{\dot{}}{1}$$
40	4 3 11 15 17	isunit	$$⊢Y\in U\leftrightarrow \left(Y{\parallel }_r\left(R\right)\underset{\dot{}}{1}\wedge Y{\parallel }_r\left({opp}_r\left(R\right)\right)\underset{\dot{}}{1}\right)$$
41	34 39 40	sylanbrc	$$⊢\phi \to Y\in U$$
42	4 26	unitgrpbas	$$⊢U={\mathrm{Base}}_{\left({\mathrm{mulGrp}}_R{\upharpoonright }_{𝑠}U\right)}$$
43	4	fvexi	$$⊢U\in \mathrm{V}$$
44		eqid	$$⊢{\mathrm{mulGrp}}_R={\mathrm{mulGrp}}_R$$
45	44 2	mgpplusg	$$⊢\underset{\dot{}}{·}={+}_{{\mathrm{mulGrp}}_R}$$
46	26 45	ressplusg	$$⊢U\in \mathrm{V}\to \underset{\dot{}}{·}={+}_{\left({\mathrm{mulGrp}}_R{\upharpoonright }_{𝑠}U\right)}$$
47	43 46	ax-mp	$$⊢\underset{\dot{}}{·}={+}_{\left({\mathrm{mulGrp}}_R{\upharpoonright }_{𝑠}U\right)}$$
48		eqid	$$⊢0_{\left({\mathrm{mulGrp}}_R{\upharpoonright }_{𝑠}U\right)}=0_{\left({\mathrm{mulGrp}}_R{\upharpoonright }_{𝑠}U\right)}$$
49	4 26 5	invrfval	$$⊢I={inv}_g\left({\mathrm{mulGrp}}_R{\upharpoonright }_{𝑠}U\right)$$
50	42 47 48 49	grpinvid1	$$⊢\left({\mathrm{mulGrp}}_R{\upharpoonright }_{𝑠}U\in \mathrm{Grp}\wedge X\in U\wedge Y\in U\right)\to \left(I\left(X\right)=Y\leftrightarrow X\underset{\dot{}}{·}Y=0_{\left({\mathrm{mulGrp}}_R{\upharpoonright }_{𝑠}U\right)}\right)$$
51	31 25 41 50	syl3anc	$$⊢\phi \to \left(I\left(X\right)=Y\leftrightarrow X\underset{\dot{}}{·}Y=0_{\left({\mathrm{mulGrp}}_R{\upharpoonright }_{𝑠}U\right)}\right)$$
52	29 51	mpbird	$$⊢\phi \to I\left(X\right)=Y$$
53	25 52	jca	$$⊢\phi \to \left(X\in U\wedge I\left(X\right)=Y\right)$$