ndmovdistr

Description: Any operation is distributive outside its domain, if the domain doesn't contain the empty set. (Contributed by NM, 24-Aug-1995)

	Ref	Expression
Hypotheses	ndmov.1	$⊢ dom F = S \times S$
	ndmov.5	$⊢ \neg \emptyset \in S$
	ndmov.6	$⊢ dom G = S \times S$
Assertion	ndmovdistr	$⊢ \neg (A \in S \land B \in S \land C \in S) \to A G (B F C) = (A G B) F (A G C)$

Step	Hyp	Ref	Expression
1		ndmov.1	$⊢ dom F = S \times S$
2		ndmov.5	$⊢ \neg \emptyset \in S$
3		ndmov.6	$⊢ dom G = S \times S$
4	1 2	ndmovrcl	$⊢ B F C \in S \to (B \in S \land C \in S)$
5	4	anim2i	$⊢ (A \in S \land B F C \in S) \to (A \in S \land (B \in S \land C \in S))$
6		3anass	$⊢ (A \in S \land B \in S \land C \in S) \leftrightarrow (A \in S \land (B \in S \land C \in S))$
7	5 6	sylibr	$⊢ (A \in S \land B F C \in S) \to (A \in S \land B \in S \land C \in S)$
8	3	ndmov	$⊢ \neg (A \in S \land B F C \in S) \to A G (B F C) = \emptyset$
9	7 8	nsyl5	$⊢ \neg (A \in S \land B \in S \land C \in S) \to A G (B F C) = \emptyset$
10	3 2	ndmovrcl	$⊢ A G B \in S \to (A \in S \land B \in S)$
11	3 2	ndmovrcl	$⊢ A G C \in S \to (A \in S \land C \in S)$
12	10 11	anim12i	$⊢ (A G B \in S \land A G C \in S) \to ((A \in S \land B \in S) \land (A \in S \land C \in S))$
13		anandi3	$⊢ (A \in S \land B \in S \land C \in S) \leftrightarrow ((A \in S \land B \in S) \land (A \in S \land C \in S))$
14	12 13	sylibr	$⊢ (A G B \in S \land A G C \in S) \to (A \in S \land B \in S \land C \in S)$
15	1	ndmov	$⊢ \neg (A G B \in S \land A G C \in S) \to (A G B) F (A G C) = \emptyset$
16	14 15	nsyl5	$⊢ \neg (A \in S \land B \in S \land C \in S) \to (A G B) F (A G C) = \emptyset$
17	9 16	eqtr4d	$⊢ \neg (A \in S \land B \in S \land C \in S) \to A G (B F C) = (A G B) F (A G C)$

Metamath Proof Explorer