Metamath Proof Explorer

Theorem rprmirredlem

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

Ref Expression
Hypotheses rprmirredlem.1 ⊢ 𝐵 = ( Base ‘ 𝑅 )
rprmirredlem.2 ⊢ 𝑈 = ( Unit ‘ 𝑅 )
rprmirredlem.3 ⊢ 0 = ( 0g ‘ 𝑅 )
rprmirredlem.4 ⊢ · = ( .r ‘ 𝑅 )
rprmirredlem.5 ⊢ ∥ = ( ∥r ‘ 𝑅 )
rprmirredlem.6 ⊢ ( 𝜑 → 𝑅 ∈ IDomn )
rprmirredlem.7 ⊢ ( 𝜑 → 𝑄 ≠ 0 )
rprmirredlem.8 ⊢ ( 𝜑 → 𝑋 ∈ ( 𝐵 ∖ 𝑈 ) )
rprmirredlem.9 ⊢ ( 𝜑 → 𝑌 ∈ 𝐵 )
rprmirredlem.10 ⊢ ( 𝜑 → 𝑄 = ( 𝑋 · 𝑌 ) )
rprmirredlem.11 ⊢ ( 𝜑 → 𝑄 ∥ 𝑋 )
Assertion rprmirredlem ( 𝜑 → 𝑌 ∈ 𝑈 )

Proof

