Theorem 0unit

Description: The additive identity is a unit if and only if 1 = 0 , i.e. we are in the zero ring. (Contributed by Mario Carneiro, 4-Dec-2014)

	Ref	Expression
Hypotheses	0unit.1	⊢ 𝑈 = ( Unit ‘ 𝑅 )
	0unit.2	⊢ 0 = ( 0g ‘ 𝑅 )
	0unit.3	⊢ 1 = ( 1r ‘ 𝑅 )
Assertion	0unit	⊢ ( 𝑅 ∈ Ring → ( 0 ∈ 𝑈 ↔ 1 = 0 ) )

Proof

Step	Hyp	Ref	Expression
1		0unit.1	⊢ 𝑈 = ( Unit ‘ 𝑅 )
2		0unit.2	⊢ 0 = ( 0g ‘ 𝑅 )
3		0unit.3	⊢ 1 = ( 1r ‘ 𝑅 )
4		eqid	⊢ ( invr ‘ 𝑅 ) = ( invr ‘ 𝑅 )
5		eqid	⊢ ( .r ‘ 𝑅 ) = ( .r ‘ 𝑅 )
6	1 4 5 3	unitrinv	⊢ ( ( 𝑅 ∈ Ring ∧ 0 ∈ 𝑈 ) → ( 0 ( .r ‘ 𝑅 ) ( ( invr ‘ 𝑅 ) ‘ 0 ) ) = 1 )
7		eqid	⊢ ( Base ‘ 𝑅 ) = ( Base ‘ 𝑅 )
8	1 4 7	ringinvcl	⊢ ( ( 𝑅 ∈ Ring ∧ 0 ∈ 𝑈 ) → ( ( invr ‘ 𝑅 ) ‘ 0 ) ∈ ( Base ‘ 𝑅 ) )
9	7 5 2	ringlz	⊢ ( ( 𝑅 ∈ Ring ∧ ( ( invr ‘ 𝑅 ) ‘ 0 ) ∈ ( Base ‘ 𝑅 ) ) → ( 0 ( .r ‘ 𝑅 ) ( ( invr ‘ 𝑅 ) ‘ 0 ) ) = 0 )
10	8 9	syldan	⊢ ( ( 𝑅 ∈ Ring ∧ 0 ∈ 𝑈 ) → ( 0 ( .r ‘ 𝑅 ) ( ( invr ‘ 𝑅 ) ‘ 0 ) ) = 0 )
11	6 10	eqtr3d	⊢ ( ( 𝑅 ∈ Ring ∧ 0 ∈ 𝑈 ) → 1 = 0 )
12		simpr	⊢ ( ( 𝑅 ∈ Ring ∧ 1 = 0 ) → 1 = 0 )
13	1 3	1unit	⊢ ( 𝑅 ∈ Ring → 1 ∈ 𝑈 )
14	13	adantr	⊢ ( ( 𝑅 ∈ Ring ∧ 1 = 0 ) → 1 ∈ 𝑈 )
15	12 14	eqeltrrd	⊢ ( ( 𝑅 ∈ Ring ∧ 1 = 0 ) → 0 ∈ 𝑈 )
16	11 15	impbida	⊢ ( 𝑅 ∈ Ring → ( 0 ∈ 𝑈 ↔ 1 = 0 ) )