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

Metamath Proof Explorer

Theorem mulerpqlem

Description: Lemma for mulerpq . (Contributed by Mario Carneiro, 8-May-2013) (New usage is discouraged.)

Ref Expression
Assertion mulerpqlem 
|- ( ( A e. ( N. X. N. ) /\ B e. ( N. X. N. ) /\ C e. ( N. X. N. ) ) -> ( A ~Q B <-> ( A .pQ C ) ~Q ( B .pQ C ) ) )

Proof

Step Hyp Ref Expression
1 xp1st 
 |-  ( A e. ( N. X. N. ) -> ( 1st ` A ) e. N. )
2 1 3ad2ant1 
 |-  ( ( A e. ( N. X. N. ) /\ B e. ( N. X. N. ) /\ C e. ( N. X. N. ) ) -> ( 1st ` A ) e. N. )
3 xp1st 
 |-  ( C e. ( N. X. N. ) -> ( 1st ` C ) e. N. )
4 3 3ad2ant3 
 |-  ( ( A e. ( N. X. N. ) /\ B e. ( N. X. N. ) /\ C e. ( N. X. N. ) ) -> ( 1st ` C ) e. N. )
5 mulclpi 
 |-  ( ( ( 1st ` A ) e. N. /\ ( 1st ` C ) e. N. ) -> ( ( 1st ` A ) .N ( 1st ` C ) ) e. N. )
6 2 4 5 syl2anc 
 |-  ( ( A e. ( N. X. N. ) /\ B e. ( N. X. N. ) /\ C e. ( N. X. N. ) ) -> ( ( 1st ` A ) .N ( 1st ` C ) ) e. N. )
7 xp2nd 
 |-  ( A e. ( N. X. N. ) -> ( 2nd ` A ) e. N. )
8 7 3ad2ant1 
 |-  ( ( A e. ( N. X. N. ) /\ B e. ( N. X. N. ) /\ C e. ( N. X. N. ) ) -> ( 2nd ` A ) e. N. )
9 xp2nd 
 |-  ( C e. ( N. X. N. ) -> ( 2nd ` C ) e. N. )
10 9 3ad2ant3 
 |-  ( ( A e. ( N. X. N. ) /\ B e. ( N. X. N. ) /\ C e. ( N. X. N. ) ) -> ( 2nd ` C ) e. N. )
11 mulclpi 
 |-  ( ( ( 2nd ` A ) e. N. /\ ( 2nd ` C ) e. N. ) -> ( ( 2nd ` A ) .N ( 2nd ` C ) ) e. N. )
12 8 10 11 syl2anc 
 |-  ( ( A e. ( N. X. N. ) /\ B e. ( N. X. N. ) /\ C e. ( N. X. N. ) ) -> ( ( 2nd ` A ) .N ( 2nd ` C ) ) e. N. )
13 xp1st 
 |-  ( B e. ( N. X. N. ) -> ( 1st ` B ) e. N. )
14 13 3ad2ant2 
 |-  ( ( A e. ( N. X. N. ) /\ B e. ( N. X. N. ) /\ C e. ( N. X. N. ) ) -> ( 1st ` B ) e. N. )
15 mulclpi 
 |-  ( ( ( 1st ` B ) e. N. /\ ( 1st ` C ) e. N. ) -> ( ( 1st ` B ) .N ( 1st ` C ) ) e. N. )
16 14 4 15 syl2anc 
 |-  ( ( A e. ( N. X. N. ) /\ B e. ( N. X. N. ) /\ C e. ( N. X. N. ) ) -> ( ( 1st ` B ) .N ( 1st ` C ) ) e. N. )
17 xp2nd 
 |-  ( B e. ( N. X. N. ) -> ( 2nd ` B ) e. N. )
18 17 3ad2ant2 
 |-  ( ( A e. ( N. X. N. ) /\ B e. ( N. X. N. ) /\ C e. ( N. X. N. ) ) -> ( 2nd ` B ) e. N. )
19 mulclpi 
 |-  ( ( ( 2nd ` B ) e. N. /\ ( 2nd ` C ) e. N. ) -> ( ( 2nd ` B ) .N ( 2nd ` C ) ) e. N. )
