Metamath Proof Explorer

Theorem 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 𝐹 = ( 𝑆 × 𝑆 )
ndmaov.6 ⊢ dom 𝐺 = ( 𝑆 × 𝑆 )
Assertion ndmaovdistr ( ¬ ( 𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆 ∧ 𝐶 ∈ 𝑆 ) → (( 𝐴 𝐺 (( 𝐵 𝐹 𝐶 )) )) = (( (( 𝐴 𝐺 𝐵 )) 𝐹 (( 𝐴 𝐺 𝐶 )) )) )

Proof

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