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 F = ( S X. S )
ndmov.5 
|- -. (/) e. S
ndmov.6 
|- dom G = ( S X. S )
Assertion ndmovdistr 
|- ( -. ( A e. S /\ B e. S /\ C e. S ) -> ( A G ( B F C ) ) = ( ( A G B ) F ( A G C ) ) )

Proof

Step Hyp Ref Expression
1 ndmov.1 
 |-  dom F = ( S X. S )
2 ndmov.5 
 |-  -. (/) e. S
3 ndmov.6 
 |-  dom G = ( S X. S )
4 1 2 ndmovrcl 
 |-  ( ( B F C ) e. S -> ( B e. S /\ C e. S ) )
5 4 anim2i 
 |-  ( ( A e. S /\ ( B F C ) e. S ) -> ( A e. S /\ ( B e. S /\ C e. S ) ) )
6 3anass 
 |-  ( ( A e. S /\ B e. S /\ C e. S ) <-> ( A e. S /\ ( B e. S /\ C e. S ) ) )
7 5 6 sylibr 
 |-  ( ( A e. S /\ ( B F C ) e. S ) -> ( A e. S /\ B e. S /\ C e. S ) )
8 3 ndmov 
 |-  ( -. ( A e. S /\ ( B F C ) e. S ) -> ( A G ( B F C ) ) = (/) )
9 7 8 nsyl5 
 |-  ( -. ( A e. S /\ B e. S /\ C e. S ) -> ( A G ( B F C ) ) = (/) )
10 3 2 ndmovrcl 
 |-  ( ( A G B ) e. S -> ( A e. S /\ B e. S ) )
11 3 2 ndmovrcl 
 |-  ( ( A G C ) e. S -> ( A e. S /\ C e. S ) )
12 10 11 anim12i 
 |-  ( ( ( A G B ) e. S /\ ( A G C ) e. S ) -> ( ( A e. S /\ B e. S ) /\ ( A e. S /\ C e. S ) ) )
13 anandi3 
 |-  ( ( A e. S /\ B e. S /\ C e. S ) <-> ( ( A e. S /\ B e. S ) /\ ( A e. S /\ C e. S ) ) )
14 12 13 sylibr 
 |-  ( ( ( A G B ) e. S /\ ( A G C ) e. S ) -> ( A e. S /\ B e. S /\ C e. S ) )
15 1 ndmov 
 |-  ( -. ( ( A G B ) e. S /\ ( A G C ) e. S ) -> ( ( A G B ) F ( A G C ) ) = (/) )
16 14 15 nsyl5 
 |-  ( -. ( A e. S /\ B e. S /\ C e. S ) -> ( ( A G B ) F ( A G C ) ) = (/) )
17 9 16 eqtr4d 
 |-  ( -. ( A e. S /\ B e. S /\ C e. S ) -> ( A G ( B F C ) ) = ( ( A G B ) F ( A G C ) ) )