20 18 10 19 syl2anc 
 |-  ( ( A e. ( N. X. N. ) /\ B e. ( N. X. N. ) /\ C e. ( N. X. N. ) ) -> ( ( 2nd ` B ) .N ( 2nd ` C ) ) e. N. )
21 enqbreq 
 |-  ( ( ( ( ( 1st ` A ) .N ( 1st ` C ) ) e. N. /\ ( ( 2nd ` A ) .N ( 2nd ` C ) ) e. N. ) /\ ( ( ( 1st ` B ) .N ( 1st ` C ) ) e. N. /\ ( ( 2nd ` B ) .N ( 2nd ` C ) ) e. N. ) ) -> ( <. ( ( 1st ` A ) .N ( 1st ` C ) ) , ( ( 2nd ` A ) .N ( 2nd ` C ) ) >. ~Q <. ( ( 1st ` B ) .N ( 1st ` C ) ) , ( ( 2nd ` B ) .N ( 2nd ` C ) ) >. <-> ( ( ( 1st ` A ) .N ( 1st ` C ) ) .N ( ( 2nd ` B ) .N ( 2nd ` C ) ) ) = ( ( ( 2nd ` A ) .N ( 2nd ` C ) ) .N ( ( 1st ` B ) .N ( 1st ` C ) ) ) ) )
22 6 12 16 20 21 syl22anc 
 |-  ( ( A e. ( N. X. N. ) /\ B e. ( N. X. N. ) /\ C e. ( N. X. N. ) ) -> ( <. ( ( 1st ` A ) .N ( 1st ` C ) ) , ( ( 2nd ` A ) .N ( 2nd ` C ) ) >. ~Q <. ( ( 1st ` B ) .N ( 1st ` C ) ) , ( ( 2nd ` B ) .N ( 2nd ` C ) ) >. <-> ( ( ( 1st ` A ) .N ( 1st ` C ) ) .N ( ( 2nd ` B ) .N ( 2nd ` C ) ) ) = ( ( ( 2nd ` A ) .N ( 2nd ` C ) ) .N ( ( 1st ` B ) .N ( 1st ` C ) ) ) ) )
23 mulpipq2 
 |-  ( ( A e. ( N. X. N. ) /\ C e. ( N. X. N. ) ) -> ( A .pQ C ) = <. ( ( 1st ` A ) .N ( 1st ` C ) ) , ( ( 2nd ` A ) .N ( 2nd ` C ) ) >. )
24 23 3adant2 
 |-  ( ( A e. ( N. X. N. ) /\ B e. ( N. X. N. ) /\ C e. ( N. X. N. ) ) -> ( A .pQ C ) = <. ( ( 1st ` A ) .N ( 1st ` C ) ) , ( ( 2nd ` A ) .N ( 2nd ` C ) ) >. )
25 mulpipq2 
 |-  ( ( B e. ( N. X. N. ) /\ C e. ( N. X. N. ) ) -> ( B .pQ C ) = <. ( ( 1st ` B ) .N ( 1st ` C ) ) , ( ( 2nd ` B ) .N ( 2nd ` C ) ) >. )
26 25 3adant1 
 |-  ( ( A e. ( N. X. N. ) /\ B e. ( N. X. N. ) /\ C e. ( N. X. N. ) ) -> ( B .pQ C ) = <. ( ( 1st ` B ) .N ( 1st ` C ) ) , ( ( 2nd ` B ) .N ( 2nd ` C ) ) >. )
27 24 26 breq12d 
 |-  ( ( A e. ( N. X. N. ) /\ B e. ( N. X. N. ) /\ C e. ( N. X. N. ) ) -> ( ( A .pQ C ) ~Q ( B .pQ C ) <-> <. ( ( 1st ` A ) .N ( 1st ` C ) ) , ( ( 2nd ` A ) .N ( 2nd ` C ) ) >. ~Q <. ( ( 1st ` B ) .N ( 1st ` C ) ) , ( ( 2nd ` B ) .N ( 2nd ` C ) ) >. ) )
