Theorem ndmaovdistr 47826

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

Hypotheses

Ref	Expression
ndmaov.1	⊢ dom 𝐹 = (𝑆 × 𝑆)
ndmaov.6	⊢ dom 𝐺 = (𝑆 × 𝑆)

Assertion

Ref	Expression
ndmaovdistr	⊢ (¬ (𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆 ∧ 𝐶 ∈ 𝑆) → ((𝐴𝐺 ((𝐵𝐹𝐶)) )) = (( ((𝐴𝐺𝐵)) 𝐹 ((𝐴𝐺𝐶)) )) )

Proof of Theorem ndmaovdistr

Step	Hyp	Ref	Expression
1		ndmaov.6	. . . . . 6 ⊢ dom 𝐺 = (𝑆 × 𝑆)
2	1	eleq2i 2861	. . . . 5 ⊢ (⟨𝐴, ((𝐵𝐹𝐶)) ⟩ ∈ dom 𝐺 ↔ ⟨𝐴, ((𝐵𝐹𝐶)) ⟩ ∈ (𝑆 × 𝑆))
3		opelxp 5695	. . . . 5 ⊢ (⟨𝐴, ((𝐵𝐹𝐶)) ⟩ ∈ (𝑆 × 𝑆) ↔ (𝐴 ∈ 𝑆 ∧ ((𝐵𝐹𝐶)) ∈ 𝑆))
4	2, 3	bitri 278	. . . 4 ⊢ (⟨𝐴, ((𝐵𝐹𝐶)) ⟩ ∈ dom 𝐺 ↔ (𝐴 ∈ 𝑆 ∧ ((𝐵𝐹𝐶)) ∈ 𝑆))
5		aovvdm 47804	. . . . . 6 ⊢ ( ((𝐵𝐹𝐶)) ∈ 𝑆 → ⟨𝐵, 𝐶⟩ ∈ dom 𝐹)
6		ndmaov.1	. . . . . . . . 9 ⊢ dom 𝐹 = (𝑆 × 𝑆)
7	6	eleq2i 2861	. . . . . . . 8 ⊢ (⟨𝐵, 𝐶⟩ ∈ dom 𝐹 ↔ ⟨𝐵, 𝐶⟩ ∈ (𝑆 × 𝑆))
8		opelxp 5695	. . . . . . . 8 ⊢ (⟨𝐵, 𝐶⟩ ∈ (𝑆 × 𝑆) ↔ (𝐵 ∈ 𝑆 ∧ 𝐶 ∈ 𝑆))
9	7, 8	bitri 278	. . . . . . 7 ⊢ (⟨𝐵, 𝐶⟩ ∈ dom 𝐹 ↔ (𝐵 ∈ 𝑆 ∧ 𝐶 ∈ 𝑆))
10		3anass 1109	. . . . . . . 8 ⊢ ((𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆 ∧ 𝐶 ∈ 𝑆) ↔ (𝐴 ∈ 𝑆 ∧ (𝐵 ∈ 𝑆 ∧ 𝐶 ∈ 𝑆)))
11	10	simplbi2com 507	. . . . . . 7 ⊢ ((𝐵 ∈ 𝑆 ∧ 𝐶 ∈ 𝑆) → (𝐴 ∈ 𝑆 → (𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆 ∧ 𝐶 ∈ 𝑆)))
12	9, 11	sylbi 220	. . . . . 6 ⊢ (⟨𝐵, 𝐶⟩ ∈ dom 𝐹 → (𝐴 ∈ 𝑆 → (𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆 ∧ 𝐶 ∈ 𝑆)))
13	5, 12	syl 18	. . . . 5 ⊢ ( ((𝐵𝐹𝐶)) ∈ 𝑆 → (𝐴 ∈ 𝑆 → (𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆 ∧ 𝐶 ∈ 𝑆)))
14	13	impcom 412	. . . 4 ⊢ ((𝐴 ∈ 𝑆 ∧ ((𝐵𝐹𝐶)) ∈ 𝑆) → (𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆 ∧ 𝐶 ∈ 𝑆))
15	4, 14	sylbi 220	. . 3 ⊢ (⟨𝐴, ((𝐵𝐹𝐶)) ⟩ ∈ dom 𝐺 → (𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆 ∧ 𝐶 ∈ 𝑆))
16		ndmaov 47802	. . 3 ⊢ (¬ ⟨𝐴, ((𝐵𝐹𝐶)) ⟩ ∈ dom 𝐺 → ((𝐴𝐺 ((𝐵𝐹𝐶)) )) = V)
17	15, 16	nsyl5 160	. 2 ⊢ (¬ (𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆 ∧ 𝐶 ∈ 𝑆) → ((𝐴𝐺 ((𝐵𝐹𝐶)) )) = V)
18	6	eleq2i 2861	. . . . 5 ⊢ (⟨ ((𝐴𝐺𝐵)) , ((𝐴𝐺𝐶)) ⟩ ∈ dom 𝐹 ↔ ⟨ ((𝐴𝐺𝐵)) , ((𝐴𝐺𝐶)) ⟩ ∈ (𝑆 × 𝑆))
19		opelxp 5695	. . . . 5 ⊢ (⟨ ((𝐴𝐺𝐵)) , ((𝐴𝐺𝐶)) ⟩ ∈ (𝑆 × 𝑆) ↔ ( ((𝐴𝐺𝐵)) ∈ 𝑆 ∧ ((𝐴𝐺𝐶)) ∈ 𝑆))
20	18, 19	bitri 278	. . . 4 ⊢ (⟨ ((𝐴𝐺𝐵)) , ((𝐴𝐺𝐶)) ⟩ ∈ dom 𝐹 ↔ ( ((𝐴𝐺𝐵)) ∈ 𝑆 ∧ ((𝐴𝐺𝐶)) ∈ 𝑆))
21		aovvdm 47804	. . . . . 6 ⊢ ( ((𝐴𝐺𝐵)) ∈ 𝑆 → ⟨𝐴, 𝐵⟩ ∈ dom 𝐺)
22	1	eleq2i 2861	. . . . . . . 8 ⊢ (⟨𝐴, 𝐵⟩ ∈ dom 𝐺 ↔ ⟨𝐴, 𝐵⟩ ∈ (𝑆 × 𝑆))
23		opelxp 5695	. . . . . . . 8 ⊢ (⟨𝐴, 𝐵⟩ ∈ (𝑆 × 𝑆) ↔ (𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆))
24	22, 23	bitri 278	. . . . . . 7 ⊢ (⟨𝐴, 𝐵⟩ ∈ dom 𝐺 ↔ (𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆))
25	1	eleq2i 2861	. . . . . . . . . 10 ⊢ (⟨𝐴, 𝐶⟩ ∈ dom 𝐺 ↔ ⟨𝐴, 𝐶⟩ ∈ (𝑆 × 𝑆))
26		opelxp 5695	. . . . . . . . . 10 ⊢ (⟨𝐴, 𝐶⟩ ∈ (𝑆 × 𝑆) ↔ (𝐴 ∈ 𝑆 ∧ 𝐶 ∈ 𝑆))
27	25, 26	bitri 278	. . . . . . . . 9 ⊢ (⟨𝐴, 𝐶⟩ ∈ dom 𝐺 ↔ (𝐴 ∈ 𝑆 ∧ 𝐶 ∈ 𝑆))
28		simpll 778	. . . . . . . . . . 11 ⊢ (((𝐴 ∈ 𝑆 ∧ 𝐶 ∈ 𝑆) ∧ (𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆)) → 𝐴 ∈ 𝑆)
29		simprr 784	. . . . . . . . . . 11 ⊢ (((𝐴 ∈ 𝑆 ∧ 𝐶 ∈ 𝑆) ∧ (𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆)) → 𝐵 ∈ 𝑆)
30		simplr 780	. . . . . . . . . . 11 ⊢ (((𝐴 ∈ 𝑆 ∧ 𝐶 ∈ 𝑆) ∧ (𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆)) → 𝐶 ∈ 𝑆)
31	28, 29, 30	3jca 1144	. . . . . . . . . 10 ⊢ (((𝐴 ∈ 𝑆 ∧ 𝐶 ∈ 𝑆) ∧ (𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆)) → (𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆 ∧ 𝐶 ∈ 𝑆))
32	31	ex 417	. . . . . . . . 9 ⊢ ((𝐴 ∈ 𝑆 ∧ 𝐶 ∈ 𝑆) → ((𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆) → (𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆 ∧ 𝐶 ∈ 𝑆)))
33	27, 32	sylbi 220	. . . . . . . 8 ⊢ (⟨𝐴, 𝐶⟩ ∈ dom 𝐺 → ((𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆) → (𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆 ∧ 𝐶 ∈ 𝑆)))
34		aovvdm 47804	. . . . . . . 8 ⊢ ( ((𝐴𝐺𝐶)) ∈ 𝑆 → ⟨𝐴, 𝐶⟩ ∈ dom 𝐺)
35	33, 34	syl11 34	. . . . . . 7 ⊢ ((𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆) → ( ((𝐴𝐺𝐶)) ∈ 𝑆 → (𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆 ∧ 𝐶 ∈ 𝑆)))
36	24, 35	sylbi 220	. . . . . 6 ⊢ (⟨𝐴, 𝐵⟩ ∈ dom 𝐺 → ( ((𝐴𝐺𝐶)) ∈ 𝑆 → (𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆 ∧ 𝐶 ∈ 𝑆)))
37	21, 36	syl 18	. . . . 5 ⊢ ( ((𝐴𝐺𝐵)) ∈ 𝑆 → ( ((𝐴𝐺𝐶)) ∈ 𝑆 → (𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆 ∧ 𝐶 ∈ 𝑆)))
38	37	imp 411	. . . 4 ⊢ (( ((𝐴𝐺𝐵)) ∈ 𝑆 ∧ ((𝐴𝐺𝐶)) ∈ 𝑆) → (𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆 ∧ 𝐶 ∈ 𝑆))
39	20, 38	sylbi 220	. . 3 ⊢ (⟨ ((𝐴𝐺𝐵)) , ((𝐴𝐺𝐶)) ⟩ ∈ dom 𝐹 → (𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆 ∧ 𝐶 ∈ 𝑆))
40		ndmaov 47802	. . 3 ⊢ (¬ ⟨ ((𝐴𝐺𝐵)) , ((𝐴𝐺𝐶)) ⟩ ∈ dom 𝐹 → (( ((𝐴𝐺𝐵)) 𝐹 ((𝐴𝐺𝐶)) )) = V)
41	39, 40	nsyl5 160	. 2 ⊢ (¬ (𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆 ∧ 𝐶 ∈ 𝑆) → (( ((𝐴𝐺𝐵)) 𝐹 ((𝐴𝐺𝐶)) )) = V)
42	17, 41	eqtr4d 2807	1 ⊢ (¬ (𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆 ∧ 𝐶 ∈ 𝑆) → ((𝐴𝐺 ((𝐵𝐹𝐶)) )) = (( ((𝐴𝐺𝐵)) 𝐹 ((𝐴𝐺𝐶)) )) )

