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 ( 𝜑𝐵 = ( Base ‘ 𝐾 ) )
drngpropd.2 ( 𝜑𝐵 = ( Base ‘ 𝐿 ) )
drngpropd.3 ( ( 𝜑 ∧ ( 𝑥𝐵𝑦𝐵 ) ) → ( 𝑥 ( +g𝐾 ) 𝑦 ) = ( 𝑥 ( +g𝐿 ) 𝑦 ) )
drngpropd.4 ( ( 𝜑 ∧ ( 𝑥𝐵𝑦𝐵 ) ) → ( 𝑥 ( .r𝐾 ) 𝑦 ) = ( 𝑥 ( .r𝐿 ) 𝑦 ) )
Assertion fldpropd ( 𝜑 → ( 𝐾 ∈ Field ↔ 𝐿 ∈ Field ) )

Proof

Step Hyp Ref Expression
1 drngpropd.1 ( 𝜑𝐵 = ( Base ‘ 𝐾 ) )
2 drngpropd.2 ( 𝜑𝐵 = ( Base ‘ 𝐿 ) )
3 drngpropd.3 ( ( 𝜑 ∧ ( 𝑥𝐵𝑦𝐵 ) ) → ( 𝑥 ( +g𝐾 ) 𝑦 ) = ( 𝑥 ( +g𝐿 ) 𝑦 ) )
4 drngpropd.4 ( ( 𝜑 ∧ ( 𝑥𝐵𝑦𝐵 ) ) → ( 𝑥 ( .r𝐾 ) 𝑦 ) = ( 𝑥 ( .r𝐿 ) 𝑦 ) )
5 1 2 3 4 drngpropd ( 𝜑 → ( 𝐾 ∈ DivRing ↔ 𝐿 ∈ DivRing ) )
6 1 2 3 4 crngpropd ( 𝜑 → ( 𝐾 ∈ CRing ↔ 𝐿 ∈ CRing ) )
7 5 6 anbi12d ( 𝜑 → ( ( 𝐾 ∈ DivRing ∧ 𝐾 ∈ CRing ) ↔ ( 𝐿 ∈ DivRing ∧ 𝐿 ∈ CRing ) ) )
8 isfld ( 𝐾 ∈ Field ↔ ( 𝐾 ∈ DivRing ∧ 𝐾 ∈ CRing ) )
9 isfld ( 𝐿 ∈ Field ↔ ( 𝐿 ∈ DivRing ∧ 𝐿 ∈ CRing ) )
10 7 8 9 3bitr4g ( 𝜑 → ( 𝐾 ∈ Field ↔ 𝐿 ∈ Field ) )