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 )