28 enqbreq2 
 |-  ( ( A e. ( N. X. N. ) /\ B e. ( N. X. N. ) ) -> ( A ~Q B <-> ( ( 1st ` A ) .N ( 2nd ` B ) ) = ( ( 1st ` B ) .N ( 2nd ` A ) ) ) )
29 28 3adant3 
 |-  ( ( A e. ( N. X. N. ) /\ B e. ( N. X. N. ) /\ C e. ( N. X. N. ) ) -> ( A ~Q B <-> ( ( 1st ` A ) .N ( 2nd ` B ) ) = ( ( 1st ` B ) .N ( 2nd ` A ) ) ) )
30 mulclpi 
 |-  ( ( ( 1st ` C ) e. N. /\ ( 2nd ` C ) e. N. ) -> ( ( 1st ` C ) .N ( 2nd ` C ) ) e. N. )
31 4 10 30 syl2anc 
 |-  ( ( A e. ( N. X. N. ) /\ B e. ( N. X. N. ) /\ C e. ( N. X. N. ) ) -> ( ( 1st ` C ) .N ( 2nd ` C ) ) e. N. )
32 mulclpi 
 |-  ( ( ( 1st ` A ) e. N. /\ ( 2nd ` B ) e. N. ) -> ( ( 1st ` A ) .N ( 2nd ` B ) ) e. N. )
33 2 18 32 syl2anc 
 |-  ( ( A e. ( N. X. N. ) /\ B e. ( N. X. N. ) /\ C e. ( N. X. N. ) ) -> ( ( 1st ` A ) .N ( 2nd ` B ) ) e. N. )
34 mulcanpi 
 |-  ( ( ( ( 1st ` C ) .N ( 2nd ` C ) ) e. N. /\ ( ( 1st ` A ) .N ( 2nd ` B ) ) e. N. ) -> ( ( ( ( 1st ` C ) .N ( 2nd ` C ) ) .N ( ( 1st ` A ) .N ( 2nd ` B ) ) ) = ( ( ( 1st ` C ) .N ( 2nd ` C ) ) .N ( ( 1st ` B ) .N ( 2nd ` A ) ) ) <-> ( ( 1st ` A ) .N ( 2nd ` B ) ) = ( ( 1st ` B ) .N ( 2nd ` A ) ) ) )
35 31 33 34 syl2anc 
 |-  ( ( A e. ( N. X. N. ) /\ B e. ( N. X. N. ) /\ C e. ( N. X. N. ) ) -> ( ( ( ( 1st ` C ) .N ( 2nd ` C ) ) .N ( ( 1st ` A ) .N ( 2nd ` B ) ) ) = ( ( ( 1st ` C ) .N ( 2nd ` C ) ) .N ( ( 1st ` B ) .N ( 2nd ` A ) ) ) <-> ( ( 1st ` A ) .N ( 2nd ` B ) ) = ( ( 1st ` B ) .N ( 2nd ` A ) ) ) )
36 mulcompi 
 |-  ( ( ( 1st ` C ) .N ( 2nd ` C ) ) .N ( ( 1st ` A ) .N ( 2nd ` B ) ) ) = ( ( ( 1st ` A ) .N ( 2nd ` B ) ) .N ( ( 1st ` C ) .N ( 2nd ` C ) ) )
37 fvex 
 |-  ( 1st ` A ) e. _V
38 fvex 
 |-  ( 2nd ` B ) e. _V
39 fvex 
 |-  ( 1st ` C ) e. _V
40 mulcompi 
 |-  ( x .N y ) = ( y .N x )
41 mulasspi 
 |-  ( ( x .N y ) .N z ) = ( x .N ( y .N z ) )
42 fvex 
 |-  ( 2nd ` C ) e. _V
43 37 38 39 40 41 42 caov4 
 |-  ( ( ( 1st ` A ) .N ( 2nd ` B ) ) .N ( ( 1st ` C ) .N ( 2nd ` C ) ) ) = ( ( ( 1st ` A ) .N ( 1st ` C ) ) .N ( ( 2nd ` B ) .N ( 2nd ` C ) ) )
