Metamath Proof Explorer

Theorem dvrunz

Description: Obsolete theorem, use drngunz instead. In a division ring the ring unit is different from the zero. (Contributed by FL, 14-Feb-2010) (Revised by Mario Carneiro, 15-Dec-2013) (Proof modification is discouraged.) (New usage is discouraged.)

Ref Expression
Hypotheses dvrunz.1 ⊢ 𝐺 = ( 1st ‘ 𝑅 )
dvrunz.2 ⊢ 𝐻 = ( 2nd ‘ 𝑅 )
dvrunz.3 ⊢ 𝑋 = ran 𝐺
dvrunz.4 ⊢ 𝑍 = ( GId ‘ 𝐺 )
dvrunz.5 ⊢ 𝑈 = ( GId ‘ 𝐻 )
Assertion dvrunz ( 𝑅 ∈ DivRingOps → 𝑈 ≠ 𝑍 )

Proof

Step Hyp Ref Expression
1 dvrunz.1 ⊢ 𝐺 = ( 1st ‘ 𝑅 )
2 dvrunz.2 ⊢ 𝐻 = ( 2nd ‘ 𝑅 )
3 dvrunz.3 ⊢ 𝑋 = ran 𝐺
4 dvrunz.4 ⊢ 𝑍 = ( GId ‘ 𝐺 )
5 dvrunz.5 ⊢ 𝑈 = ( GId ‘ 𝐻 )
6 4 fvexi ⊢ 𝑍 ∈ V
7 6 zrdivrng ⊢ ¬ ⟨ { ⟨ ⟨ 𝑍 , 𝑍 ⟩ , 𝑍 ⟩ } , { ⟨ ⟨ 𝑍 , 𝑍 ⟩ , 𝑍 ⟩ } ⟩ ∈ DivRingOps
8 1 2 3 4 drngoi ⊢ ( 𝑅 ∈ DivRingOps → ( 𝑅 ∈ RingOps ∧ ( 𝐻 ↾ ( ( 𝑋 ∖ { 𝑍 } ) × ( 𝑋 ∖ { 𝑍 } ) ) ) ∈ GrpOp ) )
9 8 simpld ⊢ ( 𝑅 ∈ DivRingOps → 𝑅 ∈ RingOps )
10 1 2 4 5 3 rngoueqz ⊢ ( 𝑅 ∈ RingOps → ( 𝑋 ≈ 1o ↔ 𝑈 = 𝑍 ) )
11 9 10 syl ⊢ ( 𝑅 ∈ DivRingOps → ( 𝑋 ≈ 1o ↔ 𝑈 = 𝑍 ) )
12 1 3 4 rngosn6 ⊢ ( 𝑅 ∈ RingOps → ( 𝑋 ≈ 1o ↔ 𝑅 = ⟨ { ⟨ ⟨ 𝑍 , 𝑍 ⟩ , 𝑍 ⟩ } , { ⟨ ⟨ 𝑍 , 𝑍 ⟩ , 𝑍 ⟩ } ⟩ ) )
13 9 12 syl ⊢ ( 𝑅 ∈ DivRingOps → ( 𝑋 ≈ 1o ↔ 𝑅 = ⟨ { ⟨ ⟨ 𝑍 , 𝑍 ⟩ , 𝑍 ⟩ } , { ⟨ ⟨ 𝑍 , 𝑍 ⟩ , 𝑍 ⟩ } ⟩ ) )
14 eleq1 ⊢ ( 𝑅 = ⟨ { ⟨ ⟨ 𝑍 , 𝑍 ⟩ , 𝑍 ⟩ } , { ⟨ ⟨ 𝑍 , 𝑍 ⟩ , 𝑍 ⟩ } ⟩ → ( 𝑅 ∈ DivRingOps ↔ ⟨ { ⟨ ⟨ 𝑍 , 𝑍 ⟩ , 𝑍 ⟩ } , { ⟨ ⟨ 𝑍 , 𝑍 ⟩ , 𝑍 ⟩ } ⟩ ∈ DivRingOps ) )
15 14 biimpd ⊢ ( 𝑅 = ⟨ { ⟨ ⟨ 𝑍 , 𝑍 ⟩ , 𝑍 ⟩ } , { ⟨ ⟨ 𝑍 , 𝑍 ⟩ , 𝑍 ⟩ } ⟩ → ( 𝑅 ∈ DivRingOps → ⟨ { ⟨ ⟨ 𝑍 , 𝑍 ⟩ , 𝑍 ⟩ } , { ⟨ ⟨ 𝑍 , 𝑍 ⟩ , 𝑍 ⟩ } ⟩ ∈ DivRingOps ) )
16 13 15 biimtrdi ⊢ ( 𝑅 ∈ DivRingOps → ( 𝑋 ≈ 1o → ( 𝑅 ∈ DivRingOps → ⟨ { ⟨ ⟨ 𝑍 , 𝑍 ⟩ , 𝑍 ⟩ } , { ⟨ ⟨ 𝑍 , 𝑍 ⟩ , 𝑍 ⟩ } ⟩ ∈ DivRingOps ) ) )
17 16 pm2.43a ⊢ ( 𝑅 ∈ DivRingOps → ( 𝑋 ≈ 1o → ⟨ { ⟨ ⟨ 𝑍 , 𝑍 ⟩ , 𝑍 ⟩ } , { ⟨ ⟨ 𝑍 , 𝑍 ⟩ , 𝑍 ⟩ } ⟩ ∈ DivRingOps ) )
18 11 17 sylbird ⊢ ( 𝑅 ∈ DivRingOps → ( 𝑈 = 𝑍 → ⟨ { ⟨ ⟨ 𝑍 , 𝑍 ⟩ , 𝑍 ⟩ } , { ⟨ ⟨ 𝑍 , 𝑍 ⟩ , 𝑍 ⟩ } ⟩ ∈ DivRingOps ) )
19 18 necon3bd ⊢ ( 𝑅 ∈ DivRingOps → ( ¬ ⟨ { ⟨ ⟨ 𝑍 , 𝑍 ⟩ , 𝑍 ⟩ } , { ⟨ ⟨ 𝑍 , 𝑍 ⟩ , 𝑍 ⟩ } ⟩ ∈ DivRingOps → 𝑈 ≠ 𝑍 ) )
20 7 19 mpi ⊢ ( 𝑅 ∈ DivRingOps → 𝑈 ≠ 𝑍 )