Metamath Proof Explorer

Theorem dvdsrpropd

Description: The divisibility relation depends only on the ring's base set and multiplication operation. (Contributed by Mario Carneiro, 26-Dec-2014)

Ref Expression
Hypotheses rngidpropd.1 ⊢φ→B=BaseK
rngidpropd.2 ⊢φ→B=BaseL
rngidpropd.3 ⊢φ∧x∈B∧y∈B→x⋅Ky=x⋅Ly
Assertion dvdsrpropd ⊢φ→∥r⁡K=∥r⁡L

Proof

Step Hyp Ref Expression
1 rngidpropd.1 ⊢φ→B=BaseK
2 rngidpropd.2 ⊢φ→B=BaseL
3 rngidpropd.3 ⊢φ∧x∈B∧y∈B→x⋅Ky=x⋅Ly
4 3 anassrs ⊢φ∧x∈B∧y∈B→x⋅Ky=x⋅Ly
5 4 eqeq1d ⊢φ∧x∈B∧y∈B→x⋅Ky=z↔x⋅Ly=z
6 5 an32s ⊢φ∧y∈B∧x∈B→x⋅Ky=z↔x⋅Ly=z
7 6 rexbidva ⊢φ∧y∈B→∃x∈Bx⋅Ky=z↔∃x∈Bx⋅Ly=z
8 7 pm5.32da ⊢φ→y∈B∧∃x∈Bx⋅Ky=z↔y∈B∧∃x∈Bx⋅Ly=z
9 1 eleq2d ⊢φ→y∈B↔y∈BaseK
10 1 rexeqdv ⊢φ→∃x∈Bx⋅Ky=z↔∃x∈BaseKx⋅Ky=z
11 9 10 anbi12d ⊢φ→y∈B∧∃x∈Bx⋅Ky=z↔y∈BaseK∧∃x∈BaseKx⋅Ky=z
12 2 eleq2d ⊢φ→y∈B↔y∈BaseL
13 2 rexeqdv ⊢φ→∃x∈Bx⋅Ly=z↔∃x∈BaseLx⋅Ly=z
14 12 13 anbi12d ⊢φ→y∈B∧∃x∈Bx⋅Ly=z↔y∈BaseL∧∃x∈BaseLx⋅Ly=z
15 8 11 14 3bitr3d ⊢φ→y∈BaseK∧∃x∈BaseKx⋅Ky=z↔y∈BaseL∧∃x∈BaseLx⋅Ly=z
16 15 opabbidv ⊢φ→yz|y∈BaseK∧∃x∈BaseKx⋅Ky=z=yz|y∈BaseL∧∃x∈BaseLx⋅Ly=z
17 eqid ⊢BaseK=BaseK
18 eqid ⊢∥r⁡K=∥r⁡K
19 eqid ⊢⋅K=⋅K
20 17 18 19 dvdsrval ⊢∥r⁡K=yz|y∈BaseK∧∃x∈BaseKx⋅Ky=z
21 eqid ⊢BaseL=BaseL
22 eqid ⊢∥r⁡L=∥r⁡L
23 eqid ⊢⋅L=⋅L
24 21 22 23 dvdsrval ⊢∥r⁡L=yz|y∈BaseL∧∃x∈BaseLx⋅Ly=z
25 16 20 24 3eqtr4g ⊢φ→∥r⁡K=∥r⁡L