Theorem dvrunz

Description: In a division ring the unit is different from the zero. (Contributed by FL, 14-Feb-2010) (Revised by Mario Carneiro, 15-Dec-2013) (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	syl6bi	⊢ ( 𝑅 ∈ 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 → 𝑈 ≠ 𝑍 )