Theorem rprmasso3

Description: In an integral domain, if a prime element divides another, they are associates. (Contributed by Thierry Arnoux, 27-May-2025)

	Ref	Expression
Hypotheses	rprmasso.b	|- B = ( Base ` R )
	rprmasso.p	|- P = ( RPrime ` R )
	rprmasso.d	|- .|| = ( ||r ` R )
	rprmasso.r	|- ( ph -> R e. IDomn )
	rprmasso.x	|- ( ph -> X e. P )
	rprmasso.1	|- ( ph -> X .|| Y )
	rprmasso2.y	|- ( ph -> Y e. P )
	rprmasso3.1	|- .x. = ( .r ` R )
	rprmasso3.u	|- U = ( Unit ` R )
Assertion	rprmasso3	|- ( ph -> E. t e. U ( t .x. X ) = Y )

Proof

Step	Hyp	Ref	Expression
1		rprmasso.b	|- B = ( Base ` R )
2		rprmasso.p	|- P = ( RPrime ` R )
3		rprmasso.d	|- .|| = ( ||r ` R )
4		rprmasso.r	|- ( ph -> R e. IDomn )
5		rprmasso.x	|- ( ph -> X e. P )
6		rprmasso.1	|- ( ph -> X .|| Y )
7		rprmasso2.y	|- ( ph -> Y e. P )
8		rprmasso3.1	|- .x. = ( .r ` R )
9		rprmasso3.u	|- U = ( Unit ` R )
10	1 2 3 4 5 6 7	rprmasso2	|- ( ph -> Y .|| X )
11		eqid	|- ( RSpan ` R ) = ( RSpan ` R )
12	1 2 4 5	rprmcl	|- ( ph -> X e. B )
13	1 2 4 7	rprmcl	|- ( ph -> Y e. B )
14	1 11 3 12 13 9 8 4	dvdsruasso	|- ( ph -> ( ( X .|| Y /\ Y .|| X ) <-> E. t e. U ( t .x. X ) = Y ) )
15	6 10 14	mpbi2and	|- ( ph -> E. t e. U ( t .x. X ) = Y )