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

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 4	unitpropd	⊢ ( 𝜑 → ( Unit ‘ 𝐾 ) = ( Unit ‘ 𝐿 ) )
6	5	adantr	⊢ ( ( 𝜑 ∧ 𝐾 ∈ Ring ) → ( Unit ‘ 𝐾 ) = ( Unit ‘ 𝐿 ) )
7	1 2	eqtr3d	⊢ ( 𝜑 → ( Base ‘ 𝐾 ) = ( Base ‘ 𝐿 ) )
8	7	adantr	⊢ ( ( 𝜑 ∧ 𝐾 ∈ Ring ) → ( Base ‘ 𝐾 ) = ( Base ‘ 𝐿 ) )
9	1	adantr	⊢ ( ( 𝜑 ∧ 𝐾 ∈ Ring ) → 𝐵 = ( Base ‘ 𝐾 ) )
10	2	adantr	⊢ ( ( 𝜑 ∧ 𝐾 ∈ Ring ) → 𝐵 = ( Base ‘ 𝐿 ) )
11	3	adantlr	⊢ ( ( ( 𝜑 ∧ 𝐾 ∈ Ring ) ∧ ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) ) → ( 𝑥 ( +g ‘ 𝐾 ) 𝑦 ) = ( 𝑥 ( +g ‘ 𝐿 ) 𝑦 ) )
12	9 10 11	grpidpropd	⊢ ( ( 𝜑 ∧ 𝐾 ∈ Ring ) → ( 0g ‘ 𝐾 ) = ( 0g ‘ 𝐿 ) )
13	12	sneqd	⊢ ( ( 𝜑 ∧ 𝐾 ∈ Ring ) → { ( 0g ‘ 𝐾 ) } = { ( 0g ‘ 𝐿 ) } )
14	8 13	difeq12d	⊢ ( ( 𝜑 ∧ 𝐾 ∈ Ring ) → ( ( Base ‘ 𝐾 ) ∖ { ( 0g ‘ 𝐾 ) } ) = ( ( Base ‘ 𝐿 ) ∖ { ( 0g ‘ 𝐿 ) } ) )
15	6 14	eqeq12d	⊢ ( ( 𝜑 ∧ 𝐾 ∈ Ring ) → ( ( Unit ‘ 𝐾 ) = ( ( Base ‘ 𝐾 ) ∖ { ( 0g ‘ 𝐾 ) } ) ↔ ( Unit ‘ 𝐿 ) = ( ( Base ‘ 𝐿 ) ∖ { ( 0g ‘ 𝐿 ) } ) ) )
16	15	pm5.32da	⊢ ( 𝜑 → ( ( 𝐾 ∈ Ring ∧ ( Unit ‘ 𝐾 ) = ( ( Base ‘ 𝐾 ) ∖ { ( 0g ‘ 𝐾 ) } ) ) ↔ ( 𝐾 ∈ Ring ∧ ( Unit ‘ 𝐿 ) = ( ( Base ‘ 𝐿 ) ∖ { ( 0g ‘ 𝐿 ) } ) ) ) )
17	1 2 3 4	ringpropd	⊢ ( 𝜑 → ( 𝐾 ∈ Ring ↔ 𝐿 ∈ Ring ) )
18	17	anbi1d	⊢ ( 𝜑 → ( ( 𝐾 ∈ Ring ∧ ( Unit ‘ 𝐿 ) = ( ( Base ‘ 𝐿 ) ∖ { ( 0g ‘ 𝐿 ) } ) ) ↔ ( 𝐿 ∈ Ring ∧ ( Unit ‘ 𝐿 ) = ( ( Base ‘ 𝐿 ) ∖ { ( 0g ‘ 𝐿 ) } ) ) ) )
19	16 18	bitrd	⊢ ( 𝜑 → ( ( 𝐾 ∈ Ring ∧ ( Unit ‘ 𝐾 ) = ( ( Base ‘ 𝐾 ) ∖ { ( 0g ‘ 𝐾 ) } ) ) ↔ ( 𝐿 ∈ Ring ∧ ( Unit ‘ 𝐿 ) = ( ( Base ‘ 𝐿 ) ∖ { ( 0g ‘ 𝐿 ) } ) ) ) )
20		eqid	⊢ ( Base ‘ 𝐾 ) = ( Base ‘ 𝐾 )
21		eqid	⊢ ( Unit ‘ 𝐾 ) = ( Unit ‘ 𝐾 )
22		eqid	⊢ ( 0g ‘ 𝐾 ) = ( 0g ‘ 𝐾 )
23	20 21 22	isdrng	⊢ ( 𝐾 ∈ DivRing ↔ ( 𝐾 ∈ Ring ∧ ( Unit ‘ 𝐾 ) = ( ( Base ‘ 𝐾 ) ∖ { ( 0g ‘ 𝐾 ) } ) ) )
24		eqid	⊢ ( Base ‘ 𝐿 ) = ( Base ‘ 𝐿 )
25		eqid	⊢ ( Unit ‘ 𝐿 ) = ( Unit ‘ 𝐿 )
26		eqid	⊢ ( 0g ‘ 𝐿 ) = ( 0g ‘ 𝐿 )
27	24 25 26	isdrng	⊢ ( 𝐿 ∈ DivRing ↔ ( 𝐿 ∈ Ring ∧ ( Unit ‘ 𝐿 ) = ( ( Base ‘ 𝐿 ) ∖ { ( 0g ‘ 𝐿 ) } ) ) )
28	19 23 27	3bitr4g	⊢ ( 𝜑 → ( 𝐾 ∈ DivRing ↔ 𝐿 ∈ DivRing ) )