Metamath Proof Explorer

Theorem rprmdvds

Description: If a ring prime Q divides a product X .x. Y , then it divides either X or Y . (Contributed by Thierry Arnoux, 18-May-2025)

Ref Expression
Hypotheses rprmdvds.b 
|- B = ( Base ` R )
rprmdvds.p 
|- P = ( RPrime ` R )
rprmdvds.d 
|- .|| = ( ||r ` R )
rprmdvds.t 
|- .x. = ( .r ` R )
rprmdvds.r 
|- ( ph -> R e. V )
rprmdvds.q 
|- ( ph -> Q e. P )
rprmdvds.x 
|- ( ph -> X e. B )
rprmdvds.y 
|- ( ph -> Y e. B )
rprmdvds.1 
|- ( ph -> Q .|| ( X .x. Y ) )
Assertion rprmdvds 
|- ( ph -> ( Q .|| X \/ Q .|| Y ) )

Proof

Step Hyp Ref Expression
1 rprmdvds.b 
 |-  B = ( Base ` R )
2 rprmdvds.p 
 |-  P = ( RPrime ` R )
3 rprmdvds.d 
 |-  .|| = ( ||r ` R )
4 rprmdvds.t 
 |-  .x. = ( .r ` R )
5 rprmdvds.r 
 |-  ( ph -> R e. V )
6 rprmdvds.q 
 |-  ( ph -> Q e. P )
7 rprmdvds.x 
 |-  ( ph -> X e. B )
8 rprmdvds.y 
 |-  ( ph -> Y e. B )
9 rprmdvds.1 
 |-  ( ph -> Q .|| ( X .x. Y ) )
10 oveq1 
 |-  ( x = X -> ( x .x. y ) = ( X .x. y ) )
11 10 breq2d 
 |-  ( x = X -> ( Q .|| ( x .x. y ) <-> Q .|| ( X .x. y ) ) )
12 breq2 
 |-  ( x = X -> ( Q .|| x <-> Q .|| X ) )
13 12 orbi1d 
 |-  ( x = X -> ( ( Q .|| x \/ Q .|| y ) <-> ( Q .|| X \/ Q .|| y ) ) )
14 11 13 imbi12d 
 |-  ( x = X -> ( ( Q .|| ( x .x. y ) -> ( Q .|| x \/ Q .|| y ) ) <-> ( Q .|| ( X .x. y ) -> ( Q .|| X \/ Q .|| y ) ) ) )
15 oveq2 
 |-  ( y = Y -> ( X .x. y ) = ( X .x. Y ) )
16 15 breq2d 
 |-  ( y = Y -> ( Q .|| ( X .x. y ) <-> Q .|| ( X .x. Y ) ) )
17 breq2 
 |-  ( y = Y -> ( Q .|| y <-> Q .|| Y ) )
18 17 orbi2d 
 |-  ( y = Y -> ( ( Q .|| X \/ Q .|| y ) <-> ( Q .|| X \/ Q .|| Y ) ) )
19 16 18 imbi12d 
 |-  ( y = Y -> ( ( Q .|| ( X .x. y ) -> ( Q .|| X \/ Q .|| y ) ) <-> ( Q .|| ( X .x. Y ) -> ( Q .|| X \/ Q .|| Y ) ) ) )
20 6 2 eleqtrdi 
 |-  ( ph -> Q e. ( RPrime ` R ) )
21 eqid 
 |-  ( Unit ` R ) = ( Unit ` R )
22 eqid 
 |-  ( 0g ` R ) = ( 0g ` R )
23 1 21 22 3 4 isrprm 
 |-  ( R e. V -> ( Q e. ( RPrime ` R ) <-> ( Q e. ( B \ ( ( Unit ` R ) u. { ( 0g ` R ) } ) ) /\ A. x e. B A. y e. B ( Q .|| ( x .x. y ) -> ( Q .|| x \/ Q .|| y ) ) ) ) )
24 23 simplbda 
 |-  ( ( R e. V /\ Q e. ( RPrime ` R ) ) -> A. x e. B A. y e. B ( Q .|| ( x .x. y ) -> ( Q .|| x \/ Q .|| y ) ) )
25 5 20 24 syl2anc 
 |-  ( ph -> A. x e. B A. y e. B ( Q .|| ( x .x. y ) -> ( Q .|| x \/ Q .|| y ) ) )
26 14 19 25 7 8 rspc2dv 
 |-  ( ph -> ( Q .|| ( X .x. Y ) -> ( Q .|| X \/ Q .|| Y ) ) )
27 9 26 mpd 
 |-  ( ph -> ( Q .|| X \/ Q .|| Y ) )