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

Metamath Proof Explorer

Theorem ring1eq0

Description: If one and zero are equal, then any two elements of a ring are equal. Alternately, every ring has one distinct from zero except the zero ring containing the single element { 0 } . (Contributed by Mario Carneiro, 10-Sep-2014)

Ref Expression
Hypotheses ring1eq0.b ⊢ 𝐵 = ( Base ‘ 𝑅 )
ring1eq0.u ⊢ 1 = ( 1r ‘ 𝑅 )
ring1eq0.z ⊢ 0 = ( 0g ‘ 𝑅 )
Assertion ring1eq0 ( ( 𝑅 ∈ Ring ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) → ( 1 = 0 → 𝑋 = 𝑌 ) )

Proof

Step Hyp Ref Expression
1 ring1eq0.b ⊢ 𝐵 = ( Base ‘ 𝑅 )
2 ring1eq0.u ⊢ 1 = ( 1r ‘ 𝑅 )
3 ring1eq0.z ⊢ 0 = ( 0g ‘ 𝑅 )
4 simpr ⊢ ( ( ( 𝑅 ∈ Ring ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) ∧ 1 = 0 ) → 1 = 0 )
5 4 oveq1d ⊢ ( ( ( 𝑅 ∈ Ring ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) ∧ 1 = 0 ) → ( 1 ( .r ‘ 𝑅 ) 𝑋 ) = ( 0 ( .r ‘ 𝑅 ) 𝑋 ) )
6 4 oveq1d ⊢ ( ( ( 𝑅 ∈ Ring ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) ∧ 1 = 0 ) → ( 1 ( .r ‘ 𝑅 ) 𝑌 ) = ( 0 ( .r ‘ 𝑅 ) 𝑌 ) )
7 simpl1 ⊢ ( ( ( 𝑅 ∈ Ring ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) ∧ 1 = 0 ) → 𝑅 ∈ Ring )
8 simpl2 ⊢ ( ( ( 𝑅 ∈ Ring ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) ∧ 1 = 0 ) → 𝑋 ∈ 𝐵 )
9 eqid ⊢ ( .r ‘ 𝑅 ) = ( .r ‘ 𝑅 )
10 1 9 3 ringlz ⊢ ( ( 𝑅 ∈ Ring ∧ 𝑋 ∈ 𝐵 ) → ( 0 ( .r ‘ 𝑅 ) 𝑋 ) = 0 )
11 7 8 10 syl2anc ⊢ ( ( ( 𝑅 ∈ Ring ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) ∧ 1 = 0 ) → ( 0 ( .r ‘ 𝑅 ) 𝑋 ) = 0 )
12 simpl3 ⊢ ( ( ( 𝑅 ∈ Ring ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) ∧ 1 = 0 ) → 𝑌 ∈ 𝐵 )
13 1 9 3 ringlz ⊢ ( ( 𝑅 ∈ Ring ∧ 𝑌 ∈ 𝐵 ) → ( 0 ( .r ‘ 𝑅 ) 𝑌 ) = 0 )
14 7 12 13 syl2anc ⊢ ( ( ( 𝑅 ∈ Ring ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) ∧ 1 = 0 ) → ( 0 ( .r ‘ 𝑅 ) 𝑌 ) = 0 )
15 11 14 eqtr4d ⊢ ( ( ( 𝑅 ∈ Ring ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) ∧ 1 = 0 ) → ( 0 ( .r ‘ 𝑅 ) 𝑋 ) = ( 0 ( .r ‘ 𝑅 ) 𝑌 ) )
16 6 15 eqtr4d ⊢ ( ( ( 𝑅 ∈ Ring ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) ∧ 1 = 0 ) → ( 1 ( .r ‘ 𝑅 ) 𝑌 ) = ( 0 ( .r ‘ 𝑅 ) 𝑋 ) )
17 5 16 eqtr4d ⊢ ( ( ( 𝑅 ∈ Ring ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) ∧ 1 = 0 ) → ( 1 ( .r ‘ 𝑅 ) 𝑋 ) = ( 1 ( .r ‘ 𝑅 ) 𝑌 ) )
18 1 9 2 ringlidm ⊢ ( ( 𝑅 ∈ Ring ∧ 𝑋 ∈ 𝐵 ) → ( 1 ( .r ‘ 𝑅 ) 𝑋 ) = 𝑋 )
19 7 8 18 syl2anc ⊢ ( ( ( 𝑅 ∈ Ring ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) ∧ 1 = 0 ) → ( 1 ( .r ‘ 𝑅 ) 𝑋 ) = 𝑋 )
20 1 9 2 ringlidm ⊢ ( ( 𝑅 ∈ Ring ∧ 𝑌 ∈ 𝐵 ) → ( 1 ( .r ‘ 𝑅 ) 𝑌 ) = 𝑌 )
21 7 12 20 syl2anc ⊢ ( ( ( 𝑅 ∈ Ring ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) ∧ 1 = 0 ) → ( 1 ( .r ‘ 𝑅 ) 𝑌 ) = 𝑌 )
22 17 19 21 3eqtr3d ⊢ ( ( ( 𝑅 ∈ Ring ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) ∧ 1 = 0 ) → 𝑋 = 𝑌 )
23 22 ex ⊢ ( ( 𝑅 ∈ Ring ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) → ( 1 = 0 → 𝑋 = 𝑌 ) )