Step Hyp Ref Expression
1 rprmirredlem.1 ⊢ 𝐵 = ( Base ‘ 𝑅 )
2 rprmirredlem.2 ⊢ 𝑈 = ( Unit ‘ 𝑅 )
3 rprmirredlem.3 ⊢ 0 = ( 0g ‘ 𝑅 )
4 rprmirredlem.4 ⊢ · = ( .r ‘ 𝑅 )
5 rprmirredlem.5 ⊢ ∥ = ( ∥r ‘ 𝑅 )
6 rprmirredlem.6 ⊢ ( 𝜑 → 𝑅 ∈ IDomn )
7 rprmirredlem.7 ⊢ ( 𝜑 → 𝑄 ≠ 0 )
8 rprmirredlem.8 ⊢ ( 𝜑 → 𝑋 ∈ ( 𝐵 ∖ 𝑈 ) )
9 rprmirredlem.9 ⊢ ( 𝜑 → 𝑌 ∈ 𝐵 )
10 rprmirredlem.10 ⊢ ( 𝜑 → 𝑄 = ( 𝑋 · 𝑌 ) )
11 rprmirredlem.11 ⊢ ( 𝜑 → 𝑄 ∥ 𝑋 )
12 6 idomcringd ⊢ ( 𝜑 → 𝑅 ∈ CRing )
13 12 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑡 ∈ 𝐵 ) ∧ ( 𝑡 · 𝑄 ) = 𝑋 ) → 𝑅 ∈ CRing )
14 9 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑡 ∈ 𝐵 ) ∧ ( 𝑡 · 𝑄 ) = 𝑋 ) → 𝑌 ∈ 𝐵 )
15 13 crngringd ⊢ ( ( ( 𝜑 ∧ 𝑡 ∈ 𝐵 ) ∧ ( 𝑡 · 𝑄 ) = 𝑋 ) → 𝑅 ∈ Ring )
16 simplr ⊢ ( ( ( 𝜑 ∧ 𝑡 ∈ 𝐵 ) ∧ ( 𝑡 · 𝑄 ) = 𝑋 ) → 𝑡 ∈ 𝐵 )
17 1 4 15 16 14 ringcld ⊢ ( ( ( 𝜑 ∧ 𝑡 ∈ 𝐵 ) ∧ ( 𝑡 · 𝑄 ) = 𝑋 ) → ( 𝑡 · 𝑌 ) ∈ 𝐵 )
18 eqid ⊢ ( 1r ‘ 𝑅 ) = ( 1r ‘ 𝑅 )
19 1 18 ringidcl ⊢ ( 𝑅 ∈ Ring → ( 1r ‘ 𝑅 ) ∈ 𝐵 )
20 15 19 syl ⊢ ( ( ( 𝜑 ∧ 𝑡 ∈ 𝐵 ) ∧ ( 𝑡 · 𝑄 ) = 𝑋 ) → ( 1r ‘ 𝑅 ) ∈ 𝐵 )
21 1 5 4 dvdsr ⊢ ( 𝑄 ∥ 𝑋 ↔ ( 𝑄 ∈ 𝐵 ∧ ∃ 𝑡 ∈ 𝐵 ( 𝑡 · 𝑄 ) = 𝑋 ) )
22 11 21 sylib ⊢ ( 𝜑 → ( 𝑄 ∈ 𝐵 ∧ ∃ 𝑡 ∈ 𝐵 ( 𝑡 · 𝑄 ) = 𝑋 ) )
23 22 simpld ⊢ ( 𝜑 → 𝑄 ∈ 𝐵 )
24 23 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑡 ∈ 𝐵 ) ∧ ( 𝑡 · 𝑄 ) = 𝑋 ) → 𝑄 ∈ 𝐵 )
25 7 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑡 ∈ 𝐵 ) ∧ ( 𝑡 · 𝑄 ) = 𝑋 ) → 𝑄 ≠ 0 )
26 24 25 eldifsnd ⊢ ( ( ( 𝜑 ∧ 𝑡 ∈ 𝐵 ) ∧ ( 𝑡 · 𝑄 ) = 𝑋 ) → 𝑄 ∈ ( 𝐵 ∖ { 0 } ) )
27 6 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑡 ∈ 𝐵 ) ∧ ( 𝑡 · 𝑄 ) = 𝑋 ) → 𝑅 ∈ IDomn )
28 simpr ⊢ ( ( ( 𝜑 ∧ 𝑡 ∈ 𝐵 ) ∧ ( 𝑡 · 𝑄 ) = 𝑋 ) → ( 𝑡 · 𝑄 ) = 𝑋 )
29 28 oveq1d ⊢ ( ( ( 𝜑 ∧ 𝑡 ∈ 𝐵 ) ∧ ( 𝑡 · 𝑄 ) = 𝑋 ) → ( ( 𝑡 · 𝑄 ) · 𝑌 ) = ( 𝑋 · 𝑌 ) )
30 10 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑡 ∈ 𝐵 ) ∧ ( 𝑡 · 𝑄 ) = 𝑋 ) → 𝑄 = ( 𝑋 · 𝑌 ) )
31 29 30 eqtr4d ⊢ ( ( ( 𝜑 ∧ 𝑡 ∈ 𝐵 ) ∧ ( 𝑡 · 𝑄 ) = 𝑋 ) → ( ( 𝑡 · 𝑄 ) · 𝑌 ) = 𝑄 )
32 1 4 13 16 14 24 crng32d ⊢ ( ( ( 𝜑 ∧ 𝑡 ∈ 𝐵 ) ∧ ( 𝑡 · 𝑄 ) = 𝑋 ) → ( ( 𝑡 · 𝑌 ) · 𝑄 ) = ( ( 𝑡 · 𝑄 ) · 𝑌 ) )
33 1 4 18 15 24 ringlidmd ⊢ ( ( ( 𝜑 ∧ 𝑡 ∈ 𝐵 ) ∧ ( 𝑡 · 𝑄 ) = 𝑋 ) → ( ( 1r ‘ 𝑅 ) · 𝑄 ) = 𝑄 )
34 31 32 33 3eqtr4d ⊢ ( ( ( 𝜑 ∧ 𝑡 ∈ 𝐵 ) ∧ ( 𝑡 · 𝑄 ) = 𝑋 ) → ( ( 𝑡 · 𝑌 ) · 𝑄 ) = ( ( 1r ‘ 𝑅 ) · 𝑄 ) )
35 1 3 4 17 20 26 27 34 idomrcan ⊢ ( ( ( 𝜑 ∧ 𝑡 ∈ 𝐵 ) ∧ ( 𝑡 · 𝑄 ) = 𝑋 ) → ( 𝑡 · 𝑌 ) = ( 1r ‘ 𝑅 ) )
36 22 simprd ⊢ ( 𝜑 → ∃ 𝑡 ∈ 𝐵 ( 𝑡 · 𝑄 ) = 𝑋 )
37 35 36 reximddv3 ⊢ ( 𝜑 → ∃ 𝑡 ∈ 𝐵 ( 𝑡 · 𝑌 ) = ( 1r ‘ 𝑅 ) )
38 37 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑡 ∈ 𝐵 ) ∧ ( 𝑡 · 𝑄 ) = 𝑋 ) → ∃ 𝑡 ∈ 𝐵 ( 𝑡 · 𝑌 ) = ( 1r ‘ 𝑅 ) )
39 1 5 4 dvdsr ⊢ ( 𝑌 ∥ ( 1r ‘ 𝑅 ) ↔ ( 𝑌 ∈ 𝐵 ∧ ∃ 𝑡 ∈ 𝐵 ( 𝑡 · 𝑌 ) = ( 1r ‘ 𝑅 ) ) )
40 14 38 39 sylanbrc ⊢ ( ( ( 𝜑 ∧ 𝑡 ∈ 𝐵 ) ∧ ( 𝑡 · 𝑄 ) = 𝑋 ) → 𝑌 ∥ ( 1r ‘ 𝑅 ) )
41 2 18 5 crngunit ⊢ ( 𝑅 ∈ CRing → ( 𝑌 ∈ 𝑈 ↔ 𝑌 ∥ ( 1r ‘ 𝑅 ) ) )
42 41 biimpar ⊢ ( ( 𝑅 ∈ CRing ∧ 𝑌 ∥ ( 1r ‘ 𝑅 ) ) → 𝑌 ∈ 𝑈 )
43 13 40 42 syl2anc ⊢ ( ( ( 𝜑 ∧ 𝑡 ∈ 𝐵 ) ∧ ( 𝑡 · 𝑄 ) = 𝑋 ) → 𝑌 ∈ 𝑈 )
44 43 36 r19.29a ⊢ ( 𝜑 → 𝑌 ∈ 𝑈 )