This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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

Proof

Step Hyp Ref Expression
1 ndmov.1 ⊢ dom 𝐹 = ( 𝑆 × 𝑆 )
2 ndmov.5 ⊢ ¬ ∅ ∈ 𝑆
3 ndmov.6 ⊢ dom 𝐺 = ( 𝑆 × 𝑆 )
4 1 2 ndmovrcl ⊢ ( ( 𝐵 𝐹 𝐶 ) ∈ 𝑆 → ( 𝐵 ∈ 𝑆 ∧ 𝐶 ∈ 𝑆 ) )
5 4 anim2i ⊢ ( ( 𝐴 ∈ 𝑆 ∧ ( 𝐵 𝐹 𝐶 ) ∈ 𝑆 ) → ( 𝐴 ∈ 𝑆 ∧ ( 𝐵 ∈ 𝑆 ∧ 𝐶 ∈ 𝑆 ) ) )
6 3anass ⊢ ( ( 𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆 ∧ 𝐶 ∈ 𝑆 ) ↔ ( 𝐴 ∈ 𝑆 ∧ ( 𝐵 ∈ 𝑆 ∧ 𝐶 ∈ 𝑆 ) ) )
7 5 6 sylibr ⊢ ( ( 𝐴 ∈ 𝑆 ∧ ( 𝐵 𝐹 𝐶 ) ∈ 𝑆 ) → ( 𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆 ∧ 𝐶 ∈ 𝑆 ) )
8 3 ndmov ⊢ ( ¬ ( 𝐴 ∈ 𝑆 ∧ ( 𝐵 𝐹 𝐶 ) ∈ 𝑆 ) → ( 𝐴 𝐺 ( 𝐵 𝐹 𝐶 ) ) = ∅ )
9 7 8 nsyl5 ⊢ ( ¬ ( 𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆 ∧ 𝐶 ∈ 𝑆 ) → ( 𝐴 𝐺 ( 𝐵 𝐹 𝐶 ) ) = ∅ )
10 3 2 ndmovrcl ⊢ ( ( 𝐴 𝐺 𝐵 ) ∈ 𝑆 → ( 𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆 ) )
11 3 2 ndmovrcl ⊢ ( ( 𝐴 𝐺 𝐶 ) ∈ 𝑆 → ( 𝐴 ∈ 𝑆 ∧ 𝐶 ∈ 𝑆 ) )
12 10 11 anim12i ⊢ ( ( ( 𝐴 𝐺 𝐵 ) ∈ 𝑆 ∧ ( 𝐴 𝐺 𝐶 ) ∈ 𝑆 ) → ( ( 𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆 ) ∧ ( 𝐴 ∈ 𝑆 ∧ 𝐶 ∈ 𝑆 ) ) )
13 anandi3 ⊢ ( ( 𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆 ∧ 𝐶 ∈ 𝑆 ) ↔ ( ( 𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆 ) ∧ ( 𝐴 ∈ 𝑆 ∧ 𝐶 ∈ 𝑆 ) ) )
14 12 13 sylibr ⊢ ( ( ( 𝐴 𝐺 𝐵 ) ∈ 𝑆 ∧ ( 𝐴 𝐺 𝐶 ) ∈ 𝑆 ) → ( 𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆 ∧ 𝐶 ∈ 𝑆 ) )
15 1 ndmov ⊢ ( ¬ ( ( 𝐴 𝐺 𝐵 ) ∈ 𝑆 ∧ ( 𝐴 𝐺 𝐶 ) ∈ 𝑆 ) → ( ( 𝐴 𝐺 𝐵 ) 𝐹 ( 𝐴 𝐺 𝐶 ) ) = ∅ )
16 14 15 nsyl5 ⊢ ( ¬ ( 𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆 ∧ 𝐶 ∈ 𝑆 ) → ( ( 𝐴 𝐺 𝐵 ) 𝐹 ( 𝐴 𝐺 𝐶 ) ) = ∅ )
17 9 16 eqtr4d ⊢ ( ¬ ( 𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆 ∧ 𝐶 ∈ 𝑆 ) → ( 𝐴 𝐺 ( 𝐵 𝐹 𝐶 ) ) = ( ( 𝐴 𝐺 𝐵 ) 𝐹 ( 𝐴 𝐺 𝐶 ) ) )