zerdivemp1x

Description: In a unital ring a left invertible element is not a zero divisor. See also ringinvnzdiv . (Contributed by Jeff Madsen, 18-Apr-2010)

	Ref	Expression
Hypotheses	zerdivempx.1	$⊢ G = 1^{st} (R)$
	zerdivempx.2	$⊢ H = 2^{nd} (R)$
	zerdivempx.3	$⊢ Z = GId (G)$
	zerdivempx.4	$⊢ X = ran G$
	zerdivempx.5	$⊢ U = GId (H)$
Assertion	zerdivemp1x	$⊢ (R \in RingOps \land A \in X \land \exists a \in X a H A = U) \to (B \in X \to (A H B = Z \to B = Z))$

Proof

Step	Hyp	Ref	Expression
1		zerdivempx.1	$⊢ G = 1^{st} (R)$
2		zerdivempx.2	$⊢ H = 2^{nd} (R)$
3		zerdivempx.3	$⊢ Z = GId (G)$
4		zerdivempx.4	$⊢ X = ran G$
5		zerdivempx.5	$⊢ U = GId (H)$
6		oveq2	$⊢ A H B = Z \to a H (A H B) = a H Z$
7		simpl1	$⊢ ((R \in RingOps \land a H (A H B) = a H Z \land B \in X) \land (a \in X \land a H A = U \land A \in X)) \to R \in RingOps$
8		simpr1	$⊢ ((R \in RingOps \land a H (A H B) = a H Z \land B \in X) \land (a \in X \land a H A = U \land A \in X)) \to a \in X$
9		simpr3	$⊢ ((R \in RingOps \land a H (A H B) = a H Z \land B \in X) \land (a \in X \land a H A = U \land A \in X)) \to A \in X$
10		simpl3	$⊢ ((R \in RingOps \land a H (A H B) = a H Z \land B \in X) \land (a \in X \land a H A = U \land A \in X)) \to B \in X$
11	1 2 4	rngoass	$⊢ (R \in RingOps \land (a \in X \land A \in X \land B \in X)) \to (a H A) H B = a H (A H B)$
12	7 8 9 10 11	syl13anc	$⊢ ((R \in RingOps \land a H (A H B) = a H Z \land B \in X) \land (a \in X \land a H A = U \land A \in X)) \to (a H A) H B = a H (A H B)$
13		eqtr	$⊢ ((a H A) H B = a H (A H B) \land a H (A H B) = a H Z) \to (a H A) H B = a H Z$
14	13	ex	$⊢ (a H A) H B = a H (A H B) \to (a H (A H B) = a H Z \to (a H A) H B = a H Z)$
15		eqtr	$⊢ (U H B = (a H A) H B \land (a H A) H B = a H Z) \to U H B = a H Z$
16	3 4 1 2	rngorz	$⊢ (R \in RingOps \land a \in X) \to a H Z = Z$
17	16	3adant3	$⊢ (R \in RingOps \land a \in X \land B \in X) \to a H Z = Z$
18	1	rneqi	$⊢ ran G = ran 1^{st} (R)$
19	4 18	eqtri	$⊢ X = ran 1^{st} (R)$
20	2 19 5	rngolidm	$⊢ (R \in RingOps \land B \in X) \to U H B = B$
21	20	3adant2	$⊢ (R \in RingOps \land a \in X \land B \in X) \to U H B = B$
22		simp1	$⊢ (U H B = a H Z \land U H B = B \land a H Z = Z) \to U H B = a H Z$
23		simp2	$⊢ (U H B = a H Z \land U H B = B \land a H Z = Z) \to U H B = B$
24		simp3	$⊢ (U H B = a H Z \land U H B = B \land a H Z = Z) \to a H Z = Z$
25	22 23 24	3eqtr3d	$⊢ (U H B = a H Z \land U H B = B \land a H Z = Z) \to B = Z$
26	25	a1d	$⊢ (U H B = a H Z \land U H B = B \land a H Z = Z) \to (A \in X \to B = Z)$
27	26	3exp	$⊢ U H B = a H Z \to (U H B = B \to (a H Z = Z \to (A \in X \to B = Z)))$
28	27	com14	$⊢ A \in X \to (U H B = B \to (a H Z = Z \to (U H B = a H Z \to B = Z)))$
29	28	com13	$⊢ a H Z = Z \to (U H B = B \to (A \in X \to (U H B = a H Z \to B = Z)))$
30	17 21 29	sylc	$⊢ (R \in RingOps \land a \in X \land B \in X) \to (A \in X \to (U H B = a H Z \to B = Z))$
31	30	3exp	$⊢ R \in RingOps \to (a \in X \to (B \in X \to (A \in X \to (U H B = a H Z \to B = Z))))$
32	31	com15	$⊢ U H B = a H Z \to (a \in X \to (B \in X \to (A \in X \to (R \in RingOps \to B = Z))))$
33	32	com24	$⊢ U H B = a H Z \to (A \in X \to (B \in X \to (a \in X \to (R \in RingOps \to B = Z))))$
34	15 33	syl	$⊢ (U H B = (a H A) H B \land (a H A) H B = a H Z) \to (A \in X \to (B \in X \to (a \in X \to (R \in RingOps \to B = Z))))$
35	34	ex	$⊢ U H B = (a H A) H B \to ((a H A) H B = a H Z \to (A \in X \to (B \in X \to (a \in X \to (R \in RingOps \to B = Z)))))$
36	35	eqcoms	$⊢ (a H A) H B = U H B \to ((a H A) H B = a H Z \to (A \in X \to (B \in X \to (a \in X \to (R \in RingOps \to B = Z)))))$
37	36	com25	$⊢ (a H A) H B = U H B \to (a \in X \to (A \in X \to (B \in X \to ((a H A) H B = a H Z \to (R \in RingOps \to B = Z)))))$
38		oveq1	$⊢ a H A = U \to (a H A) H B = U H B$
39	37 38	syl11	$⊢ a \in X \to (a H A = U \to (A \in X \to (B \in X \to ((a H A) H B = a H Z \to (R \in RingOps \to B = Z)))))$
40	39	3imp	$⊢ (a \in X \land a H A = U \land A \in X) \to (B \in X \to ((a H A) H B = a H Z \to (R \in RingOps \to B = Z)))$
41	40	com13	$⊢ (a H A) H B = a H Z \to (B \in X \to ((a \in X \land a H A = U \land A \in X) \to (R \in RingOps \to B = Z)))$
42	14 41	syl6	$⊢ (a H A) H B = a H (A H B) \to (a H (A H B) = a H Z \to (B \in X \to ((a \in X \land a H A = U \land A \in X) \to (R \in RingOps \to B = Z))))$
43	42	com15	$⊢ R \in RingOps \to (a H (A H B) = a H Z \to (B \in X \to ((a \in X \land a H A = U \land A \in X) \to ((a H A) H B = a H (A H B) \to B = Z))))$
44	43	3imp1	$⊢ ((R \in RingOps \land a H (A H B) = a H Z \land B \in X) \land (a \in X \land a H A = U \land A \in X)) \to ((a H A) H B = a H (A H B) \to B = Z)$
45	12 44	mpd	$⊢ ((R \in RingOps \land a H (A H B) = a H Z \land B \in X) \land (a \in X \land a H A = U \land A \in X)) \to B = Z$
46	45	3exp1	$⊢ R \in RingOps \to (a H (A H B) = a H Z \to (B \in X \to ((a \in X \land a H A = U \land A \in X) \to B = Z)))$
47	6 46	syl5com	$⊢ A H B = Z \to (R \in RingOps \to (B \in X \to ((a \in X \land a H A = U \land A \in X) \to B = Z)))$
48	47	com14	$⊢ (a \in X \land a H A = U \land A \in X) \to (R \in RingOps \to (B \in X \to (A H B = Z \to B = Z)))$
49	48	3exp	$⊢ a \in X \to (a H A = U \to (A \in X \to (R \in RingOps \to (B \in X \to (A H B = Z \to B = Z)))))$
50	49	rexlimiv	$⊢ \exists a \in X a H A = U \to (A \in X \to (R \in RingOps \to (B \in X \to (A H B = Z \to B = Z))))$
51	50	com13	$⊢ R \in RingOps \to (A \in X \to (\exists a \in X a H A = U \to (B \in X \to (A H B = Z \to B = Z))))$
52	51	3imp	$⊢ (R \in RingOps \land A \in X \land \exists a \in X a H A = U) \to (B \in X \to (A H B = Z \to B = Z))$

Metamath Proof Explorer

Theorem zerdivemp1x

Proof