Theorem unitmulrprm

Description: A ring unit multiplied by a ring prime is a ring prime. (Contributed by Thierry Arnoux, 3-Jun-2025)

	Ref	Expression
Hypotheses	unitmulrprm.p	$$⊢P=\mathrm{RPrime}\left(R\right)$$
	unitmulrprm.u	$$⊢U=\mathrm{Unit}\left(R\right)$$
	unitmulrprm.t	$$⊢\underset{\dot{}}{·}={\cdot }_R$$
	unitmulrprm.r	$$⊢\phi \to R\in \mathrm{IDomn}$$
	unitmulrprm.i	$$⊢\phi \to I\in U$$
	unitmulrprm.q	$$⊢\phi \to Q\in P$$
Assertion	unitmulrprm	$$⊢\phi \to I\underset{\dot{}}{·}Q\in P$$

Proof

Step	Hyp	Ref	Expression
1		unitmulrprm.p	$$⊢P=\mathrm{RPrime}\left(R\right)$$
2		unitmulrprm.u	$$⊢U=\mathrm{Unit}\left(R\right)$$
3		unitmulrprm.t	$$⊢\underset{\dot{}}{·}={\cdot }_R$$
4		unitmulrprm.r	$$⊢\phi \to R\in \mathrm{IDomn}$$
5		unitmulrprm.i	$$⊢\phi \to I\in U$$
6		unitmulrprm.q	$$⊢\phi \to Q\in P$$
7		eqid	$$⊢{\mathrm{Base}}_R={\mathrm{Base}}_R$$
8		eqid	$$⊢{\parallel }_r\left(R\right)={\parallel }_r\left(R\right)$$
9	7 1 4 6	rprmcl	$$⊢\phi \to Q\in {\mathrm{Base}}_R$$
10		oveq1	$$⊢i=I\to i\underset{\dot{}}{·}Q=I\underset{\dot{}}{·}Q$$
11	10	eqeq1d	$$⊢i=I\to \left(i\underset{\dot{}}{·}Q=I\underset{\dot{}}{·}Q\leftrightarrow I\underset{\dot{}}{·}Q=I\underset{\dot{}}{·}Q\right)$$
12	7 2	unitcl	$$⊢I\in U\to I\in {\mathrm{Base}}_R$$
13	5 12	syl	$$⊢\phi \to I\in {\mathrm{Base}}_R$$
14		eqidd	$$⊢\phi \to I\underset{\dot{}}{·}Q=I\underset{\dot{}}{·}Q$$
15	11 13 14	rspcedvdw	$$⊢\phi \to \exists i\in {\mathrm{Base}}_{R}i\underset{\dot{}}{·}Q=I\underset{\dot{}}{·}Q$$
16	7 8 3	dvdsr	$$⊢Q{\parallel }_r\left(R\right)\left(I\underset{\dot{}}{·}Q\right)\leftrightarrow \left(Q\in {\mathrm{Base}}_R\wedge \exists i\in {\mathrm{Base}}_{R}i\underset{\dot{}}{·}Q=I\underset{\dot{}}{·}Q\right)$$
17	9 15 16	sylanbrc	$$⊢\phi \to Q{\parallel }_r\left(R\right)\left(I\underset{\dot{}}{·}Q\right)$$
18	4	idomringd	$$⊢\phi \to R\in \mathrm{Ring}$$
19	7 3 18 13 9	ringcld	$$⊢\phi \to I\underset{\dot{}}{·}Q\in {\mathrm{Base}}_R$$
20		oveq1	$$⊢i={inv}_r\left(R\right)\left(I\right)\to i\underset{\dot{}}{·}\left(I\underset{\dot{}}{·}Q\right)={inv}_r\left(R\right)\left(I\right)\underset{\dot{}}{·}\left(I\underset{\dot{}}{·}Q\right)$$
21	20	eqeq1d	$$⊢i={inv}_r\left(R\right)\left(I\right)\to \left(i\underset{\dot{}}{·}\left(I\underset{\dot{}}{·}Q\right)=Q\leftrightarrow {inv}_r\left(R\right)\left(I\right)\underset{\dot{}}{·}\left(I\underset{\dot{}}{·}Q\right)=Q\right)$$
22		eqid	$$⊢{inv}_r\left(R\right)={inv}_r\left(R\right)$$
23	2 22 7	ringinvcl	$$⊢\left(R\in \mathrm{Ring}\wedge I\in U\right)\to {inv}_r\left(R\right)\left(I\right)\in {\mathrm{Base}}_R$$
24	18 5 23	syl2anc	$$⊢\phi \to {inv}_r\left(R\right)\left(I\right)\in {\mathrm{Base}}_R$$
25		eqid	$$⊢1_R=1_R$$
26	2 22 3 25	unitlinv	$$⊢\left(R\in \mathrm{Ring}\wedge I\in U\right)\to {inv}_r\left(R\right)\left(I\right)\underset{\dot{}}{·}I=1_R$$
27	18 5 26	syl2anc	$$⊢\phi \to {inv}_r\left(R\right)\left(I\right)\underset{\dot{}}{·}I=1_R$$
28	27	oveq1d	$$⊢\phi \to \left({inv}_r\left(R\right)\left(I\right)\underset{\dot{}}{·}I\right)\underset{\dot{}}{·}Q=1_R\underset{\dot{}}{·}Q$$
29	7 3 18 24 13 9	ringassd	$$⊢\phi \to \left({inv}_r\left(R\right)\left(I\right)\underset{\dot{}}{·}I\right)\underset{\dot{}}{·}Q={inv}_r\left(R\right)\left(I\right)\underset{\dot{}}{·}\left(I\underset{\dot{}}{·}Q\right)$$
30	7 3 25 18 9	ringlidmd	$$⊢\phi \to 1_R\underset{\dot{}}{·}Q=Q$$
31	28 29 30	3eqtr3d	$$⊢\phi \to {inv}_r\left(R\right)\left(I\right)\underset{\dot{}}{·}\left(I\underset{\dot{}}{·}Q\right)=Q$$
32	21 24 31	rspcedvdw	$$⊢\phi \to \exists i\in {\mathrm{Base}}_{R}i\underset{\dot{}}{·}\left(I\underset{\dot{}}{·}Q\right)=Q$$
33	7 8 3	dvdsr	$$⊢\left(I\underset{\dot{}}{·}Q\right){\parallel }_r\left(R\right)Q\leftrightarrow \left(I\underset{\dot{}}{·}Q\in {\mathrm{Base}}_R\wedge \exists i\in {\mathrm{Base}}_{R}i\underset{\dot{}}{·}\left(I\underset{\dot{}}{·}Q\right)=Q\right)$$
34	19 32 33	sylanbrc	$$⊢\phi \to \left(I\underset{\dot{}}{·}Q\right){\parallel }_r\left(R\right)Q$$
35	7 1 8 4 6 17 34	rprmasso	$$⊢\phi \to I\underset{\dot{}}{·}Q\in P$$