Theorem drngid

Description: A division ring's unit 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 ‘ 𝐺 ) )