Metamath Proof Explorer

Theorem rngoueqz

Description: Obsolete as of 23-Jan-2020. Use 0ring01eqbi instead. In a unital ring the zero equals the ring unity iff the ring is the zero ring. (Contributed by FL, 14-Feb-2010) (New usage is discouraged.) (Proof modification is discouraged.)

Ref Expression
Hypotheses uznzr.1 ⊢ 𝐺 = ( 1st ‘ 𝑅 )
uznzr.2 ⊢ 𝐻 = ( 2nd ‘ 𝑅 )
uznzr.3 ⊢ 𝑍 = ( GId ‘ 𝐺 )
uznzr.4 ⊢ 𝑈 = ( GId ‘ 𝐻 )
uznzr.5 ⊢ 𝑋 = ran 𝐺
Assertion rngoueqz ( 𝑅 ∈ RingOps → ( 𝑋 ≈ 1o ↔ 𝑈 = 𝑍 ) )

Proof

Step Hyp Ref Expression
1 uznzr.1 ⊢ 𝐺 = ( 1st ‘ 𝑅 )
2 uznzr.2 ⊢ 𝐻 = ( 2nd ‘ 𝑅 )
3 uznzr.3 ⊢ 𝑍 = ( GId ‘ 𝐺 )
4 uznzr.4 ⊢ 𝑈 = ( GId ‘ 𝐻 )
5 uznzr.5 ⊢ 𝑋 = ran 𝐺
6 1 5 3 rngo0cl ⊢ ( 𝑅 ∈ RingOps → 𝑍 ∈ 𝑋 )
7 en1eqsn ⊢ ( ( 𝑍 ∈ 𝑋 ∧ 𝑋 ≈ 1o ) → 𝑋 = { 𝑍 } )
8 1 rneqi ⊢ ran 𝐺 = ran ( 1st ‘ 𝑅 )
9 8 2 4 rngo1cl ⊢ ( 𝑅 ∈ RingOps → 𝑈 ∈ ran 𝐺 )
10 eleq2 ⊢ ( 𝑋 = { 𝑍 } → ( 𝑈 ∈ 𝑋 ↔ 𝑈 ∈ { 𝑍 } ) )
11 10 biimpd ⊢ ( 𝑋 = { 𝑍 } → ( 𝑈 ∈ 𝑋 → 𝑈 ∈ { 𝑍 } ) )
12 elsni ⊢ ( 𝑈 ∈ { 𝑍 } → 𝑈 = 𝑍 )
13 11 12 syl6com ⊢ ( 𝑈 ∈ 𝑋 → ( 𝑋 = { 𝑍 } → 𝑈 = 𝑍 ) )
14 5 eqcomi ⊢ ran 𝐺 = 𝑋
15 13 14 eleq2s ⊢ ( 𝑈 ∈ ran 𝐺 → ( 𝑋 = { 𝑍 } → 𝑈 = 𝑍 ) )
16 9 15 syl ⊢ ( 𝑅 ∈ RingOps → ( 𝑋 = { 𝑍 } → 𝑈 = 𝑍 ) )
17 7 16 syl5com ⊢ ( ( 𝑍 ∈ 𝑋 ∧ 𝑋 ≈ 1o ) → ( 𝑅 ∈ RingOps → 𝑈 = 𝑍 ) )
18 17 ex ⊢ ( 𝑍 ∈ 𝑋 → ( 𝑋 ≈ 1o → ( 𝑅 ∈ RingOps → 𝑈 = 𝑍 ) ) )
19 18 com23 ⊢ ( 𝑍 ∈ 𝑋 → ( 𝑅 ∈ RingOps → ( 𝑋 ≈ 1o → 𝑈 = 𝑍 ) ) )
20 6 19 mpcom ⊢ ( 𝑅 ∈ RingOps → ( 𝑋 ≈ 1o → 𝑈 = 𝑍 ) )
21 1 5 rngone0 ⊢ ( 𝑅 ∈ RingOps → 𝑋 ≠ ∅ )
22 oveq2 ⊢ ( 𝑈 = 𝑍 → ( 𝑥 𝐻 𝑈 ) = ( 𝑥 𝐻 𝑍 ) )
23 22 ralrimivw ⊢ ( 𝑈 = 𝑍 → ∀ 𝑥 ∈ 𝑋 ( 𝑥 𝐻 𝑈 ) = ( 𝑥 𝐻 𝑍 ) )
24 3 5 1 2 rngorz ⊢ ( ( 𝑅 ∈ RingOps ∧ 𝑥 ∈ 𝑋 ) → ( 𝑥 𝐻 𝑍 ) = 𝑍 )
25 24 ralrimiva ⊢ ( 𝑅 ∈ RingOps → ∀ 𝑥 ∈ 𝑋 ( 𝑥 𝐻 𝑍 ) = 𝑍 )
26 5 8 eqtri ⊢ 𝑋 = ran ( 1st ‘ 𝑅 )
27 2 26 4 rngoridm ⊢ ( ( 𝑅 ∈ RingOps ∧ 𝑥 ∈ 𝑋 ) → ( 𝑥 𝐻 𝑈 ) = 𝑥 )
28 27 ralrimiva ⊢ ( 𝑅 ∈ RingOps → ∀ 𝑥 ∈ 𝑋 ( 𝑥 𝐻 𝑈 ) = 𝑥 )
29 r19.26 ⊢ ( ∀ 𝑥 ∈ 𝑋 ( ( 𝑥 𝐻 𝑈 ) = 𝑥 ∧ ( 𝑥 𝐻 𝑈 ) = ( 𝑥 𝐻 𝑍 ) ) ↔ ( ∀ 𝑥 ∈ 𝑋 ( 𝑥 𝐻 𝑈 ) = 𝑥 ∧ ∀ 𝑥 ∈ 𝑋 ( 𝑥 𝐻 𝑈 ) = ( 𝑥 𝐻 𝑍 ) ) )
30 r19.26 ⊢ ( ∀ 𝑥 ∈ 𝑋 ( ( ( 𝑥 𝐻 𝑈 ) = 𝑥 ∧ ( 𝑥 𝐻 𝑈 ) = ( 𝑥 𝐻 𝑍 ) ) ∧ ( 𝑥 𝐻 𝑍 ) = 𝑍 ) ↔ ( ∀ 𝑥 ∈ 𝑋 ( ( 𝑥 𝐻 𝑈 ) = 𝑥 ∧ ( 𝑥 𝐻 𝑈 ) = ( 𝑥 𝐻 𝑍 ) ) ∧ ∀ 𝑥 ∈ 𝑋 ( 𝑥 𝐻 𝑍 ) = 𝑍 ) )
31 eqtr ⊢ ( ( 𝑥 = ( 𝑥 𝐻 𝑈 ) ∧ ( 𝑥 𝐻 𝑈 ) = ( 𝑥 𝐻 𝑍 ) ) → 𝑥 = ( 𝑥 𝐻 𝑍 ) )
32 eqtr ⊢ ( ( 𝑥 = ( 𝑥 𝐻 𝑍 ) ∧ ( 𝑥 𝐻 𝑍 ) = 𝑍 ) → 𝑥 = 𝑍 )
33 32 ex ⊢ ( 𝑥 = ( 𝑥 𝐻 𝑍 ) → ( ( 𝑥 𝐻 𝑍 ) = 𝑍 → 𝑥 = 𝑍 ) )
34 31 33 syl ⊢ ( ( 𝑥 = ( 𝑥 𝐻 𝑈 ) ∧ ( 𝑥 𝐻 𝑈 ) = ( 𝑥 𝐻 𝑍 ) ) → ( ( 𝑥 𝐻 𝑍 ) = 𝑍 → 𝑥 = 𝑍 ) )
35 34 ex ⊢ ( 𝑥 = ( 𝑥 𝐻 𝑈 ) → ( ( 𝑥 𝐻 𝑈 ) = ( 𝑥 𝐻 𝑍 ) → ( ( 𝑥 𝐻 𝑍 ) = 𝑍 → 𝑥 = 𝑍 ) ) )
36 35 eqcoms ⊢ ( ( 𝑥 𝐻 𝑈 ) = 𝑥 → ( ( 𝑥 𝐻 𝑈 ) = ( 𝑥 𝐻 𝑍 ) → ( ( 𝑥 𝐻 𝑍 ) = 𝑍 → 𝑥 = 𝑍 ) ) )
37 36 imp31 ⊢ ( ( ( ( 𝑥 𝐻 𝑈 ) = 𝑥 ∧ ( 𝑥 𝐻 𝑈 ) = ( 𝑥 𝐻 𝑍 ) ) ∧ ( 𝑥 𝐻 𝑍 ) = 𝑍 ) → 𝑥 = 𝑍 )
38 37 ralimi ⊢ ( ∀ 𝑥 ∈ 𝑋 ( ( ( 𝑥 𝐻 𝑈 ) = 𝑥 ∧ ( 𝑥 𝐻 𝑈 ) = ( 𝑥 𝐻 𝑍 ) ) ∧ ( 𝑥 𝐻 𝑍 ) = 𝑍 ) → ∀ 𝑥 ∈ 𝑋 𝑥 = 𝑍 )
39 eqsn ⊢ ( 𝑋 ≠ ∅ → ( 𝑋 = { 𝑍 } ↔ ∀ 𝑥 ∈ 𝑋 𝑥 = 𝑍 ) )
40 ensn1g ⊢ ( 𝑍 ∈ 𝑋 → { 𝑍 } ≈ 1o )
41 6 40 syl ⊢ ( 𝑅 ∈ RingOps → { 𝑍 } ≈ 1o )
42 breq1 ⊢ ( 𝑋 = { 𝑍 } → ( 𝑋 ≈ 1o ↔ { 𝑍 } ≈ 1o ) )
43 41 42 imbitrrid ⊢ ( 𝑋 = { 𝑍 } → ( 𝑅 ∈ RingOps → 𝑋 ≈ 1o ) )
44 39 43 biimtrrdi ⊢ ( 𝑋 ≠ ∅ → ( ∀ 𝑥 ∈ 𝑋 𝑥 = 𝑍 → ( 𝑅 ∈ RingOps → 𝑋 ≈ 1o ) ) )
45 44 com3l ⊢ ( ∀ 𝑥 ∈ 𝑋 𝑥 = 𝑍 → ( 𝑅 ∈ RingOps → ( 𝑋 ≠ ∅ → 𝑋 ≈ 1o ) ) )
46 38 45 syl ⊢ ( ∀ 𝑥 ∈ 𝑋 ( ( ( 𝑥 𝐻 𝑈 ) = 𝑥 ∧ ( 𝑥 𝐻 𝑈 ) = ( 𝑥 𝐻 𝑍 ) ) ∧ ( 𝑥 𝐻 𝑍 ) = 𝑍 ) → ( 𝑅 ∈ RingOps → ( 𝑋 ≠ ∅ → 𝑋 ≈ 1o ) ) )
47 30 46 sylbir ⊢ ( ( ∀ 𝑥 ∈ 𝑋 ( ( 𝑥 𝐻 𝑈 ) = 𝑥 ∧ ( 𝑥 𝐻 𝑈 ) = ( 𝑥 𝐻 𝑍 ) ) ∧ ∀ 𝑥 ∈ 𝑋 ( 𝑥 𝐻 𝑍 ) = 𝑍 ) → ( 𝑅 ∈ RingOps → ( 𝑋 ≠ ∅ → 𝑋 ≈ 1o ) ) )
48 47 ex ⊢ ( ∀ 𝑥 ∈ 𝑋 ( ( 𝑥 𝐻 𝑈 ) = 𝑥 ∧ ( 𝑥 𝐻 𝑈 ) = ( 𝑥 𝐻 𝑍 ) ) → ( ∀ 𝑥 ∈ 𝑋 ( 𝑥 𝐻 𝑍 ) = 𝑍 → ( 𝑅 ∈ RingOps → ( 𝑋 ≠ ∅ → 𝑋 ≈ 1o ) ) ) )
49 29 48 sylbir ⊢ ( ( ∀ 𝑥 ∈ 𝑋 ( 𝑥 𝐻 𝑈 ) = 𝑥 ∧ ∀ 𝑥 ∈ 𝑋 ( 𝑥 𝐻 𝑈 ) = ( 𝑥 𝐻 𝑍 ) ) → ( ∀ 𝑥 ∈ 𝑋 ( 𝑥 𝐻 𝑍 ) = 𝑍 → ( 𝑅 ∈ RingOps → ( 𝑋 ≠ ∅ → 𝑋 ≈ 1o ) ) ) )
50 49 ex ⊢ ( ∀ 𝑥 ∈ 𝑋 ( 𝑥 𝐻 𝑈 ) = 𝑥 → ( ∀ 𝑥 ∈ 𝑋 ( 𝑥 𝐻 𝑈 ) = ( 𝑥 𝐻 𝑍 ) → ( ∀ 𝑥 ∈ 𝑋 ( 𝑥 𝐻 𝑍 ) = 𝑍 → ( 𝑅 ∈ RingOps → ( 𝑋 ≠ ∅ → 𝑋 ≈ 1o ) ) ) ) )
51 50 com24 ⊢ ( ∀ 𝑥 ∈ 𝑋 ( 𝑥 𝐻 𝑈 ) = 𝑥 → ( 𝑅 ∈ RingOps → ( ∀ 𝑥 ∈ 𝑋 ( 𝑥 𝐻 𝑍 ) = 𝑍 → ( ∀ 𝑥 ∈ 𝑋 ( 𝑥 𝐻 𝑈 ) = ( 𝑥 𝐻 𝑍 ) → ( 𝑋 ≠ ∅ → 𝑋 ≈ 1o ) ) ) ) )
52 28 51 mpcom ⊢ ( 𝑅 ∈ RingOps → ( ∀ 𝑥 ∈ 𝑋 ( 𝑥 𝐻 𝑍 ) = 𝑍 → ( ∀ 𝑥 ∈ 𝑋 ( 𝑥 𝐻 𝑈 ) = ( 𝑥 𝐻 𝑍 ) → ( 𝑋 ≠ ∅ → 𝑋 ≈ 1o ) ) ) )
53 25 52 mpd ⊢ ( 𝑅 ∈ RingOps → ( ∀ 𝑥 ∈ 𝑋 ( 𝑥 𝐻 𝑈 ) = ( 𝑥 𝐻 𝑍 ) → ( 𝑋 ≠ ∅ → 𝑋 ≈ 1o ) ) )
54 23 53 syl5com ⊢ ( 𝑈 = 𝑍 → ( 𝑅 ∈ RingOps → ( 𝑋 ≠ ∅ → 𝑋 ≈ 1o ) ) )
55 54 com13 ⊢ ( 𝑋 ≠ ∅ → ( 𝑅 ∈ RingOps → ( 𝑈 = 𝑍 → 𝑋 ≈ 1o ) ) )
56 21 55 mpcom ⊢ ( 𝑅 ∈ RingOps → ( 𝑈 = 𝑍 → 𝑋 ≈ 1o ) )
57 20 56 impbid ⊢ ( 𝑅 ∈ RingOps → ( 𝑋 ≈ 1o ↔ 𝑈 = 𝑍 ) )