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

Metamath Proof Explorer

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 } ) ) )