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 ⊢ G = 1 st ⁡ R
dvrunz.2 ⊢ H = 2 nd ⁡ R
dvrunz.3 ⊢ X = ran ⁡ G
dvrunz.4 ⊢ Z = GId ⁡ G
dvrunz.5 ⊢ U = GId ⁡ H
Assertion dvrunz ⊢ R ∈ DivRingOps → U ≠ Z

Proof

Step Hyp Ref Expression
1 dvrunz.1 ⊢ G = 1 st ⁡ R
2 dvrunz.2 ⊢ H = 2 nd ⁡ R
3 dvrunz.3 ⊢ X = ran ⁡ G
4 dvrunz.4 ⊢ Z = GId ⁡ G
5 dvrunz.5 ⊢ U = GId ⁡ H
6 4 fvexi ⊢ Z ∈ V
7 6 zrdivrng ⊢ ¬ Z Z Z Z Z Z ∈ DivRingOps
8 1 2 3 4 drngoi ⊢ R ∈ DivRingOps → R ∈ RingOps ∧ H ↾ X ∖ Z × X ∖ Z ∈ GrpOp
9 8 simpld ⊢ R ∈ DivRingOps → R ∈ RingOps
10 1 2 4 5 3 rngoueqz ⊢ R ∈ RingOps → X ≈ 1 𝑜 ↔ U = Z
11 9 10 syl ⊢ R ∈ DivRingOps → X ≈ 1 𝑜 ↔ U = Z
12 1 3 4 rngosn6 ⊢ R ∈ RingOps → X ≈ 1 𝑜 ↔ R = Z Z Z Z Z Z
13 9 12 syl ⊢ R ∈ DivRingOps → X ≈ 1 𝑜 ↔ R = Z Z Z Z Z Z
14 eleq1 ⊢ R = Z Z Z Z Z Z → R ∈ DivRingOps ↔ Z Z Z Z Z Z ∈ DivRingOps
15 14 biimpd ⊢ R = Z Z Z Z Z Z → R ∈ DivRingOps → Z Z Z Z Z Z ∈ DivRingOps
16 13 15 biimtrdi ⊢ R ∈ DivRingOps → X ≈ 1 𝑜 → R ∈ DivRingOps → Z Z Z Z Z Z ∈ DivRingOps
17 16 pm2.43a ⊢ R ∈ DivRingOps → X ≈ 1 𝑜 → Z Z Z Z Z Z ∈ DivRingOps
18 11 17 sylbird ⊢ R ∈ DivRingOps → U = Z → Z Z Z Z Z Z ∈ DivRingOps
19 18 necon3bd ⊢ R ∈ DivRingOps → ¬ Z Z Z Z Z Z ∈ DivRingOps → U ≠ Z
20 7 19 mpi ⊢ R ∈ DivRingOps → U ≠ Z