Theorem drngmul0or

Description: A product is zero iff one of its factors is zero. (Contributed by NM, 8-Oct-2014)

	Ref	Expression
Hypotheses	drngmuleq0.b	$$⊢B={\mathrm{Base}}_R$$
	drngmuleq0.o	$$⊢\underset{\dot{}}{0}=0_R$$
	drngmuleq0.t	$$⊢\underset{\dot{}}{·}={\cdot }_R$$
	drngmuleq0.r	$$⊢\phi \to R\in \mathrm{DivRing}$$
	drngmuleq0.x	$$⊢\phi \to X\in B$$
	drngmuleq0.y	$$⊢\phi \to Y\in B$$
Assertion	drngmul0or	$$⊢\phi \to \left(X\underset{\dot{}}{·}Y=\underset{\dot{}}{0}\leftrightarrow \left(X=\underset{\dot{}}{0}\vee Y=\underset{\dot{}}{0}\right)\right)$$

Proof

Step	Hyp	Ref	Expression
1		drngmuleq0.b	$$⊢B={\mathrm{Base}}_R$$
2		drngmuleq0.o	$$⊢\underset{\dot{}}{0}=0_R$$
3		drngmuleq0.t	$$⊢\underset{\dot{}}{·}={\cdot }_R$$
4		drngmuleq0.r	$$⊢\phi \to R\in \mathrm{DivRing}$$
5		drngmuleq0.x	$$⊢\phi \to X\in B$$
6		drngmuleq0.y	$$⊢\phi \to Y\in B$$
7		df-ne	$$⊢X\ne \underset{\dot{}}{0}\leftrightarrow \neg X=\underset{\dot{}}{0}$$
8		oveq2	$$⊢X\underset{\dot{}}{·}Y=\underset{\dot{}}{0}\to {inv}_r\left(R\right)\left(X\right)\underset{\dot{}}{·}\left(X\underset{\dot{}}{·}Y\right)={inv}_r\left(R\right)\left(X\right)\underset{\dot{}}{·}\underset{\dot{}}{0}$$
9	8	ad2antlr	$$⊢\left(\left(\phi \wedge X\underset{\dot{}}{·}Y=\underset{\dot{}}{0}\right)\wedge X\ne \underset{\dot{}}{0}\right)\to {inv}_r\left(R\right)\left(X\right)\underset{\dot{}}{·}\left(X\underset{\dot{}}{·}Y\right)={inv}_r\left(R\right)\left(X\right)\underset{\dot{}}{·}\underset{\dot{}}{0}$$
10	4	adantr	$$⊢\left(\phi \wedge X\ne \underset{\dot{}}{0}\right)\to R\in \mathrm{DivRing}$$
11	5	adantr	$$⊢\left(\phi \wedge X\ne \underset{\dot{}}{0}\right)\to X\in B$$
12		simpr	$$⊢\left(\phi \wedge X\ne \underset{\dot{}}{0}\right)\to X\ne \underset{\dot{}}{0}$$
13		eqid	$$⊢1_R=1_R$$
14		eqid	$$⊢{inv}_r\left(R\right)={inv}_r\left(R\right)$$
15	1 2 3 13 14	drnginvrl	$$⊢\left(R\in \mathrm{DivRing}\wedge X\in B\wedge X\ne \underset{\dot{}}{0}\right)\to {inv}_r\left(R\right)\left(X\right)\underset{\dot{}}{·}X=1_R$$
16	10 11 12 15	syl3anc	$$⊢\left(\phi \wedge X\ne \underset{\dot{}}{0}\right)\to {inv}_r\left(R\right)\left(X\right)\underset{\dot{}}{·}X=1_R$$
17	16	oveq1d	$$⊢\left(\phi \wedge X\ne \underset{\dot{}}{0}\right)\to \left({inv}_r\left(R\right)\left(X\right)\underset{\dot{}}{·}X\right)\underset{\dot{}}{·}Y=1_R\underset{\dot{}}{·}Y$$
18		drngring	$$⊢R\in \mathrm{DivRing}\to R\in \mathrm{Ring}$$
19	4 18	syl	$$⊢\phi \to R\in \mathrm{Ring}$$
20	19	adantr	$$⊢\left(\phi \wedge X\ne \underset{\dot{}}{0}\right)\to R\in \mathrm{Ring}$$
21	1 2 14	drnginvrcl	$$⊢\left(R\in \mathrm{DivRing}\wedge X\in B\wedge X\ne \underset{\dot{}}{0}\right)\to {inv}_r\left(R\right)\left(X\right)\in B$$
22	10 11 12 21	syl3anc	$$⊢\left(\phi \wedge X\ne \underset{\dot{}}{0}\right)\to {inv}_r\left(R\right)\left(X\right)\in B$$
23	6	adantr	$$⊢\left(\phi \wedge X\ne \underset{\dot{}}{0}\right)\to Y\in B$$
24	1 3	ringass	$$⊢\left(R\in \mathrm{Ring}\wedge \left({inv}_r\left(R\right)\left(X\right)\in B\wedge X\in B\wedge Y\in B\right)\right)\to \left({inv}_r\left(R\right)\left(X\right)\underset{\dot{}}{·}X\right)\underset{\dot{}}{·}Y={inv}_r\left(R\right)\left(X\right)\underset{\dot{}}{·}\left(X\underset{\dot{}}{·}Y\right)$$
25	20 22 11 23 24	syl13anc	$$⊢\left(\phi \wedge X\ne \underset{\dot{}}{0}\right)\to \left({inv}_r\left(R\right)\left(X\right)\underset{\dot{}}{·}X\right)\underset{\dot{}}{·}Y={inv}_r\left(R\right)\left(X\right)\underset{\dot{}}{·}\left(X\underset{\dot{}}{·}Y\right)$$
26	1 3 13	ringlidm	$$⊢\left(R\in \mathrm{Ring}\wedge Y\in B\right)\to 1_R\underset{\dot{}}{·}Y=Y$$
27	19 6 26	syl2anc	$$⊢\phi \to 1_R\underset{\dot{}}{·}Y=Y$$
28	27	adantr	$$⊢\left(\phi \wedge X\ne \underset{\dot{}}{0}\right)\to 1_R\underset{\dot{}}{·}Y=Y$$
29	17 25 28	3eqtr3d	$$⊢\left(\phi \wedge X\ne \underset{\dot{}}{0}\right)\to {inv}_r\left(R\right)\left(X\right)\underset{\dot{}}{·}\left(X\underset{\dot{}}{·}Y\right)=Y$$
30	29	adantlr	$$⊢\left(\left(\phi \wedge X\underset{\dot{}}{·}Y=\underset{\dot{}}{0}\right)\wedge X\ne \underset{\dot{}}{0}\right)\to {inv}_r\left(R\right)\left(X\right)\underset{\dot{}}{·}\left(X\underset{\dot{}}{·}Y\right)=Y$$
31	19	adantr	$$⊢\left(\phi \wedge X\underset{\dot{}}{·}Y=\underset{\dot{}}{0}\right)\to R\in \mathrm{Ring}$$
32	31	adantr	$$⊢\left(\left(\phi \wedge X\underset{\dot{}}{·}Y=\underset{\dot{}}{0}\right)\wedge X\ne \underset{\dot{}}{0}\right)\to R\in \mathrm{Ring}$$
33	22	adantlr	$$⊢\left(\left(\phi \wedge X\underset{\dot{}}{·}Y=\underset{\dot{}}{0}\right)\wedge X\ne \underset{\dot{}}{0}\right)\to {inv}_r\left(R\right)\left(X\right)\in B$$
34	1 3 2	ringrz	$$⊢\left(R\in \mathrm{Ring}\wedge {inv}_r\left(R\right)\left(X\right)\in B\right)\to {inv}_r\left(R\right)\left(X\right)\underset{\dot{}}{·}\underset{\dot{}}{0}=\underset{\dot{}}{0}$$
35	32 33 34	syl2anc	$$⊢\left(\left(\phi \wedge X\underset{\dot{}}{·}Y=\underset{\dot{}}{0}\right)\wedge X\ne \underset{\dot{}}{0}\right)\to {inv}_r\left(R\right)\left(X\right)\underset{\dot{}}{·}\underset{\dot{}}{0}=\underset{\dot{}}{0}$$
36	9 30 35	3eqtr3d	$$⊢\left(\left(\phi \wedge X\underset{\dot{}}{·}Y=\underset{\dot{}}{0}\right)\wedge X\ne \underset{\dot{}}{0}\right)\to Y=\underset{\dot{}}{0}$$
37	36	ex	$$⊢\left(\phi \wedge X\underset{\dot{}}{·}Y=\underset{\dot{}}{0}\right)\to \left(X\ne \underset{\dot{}}{0}\to Y=\underset{\dot{}}{0}\right)$$
38	7 37	syl5bir	$$⊢\left(\phi \wedge X\underset{\dot{}}{·}Y=\underset{\dot{}}{0}\right)\to \left(\neg X=\underset{\dot{}}{0}\to Y=\underset{\dot{}}{0}\right)$$
39	38	orrd	$$⊢\left(\phi \wedge X\underset{\dot{}}{·}Y=\underset{\dot{}}{0}\right)\to \left(X=\underset{\dot{}}{0}\vee Y=\underset{\dot{}}{0}\right)$$
40	39	ex	$$⊢\phi \to \left(X\underset{\dot{}}{·}Y=\underset{\dot{}}{0}\to \left(X=\underset{\dot{}}{0}\vee Y=\underset{\dot{}}{0}\right)\right)$$
41	1 3 2	ringlz	$$⊢\left(R\in \mathrm{Ring}\wedge Y\in B\right)\to \underset{\dot{}}{0}\underset{\dot{}}{·}Y=\underset{\dot{}}{0}$$
42	19 6 41	syl2anc	$$⊢\phi \to \underset{\dot{}}{0}\underset{\dot{}}{·}Y=\underset{\dot{}}{0}$$
43		oveq1	$$⊢X=\underset{\dot{}}{0}\to X\underset{\dot{}}{·}Y=\underset{\dot{}}{0}\underset{\dot{}}{·}Y$$
44	43	eqeq1d	$$⊢X=\underset{\dot{}}{0}\to \left(X\underset{\dot{}}{·}Y=\underset{\dot{}}{0}\leftrightarrow \underset{\dot{}}{0}\underset{\dot{}}{·}Y=\underset{\dot{}}{0}\right)$$
45	42 44	syl5ibrcom	$$⊢\phi \to \left(X=\underset{\dot{}}{0}\to X\underset{\dot{}}{·}Y=\underset{\dot{}}{0}\right)$$
46	1 3 2	ringrz	$$⊢\left(R\in \mathrm{Ring}\wedge X\in B\right)\to X\underset{\dot{}}{·}\underset{\dot{}}{0}=\underset{\dot{}}{0}$$
47	19 5 46	syl2anc	$$⊢\phi \to X\underset{\dot{}}{·}\underset{\dot{}}{0}=\underset{\dot{}}{0}$$
48		oveq2	$$⊢Y=\underset{\dot{}}{0}\to X\underset{\dot{}}{·}Y=X\underset{\dot{}}{·}\underset{\dot{}}{0}$$
49	48	eqeq1d	$$⊢Y=\underset{\dot{}}{0}\to \left(X\underset{\dot{}}{·}Y=\underset{\dot{}}{0}\leftrightarrow X\underset{\dot{}}{·}\underset{\dot{}}{0}=\underset{\dot{}}{0}\right)$$
50	47 49	syl5ibrcom	$$⊢\phi \to \left(Y=\underset{\dot{}}{0}\to X\underset{\dot{}}{·}Y=\underset{\dot{}}{0}\right)$$
51	45 50	jaod	$$⊢\phi \to \left(\left(X=\underset{\dot{}}{0}\vee Y=\underset{\dot{}}{0}\right)\to X\underset{\dot{}}{·}Y=\underset{\dot{}}{0}\right)$$
52	40 51	impbid	$$⊢\phi \to \left(X\underset{\dot{}}{·}Y=\underset{\dot{}}{0}\leftrightarrow \left(X=\underset{\dot{}}{0}\vee Y=\underset{\dot{}}{0}\right)\right)$$