Metamath Proof Explorer

Theorem divsclw

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

Ref Expression
Assertion divsclw ⊢ A ∈ No ∧ B ∈ No ∧ B ≠ 0 s ∧ ∃ x ∈ No B ⋅ s x = 1 s → A / su B ∈ No

Proof

Step Hyp Ref Expression
1 divsval ⊢ A ∈ No ∧ B ∈ No ∧ B ≠ 0 s → A / su B = ι y ∈ No | B ⋅ s y = A
2 1 adantr ⊢ A ∈ No ∧ B ∈ No ∧ B ≠ 0 s ∧ ∃ x ∈ No B ⋅ s x = 1 s → A / su B = ι y ∈ No | B ⋅ s y = A
3 3anrot ⊢ A ∈ No ∧ B ∈ No ∧ B ≠ 0 s ↔ B ∈ No ∧ B ≠ 0 s ∧ A ∈ No
4 noreceuw ⊢ B ∈ No ∧ B ≠ 0 s ∧ A ∈ No ∧ ∃ x ∈ No B ⋅ s x = 1 s → ∃! y ∈ No B ⋅ s y = A
5 3 4 sylanb ⊢ A ∈ No ∧ B ∈ No ∧ B ≠ 0 s ∧ ∃ x ∈ No B ⋅ s x = 1 s → ∃! y ∈ No B ⋅ s y = A
6 riotacl ⊢ ∃! y ∈ No B ⋅ s y = A → ι y ∈ No | B ⋅ s y = A ∈ No
7 5 6 syl ⊢ A ∈ No ∧ B ∈ No ∧ B ≠ 0 s ∧ ∃ x ∈ No B ⋅ s x = 1 s → ι y ∈ No | B ⋅ s y = A ∈ No
8 2 7 eqeltrd ⊢ A ∈ No ∧ B ∈ No ∧ B ≠ 0 s ∧ ∃ x ∈ No B ⋅ s x = 1 s → A / su B ∈ No