44 36 43 eqtri 
 |-  ( ( ( 1st ` C ) .N ( 2nd ` C ) ) .N ( ( 1st ` A ) .N ( 2nd ` B ) ) ) = ( ( ( 1st ` A ) .N ( 1st ` C ) ) .N ( ( 2nd ` B ) .N ( 2nd ` C ) ) )
45 mulcompi 
 |-  ( ( ( 1st ` C ) .N ( 2nd ` C ) ) .N ( ( 1st ` B ) .N ( 2nd ` A ) ) ) = ( ( ( 1st ` B ) .N ( 2nd ` A ) ) .N ( ( 1st ` C ) .N ( 2nd ` C ) ) )
46 fvex 
 |-  ( 1st ` B ) e. _V
47 fvex 
 |-  ( 2nd ` A ) e. _V
48 46 47 39 40 41 42 caov4 
 |-  ( ( ( 1st ` B ) .N ( 2nd ` A ) ) .N ( ( 1st ` C ) .N ( 2nd ` C ) ) ) = ( ( ( 1st ` B ) .N ( 1st ` C ) ) .N ( ( 2nd ` A ) .N ( 2nd ` C ) ) )
49 mulcompi 
 |-  ( ( ( 1st ` B ) .N ( 1st ` C ) ) .N ( ( 2nd ` A ) .N ( 2nd ` C ) ) ) = ( ( ( 2nd ` A ) .N ( 2nd ` C ) ) .N ( ( 1st ` B ) .N ( 1st ` C ) ) )
50 45 48 49 3eqtri 
 |-  ( ( ( 1st ` C ) .N ( 2nd ` C ) ) .N ( ( 1st ` B ) .N ( 2nd ` A ) ) ) = ( ( ( 2nd ` A ) .N ( 2nd ` C ) ) .N ( ( 1st ` B ) .N ( 1st ` C ) ) )
51 44 50 eqeq12i 
 |-  ( ( ( ( 1st ` C ) .N ( 2nd ` C ) ) .N ( ( 1st ` A ) .N ( 2nd ` B ) ) ) = ( ( ( 1st ` C ) .N ( 2nd ` C ) ) .N ( ( 1st ` B ) .N ( 2nd ` A ) ) ) <-> ( ( ( 1st ` A ) .N ( 1st ` C ) ) .N ( ( 2nd ` B ) .N ( 2nd ` C ) ) ) = ( ( ( 2nd ` A ) .N ( 2nd ` C ) ) .N ( ( 1st ` B ) .N ( 1st ` C ) ) ) )
52 51 a1i 
 |-  ( ( A e. ( N. X. N. ) /\ B e. ( N. X. N. ) /\ C e. ( N. X. N. ) ) -> ( ( ( ( 1st ` C ) .N ( 2nd ` C ) ) .N ( ( 1st ` A ) .N ( 2nd ` B ) ) ) = ( ( ( 1st ` C ) .N ( 2nd ` C ) ) .N ( ( 1st ` B ) .N ( 2nd ` A ) ) ) <-> ( ( ( 1st ` A ) .N ( 1st ` C ) ) .N ( ( 2nd ` B ) .N ( 2nd ` C ) ) ) = ( ( ( 2nd ` A ) .N ( 2nd ` C ) ) .N ( ( 1st ` B ) .N ( 1st ` C ) ) ) ) )
53 29 35 52 3bitr2d 
 |-  ( ( A e. ( N. X. N. ) /\ B e. ( N. X. N. ) /\ C e. ( N. X. N. ) ) -> ( A ~Q B <-> ( ( ( 1st ` A ) .N ( 1st ` C ) ) .N ( ( 2nd ` B ) .N ( 2nd ` C ) ) ) = ( ( ( 2nd ` A ) .N ( 2nd ` C ) ) .N ( ( 1st ` B ) .N ( 1st ` C ) ) ) ) )
54 22 27 53 3bitr4rd 
 |-  ( ( A e. ( N. X. N. ) /\ B e. ( N. X. N. ) /\ C e. ( N. X. N. ) ) -> ( A ~Q B <-> ( A .pQ C ) ~Q ( B .pQ C ) ) )