Metamath Proof Explorer

Theorem isnzr2hash

Description: Equivalent characterization of nonzero rings: they have at least two elements. Analogous to isnzr2 . (Contributed by AV, 14-Apr-2019)

Ref Expression
Hypothesis isnzr2hash.b ⊢ 𝐵 = ( Base ‘ 𝑅 )
Assertion isnzr2hash ( 𝑅 ∈ NzRing ↔ ( 𝑅 ∈ Ring ∧ 1 < ( ♯ ‘ 𝐵 ) ) )

Proof

Step Hyp Ref Expression
1 isnzr2hash.b ⊢ 𝐵 = ( Base ‘ 𝑅 )
2 eqid ⊢ ( 1r ‘ 𝑅 ) = ( 1r ‘ 𝑅 )
3 eqid ⊢ ( 0g ‘ 𝑅 ) = ( 0g ‘ 𝑅 )
4 2 3 isnzr ⊢ ( 𝑅 ∈ NzRing ↔ ( 𝑅 ∈ Ring ∧ ( 1r ‘ 𝑅 ) ≠ ( 0g ‘ 𝑅 ) ) )
5 1 2 ringidcl ⊢ ( 𝑅 ∈ Ring → ( 1r ‘ 𝑅 ) ∈ 𝐵 )
6 1 3 ring0cl ⊢ ( 𝑅 ∈ Ring → ( 0g ‘ 𝑅 ) ∈ 𝐵 )
7 1xr ⊢ 1 ∈ ℝ*
8 7 a1i ⊢ ( ( ( ( 1r ‘ 𝑅 ) ∈ 𝐵 ∧ ( 0g ‘ 𝑅 ) ∈ 𝐵 ) ∧ ( 1r ‘ 𝑅 ) ≠ ( 0g ‘ 𝑅 ) ) → 1 ∈ ℝ* )
9 prex ⊢ { ( 1r ‘ 𝑅 ) , ( 0g ‘ 𝑅 ) } ∈ V
10 hashxrcl ⊢ ( { ( 1r ‘ 𝑅 ) , ( 0g ‘ 𝑅 ) } ∈ V → ( ♯ ‘ { ( 1r ‘ 𝑅 ) , ( 0g ‘ 𝑅 ) } ) ∈ ℝ* )
11 9 10 mp1i ⊢ ( ( ( ( 1r ‘ 𝑅 ) ∈ 𝐵 ∧ ( 0g ‘ 𝑅 ) ∈ 𝐵 ) ∧ ( 1r ‘ 𝑅 ) ≠ ( 0g ‘ 𝑅 ) ) → ( ♯ ‘ { ( 1r ‘ 𝑅 ) , ( 0g ‘ 𝑅 ) } ) ∈ ℝ* )
12 1 fvexi ⊢ 𝐵 ∈ V
13 hashxrcl ⊢ ( 𝐵 ∈ V → ( ♯ ‘ 𝐵 ) ∈ ℝ* )
14 12 13 mp1i ⊢ ( ( ( ( 1r ‘ 𝑅 ) ∈ 𝐵 ∧ ( 0g ‘ 𝑅 ) ∈ 𝐵 ) ∧ ( 1r ‘ 𝑅 ) ≠ ( 0g ‘ 𝑅 ) ) → ( ♯ ‘ 𝐵 ) ∈ ℝ* )
15 1lt2 ⊢ 1 < 2
16 hashprg ⊢ ( ( ( 1r ‘ 𝑅 ) ∈ 𝐵 ∧ ( 0g ‘ 𝑅 ) ∈ 𝐵 ) → ( ( 1r ‘ 𝑅 ) ≠ ( 0g ‘ 𝑅 ) ↔ ( ♯ ‘ { ( 1r ‘ 𝑅 ) , ( 0g ‘ 𝑅 ) } ) = 2 ) )
17 16 biimpa ⊢ ( ( ( ( 1r ‘ 𝑅 ) ∈ 𝐵 ∧ ( 0g ‘ 𝑅 ) ∈ 𝐵 ) ∧ ( 1r ‘ 𝑅 ) ≠ ( 0g ‘ 𝑅 ) ) → ( ♯ ‘ { ( 1r ‘ 𝑅 ) , ( 0g ‘ 𝑅 ) } ) = 2 )
18 15 17 breqtrrid ⊢ ( ( ( ( 1r ‘ 𝑅 ) ∈ 𝐵 ∧ ( 0g ‘ 𝑅 ) ∈ 𝐵 ) ∧ ( 1r ‘ 𝑅 ) ≠ ( 0g ‘ 𝑅 ) ) → 1 < ( ♯ ‘ { ( 1r ‘ 𝑅 ) , ( 0g ‘ 𝑅 ) } ) )
19 simpl ⊢ ( ( ( ( 1r ‘ 𝑅 ) ∈ 𝐵 ∧ ( 0g ‘ 𝑅 ) ∈ 𝐵 ) ∧ ( 1r ‘ 𝑅 ) ≠ ( 0g ‘ 𝑅 ) ) → ( ( 1r ‘ 𝑅 ) ∈ 𝐵 ∧ ( 0g ‘ 𝑅 ) ∈ 𝐵 ) )
20 fvex ⊢ ( 1r ‘ 𝑅 ) ∈ V
21 fvex ⊢ ( 0g ‘ 𝑅 ) ∈ V
22 20 21 prss ⊢ ( ( ( 1r ‘ 𝑅 ) ∈ 𝐵 ∧ ( 0g ‘ 𝑅 ) ∈ 𝐵 ) ↔ { ( 1r ‘ 𝑅 ) , ( 0g ‘ 𝑅 ) } ⊆ 𝐵 )
23 19 22 sylib ⊢ ( ( ( ( 1r ‘ 𝑅 ) ∈ 𝐵 ∧ ( 0g ‘ 𝑅 ) ∈ 𝐵 ) ∧ ( 1r ‘ 𝑅 ) ≠ ( 0g ‘ 𝑅 ) ) → { ( 1r ‘ 𝑅 ) , ( 0g ‘ 𝑅 ) } ⊆ 𝐵 )
24 hashss ⊢ ( ( 𝐵 ∈ V ∧ { ( 1r ‘ 𝑅 ) , ( 0g ‘ 𝑅 ) } ⊆ 𝐵 ) → ( ♯ ‘ { ( 1r ‘ 𝑅 ) , ( 0g ‘ 𝑅 ) } ) ≤ ( ♯ ‘ 𝐵 ) )
25 12 23 24 sylancr ⊢ ( ( ( ( 1r ‘ 𝑅 ) ∈ 𝐵 ∧ ( 0g ‘ 𝑅 ) ∈ 𝐵 ) ∧ ( 1r ‘ 𝑅 ) ≠ ( 0g ‘ 𝑅 ) ) → ( ♯ ‘ { ( 1r ‘ 𝑅 ) , ( 0g ‘ 𝑅 ) } ) ≤ ( ♯ ‘ 𝐵 ) )
26 8 11 14 18 25 xrltletrd ⊢ ( ( ( ( 1r ‘ 𝑅 ) ∈ 𝐵 ∧ ( 0g ‘ 𝑅 ) ∈ 𝐵 ) ∧ ( 1r ‘ 𝑅 ) ≠ ( 0g ‘ 𝑅 ) ) → 1 < ( ♯ ‘ 𝐵 ) )
27 26 ex ⊢ ( ( ( 1r ‘ 𝑅 ) ∈ 𝐵 ∧ ( 0g ‘ 𝑅 ) ∈ 𝐵 ) → ( ( 1r ‘ 𝑅 ) ≠ ( 0g ‘ 𝑅 ) → 1 < ( ♯ ‘ 𝐵 ) ) )
28 5 6 27 syl2anc ⊢ ( 𝑅 ∈ Ring → ( ( 1r ‘ 𝑅 ) ≠ ( 0g ‘ 𝑅 ) → 1 < ( ♯ ‘ 𝐵 ) ) )
29 28 imdistani ⊢ ( ( 𝑅 ∈ Ring ∧ ( 1r ‘ 𝑅 ) ≠ ( 0g ‘ 𝑅 ) ) → ( 𝑅 ∈ Ring ∧ 1 < ( ♯ ‘ 𝐵 ) ) )
30 simpl ⊢ ( ( 𝑅 ∈ Ring ∧ 1 < ( ♯ ‘ 𝐵 ) ) → 𝑅 ∈ Ring )
31 1 2 3 ring1ne0 ⊢ ( ( 𝑅 ∈ Ring ∧ 1 < ( ♯ ‘ 𝐵 ) ) → ( 1r ‘ 𝑅 ) ≠ ( 0g ‘ 𝑅 ) )
32 30 31 jca ⊢ ( ( 𝑅 ∈ Ring ∧ 1 < ( ♯ ‘ 𝐵 ) ) → ( 𝑅 ∈ Ring ∧ ( 1r ‘ 𝑅 ) ≠ ( 0g ‘ 𝑅 ) ) )
33 29 32 impbii ⊢ ( ( 𝑅 ∈ Ring ∧ ( 1r ‘ 𝑅 ) ≠ ( 0g ‘ 𝑅 ) ) ↔ ( 𝑅 ∈ Ring ∧ 1 < ( ♯ ‘ 𝐵 ) ) )
34 4 33 bitri ⊢ ( 𝑅 ∈ NzRing ↔ ( 𝑅 ∈ Ring ∧ 1 < ( ♯ ‘ 𝐵 ) ) )