ndmaovdistr

Description: Any operation is distributive outside its domain. In contrast to ndmovdistr where it is required that the operation's domain doesn't contain the empty set ( -. (/) e. S ), no additional assumption is required. (Contributed by Alexander van der Vekens, 26-May-2017)

	Ref	Expression
Hypotheses	ndmaov.1	$⊢ dom F = S \times S$
	ndmaov.6	$⊢ dom G = S \times S$
Assertion	ndmaovdistr	$⊢ \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))))$

Proof

Step	Hyp	Ref	Expression
1		ndmaov.1	$⊢ dom F = S \times S$
2		ndmaov.6	$⊢ dom G = S \times S$
3	2	eleq2i	$⊢ ⟨A, ((B F C))⟩ \in dom G \leftrightarrow ⟨A, ((B F C))⟩ \in (S \times S)$
4		opelxp	$⊢ ⟨A, ((B F C))⟩ \in (S \times S) \leftrightarrow (A \in S \land ((B F C)) \in S)$
5	3 4	bitri	$⊢ ⟨A, ((B F C))⟩ \in dom G \leftrightarrow (A \in S \land ((B F C)) \in S)$
6		aovvdm	$⊢ ((B F C)) \in S \to ⟨B, C⟩ \in dom F$
7	1	eleq2i	$⊢ ⟨B, C⟩ \in dom F \leftrightarrow ⟨B, C⟩ \in (S \times S)$
8		opelxp	$⊢ ⟨B, C⟩ \in (S \times S) \leftrightarrow (B \in S \land C \in S)$
9	7 8	bitri	$⊢ ⟨B, C⟩ \in dom F \leftrightarrow (B \in S \land C \in S)$
10		3anass	$⊢ (A \in S \land B \in S \land C \in S) \leftrightarrow (A \in S \land (B \in S \land C \in S))$
11	10	simplbi2com	$⊢ (B \in S \land C \in S) \to (A \in S \to (A \in S \land B \in S \land C \in S))$
12	9 11	sylbi	$⊢ ⟨B, C⟩ \in dom F \to (A \in S \to (A \in S \land B \in S \land C \in S))$
13	6 12	syl	$⊢ ((B F C)) \in S \to (A \in S \to (A \in S \land B \in S \land C \in S))$
14	13	impcom	$⊢ (A \in S \land ((B F C)) \in S) \to (A \in S \land B \in S \land C \in S)$
15	5 14	sylbi	$⊢ ⟨A, ((B F C))⟩ \in dom G \to (A \in S \land B \in S \land C \in S)$
16		ndmaov	$⊢ \neg ⟨A, ((B F C))⟩ \in dom G \to ((A G ((B F C)))) = V$
17	15 16	nsyl5	$⊢ \neg (A \in S \land B \in S \land C \in S) \to ((A G ((B F C)))) = V$
18	1	eleq2i	$⊢ ⟨((A G B)), ((A G C))⟩ \in dom F \leftrightarrow ⟨((A G B)), ((A G C))⟩ \in (S \times S)$
19		opelxp	$⊢ ⟨((A G B)), ((A G C))⟩ \in (S \times S) \leftrightarrow (((A G B)) \in S \land ((A G C)) \in S)$
20	18 19	bitri	$⊢ ⟨((A G B)), ((A G C))⟩ \in dom F \leftrightarrow (((A G B)) \in S \land ((A G C)) \in S)$
21		aovvdm	$⊢ ((A G B)) \in S \to ⟨A, B⟩ \in dom G$
22	2	eleq2i	$⊢ ⟨A, B⟩ \in dom G \leftrightarrow ⟨A, B⟩ \in (S \times S)$
23		opelxp	$⊢ ⟨A, B⟩ \in (S \times S) \leftrightarrow (A \in S \land B \in S)$
24	22 23	bitri	$⊢ ⟨A, B⟩ \in dom G \leftrightarrow (A \in S \land B \in S)$
25	2	eleq2i	$⊢ ⟨A, C⟩ \in dom G \leftrightarrow ⟨A, C⟩ \in (S \times S)$
26		opelxp	$⊢ ⟨A, C⟩ \in (S \times S) \leftrightarrow (A \in S \land C \in S)$
27	25 26	bitri	$⊢ ⟨A, C⟩ \in dom G \leftrightarrow (A \in S \land C \in S)$
28		simpll	$⊢ ((A \in S \land C \in S) \land (A \in S \land B \in S)) \to A \in S$
29		simprr	$⊢ ((A \in S \land C \in S) \land (A \in S \land B \in S)) \to B \in S$
30		simplr	$⊢ ((A \in S \land C \in S) \land (A \in S \land B \in S)) \to C \in S$
31	28 29 30	3jca	$⊢ ((A \in S \land C \in S) \land (A \in S \land B \in S)) \to (A \in S \land B \in S \land C \in S)$
32	31	ex	$⊢ (A \in S \land C \in S) \to ((A \in S \land B \in S) \to (A \in S \land B \in S \land C \in S))$
33	27 32	sylbi	$⊢ ⟨A, C⟩ \in dom G \to ((A \in S \land B \in S) \to (A \in S \land B \in S \land C \in S))$
34		aovvdm	$⊢ ((A G C)) \in S \to ⟨A, C⟩ \in dom G$
35	33 34	syl11	$⊢ (A \in S \land B \in S) \to (((A G C)) \in S \to (A \in S \land B \in S \land C \in S))$
36	24 35	sylbi	$⊢ ⟨A, B⟩ \in dom G \to (((A G C)) \in S \to (A \in S \land B \in S \land C \in S))$
37	21 36	syl	$⊢ ((A G B)) \in S \to (((A G C)) \in S \to (A \in S \land B \in S \land C \in S))$
38	37	imp	$⊢ (((A G B)) \in S \land ((A G C)) \in S) \to (A \in S \land B \in S \land C \in S)$
39	20 38	sylbi	$⊢ ⟨((A G B)), ((A G C))⟩ \in dom F \to (A \in S \land B \in S \land C \in S)$
40		ndmaov	$⊢ \neg ⟨((A G B)), ((A G C))⟩ \in dom F \to ((((A G B)) F ((A G C)))) = V$
41	39 40	nsyl5	$⊢ \neg (A \in S \land B \in S \land C \in S) \to ((((A G B)) F ((A G C)))) = V$
42	17 41	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

Theorem ndmaovdistr

Proof