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	$⊢ 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 \in DivRingOps \to U \neq 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 \in V$
7	6	zrdivrng	$⊢ \neg ⟨\{⟨⟨Z, Z⟩, Z⟩\}, \{⟨⟨Z, Z⟩, Z⟩\}⟩ \in DivRingOps$
8	1 2 3 4	drngoi	$⊢ R \in DivRingOps \to (R \in RingOps \land {H ↾}_{((X ∖ \{Z\}) \times (X ∖ \{Z\}))} \in GrpOp)$
9	8	simpld	$⊢ R \in DivRingOps \to R \in RingOps$
10	1 2 4 5 3	rngoueqz	$⊢ R \in RingOps \to (X \approx 1_{𝑜} \leftrightarrow U = Z)$
11	9 10	syl	$⊢ R \in DivRingOps \to (X \approx 1_{𝑜} \leftrightarrow U = Z)$
12	1 3 4	rngosn6	$⊢ R \in RingOps \to (X \approx 1_{𝑜} \leftrightarrow R = ⟨\{⟨⟨Z, Z⟩, Z⟩\}, \{⟨⟨Z, Z⟩, Z⟩\}⟩)$
13	9 12	syl	$⊢ R \in DivRingOps \to (X \approx 1_{𝑜} \leftrightarrow R = ⟨\{⟨⟨Z, Z⟩, Z⟩\}, \{⟨⟨Z, Z⟩, Z⟩\}⟩)$
14		eleq1	$⊢ R = ⟨\{⟨⟨Z, Z⟩, Z⟩\}, \{⟨⟨Z, Z⟩, Z⟩\}⟩ \to (R \in DivRingOps \leftrightarrow ⟨\{⟨⟨Z, Z⟩, Z⟩\}, \{⟨⟨Z, Z⟩, Z⟩\}⟩ \in DivRingOps)$
15	14	biimpd	$⊢ R = ⟨\{⟨⟨Z, Z⟩, Z⟩\}, \{⟨⟨Z, Z⟩, Z⟩\}⟩ \to (R \in DivRingOps \to ⟨\{⟨⟨Z, Z⟩, Z⟩\}, \{⟨⟨Z, Z⟩, Z⟩\}⟩ \in DivRingOps)$
16	13 15	syl6bi	$⊢ R \in DivRingOps \to (X \approx 1_{𝑜} \to (R \in DivRingOps \to ⟨\{⟨⟨Z, Z⟩, Z⟩\}, \{⟨⟨Z, Z⟩, Z⟩\}⟩ \in DivRingOps))$
17	16	pm2.43a	$⊢ R \in DivRingOps \to (X \approx 1_{𝑜} \to ⟨\{⟨⟨Z, Z⟩, Z⟩\}, \{⟨⟨Z, Z⟩, Z⟩\}⟩ \in DivRingOps)$
18	11 17	sylbird	$⊢ R \in DivRingOps \to (U = Z \to ⟨\{⟨⟨Z, Z⟩, Z⟩\}, \{⟨⟨Z, Z⟩, Z⟩\}⟩ \in DivRingOps)$
19	18	necon3bd	$⊢ R \in DivRingOps \to (\neg ⟨\{⟨⟨Z, Z⟩, Z⟩\}, \{⟨⟨Z, Z⟩, Z⟩\}⟩ \in DivRingOps \to U \neq Z)$
20	7 19	mpi	$⊢ R \in DivRingOps \to U \neq Z$

Metamath Proof Explorer

Theorem dvrunz

Proof