drngpropd

Description: If two structures have the same group components (properties), one is a division ring iff the other one is. (Contributed by Mario Carneiro, 27-Jun-2015)

	Ref	Expression
Hypotheses	drngpropd.1	$⊢ φ \to B = {Base}_{K}$
	drngpropd.2	$⊢ φ \to B = {Base}_{L}$
	drngpropd.3	$⊢ (φ \land (x \in B \land y \in B)) \to x +_{K} y = x +_{L} y$
	drngpropd.4	$⊢ (φ \land (x \in B \land y \in B)) \to x \cdot_{K} y = x \cdot_{L} y$
Assertion	drngpropd	$⊢ φ \to (K \in DivRing \leftrightarrow L \in DivRing)$

Proof

Step	Hyp	Ref	Expression
1		drngpropd.1	$⊢ φ \to B = {Base}_{K}$
2		drngpropd.2	$⊢ φ \to B = {Base}_{L}$
3		drngpropd.3	$⊢ (φ \land (x \in B \land y \in B)) \to x +_{K} y = x +_{L} y$
4		drngpropd.4	$⊢ (φ \land (x \in B \land y \in B)) \to x \cdot_{K} y = x \cdot_{L} y$
5	1 2 4	unitpropd	$⊢ φ \to Unit (K) = Unit (L)$
6	5	adantr	$⊢ (φ \land K \in Ring) \to Unit (K) = Unit (L)$
7	1 2	eqtr3d	$⊢ φ \to {Base}_{K} = {Base}_{L}$
8	7	adantr	$⊢ (φ \land K \in Ring) \to {Base}_{K} = {Base}_{L}$
9	1	adantr	$⊢ (φ \land K \in Ring) \to B = {Base}_{K}$
10	2	adantr	$⊢ (φ \land K \in Ring) \to B = {Base}_{L}$
11	3	adantlr	$⊢ ((φ \land K \in Ring) \land (x \in B \land y \in B)) \to x +_{K} y = x +_{L} y$
12	9 10 11	grpidpropd	$⊢ (φ \land K \in Ring) \to 0_{K} = 0_{L}$
13	12	sneqd	$⊢ (φ \land K \in Ring) \to \{0_{K}\} = \{0_{L}\}$
14	8 13	difeq12d	$⊢ (φ \land K \in Ring) \to {Base}_{K} ∖ \{0_{K}\} = {Base}_{L} ∖ \{0_{L}\}$
15	6 14	eqeq12d	$⊢ (φ \land K \in Ring) \to (Unit (K) = {Base}_{K} ∖ \{0_{K}\} \leftrightarrow Unit (L) = {Base}_{L} ∖ \{0_{L}\})$
16	15	pm5.32da	$⊢ φ \to ((K \in Ring \land Unit (K) = {Base}_{K} ∖ \{0_{K}\}) \leftrightarrow (K \in Ring \land Unit (L) = {Base}_{L} ∖ \{0_{L}\}))$
17	1 2 3 4	ringpropd	$⊢ φ \to (K \in Ring \leftrightarrow L \in Ring)$
18	17	anbi1d	$⊢ φ \to ((K \in Ring \land Unit (L) = {Base}_{L} ∖ \{0_{L}\}) \leftrightarrow (L \in Ring \land Unit (L) = {Base}_{L} ∖ \{0_{L}\}))$
19	16 18	bitrd	$⊢ φ \to ((K \in Ring \land Unit (K) = {Base}_{K} ∖ \{0_{K}\}) \leftrightarrow (L \in Ring \land Unit (L) = {Base}_{L} ∖ \{0_{L}\}))$
20		eqid	$⊢ {Base}_{K} = {Base}_{K}$
21		eqid	$⊢ Unit (K) = Unit (K)$
22		eqid	$⊢ 0_{K} = 0_{K}$
23	20 21 22	isdrng	$⊢ K \in DivRing \leftrightarrow (K \in Ring \land Unit (K) = {Base}_{K} ∖ \{0_{K}\})$
24		eqid	$⊢ {Base}_{L} = {Base}_{L}$
25		eqid	$⊢ Unit (L) = Unit (L)$
26		eqid	$⊢ 0_{L} = 0_{L}$
27	24 25 26	isdrng	$⊢ L \in DivRing \leftrightarrow (L \in Ring \land Unit (L) = {Base}_{L} ∖ \{0_{L}\})$
28	19 23 27	3bitr4g	$⊢ φ \to (K \in DivRing \leftrightarrow L \in DivRing)$

Metamath Proof Explorer

Theorem drngpropd

Proof