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

Metamath Proof Explorer

Theorem ring1ne0

Description: If a ring has at least two elements, its one and zero are different. (Contributed by AV, 13-Apr-2019)

Ref Expression
Hypotheses ring1ne0.b ⊢ 𝐵 = ( Base ‘ 𝑅 )
ring1ne0.u ⊢ 1 = ( 1r ‘ 𝑅 )
ring1ne0.z ⊢ 0 = ( 0g ‘ 𝑅 )
Assertion ring1ne0 ( ( 𝑅 ∈ Ring ∧ 1 < ( ♯ ‘ 𝐵 ) ) → 1 ≠ 0 )

Proof

Step Hyp Ref Expression
1 ring1ne0.b ⊢ 𝐵 = ( Base ‘ 𝑅 )
2 ring1ne0.u ⊢ 1 = ( 1r ‘ 𝑅 )
3 ring1ne0.z ⊢ 0 = ( 0g ‘ 𝑅 )
4 1 fvexi ⊢ 𝐵 ∈ V
5 hashgt12el ⊢ ( ( 𝐵 ∈ V ∧ 1 < ( ♯ ‘ 𝐵 ) ) → ∃ 𝑥 ∈ 𝐵 ∃ 𝑦 ∈ 𝐵 𝑥 ≠ 𝑦 )
6 4 5 mpan ⊢ ( 1 < ( ♯ ‘ 𝐵 ) → ∃ 𝑥 ∈ 𝐵 ∃ 𝑦 ∈ 𝐵 𝑥 ≠ 𝑦 )
7 6 adantl ⊢ ( ( 𝑅 ∈ Ring ∧ 1 < ( ♯ ‘ 𝐵 ) ) → ∃ 𝑥 ∈ 𝐵 ∃ 𝑦 ∈ 𝐵 𝑥 ≠ 𝑦 )
8 1 2 3 ring1eq0 ⊢ ( ( 𝑅 ∈ Ring ∧ 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) → ( 1 = 0 → 𝑥 = 𝑦 ) )
9 8 necon3d ⊢ ( ( 𝑅 ∈ Ring ∧ 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) → ( 𝑥 ≠ 𝑦 → 1 ≠ 0 ) )
10 9 3expib ⊢ ( 𝑅 ∈ Ring → ( ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) → ( 𝑥 ≠ 𝑦 → 1 ≠ 0 ) ) )
11 10 adantr ⊢ ( ( 𝑅 ∈ Ring ∧ 1 < ( ♯ ‘ 𝐵 ) ) → ( ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) → ( 𝑥 ≠ 𝑦 → 1 ≠ 0 ) ) )
12 11 com3l ⊢ ( ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) → ( 𝑥 ≠ 𝑦 → ( ( 𝑅 ∈ Ring ∧ 1 < ( ♯ ‘ 𝐵 ) ) → 1 ≠ 0 ) ) )
13 12 rexlimivv ⊢ ( ∃ 𝑥 ∈ 𝐵 ∃ 𝑦 ∈ 𝐵 𝑥 ≠ 𝑦 → ( ( 𝑅 ∈ Ring ∧ 1 < ( ♯ ‘ 𝐵 ) ) → 1 ≠ 0 ) )
14 7 13 mpcom ⊢ ( ( 𝑅 ∈ Ring ∧ 1 < ( ♯ ‘ 𝐵 ) ) → 1 ≠ 0 )