Syntax hints:  ¬ wn 3   → wi 4   ∧ wa 400   ∧ w3a 1101   = wceq 1567   ∈ wcel 2149  Vcvv 3463  ⟨cop 4597   × cxp 5657  dom cdm 5659   ((caov 47737

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1822  ax-4 1836  ax-5 1937  ax-6 1994  ax-7 2035  ax-8 2151  ax-9 2159  ax-10 2182  ax-11 2198  ax-12 2219  ax-ext 2741  ax-sep 5258  ax-nul 5268  ax-pr 5402

This theorem depends on definitions:  df-bi 210  df-an 401  df-or 861  df-3an 1103  df-tru 1570  df-fal 1580  df-ex 1807  df-nf 1811  df-sb 2098  df-mo 2573  df-eu 2603  df-clab 2748  df-cleq 2761  df-clel 2844  df-nfc 2918  df-ne 2965  df-ral 3086  df-rex 3096  df-rab 3424  df-v 3465  df-sbc 3754  df-csb 3862  df-dif 3916  df-un 3918  df-in 3920  df-ss 3930  df-nul 4295  df-if 4490  df-sn 4592  df-pr 4594  df-op 4598  df-uni 4874  df-int 4914  df-br 5111  df-opab 5175  df-id 5554  df-xp 5665  df-rel 5666  df-cnv 5667  df-co 5668  df-dm 5669  df-res 5671  df-iota 6489  df-fun 6535  df-fv 6541  df-aiota 47704  df-dfat 47738  df-afv 47739  df-aov 47740

This theorem is referenced by: (None)