Metamath Proof Explorer

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 = ( RPrime ` R )
unitmulrprm.u 
|- U = ( Unit ` R )
unitmulrprm.t 
|- .x. = ( .r ` R )
unitmulrprm.r 
|- ( ph -> R e. IDomn )
unitmulrprm.i 
|- ( ph -> I e. U )
unitmulrprm.q 
|- ( ph -> Q e. P )
Assertion unitmulrprm 
|- ( ph -> ( I .x. Q ) e. P )

Proof

Step Hyp Ref Expression
1 unitmulrprm.p 
 |-  P = ( RPrime ` R )
2 unitmulrprm.u 
 |-  U = ( Unit ` R )
3 unitmulrprm.t 
 |-  .x. = ( .r ` R )
4 unitmulrprm.r 
 |-  ( ph -> R e. IDomn )
5 unitmulrprm.i 
 |-  ( ph -> I e. U )
6 unitmulrprm.q 
 |-  ( ph -> Q e. P )
7 eqid 
 |-  ( Base ` R ) = ( Base ` R )
8 eqid 
 |-  ( ||r ` R ) = ( ||r ` R )
9 7 1 4 6 rprmcl 
 |-  ( ph -> Q e. ( Base ` R ) )
10 oveq1 
 |-  ( i = I -> ( i .x. Q ) = ( I .x. Q ) )
11 10 eqeq1d 
 |-  ( i = I -> ( ( i .x. Q ) = ( I .x. Q ) <-> ( I .x. Q ) = ( I .x. Q ) ) )
12 7 2 unitcl 
 |-  ( I e. U -> I e. ( Base ` R ) )
13 5 12 syl 
 |-  ( ph -> I e. ( Base ` R ) )
14 eqidd 
 |-  ( ph -> ( I .x. Q ) = ( I .x. Q ) )
15 11 13 14 rspcedvdw 
 |-  ( ph -> E. i e. ( Base ` R ) ( i .x. Q ) = ( I .x. Q ) )
16 7 8 3 dvdsr 
 |-  ( Q ( ||r ` R ) ( I .x. Q ) <-> ( Q e. ( Base ` R ) /\ E. i e. ( Base ` R ) ( i .x. Q ) = ( I .x. Q ) ) )
17 9 15 16 sylanbrc 
 |-  ( ph -> Q ( ||r ` R ) ( I .x. Q ) )
18 4 idomringd 
 |-  ( ph -> R e. Ring )
19 7 3 18 13 9 ringcld 
 |-  ( ph -> ( I .x. Q ) e. ( Base ` R ) )
20 oveq1 
 |-  ( i = ( ( invr ` R ) ` I ) -> ( i .x. ( I .x. Q ) ) = ( ( ( invr ` R ) ` I ) .x. ( I .x. Q ) ) )
21 20 eqeq1d 
 |-  ( i = ( ( invr ` R ) ` I ) -> ( ( i .x. ( I .x. Q ) ) = Q <-> ( ( ( invr ` R ) ` I ) .x. ( I .x. Q ) ) = Q ) )
22 eqid 
 |-  ( invr ` R ) = ( invr ` R )
23 2 22 7 ringinvcl 
 |-  ( ( R e. Ring /\ I e. U ) -> ( ( invr ` R ) ` I ) e. ( Base ` R ) )
24 18 5 23 syl2anc 
 |-  ( ph -> ( ( invr ` R ) ` I ) e. ( Base ` R ) )
25 eqid 
 |-  ( 1r ` R ) = ( 1r ` R )
26 2 22 3 25 unitlinv 
 |-  ( ( R e. Ring /\ I e. U ) -> ( ( ( invr ` R ) ` I ) .x. I ) = ( 1r ` R ) )
27 18 5 26 syl2anc 
 |-  ( ph -> ( ( ( invr ` R ) ` I ) .x. I ) = ( 1r ` R ) )
28 27 oveq1d 
 |-  ( ph -> ( ( ( ( invr ` R ) ` I ) .x. I ) .x. Q ) = ( ( 1r ` R ) .x. Q ) )
29 7 3 18 24 13 9 ringassd 
 |-  ( ph -> ( ( ( ( invr ` R ) ` I ) .x. I ) .x. Q ) = ( ( ( invr ` R ) ` I ) .x. ( I .x. Q ) ) )
30 7 3 25 18 9 ringlidmd 
 |-  ( ph -> ( ( 1r ` R ) .x. Q ) = Q )
31 28 29 30 3eqtr3d 
 |-  ( ph -> ( ( ( invr ` R ) ` I ) .x. ( I .x. Q ) ) = Q )
32 21 24 31 rspcedvdw 
 |-  ( ph -> E. i e. ( Base ` R ) ( i .x. ( I .x. Q ) ) = Q )
33 7 8 3 dvdsr 
 |-  ( ( I .x. Q ) ( ||r ` R ) Q <-> ( ( I .x. Q ) e. ( Base ` R ) /\ E. i e. ( Base ` R ) ( i .x. ( I .x. Q ) ) = Q ) )
34 19 32 33 sylanbrc 
 |-  ( ph -> ( I .x. Q ) ( ||r ` R ) Q )
35 7 1 8 4 6 17 34 rprmasso 
 |-  ( ph -> ( I .x. Q ) e. P )