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

Metamath Proof Explorer

Theorem fldpropd

Description: If two structures have the same group components (properties), one is a field iff the other one is. (Contributed by Mario Carneiro, 8-Feb-2015)

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

Proof

Step Hyp Ref Expression
1 drngpropd.1 ⊢ φ → B = Base K
2 drngpropd.2 ⊢ φ → B = Base L
3 drngpropd.3 ⊢ φ ∧ x ∈ B ∧ y ∈ B → x + K y = x + L y
4 drngpropd.4 ⊢ φ ∧ x ∈ B ∧ y ∈ B → x ⋅ K y = x ⋅ L y
5 1 2 3 4 drngpropd ⊢ φ → K ∈ DivRing ↔ L ∈ DivRing
6 1 2 3 4 crngpropd ⊢ φ → K ∈ CRing ↔ L ∈ CRing
7 5 6 anbi12d ⊢ φ → K ∈ DivRing ∧ K ∈ CRing ↔ L ∈ DivRing ∧ L ∈ CRing
8 isfld ⊢ K ∈ Field ↔ K ∈ DivRing ∧ K ∈ CRing
9 isfld ⊢ L ∈ Field ↔ L ∈ DivRing ∧ L ∈ CRing
10 7 8 9 3bitr4g ⊢ φ → K ∈ Field ↔ L ∈ Field