Metamath Proof Explorer


Theorem divsclw

Description: Weak division closure law. (Contributed by Scott Fenton, 12-Mar-2025)

Ref Expression
Assertion divsclw ( ( ( 𝐴 No 𝐵 No 𝐵 ≠ 0s ) ∧ ∃ 𝑥 No ( 𝐵 ·s 𝑥 ) = 1s ) → ( 𝐴 /su 𝐵 ) ∈ No )

Proof

Step Hyp Ref Expression
1 divsval ( ( 𝐴 No 𝐵 No 𝐵 ≠ 0s ) → ( 𝐴 /su 𝐵 ) = ( 𝑦 No ( 𝐵 ·s 𝑦 ) = 𝐴 ) )
2 1 adantr ( ( ( 𝐴 No 𝐵 No 𝐵 ≠ 0s ) ∧ ∃ 𝑥 No ( 𝐵 ·s 𝑥 ) = 1s ) → ( 𝐴 /su 𝐵 ) = ( 𝑦 No ( 𝐵 ·s 𝑦 ) = 𝐴 ) )
3 3anrot ( ( 𝐴 No 𝐵 No 𝐵 ≠ 0s ) ↔ ( 𝐵 No 𝐵 ≠ 0s𝐴 No ) )
4 noreceuw ( ( ( 𝐵 No 𝐵 ≠ 0s𝐴 No ) ∧ ∃ 𝑥 No ( 𝐵 ·s 𝑥 ) = 1s ) → ∃! 𝑦 No ( 𝐵 ·s 𝑦 ) = 𝐴 )
5 3 4 sylanb ( ( ( 𝐴 No 𝐵 No 𝐵 ≠ 0s ) ∧ ∃ 𝑥 No ( 𝐵 ·s 𝑥 ) = 1s ) → ∃! 𝑦 No ( 𝐵 ·s 𝑦 ) = 𝐴 )
6 riotacl ( ∃! 𝑦 No ( 𝐵 ·s 𝑦 ) = 𝐴 → ( 𝑦 No ( 𝐵 ·s 𝑦 ) = 𝐴 ) ∈ No )
7 5 6 syl ( ( ( 𝐴 No 𝐵 No 𝐵 ≠ 0s ) ∧ ∃ 𝑥 No ( 𝐵 ·s 𝑥 ) = 1s ) → ( 𝑦 No ( 𝐵 ·s 𝑦 ) = 𝐴 ) ∈ No )
8 2 7 eqeltrd ( ( ( 𝐴 No 𝐵 No 𝐵 ≠ 0s ) ∧ ∃ 𝑥 No ( 𝐵 ·s 𝑥 ) = 1s ) → ( 𝐴 /su 𝐵 ) ∈ No )