This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem nzrpropd

Description: If two structures have the same components (properties), one is a nonzero ring iff the other one is. (Contributed by SN, 21-Jun-2025)

Ref Expression
Hypotheses nzrpropd.1 ⊢ φ → B = Base K
nzrpropd.2 ⊢ φ → B = Base L
nzrpropd.3 ⊢ φ ∧ x ∈ B ∧ y ∈ B → x + K y = x + L y
nzrpropd.4 ⊢ φ ∧ x ∈ B ∧ y ∈ B → x ⋅ K y = x ⋅ L y
Assertion nzrpropd ⊢ φ → K ∈ NzRing ↔ L ∈ NzRing

Proof

Step Hyp Ref Expression
1 nzrpropd.1 ⊢ φ → B = Base K
2 nzrpropd.2 ⊢ φ → B = Base L
3 nzrpropd.3 ⊢ φ ∧ x ∈ B ∧ y ∈ B → x + K y = x + L y
4 nzrpropd.4 ⊢ φ ∧ x ∈ B ∧ y ∈ B → x ⋅ K y = x ⋅ L y
5 1 2 3 4 ringpropd ⊢ φ → K ∈ Ring ↔ L ∈ Ring
6 1 2 4 rngidpropd ⊢ φ → 1 K = 1 L
7 1 2 3 grpidpropd ⊢ φ → 0 K = 0 L
8 6 7 neeq12d ⊢ φ → 1 K ≠ 0 K ↔ 1 L ≠ 0 L
9 5 8 anbi12d ⊢ φ → K ∈ Ring ∧ 1 K ≠ 0 K ↔ L ∈ Ring ∧ 1 L ≠ 0 L
10 eqid ⊢ 1 K = 1 K
11 eqid ⊢ 0 K = 0 K
12 10 11 isnzr ⊢ K ∈ NzRing ↔ K ∈ Ring ∧ 1 K ≠ 0 K
13 eqid ⊢ 1 L = 1 L
14 eqid ⊢ 0 L = 0 L
15 13 14 isnzr ⊢ L ∈ NzRing ↔ L ∈ Ring ∧ 1 L ≠ 0 L
16 9 12 15 3bitr4g ⊢ φ → K ∈ NzRing ↔ L ∈ NzRing