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

Metamath Proof Explorer

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