Theorem drnginvmuld

Description: Inverse of a nonzero product. (Contributed by SN, 14-Aug-2024)

	Ref	Expression
Hypotheses	drnginvmuld.b	$$⊢B={\mathrm{Base}}_R$$
	drnginvmuld.z	$$⊢\underset{\dot{}}{0}=0_R$$
	drnginvmuld.t	$$⊢\underset{\dot{}}{·}={\cdot }_R$$
	drnginvmuld.i	$$⊢I={inv}_r\left(R\right)$$
	drnginvmuld.r	$$⊢\phi \to R\in \mathrm{DivRing}$$
	drnginvmuld.x	$$⊢\phi \to X\in B$$
	drnginvmuld.y	$$⊢\phi \to Y\in B$$
	drnginvmuld.1	$$⊢\phi \to X\ne \underset{\dot{}}{0}$$
	drnginvmuld.2	$$⊢\phi \to Y\ne \underset{\dot{}}{0}$$
Assertion	drnginvmuld	$$⊢\phi \to I\left(X\underset{\dot{}}{·}Y\right)=I\left(Y\right)\underset{\dot{}}{·}I\left(X\right)$$

Proof

Step	Hyp	Ref	Expression
1		drnginvmuld.b	$$⊢B={\mathrm{Base}}_R$$
2		drnginvmuld.z	$$⊢\underset{\dot{}}{0}=0_R$$
3		drnginvmuld.t	$$⊢\underset{\dot{}}{·}={\cdot }_R$$
4		drnginvmuld.i	$$⊢I={inv}_r\left(R\right)$$
5		drnginvmuld.r	$$⊢\phi \to R\in \mathrm{DivRing}$$
6		drnginvmuld.x	$$⊢\phi \to X\in B$$
7		drnginvmuld.y	$$⊢\phi \to Y\in B$$
8		drnginvmuld.1	$$⊢\phi \to X\ne \underset{\dot{}}{0}$$
9		drnginvmuld.2	$$⊢\phi \to Y\ne \underset{\dot{}}{0}$$
10	5	drngringd	$$⊢\phi \to R\in \mathrm{Ring}$$
11	1 3 10 6 7	ringcld	$$⊢\phi \to X\underset{\dot{}}{·}Y\in B$$
12	1 2 3 5 6 7	drngmulne0	$$⊢\phi \to \left(X\underset{\dot{}}{·}Y\ne \underset{\dot{}}{0}\leftrightarrow \left(X\ne \underset{\dot{}}{0}\wedge Y\ne \underset{\dot{}}{0}\right)\right)$$
13	8 9 12	mpbir2and	$$⊢\phi \to X\underset{\dot{}}{·}Y\ne \underset{\dot{}}{0}$$
14	1 2 4 5 11 13	drnginvrcld	$$⊢\phi \to I\left(X\underset{\dot{}}{·}Y\right)\in B$$
15	1 2 4 5 7 9	drnginvrcld	$$⊢\phi \to I\left(Y\right)\in B$$
16	1 2 4 5 6 8	drnginvrcld	$$⊢\phi \to I\left(X\right)\in B$$
17	1 3 10 15 16	ringcld	$$⊢\phi \to I\left(Y\right)\underset{\dot{}}{·}I\left(X\right)\in B$$
18		eqid	$$⊢1_R=1_R$$
19	1 2 3 18 4 5 6 8	drnginvrld	$$⊢\phi \to I\left(X\right)\underset{\dot{}}{·}X=1_R$$
20	19	oveq1d	$$⊢\phi \to \left(I\left(X\right)\underset{\dot{}}{·}X\right)\underset{\dot{}}{·}Y=1_R\underset{\dot{}}{·}Y$$
21	1 3 18 10 7	ringlidmd	$$⊢\phi \to 1_R\underset{\dot{}}{·}Y=Y$$
22	20 21	eqtrd	$$⊢\phi \to \left(I\left(X\right)\underset{\dot{}}{·}X\right)\underset{\dot{}}{·}Y=Y$$
23	22	oveq2d	$$⊢\phi \to I\left(Y\right)\underset{\dot{}}{·}\left(\left(I\left(X\right)\underset{\dot{}}{·}X\right)\underset{\dot{}}{·}Y\right)=I\left(Y\right)\underset{\dot{}}{·}Y$$
24	23	eqcomd	$$⊢\phi \to I\left(Y\right)\underset{\dot{}}{·}Y=I\left(Y\right)\underset{\dot{}}{·}\left(\left(I\left(X\right)\underset{\dot{}}{·}X\right)\underset{\dot{}}{·}Y\right)$$
25	1 2 3 18 4 5 7 9	drnginvrld	$$⊢\phi \to I\left(Y\right)\underset{\dot{}}{·}Y=1_R$$
26	1 3 10 16 6 7	ringassd	$$⊢\phi \to \left(I\left(X\right)\underset{\dot{}}{·}X\right)\underset{\dot{}}{·}Y=I\left(X\right)\underset{\dot{}}{·}\left(X\underset{\dot{}}{·}Y\right)$$
27	26	oveq2d	$$⊢\phi \to I\left(Y\right)\underset{\dot{}}{·}\left(\left(I\left(X\right)\underset{\dot{}}{·}X\right)\underset{\dot{}}{·}Y\right)=I\left(Y\right)\underset{\dot{}}{·}\left(I\left(X\right)\underset{\dot{}}{·}\left(X\underset{\dot{}}{·}Y\right)\right)$$
28	24 25 27	3eqtr3d	$$⊢\phi \to 1_R=I\left(Y\right)\underset{\dot{}}{·}\left(I\left(X\right)\underset{\dot{}}{·}\left(X\underset{\dot{}}{·}Y\right)\right)$$
29	1 2 3 18 4 5 11 13	drnginvrld	$$⊢\phi \to I\left(X\underset{\dot{}}{·}Y\right)\underset{\dot{}}{·}\left(X\underset{\dot{}}{·}Y\right)=1_R$$
30	1 3 10 15 16 11	ringassd	$$⊢\phi \to \left(I\left(Y\right)\underset{\dot{}}{·}I\left(X\right)\right)\underset{\dot{}}{·}\left(X\underset{\dot{}}{·}Y\right)=I\left(Y\right)\underset{\dot{}}{·}\left(I\left(X\right)\underset{\dot{}}{·}\left(X\underset{\dot{}}{·}Y\right)\right)$$
31	28 29 30	3eqtr4d	$$⊢\phi \to I\left(X\underset{\dot{}}{·}Y\right)\underset{\dot{}}{·}\left(X\underset{\dot{}}{·}Y\right)=\left(I\left(Y\right)\underset{\dot{}}{·}I\left(X\right)\right)\underset{\dot{}}{·}\left(X\underset{\dot{}}{·}Y\right)$$
32	1 2 3 5 14 17 11 13 31	drngmulcan2ad	$$⊢\phi \to I\left(X\underset{\dot{}}{·}Y\right)=I\left(Y\right)\underset{\dot{}}{·}I\left(X\right)$$