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

Metamath Proof Explorer

Theorem drngid

Description: A division ring's unity is the identity element of its multiplicative group. (Contributed by NM, 7-Sep-2011)

Ref Expression
Hypotheses drngid.b ⊢ 𝐵 = ( Base ‘ 𝑅 )
drngid.z ⊢ 0 = ( 0g ‘ 𝑅 )
drngid.u ⊢ 1 = ( 1r ‘ 𝑅 )
drngid.g ⊢ 𝐺 = ( ( mulGrp ‘ 𝑅 ) ↾s ( 𝐵 ∖ { 0 } ) )
Assertion drngid ( 𝑅 ∈ DivRing → 1 = ( 0g ‘ 𝐺 ) )

Proof

Step Hyp Ref Expression
1 drngid.b ⊢ 𝐵 = ( Base ‘ 𝑅 )
2 drngid.z ⊢ 0 = ( 0g ‘ 𝑅 )
3 drngid.u ⊢ 1 = ( 1r ‘ 𝑅 )
4 drngid.g ⊢ 𝐺 = ( ( mulGrp ‘ 𝑅 ) ↾s ( 𝐵 ∖ { 0 } ) )
5 drngring ⊢ ( 𝑅 ∈ DivRing → 𝑅 ∈ Ring )
6 eqid ⊢ ( Unit ‘ 𝑅 ) = ( Unit ‘ 𝑅 )
7 eqid ⊢ ( ( mulGrp ‘ 𝑅 ) ↾s ( Unit ‘ 𝑅 ) ) = ( ( mulGrp ‘ 𝑅 ) ↾s ( Unit ‘ 𝑅 ) )
8 6 7 3 unitgrpid ⊢ ( 𝑅 ∈ Ring → 1 = ( 0g ‘ ( ( mulGrp ‘ 𝑅 ) ↾s ( Unit ‘ 𝑅 ) ) ) )
9 5 8 syl ⊢ ( 𝑅 ∈ DivRing → 1 = ( 0g ‘ ( ( mulGrp ‘ 𝑅 ) ↾s ( Unit ‘ 𝑅 ) ) ) )
10 1 6 2 isdrng ⊢ ( 𝑅 ∈ DivRing ↔ ( 𝑅 ∈ Ring ∧ ( Unit ‘ 𝑅 ) = ( 𝐵 ∖ { 0 } ) ) )
11 10 simprbi ⊢ ( 𝑅 ∈ DivRing → ( Unit ‘ 𝑅 ) = ( 𝐵 ∖ { 0 } ) )
12 11 oveq2d ⊢ ( 𝑅 ∈ DivRing → ( ( mulGrp ‘ 𝑅 ) ↾s ( Unit ‘ 𝑅 ) ) = ( ( mulGrp ‘ 𝑅 ) ↾s ( 𝐵 ∖ { 0 } ) ) )
13 12 4 eqtr4di ⊢ ( 𝑅 ∈ DivRing → ( ( mulGrp ‘ 𝑅 ) ↾s ( Unit ‘ 𝑅 ) ) = 𝐺 )
14 13 fveq2d ⊢ ( 𝑅 ∈ DivRing → ( 0g ‘ ( ( mulGrp ‘ 𝑅 ) ↾s ( Unit ‘ 𝑅 ) ) ) = ( 0g ‘ 𝐺 ) )
15 9 14 eqtrd ⊢ ( 𝑅 ∈ DivRing → 1 = ( 0g ‘ 𝐺 ) )