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 13 crngringd 
 |-  ( ( ( ph /\ t e. B ) /\ ( t .x. Q ) = X ) -> R e. Ring )
16 simplr 
 |-  ( ( ( ph /\ t e. B ) /\ ( t .x. Q ) = X ) -> t e. B )
17 1 4 15 16 14 ringcld 
 |-  ( ( ( ph /\ t e. B ) /\ ( t .x. Q ) = X ) -> ( t .x. Y ) e. B )
18 eqid 
 |-  ( 1r ` R ) = ( 1r ` R )
19 1 18 ringidcl 
 |-  ( R e. Ring -> ( 1r ` R ) e. B )
20 15 19 syl 
 |-  ( ( ( ph /\ t e. B ) /\ ( t .x. Q ) = X ) -> ( 1r ` R ) e. B )
21 1 5 4 dvdsr 
 |-  ( Q .|| X <-> ( Q e. B /\ E. t e. B ( t .x. Q ) = X ) )
22 11 21 sylib 
 |-  ( ph -> ( Q e. B /\ E. t e. B ( t .x. Q ) = X ) )
23 22 simpld 
 |-  ( ph -> Q e. B )
24 23 ad2antrr 
 |-  ( ( ( ph /\ t e. B ) /\ ( t .x. Q ) = X ) -> Q e. B )
25 7 ad2antrr 
 |-  ( ( ( ph /\ t e. B ) /\ ( t .x. Q ) = X ) -> Q =/= .0. )
26 24 25 eldifsnd 
 |-  ( ( ( ph /\ t e. B ) /\ ( t .x. Q ) = X ) -> Q e. ( B \ { .0. } ) )
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 16 14 24 cringmul32d 
 |-  ( ( ( ph /\ t e. B ) /\ ( t .x. Q ) = X ) -> ( ( t .x. Y ) .x. Q ) = ( ( t .x. Q ) .x. Y ) )
33 1 4 18 15 24 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 17 20 26 27 34 idomrcan 
 |-  ( ( ( ph /\ t e. B ) /\ ( t .x. Q ) = X ) -> ( t .x. Y ) = ( 1r ` R ) )
36 22 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 18 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 )