rngoueqz

Description: Obsolete as of 23-Jan-2020. Use 0ring01eqbi instead. In a unital ring the zero equals the ring unity iff the ring is the zero ring. (Contributed by FL, 14-Feb-2010) (New usage is discouraged.)

	Ref	Expression
Hypotheses	uznzr.1	$⊢ G = 1^{st} (R)$
	uznzr.2	$⊢ H = 2^{nd} (R)$
	uznzr.3	$⊢ Z = GId (G)$
	uznzr.4	$⊢ U = GId (H)$
	uznzr.5	$⊢ X = ran G$
Assertion	rngoueqz	$⊢ R \in RingOps \to (X \approx 1_{𝑜} \leftrightarrow U = Z)$

Proof

Step	Hyp	Ref	Expression
1		uznzr.1	$⊢ G = 1^{st} (R)$
2		uznzr.2	$⊢ H = 2^{nd} (R)$
3		uznzr.3	$⊢ Z = GId (G)$
4		uznzr.4	$⊢ U = GId (H)$
5		uznzr.5	$⊢ X = ran G$
6	1 5 3	rngo0cl	$⊢ R \in RingOps \to Z \in X$
7		en1eqsn	$⊢ (Z \in X \land X \approx 1_{𝑜}) \to X = \{Z\}$
8	1	rneqi	$⊢ ran G = ran 1^{st} (R)$
9	8 2 4	rngo1cl	$⊢ R \in RingOps \to U \in ran G$
10		eleq2	$⊢ X = \{Z\} \to (U \in X \leftrightarrow U \in \{Z\})$
11	10	biimpd	$⊢ X = \{Z\} \to (U \in X \to U \in \{Z\})$
12		elsni	$⊢ U \in \{Z\} \to U = Z$
13	11 12	syl6com	$⊢ U \in X \to (X = \{Z\} \to U = Z)$
14	5	eqcomi	$⊢ ran G = X$
15	13 14	eleq2s	$⊢ U \in ran G \to (X = \{Z\} \to U = Z)$
16	9 15	syl	$⊢ R \in RingOps \to (X = \{Z\} \to U = Z)$
17	7 16	syl5com	$⊢ (Z \in X \land X \approx 1_{𝑜}) \to (R \in RingOps \to U = Z)$
18	17	ex	$⊢ Z \in X \to (X \approx 1_{𝑜} \to (R \in RingOps \to U = Z))$
19	18	com23	$⊢ Z \in X \to (R \in RingOps \to (X \approx 1_{𝑜} \to U = Z))$
20	6 19	mpcom	$⊢ R \in RingOps \to (X \approx 1_{𝑜} \to U = Z)$
21	1 5	rngone0	$⊢ R \in RingOps \to X \neq \emptyset$
22		oveq2	$⊢ U = Z \to x H U = x H Z$
23	22	ralrimivw	$⊢ U = Z \to \forall x \in X x H U = x H Z$
24	3 5 1 2	rngorz	$⊢ (R \in RingOps \land x \in X) \to x H Z = Z$
25	24	ralrimiva	$⊢ R \in RingOps \to \forall x \in X x H Z = Z$
26	5 8	eqtri	$⊢ X = ran 1^{st} (R)$
27	2 26 4	rngoridm	$⊢ (R \in RingOps \land x \in X) \to x H U = x$
28	27	ralrimiva	$⊢ R \in RingOps \to \forall x \in X x H U = x$
29		r19.26	$⊢ \forall x \in X (x H U = x \land x H U = x H Z) \leftrightarrow (\forall x \in X x H U = x \land \forall x \in X x H U = x H Z)$
30		r19.26	$⊢ \forall x \in X ((x H U = x \land x H U = x H Z) \land x H Z = Z) \leftrightarrow (\forall x \in X (x H U = x \land x H U = x H Z) \land \forall x \in X x H Z = Z)$
31		eqtr	$⊢ (x = x H U \land x H U = x H Z) \to x = x H Z$
32		eqtr	$⊢ (x = x H Z \land x H Z = Z) \to x = Z$
33	32	ex	$⊢ x = x H Z \to (x H Z = Z \to x = Z)$
34	31 33	syl	$⊢ (x = x H U \land x H U = x H Z) \to (x H Z = Z \to x = Z)$
35	34	ex	$⊢ x = x H U \to (x H U = x H Z \to (x H Z = Z \to x = Z))$
36	35	eqcoms	$⊢ x H U = x \to (x H U = x H Z \to (x H Z = Z \to x = Z))$
37	36	imp31	$⊢ ((x H U = x \land x H U = x H Z) \land x H Z = Z) \to x = Z$
38	37	ralimi	$⊢ \forall x \in X ((x H U = x \land x H U = x H Z) \land x H Z = Z) \to \forall x \in X x = Z$
39		eqsn	$⊢ X \neq \emptyset \to (X = \{Z\} \leftrightarrow \forall x \in X x = Z)$
40		ensn1g	$⊢ Z \in X \to \{Z\} \approx 1_{𝑜}$
41	6 40	syl	$⊢ R \in RingOps \to \{Z\} \approx 1_{𝑜}$
42		breq1	$⊢ X = \{Z\} \to (X \approx 1_{𝑜} \leftrightarrow \{Z\} \approx 1_{𝑜})$
43	41 42	imbitrrid	$⊢ X = \{Z\} \to (R \in RingOps \to X \approx 1_{𝑜})$
44	39 43	syl6bir	$⊢ X \neq \emptyset \to (\forall x \in X x = Z \to (R \in RingOps \to X \approx 1_{𝑜}))$
45	44	com3l	$⊢ \forall x \in X x = Z \to (R \in RingOps \to (X \neq \emptyset \to X \approx 1_{𝑜}))$
46	38 45	syl	$⊢ \forall x \in X ((x H U = x \land x H U = x H Z) \land x H Z = Z) \to (R \in RingOps \to (X \neq \emptyset \to X \approx 1_{𝑜}))$
47	30 46	sylbir	$⊢ (\forall x \in X (x H U = x \land x H U = x H Z) \land \forall x \in X x H Z = Z) \to (R \in RingOps \to (X \neq \emptyset \to X \approx 1_{𝑜}))$
48	47	ex	$⊢ \forall x \in X (x H U = x \land x H U = x H Z) \to (\forall x \in X x H Z = Z \to (R \in RingOps \to (X \neq \emptyset \to X \approx 1_{𝑜})))$
49	29 48	sylbir	$⊢ (\forall x \in X x H U = x \land \forall x \in X x H U = x H Z) \to (\forall x \in X x H Z = Z \to (R \in RingOps \to (X \neq \emptyset \to X \approx 1_{𝑜})))$
50	49	ex	$⊢ \forall x \in X x H U = x \to (\forall x \in X x H U = x H Z \to (\forall x \in X x H Z = Z \to (R \in RingOps \to (X \neq \emptyset \to X \approx 1_{𝑜}))))$
51	50	com24	$⊢ \forall x \in X x H U = x \to (R \in RingOps \to (\forall x \in X x H Z = Z \to (\forall x \in X x H U = x H Z \to (X \neq \emptyset \to X \approx 1_{𝑜}))))$
52	28 51	mpcom	$⊢ R \in RingOps \to (\forall x \in X x H Z = Z \to (\forall x \in X x H U = x H Z \to (X \neq \emptyset \to X \approx 1_{𝑜})))$
53	25 52	mpd	$⊢ R \in RingOps \to (\forall x \in X x H U = x H Z \to (X \neq \emptyset \to X \approx 1_{𝑜}))$
54	23 53	syl5com	$⊢ U = Z \to (R \in RingOps \to (X \neq \emptyset \to X \approx 1_{𝑜}))$
55	54	com13	$⊢ X \neq \emptyset \to (R \in RingOps \to (U = Z \to X \approx 1_{𝑜}))$
56	21 55	mpcom	$⊢ R \in RingOps \to (U = Z \to X \approx 1_{𝑜})$
57	20 56	impbid	$⊢ R \in RingOps \to (X \approx 1_{𝑜} \leftrightarrow U = Z)$

Metamath Proof Explorer

Theorem rngoueqz

Proof