divrngcl

Description: The product of two nonzero elements of a division ring is nonzero. (Contributed by Jeff Madsen, 9-Jun-2010)

	Ref	Expression
Hypotheses	isdivrng1.1	$⊢ G = 1^{st} (R)$
	isdivrng1.2	$⊢ H = 2^{nd} (R)$
	isdivrng1.3	$⊢ Z = GId (G)$
	isdivrng1.4	$⊢ X = ran G$
Assertion	divrngcl	$⊢ (R \in DivRingOps \land A \in (X ∖ \{Z\}) \land B \in (X ∖ \{Z\})) \to A H B \in (X ∖ \{Z\})$

Proof

Step	Hyp	Ref	Expression
1		isdivrng1.1	$⊢ G = 1^{st} (R)$
2		isdivrng1.2	$⊢ H = 2^{nd} (R)$
3		isdivrng1.3	$⊢ Z = GId (G)$
4		isdivrng1.4	$⊢ X = ran G$
5	1 2 3 4	isdrngo1	$⊢ R \in DivRingOps \leftrightarrow (R \in RingOps \land {H ↾}_{((X ∖ \{Z\}) \times (X ∖ \{Z\}))} \in GrpOp)$
6		ovres	$⊢ (A \in (X ∖ \{Z\}) \land B \in (X ∖ \{Z\})) \to A ({H ↾}_{((X ∖ \{Z\}) \times (X ∖ \{Z\}))}) B = A H B$
7	6	adantl	$⊢ ((R \in RingOps \land {H ↾}_{((X ∖ \{Z\}) \times (X ∖ \{Z\}))} \in GrpOp) \land (A \in (X ∖ \{Z\}) \land B \in (X ∖ \{Z\}))) \to A ({H ↾}_{((X ∖ \{Z\}) \times (X ∖ \{Z\}))}) B = A H B$
8		eqid	$⊢ ran ({H ↾}_{((X ∖ \{Z\}) \times (X ∖ \{Z\}))}) = ran ({H ↾}_{((X ∖ \{Z\}) \times (X ∖ \{Z\}))})$
9	8	grpocl	$⊢ ({H ↾}_{((X ∖ \{Z\}) \times (X ∖ \{Z\}))} \in GrpOp \land A \in ran ({H ↾}_{((X ∖ \{Z\}) \times (X ∖ \{Z\}))}) \land B \in ran ({H ↾}_{((X ∖ \{Z\}) \times (X ∖ \{Z\}))})) \to A ({H ↾}_{((X ∖ \{Z\}) \times (X ∖ \{Z\}))}) B \in ran ({H ↾}_{((X ∖ \{Z\}) \times (X ∖ \{Z\}))})$
10	9	3expib	$⊢ {H ↾}_{((X ∖ \{Z\}) \times (X ∖ \{Z\}))} \in GrpOp \to ((A \in ran ({H ↾}_{((X ∖ \{Z\}) \times (X ∖ \{Z\}))}) \land B \in ran ({H ↾}_{((X ∖ \{Z\}) \times (X ∖ \{Z\}))})) \to A ({H ↾}_{((X ∖ \{Z\}) \times (X ∖ \{Z\}))}) B \in ran ({H ↾}_{((X ∖ \{Z\}) \times (X ∖ \{Z\}))}))$
11	10	adantl	$⊢ (R \in RingOps \land {H ↾}_{((X ∖ \{Z\}) \times (X ∖ \{Z\}))} \in GrpOp) \to ((A \in ran ({H ↾}_{((X ∖ \{Z\}) \times (X ∖ \{Z\}))}) \land B \in ran ({H ↾}_{((X ∖ \{Z\}) \times (X ∖ \{Z\}))})) \to A ({H ↾}_{((X ∖ \{Z\}) \times (X ∖ \{Z\}))}) B \in ran ({H ↾}_{((X ∖ \{Z\}) \times (X ∖ \{Z\}))}))$
12		grporndm	$⊢ {H ↾}_{((X ∖ \{Z\}) \times (X ∖ \{Z\}))} \in GrpOp \to ran ({H ↾}_{((X ∖ \{Z\}) \times (X ∖ \{Z\}))}) = dom dom ({H ↾}_{((X ∖ \{Z\}) \times (X ∖ \{Z\}))})$
13	12	adantl	$⊢ (R \in RingOps \land {H ↾}_{((X ∖ \{Z\}) \times (X ∖ \{Z\}))} \in GrpOp) \to ran ({H ↾}_{((X ∖ \{Z\}) \times (X ∖ \{Z\}))}) = dom dom ({H ↾}_{((X ∖ \{Z\}) \times (X ∖ \{Z\}))})$
14		difss	$⊢ X ∖ \{Z\} \subseteq X$
15		xpss12	$⊢ (X ∖ \{Z\} \subseteq X \land X ∖ \{Z\} \subseteq X) \to (X ∖ \{Z\}) \times (X ∖ \{Z\}) \subseteq X \times X$
16	14 14 15	mp2an	$⊢ (X ∖ \{Z\}) \times (X ∖ \{Z\}) \subseteq X \times X$
17	1 2 4	rngosm	$⊢ R \in RingOps \to H : X \times X ⟶ X$
18	17	fdmd	$⊢ R \in RingOps \to dom H = X \times X$
19	16 18	sseqtrrid	$⊢ R \in RingOps \to (X ∖ \{Z\}) \times (X ∖ \{Z\}) \subseteq dom H$
20		ssdmres	$⊢ (X ∖ \{Z\}) \times (X ∖ \{Z\}) \subseteq dom H \leftrightarrow dom ({H ↾}_{((X ∖ \{Z\}) \times (X ∖ \{Z\}))}) = (X ∖ \{Z\}) \times (X ∖ \{Z\})$
21	19 20	sylib	$⊢ R \in RingOps \to dom ({H ↾}_{((X ∖ \{Z\}) \times (X ∖ \{Z\}))}) = (X ∖ \{Z\}) \times (X ∖ \{Z\})$
22	21	adantr	$⊢ (R \in RingOps \land {H ↾}_{((X ∖ \{Z\}) \times (X ∖ \{Z\}))} \in GrpOp) \to dom ({H ↾}_{((X ∖ \{Z\}) \times (X ∖ \{Z\}))}) = (X ∖ \{Z\}) \times (X ∖ \{Z\})$
23	22	dmeqd	$⊢ (R \in RingOps \land {H ↾}_{((X ∖ \{Z\}) \times (X ∖ \{Z\}))} \in GrpOp) \to dom dom ({H ↾}_{((X ∖ \{Z\}) \times (X ∖ \{Z\}))}) = dom ((X ∖ \{Z\}) \times (X ∖ \{Z\}))$
24		dmxpid	$⊢ dom ((X ∖ \{Z\}) \times (X ∖ \{Z\})) = X ∖ \{Z\}$
25	23 24	eqtrdi	$⊢ (R \in RingOps \land {H ↾}_{((X ∖ \{Z\}) \times (X ∖ \{Z\}))} \in GrpOp) \to dom dom ({H ↾}_{((X ∖ \{Z\}) \times (X ∖ \{Z\}))}) = X ∖ \{Z\}$
26	13 25	eqtrd	$⊢ (R \in RingOps \land {H ↾}_{((X ∖ \{Z\}) \times (X ∖ \{Z\}))} \in GrpOp) \to ran ({H ↾}_{((X ∖ \{Z\}) \times (X ∖ \{Z\}))}) = X ∖ \{Z\}$
27	26	eleq2d	$⊢ (R \in RingOps \land {H ↾}_{((X ∖ \{Z\}) \times (X ∖ \{Z\}))} \in GrpOp) \to (A \in ran ({H ↾}_{((X ∖ \{Z\}) \times (X ∖ \{Z\}))}) \leftrightarrow A \in (X ∖ \{Z\}))$
28	26	eleq2d	$⊢ (R \in RingOps \land {H ↾}_{((X ∖ \{Z\}) \times (X ∖ \{Z\}))} \in GrpOp) \to (B \in ran ({H ↾}_{((X ∖ \{Z\}) \times (X ∖ \{Z\}))}) \leftrightarrow B \in (X ∖ \{Z\}))$
29	27 28	anbi12d	$⊢ (R \in RingOps \land {H ↾}_{((X ∖ \{Z\}) \times (X ∖ \{Z\}))} \in GrpOp) \to ((A \in ran ({H ↾}_{((X ∖ \{Z\}) \times (X ∖ \{Z\}))}) \land B \in ran ({H ↾}_{((X ∖ \{Z\}) \times (X ∖ \{Z\}))})) \leftrightarrow (A \in (X ∖ \{Z\}) \land B \in (X ∖ \{Z\})))$
30	26	eleq2d	$⊢ (R \in RingOps \land {H ↾}_{((X ∖ \{Z\}) \times (X ∖ \{Z\}))} \in GrpOp) \to (A ({H ↾}_{((X ∖ \{Z\}) \times (X ∖ \{Z\}))}) B \in ran ({H ↾}_{((X ∖ \{Z\}) \times (X ∖ \{Z\}))}) \leftrightarrow A ({H ↾}_{((X ∖ \{Z\}) \times (X ∖ \{Z\}))}) B \in (X ∖ \{Z\}))$
31	11 29 30	3imtr3d	$⊢ (R \in RingOps \land {H ↾}_{((X ∖ \{Z\}) \times (X ∖ \{Z\}))} \in GrpOp) \to ((A \in (X ∖ \{Z\}) \land B \in (X ∖ \{Z\})) \to A ({H ↾}_{((X ∖ \{Z\}) \times (X ∖ \{Z\}))}) B \in (X ∖ \{Z\}))$
32	31	imp	$⊢ ((R \in RingOps \land {H ↾}_{((X ∖ \{Z\}) \times (X ∖ \{Z\}))} \in GrpOp) \land (A \in (X ∖ \{Z\}) \land B \in (X ∖ \{Z\}))) \to A ({H ↾}_{((X ∖ \{Z\}) \times (X ∖ \{Z\}))}) B \in (X ∖ \{Z\})$
33	7 32	eqeltrrd	$⊢ ((R \in RingOps \land {H ↾}_{((X ∖ \{Z\}) \times (X ∖ \{Z\}))} \in GrpOp) \land (A \in (X ∖ \{Z\}) \land B \in (X ∖ \{Z\}))) \to A H B \in (X ∖ \{Z\})$
34	33	3impb	$⊢ ((R \in RingOps \land {H ↾}_{((X ∖ \{Z\}) \times (X ∖ \{Z\}))} \in GrpOp) \land A \in (X ∖ \{Z\}) \land B \in (X ∖ \{Z\})) \to A H B \in (X ∖ \{Z\})$
35	5 34	syl3an1b	$⊢ (R \in DivRingOps \land A \in (X ∖ \{Z\}) \land B \in (X ∖ \{Z\})) \to A H B \in (X ∖ \{Z\})$

Metamath Proof Explorer

Theorem divrngcl

Proof