Metamath Proof Explorer

Theorem rprmirredlem

Description: Lemma for rprmirred . (Contributed by Thierry Arnoux, 18-May-2025)

Ref Expression
Hypotheses rprmirredlem.1 
|- B = ( Base ` R )
rprmirredlem.2 
|- U = ( Unit ` R )
rprmirredlem.3 
|- .0. = ( 0g ` R )
rprmirredlem.4 
|- .x. = ( .r ` R )
rprmirredlem.5 
|- .|| = ( ||r ` R )
rprmirredlem.6 
|- ( ph -> R e. IDomn )
rprmirredlem.7 
|- ( ph -> Q =/= .0. )
rprmirredlem.8 
|- ( ph -> X e. ( B \ U ) )
rprmirredlem.9 
|- ( ph -> Y e. B )
rprmirredlem.10 
|- ( ph -> Q = ( X .x. Y ) )
rprmirredlem.11 
|- ( ph -> Q .|| X )
Assertion rprmirredlem 
|- ( ph -> Y e. U )

Proof

Step Hyp Ref Expression
1 rprmirredlem.1 
 |-  B = ( Base ` R )
2 rprmirredlem.2 
 |-  U = ( Unit ` R )
3 rprmirredlem.3 
 |-  .0. = ( 0g ` R )
4 rprmirredlem.4 
 |-  .x. = ( .r ` R )
5 rprmirredlem.5 
 |-  .|| = ( ||r ` R )
6 rprmirredlem.6 
 |-  ( ph -> R e. IDomn )
7 rprmirredlem.7 
 |-  ( ph -> Q =/= .0. )
8 rprmirredlem.8 
 |-  ( ph -> X e. ( B \ U ) )
9 rprmirredlem.9 
 |-  ( ph -> Y e. B )
10 rprmirredlem.10 
 |-  ( ph -> Q = ( X .x. Y ) )
11 rprmirredlem.11 
 |-  ( ph -> Q .|| X )
12 6 idomcringd 
 |-  ( ph -> R e. CRing )
13 12 ad2antrr 
 |-  ( ( ( ph /\ t e. B ) /\ ( t .x. Q ) = X ) -> R e. CRing )
14 9 ad2antrr 
 |-  ( ( ( ph /\ t e. B ) /\ ( t .x. Q ) = X ) -> Y e. B )
15 1 5 4 dvdsr 
 |-  ( Q .|| X <-> ( Q e. B /\ E. t e. B ( t .x. Q ) = X ) )
16 11 15 sylib 
 |-  ( ph -> ( Q e. B /\ E. t e. B ( t .x. Q ) = X ) )
17 16 simpld 
 |-  ( ph -> Q e. B )
18 17 ad2antrr 
 |-  ( ( ( ph /\ t e. B ) /\ ( t .x. Q ) = X ) -> Q e. B )
19 7 ad2antrr 
 |-  ( ( ( ph /\ t e. B ) /\ ( t .x. Q ) = X ) -> Q =/= .0. )
20 18 19 eldifsnd 
 |-  ( ( ( ph /\ t e. B ) /\ ( t .x. Q ) = X ) -> Q e. ( B \ { .0. } ) )
21 13 crngringd 
 |-  ( ( ( ph /\ t e. B ) /\ ( t .x. Q ) = X ) -> R e. Ring )
22 simplr 
 |-  ( ( ( ph /\ t e. B ) /\ ( t .x. Q ) = X ) -> t e. B )
23 1 4 21 22 14 ringcld 
 |-  ( ( ( ph /\ t e. B ) /\ ( t .x. Q ) = X ) -> ( t .x. Y ) e. B )
24 eqid 
 |-  ( 1r ` R ) = ( 1r ` R )
25 1 24 ringidcl 
 |-  ( R e. Ring -> ( 1r ` R ) e. B )
26 21 25 syl 
 |-  ( ( ( ph /\ t e. B ) /\ ( t .x. Q ) = X ) -> ( 1r ` R ) e. B )
27 6 ad2antrr 
 |-  ( ( ( ph /\ t e. B ) /\ ( t .x. Q ) = X ) -> R e. IDomn )
28 simpr 
 |-  ( ( ( ph /\ t e. B ) /\ ( t .x. Q ) = X ) -> ( t .x. Q ) = X )
29 28 oveq1d 
 |-  ( ( ( ph /\ t e. B ) /\ ( t .x. Q ) = X ) -> ( ( t .x. Q ) .x. Y ) = ( X .x. Y ) )
30 10 ad2antrr 
 |-  ( ( ( ph /\ t e. B ) /\ ( t .x. Q ) = X ) -> Q = ( X .x. Y ) )
31 29 30 eqtr4d 
 |-  ( ( ( ph /\ t e. B ) /\ ( t .x. Q ) = X ) -> ( ( t .x. Q ) .x. Y ) = Q )
32 1 4 13 22 14 18 cringmul32d 
 |-  ( ( ( ph /\ t e. B ) /\ ( t .x. Q ) = X ) -> ( ( t .x. Y ) .x. Q ) = ( ( t .x. Q ) .x. Y ) )
33 1 4 24 21 18 ringlidmd 
 |-  ( ( ( ph /\ t e. B ) /\ ( t .x. Q ) = X ) -> ( ( 1r ` R ) .x. Q ) = Q )
34 31 32 33 3eqtr4d 
 |-  ( ( ( ph /\ t e. B ) /\ ( t .x. Q ) = X ) -> ( ( t .x. Y ) .x. Q ) = ( ( 1r ` R ) .x. Q ) )
35 1 3 4 20 23 26 27 34 idomrcan 
 |-  ( ( ( ph /\ t e. B ) /\ ( t .x. Q ) = X ) -> ( t .x. Y ) = ( 1r ` R ) )
36 16 simprd 
 |-  ( ph -> E. t e. B ( t .x. Q ) = X )
37 35 36 reximddv3 
 |-  ( ph -> E. t e. B ( t .x. Y ) = ( 1r ` R ) )
38 37 ad2antrr 
 |-  ( ( ( ph /\ t e. B ) /\ ( t .x. Q ) = X ) -> E. t e. B ( t .x. Y ) = ( 1r ` R ) )
39 1 5 4 dvdsr 
 |-  ( Y .|| ( 1r ` R ) <-> ( Y e. B /\ E. t e. B ( t .x. Y ) = ( 1r ` R ) ) )
40 14 38 39 sylanbrc 
 |-  ( ( ( ph /\ t e. B ) /\ ( t .x. Q ) = X ) -> Y .|| ( 1r ` R ) )
41 2 24 5 crngunit 
 |-  ( R e. CRing -> ( Y e. U <-> Y .|| ( 1r ` R ) ) )
42 41 biimpar 
 |-  ( ( R e. CRing /\ Y .|| ( 1r ` R ) ) -> Y e. U )
43 13 40 42 syl2anc 
 |-  ( ( ( ph /\ t e. B ) /\ ( t .x. Q ) = X ) -> Y e. U )
44 43 36 r19.29a 
 |-  ( ph -> Y e. U )