Theorem isdrng

Description: The predicate "is a division ring". (Contributed by NM, 18-Oct-2012) (Revised by Mario Carneiro, 2-Dec-2014)

	Ref	Expression
Hypotheses	isdrng.b	⊢ 𝐵 = ( Base ‘ 𝑅 )
	isdrng.u	⊢ 𝑈 = ( Unit ‘ 𝑅 )
	isdrng.z	⊢ 0 = ( 0g ‘ 𝑅 )
Assertion	isdrng	⊢ ( 𝑅 ∈ DivRing ↔ ( 𝑅 ∈ Ring ∧ 𝑈 = ( 𝐵 ∖ { 0 } ) ) )

Proof

Step	Hyp	Ref	Expression
1		isdrng.b	⊢ 𝐵 = ( Base ‘ 𝑅 )
2		isdrng.u	⊢ 𝑈 = ( Unit ‘ 𝑅 )
3		isdrng.z	⊢ 0 = ( 0g ‘ 𝑅 )
4		fveq2	⊢ ( 𝑟 = 𝑅 → ( Unit ‘ 𝑟 ) = ( Unit ‘ 𝑅 ) )
5	4 2	eqtr4di	⊢ ( 𝑟 = 𝑅 → ( Unit ‘ 𝑟 ) = 𝑈 )
6		fveq2	⊢ ( 𝑟 = 𝑅 → ( Base ‘ 𝑟 ) = ( Base ‘ 𝑅 ) )
7	6 1	eqtr4di	⊢ ( 𝑟 = 𝑅 → ( Base ‘ 𝑟 ) = 𝐵 )
8		fveq2	⊢ ( 𝑟 = 𝑅 → ( 0g ‘ 𝑟 ) = ( 0g ‘ 𝑅 ) )
9	8 3	eqtr4di	⊢ ( 𝑟 = 𝑅 → ( 0g ‘ 𝑟 ) = 0 )
10	9	sneqd	⊢ ( 𝑟 = 𝑅 → { ( 0g ‘ 𝑟 ) } = { 0 } )
11	7 10	difeq12d	⊢ ( 𝑟 = 𝑅 → ( ( Base ‘ 𝑟 ) ∖ { ( 0g ‘ 𝑟 ) } ) = ( 𝐵 ∖ { 0 } ) )
12	5 11	eqeq12d	⊢ ( 𝑟 = 𝑅 → ( ( Unit ‘ 𝑟 ) = ( ( Base ‘ 𝑟 ) ∖ { ( 0g ‘ 𝑟 ) } ) ↔ 𝑈 = ( 𝐵 ∖ { 0 } ) ) )
13		df-drng	⊢ DivRing = { 𝑟 ∈ Ring ∣ ( Unit ‘ 𝑟 ) = ( ( Base ‘ 𝑟 ) ∖ { ( 0g ‘ 𝑟 ) } ) }
14	12 13	elrab2	⊢ ( 𝑅 ∈ DivRing ↔ ( 𝑅 ∈ Ring ∧ 𝑈 = ( 𝐵 ∖ { 0 } ) ) )