Metamath Proof Explorer

Theorem mulcanenq

Description: Lemma for distributive law: cancellation of common factor. (Contributed by NM, 2-Sep-1995) (Revised by Mario Carneiro, 8-May-2013) (New usage is discouraged.)

Ref Expression
Assertion mulcanenq 
|- ( ( A e. N. /\ B e. N. /\ C e. N. ) -> <. ( A .N B ) , ( A .N C ) >. ~Q <. B , C >. )

Proof

Step Hyp Ref Expression
1 oveq2 
 |-  ( b = B -> ( A .N b ) = ( A .N B ) )
2 1 opeq1d 
 |-  ( b = B -> <. ( A .N b ) , ( A .N c ) >. = <. ( A .N B ) , ( A .N c ) >. )
3 opeq1 
 |-  ( b = B -> <. b , c >. = <. B , c >. )
4 2 3 breq12d 
 |-  ( b = B -> ( <. ( A .N b ) , ( A .N c ) >. ~Q <. b , c >. <-> <. ( A .N B ) , ( A .N c ) >. ~Q <. B , c >. ) )
5 4 imbi2d 
 |-  ( b = B -> ( ( A e. N. -> <. ( A .N b ) , ( A .N c ) >. ~Q <. b , c >. ) <-> ( A e. N. -> <. ( A .N B ) , ( A .N c ) >. ~Q <. B , c >. ) ) )
6 oveq2 
 |-  ( c = C -> ( A .N c ) = ( A .N C ) )
7 6 opeq2d 
 |-  ( c = C -> <. ( A .N B ) , ( A .N c ) >. = <. ( A .N B ) , ( A .N C ) >. )
8 opeq2 
 |-  ( c = C -> <. B , c >. = <. B , C >. )
9 7 8 breq12d 
 |-  ( c = C -> ( <. ( A .N B ) , ( A .N c ) >. ~Q <. B , c >. <-> <. ( A .N B ) , ( A .N C ) >. ~Q <. B , C >. ) )
10 9 imbi2d 
 |-  ( c = C -> ( ( A e. N. -> <. ( A .N B ) , ( A .N c ) >. ~Q <. B , c >. ) <-> ( A e. N. -> <. ( A .N B ) , ( A .N C ) >. ~Q <. B , C >. ) ) )
11 mulcompi 
 |-  ( b .N c ) = ( c .N b )
12 11 oveq2i 
 |-  ( A .N ( b .N c ) ) = ( A .N ( c .N b ) )
13 mulasspi 
 |-  ( ( A .N b ) .N c ) = ( A .N ( b .N c ) )
14 mulasspi 
 |-  ( ( A .N c ) .N b ) = ( A .N ( c .N b ) )
15 12 13 14 3eqtr4i 
 |-  ( ( A .N b ) .N c ) = ( ( A .N c ) .N b )
16 mulclpi 
 |-  ( ( A e. N. /\ b e. N. ) -> ( A .N b ) e. N. )
17 16 3adant3 
 |-  ( ( A e. N. /\ b e. N. /\ c e. N. ) -> ( A .N b ) e. N. )
18 mulclpi 
 |-  ( ( A e. N. /\ c e. N. ) -> ( A .N c ) e. N. )
19 18 3adant2 
 |-  ( ( A e. N. /\ b e. N. /\ c e. N. ) -> ( A .N c ) e. N. )
20 3simpc 
 |-  ( ( A e. N. /\ b e. N. /\ c e. N. ) -> ( b e. N. /\ c e. N. ) )
21 enqbreq 
 |-  ( ( ( ( A .N b ) e. N. /\ ( A .N c ) e. N. ) /\ ( b e. N. /\ c e. N. ) ) -> ( <. ( A .N b ) , ( A .N c ) >. ~Q <. b , c >. <-> ( ( A .N b ) .N c ) = ( ( A .N c ) .N b ) ) )
22 17 19 20 21 syl21anc 
 |-  ( ( A e. N. /\ b e. N. /\ c e. N. ) -> ( <. ( A .N b ) , ( A .N c ) >. ~Q <. b , c >. <-> ( ( A .N b ) .N c ) = ( ( A .N c ) .N b ) ) )
23 15 22 mpbiri 
 |-  ( ( A e. N. /\ b e. N. /\ c e. N. ) -> <. ( A .N b ) , ( A .N c ) >. ~Q <. b , c >. )
24 23 3expb 
 |-  ( ( A e. N. /\ ( b e. N. /\ c e. N. ) ) -> <. ( A .N b ) , ( A .N c ) >. ~Q <. b , c >. )
25 24 expcom 
 |-  ( ( b e. N. /\ c e. N. ) -> ( A e. N. -> <. ( A .N b ) , ( A .N c ) >. ~Q <. b , c >. ) )
26 5 10 25 vtocl2ga 
 |-  ( ( B e. N. /\ C e. N. ) -> ( A e. N. -> <. ( A .N B ) , ( A .N C ) >. ~Q <. B , C >. ) )
27 26 impcom 
 |-  ( ( A e. N. /\ ( B e. N. /\ C e. N. ) ) -> <. ( A .N B ) , ( A .N C ) >. ~Q <. B , C >. )
28 27 3impb 
 |-  ( ( A e. N. /\ B e. N. /\ C e. N. ) -> <. ( A .N B ) , ( A .N C ) >. ~Q <. B , C >. )