Metamath Proof Explorer

Theorem 01eq0ringOLD

Description: Obsolete version of 01eq0ring as of 23-Feb-2025. (Contributed by AV, 16-Apr-2019) (Proof modification is discouraged.) (New usage is discouraged.)

Ref Expression
Hypotheses 0ring.b ⊢ 𝐵 = ( Base ‘ 𝑅 )
0ring.0 ⊢ 0 = ( 0g ‘ 𝑅 )
0ring01eq.1 ⊢ 1 = ( 1r ‘ 𝑅 )
Assertion 01eq0ringOLD ( ( 𝑅 ∈ Ring ∧ 0 = 1 ) → 𝐵 = { 0 } )

Proof

Step Hyp Ref Expression
1 0ring.b ⊢ 𝐵 = ( Base ‘ 𝑅 )
2 0ring.0 ⊢ 0 = ( 0g ‘ 𝑅 )
3 0ring01eq.1 ⊢ 1 = ( 1r ‘ 𝑅 )
4 1 fvexi ⊢ 𝐵 ∈ V
5 hashv01gt1 ⊢ ( 𝐵 ∈ V → ( ( ♯ ‘ 𝐵 ) = 0 ∨ ( ♯ ‘ 𝐵 ) = 1 ∨ 1 < ( ♯ ‘ 𝐵 ) ) )
6 4 5 ax-mp ⊢ ( ( ♯ ‘ 𝐵 ) = 0 ∨ ( ♯ ‘ 𝐵 ) = 1 ∨ 1 < ( ♯ ‘ 𝐵 ) )
7 hasheq0 ⊢ ( 𝐵 ∈ V → ( ( ♯ ‘ 𝐵 ) = 0 ↔ 𝐵 = ∅ ) )
8 4 7 ax-mp ⊢ ( ( ♯ ‘ 𝐵 ) = 0 ↔ 𝐵 = ∅ )
9 ne0i ⊢ ( 0 ∈ 𝐵 → 𝐵 ≠ ∅ )
10 eqneqall ⊢ ( 𝐵 = ∅ → ( 𝐵 ≠ ∅ → ( ( ♯ ‘ 𝐵 ) ≠ 1 → 0 ≠ 1 ) ) )
11 9 10 syl5com ⊢ ( 0 ∈ 𝐵 → ( 𝐵 = ∅ → ( ( ♯ ‘ 𝐵 ) ≠ 1 → 0 ≠ 1 ) ) )
12 8 11 biimtrid ⊢ ( 0 ∈ 𝐵 → ( ( ♯ ‘ 𝐵 ) = 0 → ( ( ♯ ‘ 𝐵 ) ≠ 1 → 0 ≠ 1 ) ) )
13 1 2 ring0cl ⊢ ( 𝑅 ∈ Ring → 0 ∈ 𝐵 )
14 12 13 syl11 ⊢ ( ( ♯ ‘ 𝐵 ) = 0 → ( 𝑅 ∈ Ring → ( ( ♯ ‘ 𝐵 ) ≠ 1 → 0 ≠ 1 ) ) )
15 eqneqall ⊢ ( ( ♯ ‘ 𝐵 ) = 1 → ( ( ♯ ‘ 𝐵 ) ≠ 1 → 0 ≠ 1 ) )
16 15 a1d ⊢ ( ( ♯ ‘ 𝐵 ) = 1 → ( 𝑅 ∈ Ring → ( ( ♯ ‘ 𝐵 ) ≠ 1 → 0 ≠ 1 ) ) )
17 1 3 2 ring1ne0 ⊢ ( ( 𝑅 ∈ Ring ∧ 1 < ( ♯ ‘ 𝐵 ) ) → 1 ≠ 0 )
18 17 necomd ⊢ ( ( 𝑅 ∈ Ring ∧ 1 < ( ♯ ‘ 𝐵 ) ) → 0 ≠ 1 )
19 18 ex ⊢ ( 𝑅 ∈ Ring → ( 1 < ( ♯ ‘ 𝐵 ) → 0 ≠ 1 ) )
20 19 a1i ⊢ ( ( ♯ ‘ 𝐵 ) ≠ 1 → ( 𝑅 ∈ Ring → ( 1 < ( ♯ ‘ 𝐵 ) → 0 ≠ 1 ) ) )
21 20 com13 ⊢ ( 1 < ( ♯ ‘ 𝐵 ) → ( 𝑅 ∈ Ring → ( ( ♯ ‘ 𝐵 ) ≠ 1 → 0 ≠ 1 ) ) )
22 14 16 21 3jaoi ⊢ ( ( ( ♯ ‘ 𝐵 ) = 0 ∨ ( ♯ ‘ 𝐵 ) = 1 ∨ 1 < ( ♯ ‘ 𝐵 ) ) → ( 𝑅 ∈ Ring → ( ( ♯ ‘ 𝐵 ) ≠ 1 → 0 ≠ 1 ) ) )
23 6 22 ax-mp ⊢ ( 𝑅 ∈ Ring → ( ( ♯ ‘ 𝐵 ) ≠ 1 → 0 ≠ 1 ) )
24 23 necon4d ⊢ ( 𝑅 ∈ Ring → ( 0 = 1 → ( ♯ ‘ 𝐵 ) = 1 ) )
25 24 imp ⊢ ( ( 𝑅 ∈ Ring ∧ 0 = 1 ) → ( ♯ ‘ 𝐵 ) = 1 )
26 1 2 0ring ⊢ ( ( 𝑅 ∈ Ring ∧ ( ♯ ‘ 𝐵 ) = 1 ) → 𝐵 = { 0 } )
27 25 26 syldan ⊢ ( ( 𝑅 ∈ Ring ∧ 0 = 1 ) → 𝐵 = { 0 } )