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 = Base K
rngidpropd.2 ⊢ φ → B = Base L
rngidpropd.3 ⊢ φ ∧ x ∈ B ∧ y ∈ B → x ⋅ K y = x ⋅ L y
Assertion dvdsrpropd ⊢ φ → ∥ r ⁡ K = ∥ r ⁡ L

Proof

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