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 = {Base}_{R}$
	drngmuleq0.o	$⊢ \underset{˙}{0} = 0_{R}$
	drngmuleq0.t	$⊢ \underset{˙}{\cdot} = \cdot_{R}$
	drngmuleq0.r	$⊢ φ \to R \in DivRing$
	drngmuleq0.x	$⊢ φ \to X \in B$
	drngmuleq0.y	$⊢ φ \to Y \in B$
Assertion	drngmul0or	$⊢ φ \to (X \underset{˙}{\cdot} Y = \underset{˙}{0} \leftrightarrow (X = \underset{˙}{0} \lor Y = \underset{˙}{0}))$

Proof

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

Metamath Proof Explorer

Theorem drngmul0or

Proof