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

Metamath Proof Explorer

Theorem adderpqlem

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

Ref Expression
Assertion adderpqlem 
|- ( ( 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 xp2nd 
 |-  ( C e. ( N. X. N. ) -> ( 2nd ` C ) e. N. )
4 3 3ad2ant3 
 |-  ( ( A e. ( N. X. N. ) /\ B e. ( N. X. N. ) /\ C e. ( N. X. N. ) ) -> ( 2nd ` C ) e. N. )
5 mulclpi 
 |-  ( ( ( 1st ` A ) e. N. /\ ( 2nd ` C ) e. N. ) -> ( ( 1st ` A ) .N ( 2nd ` 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 ( 2nd ` C ) ) e. N. )
7 xp1st 
 |-  ( C e. ( N. X. N. ) -> ( 1st ` C ) e. N. )
8 7 3ad2ant3 
 |-  ( ( A e. ( N. X. N. ) /\ B e. ( N. X. N. ) /\ C e. ( N. X. N. ) ) -> ( 1st ` C ) e. N. )
9 xp2nd 
 |-  ( A e. ( N. X. N. ) -> ( 2nd ` A ) e. N. )
10 9 3ad2ant1 
 |-  ( ( A e. ( N. X. N. ) /\ B e. ( N. X. N. ) /\ C e. ( N. X. N. ) ) -> ( 2nd ` A ) e. N. )
11 mulclpi 
 |-  ( ( ( 1st ` C ) e. N. /\ ( 2nd ` A ) e. N. ) -> ( ( 1st ` C ) .N ( 2nd ` A ) ) e. N. )
12 8 10 11 syl2anc 
 |-  ( ( A e. ( N. X. N. ) /\ B e. ( N. X. N. ) /\ C e. ( N. X. N. ) ) -> ( ( 1st ` C ) .N ( 2nd ` A ) ) e. N. )
13 addclpi 
 |-  ( ( ( ( 1st ` A ) .N ( 2nd ` C ) ) e. N. /\ ( ( 1st ` C ) .N ( 2nd ` A ) ) e. N. ) -> ( ( ( 1st ` A ) .N ( 2nd ` C ) ) +N ( ( 1st ` C ) .N ( 2nd ` A ) ) ) e. N. )
14 6 12 13 syl2anc 
 |-  ( ( A e. ( N. X. N. ) /\ B e. ( N. X. N. ) /\ C e. ( N. X. N. ) ) -> ( ( ( 1st ` A ) .N ( 2nd ` C ) ) +N ( ( 1st ` C ) .N ( 2nd ` A ) ) ) e. N. )
15 mulclpi 
 |-  ( ( ( 2nd ` A ) e. N. /\ ( 2nd ` C ) e. N. ) -> ( ( 2nd ` A ) .N ( 2nd ` C ) ) e. N. )
16 10 4 15 syl2anc 
 |-  ( ( A e. ( N. X. N. ) /\ B e. ( N. X. N. ) /\ C e. ( N. X. N. ) ) -> ( ( 2nd ` A ) .N ( 2nd ` C ) ) e. N. )
17 xp1st 
 |-  ( B e. ( N. X. N. ) -> ( 1st ` B ) e. N. )
18 17 3ad2ant2 
 |-  ( ( A e. ( N. X. N. ) /\ B e. ( N. X. N. ) /\ C e. ( N. X. N. ) ) -> ( 1st ` B ) e. N. )
19 mulclpi 
 |-  ( ( ( 1st ` B ) e. N. /\ ( 2nd ` C ) e. N. ) -> ( ( 1st ` B ) .N ( 2nd ` C ) ) e. N. )
20 18 4 19 syl2anc 
 |-  ( ( A e. ( N. X. N. ) /\ B e. ( N. X. N. ) /\ C e. ( N. X. N. ) ) -> ( ( 1st ` B ) .N ( 2nd ` C ) ) e. N. )
21 xp2nd 
 |-  ( B e. ( N. X. N. ) -> ( 2nd ` B ) e. N. )
22 21 3ad2ant2 
 |-  ( ( A e. ( N. X. N. ) /\ B e. ( N. X. N. ) /\ C e. ( N. X. N. ) ) -> ( 2nd ` B ) e. N. )
23 mulclpi 
 |-  ( ( ( 1st ` C ) e. N. /\ ( 2nd ` B ) e. N. ) -> ( ( 1st ` C ) .N ( 2nd ` B ) ) e. N. )
24 8 22 23 syl2anc 
 |-  ( ( A e. ( N. X. N. ) /\ B e. ( N. X. N. ) /\ C e. ( N. X. N. ) ) -> ( ( 1st ` C ) .N ( 2nd ` B ) ) e. N. )
25 addclpi 
 |-  ( ( ( ( 1st ` B ) .N ( 2nd ` C ) ) e. N. /\ ( ( 1st ` C ) .N ( 2nd ` B ) ) e. N. ) -> ( ( ( 1st ` B ) .N ( 2nd ` C ) ) +N ( ( 1st ` C ) .N ( 2nd ` B ) ) ) e. N. )
26 20 24 25 syl2anc 
 |-  ( ( A e. ( N. X. N. ) /\ B e. ( N. X. N. ) /\ C e. ( N. X. N. ) ) -> ( ( ( 1st ` B ) .N ( 2nd ` C ) ) +N ( ( 1st ` C ) .N ( 2nd ` B ) ) ) e. N. )
27 mulclpi 
 |-  ( ( ( 2nd ` B ) e. N. /\ ( 2nd ` C ) e. N. ) -> ( ( 2nd ` B ) .N ( 2nd ` C ) ) e. N. )
28 22 4 27 syl2anc 
 |-  ( ( A e. ( N. X. N. ) /\ B e. ( N. X. N. ) /\ C e. ( N. X. N. ) ) -> ( ( 2nd ` B ) .N ( 2nd ` C ) ) e. N. )
29 enqbreq 
 |-  ( ( ( ( ( ( 1st ` A ) .N ( 2nd ` C ) ) +N ( ( 1st ` C ) .N ( 2nd ` A ) ) ) e. N. /\ ( ( 2nd ` A ) .N ( 2nd ` C ) ) e. N. ) /\ ( ( ( ( 1st ` B ) .N ( 2nd ` C ) ) +N ( ( 1st ` C ) .N ( 2nd ` B ) ) ) e. N. /\ ( ( 2nd ` B ) .N ( 2nd ` C ) ) e. N. ) ) -> ( <. ( ( ( 1st ` A ) .N ( 2nd ` C ) ) +N ( ( 1st ` C ) .N ( 2nd ` A ) ) ) , ( ( 2nd ` A ) .N ( 2nd ` C ) ) >. ~Q <. ( ( ( 1st ` B ) .N ( 2nd ` C ) ) +N ( ( 1st ` C ) .N ( 2nd ` B ) ) ) , ( ( 2nd ` B ) .N ( 2nd ` C ) ) >. <-> ( ( ( ( 1st ` A ) .N ( 2nd ` C ) ) +N ( ( 1st ` C ) .N ( 2nd ` A ) ) ) .N ( ( 2nd ` B ) .N ( 2nd ` C ) ) ) = ( ( ( 2nd ` A ) .N ( 2nd ` C ) ) .N ( ( ( 1st ` B ) .N ( 2nd ` C ) ) +N ( ( 1st ` C ) .N ( 2nd ` B ) ) ) ) ) )
30 14 16 26 28 29 syl22anc 
 |-  ( ( A e. ( N. X. N. ) /\ B e. ( N. X. N. ) /\ C e. ( N. X. N. ) ) -> ( <. ( ( ( 1st ` A ) .N ( 2nd ` C ) ) +N ( ( 1st ` C ) .N ( 2nd ` A ) ) ) , ( ( 2nd ` A ) .N ( 2nd ` C ) ) >. ~Q <. ( ( ( 1st ` B ) .N ( 2nd ` C ) ) +N ( ( 1st ` C ) .N ( 2nd ` B ) ) ) , ( ( 2nd ` B ) .N ( 2nd ` C ) ) >. <-> ( ( ( ( 1st ` A ) .N ( 2nd ` C ) ) +N ( ( 1st ` C ) .N ( 2nd ` A ) ) ) .N ( ( 2nd ` B ) .N ( 2nd ` C ) ) ) = ( ( ( 2nd ` A ) .N ( 2nd ` C ) ) .N ( ( ( 1st ` B ) .N ( 2nd ` C ) ) +N ( ( 1st ` C ) .N ( 2nd ` B ) ) ) ) ) )
31 addpipq2 
 |-  ( ( A e. ( N. X. N. ) /\ C e. ( N. X. N. ) ) -> ( A +pQ C ) = <. ( ( ( 1st ` A ) .N ( 2nd ` C ) ) +N ( ( 1st ` C ) .N ( 2nd ` A ) ) ) , ( ( 2nd ` A ) .N ( 2nd ` C ) ) >. )
32 31 3adant2 
 |-  ( ( A e. ( N. X. N. ) /\ B e. ( N. X. N. ) /\ C e. ( N. X. N. ) ) -> ( A +pQ C ) = <. ( ( ( 1st ` A ) .N ( 2nd ` C ) ) +N ( ( 1st ` C ) .N ( 2nd ` A ) ) ) , ( ( 2nd ` A ) .N ( 2nd ` C ) ) >. )
33 addpipq2 
 |-  ( ( B e. ( N. X. N. ) /\ C e. ( N. X. N. ) ) -> ( B +pQ C ) = <. ( ( ( 1st ` B ) .N ( 2nd ` C ) ) +N ( ( 1st ` C ) .N ( 2nd ` B ) ) ) , ( ( 2nd ` B ) .N ( 2nd ` C ) ) >. )
34 33 3adant1 
 |-  ( ( A e. ( N. X. N. ) /\ B e. ( N. X. N. ) /\ C e. ( N. X. N. ) ) -> ( B +pQ C ) = <. ( ( ( 1st ` B ) .N ( 2nd ` C ) ) +N ( ( 1st ` C ) .N ( 2nd ` B ) ) ) , ( ( 2nd ` B ) .N ( 2nd ` C ) ) >. )
35 32 34 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 ( 2nd ` C ) ) +N ( ( 1st ` C ) .N ( 2nd ` A ) ) ) , ( ( 2nd ` A ) .N ( 2nd ` C ) ) >. ~Q <. ( ( ( 1st ` B ) .N ( 2nd ` C ) ) +N ( ( 1st ` C ) .N ( 2nd ` B ) ) ) , ( ( 2nd ` B ) .N ( 2nd ` C ) ) >. ) )
36 enqbreq2 
 |-  ( ( A e. ( N. X. N. ) /\ B e. ( N. X. N. ) ) -> ( A ~Q B <-> ( ( 1st ` A ) .N ( 2nd ` B ) ) = ( ( 1st ` B ) .N ( 2nd ` A ) ) ) )
37 36 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 ) ) ) )
38 mulclpi 
 |-  ( ( ( 2nd ` C ) e. N. /\ ( 2nd ` C ) e. N. ) -> ( ( 2nd ` C ) .N ( 2nd ` C ) ) e. N. )
39 4 4 38 syl2anc 
 |-  ( ( A e. ( N. X. N. ) /\ B e. ( N. X. N. ) /\ C e. ( N. X. N. ) ) -> ( ( 2nd ` C ) .N ( 2nd ` C ) ) e. N. )
40 mulclpi 
 |-  ( ( ( 1st ` A ) e. N. /\ ( 2nd ` B ) e. N. ) -> ( ( 1st ` A ) .N ( 2nd ` B ) ) e. N. )
41 2 22 40 syl2anc 
 |-  ( ( A e. ( N. X. N. ) /\ B e. ( N. X. N. ) /\ C e. ( N. X. N. ) ) -> ( ( 1st ` A ) .N ( 2nd ` B ) ) e. N. )
42 mulcanpi 
 |-  ( ( ( ( 2nd ` C ) .N ( 2nd ` C ) ) e. N. /\ ( ( 1st ` A ) .N ( 2nd ` B ) ) e. N. ) -> ( ( ( ( 2nd ` C ) .N ( 2nd ` C ) ) .N ( ( 1st ` A ) .N ( 2nd ` B ) ) ) = ( ( ( 2nd ` C ) .N ( 2nd ` C ) ) .N ( ( 1st ` B ) .N ( 2nd ` A ) ) ) <-> ( ( 1st ` A ) .N ( 2nd ` B ) ) = ( ( 1st ` B ) .N ( 2nd ` A ) ) ) )
43 39 41 42 syl2anc 
 |-  ( ( A e. ( N. X. N. ) /\ B e. ( N. X. N. ) /\ C e. ( N. X. N. ) ) -> ( ( ( ( 2nd ` C ) .N ( 2nd ` C ) ) .N ( ( 1st ` A ) .N ( 2nd ` B ) ) ) = ( ( ( 2nd ` C ) .N ( 2nd ` C ) ) .N ( ( 1st ` B ) .N ( 2nd ` A ) ) ) <-> ( ( 1st ` A ) .N ( 2nd ` B ) ) = ( ( 1st ` B ) .N ( 2nd ` A ) ) ) )
44 mulclpi 
 |-  ( ( ( ( 2nd ` A ) .N ( 2nd ` C ) ) e. N. /\ ( ( 1st ` C ) .N ( 2nd ` B ) ) e. N. ) -> ( ( ( 2nd ` A ) .N ( 2nd ` C ) ) .N ( ( 1st ` C ) .N ( 2nd ` B ) ) ) e. N. )
45 16 24 44 syl2anc 
 |-  ( ( A e. ( N. X. N. ) /\ B e. ( N. X. N. ) /\ C e. ( N. X. N. ) ) -> ( ( ( 2nd ` A ) .N ( 2nd ` C ) ) .N ( ( 1st ` C ) .N ( 2nd ` B ) ) ) e. N. )
46 mulclpi 
 |-  ( ( ( ( 2nd ` C ) .N ( 2nd ` C ) ) e. N. /\ ( ( 1st ` A ) .N ( 2nd ` B ) ) e. N. ) -> ( ( ( 2nd ` C ) .N ( 2nd ` C ) ) .N ( ( 1st ` A ) .N ( 2nd ` B ) ) ) e. N. )
47 39 41 46 syl2anc 
 |-  ( ( A e. ( N. X. N. ) /\ B e. ( N. X. N. ) /\ C e. ( N. X. N. ) ) -> ( ( ( 2nd ` C ) .N ( 2nd ` C ) ) .N ( ( 1st ` A ) .N ( 2nd ` B ) ) ) e. N. )
48 addcanpi 
 |-  ( ( ( ( ( 2nd ` A ) .N ( 2nd ` C ) ) .N ( ( 1st ` C ) .N ( 2nd ` B ) ) ) e. N. /\ ( ( ( 2nd ` C ) .N ( 2nd ` C ) ) .N ( ( 1st ` A ) .N ( 2nd ` B ) ) ) e. N. ) -> ( ( ( ( ( 2nd ` A ) .N ( 2nd ` C ) ) .N ( ( 1st ` C ) .N ( 2nd ` B ) ) ) +N ( ( ( 2nd ` C ) .N ( 2nd ` C ) ) .N ( ( 1st ` A ) .N ( 2nd ` B ) ) ) ) = ( ( ( ( 2nd ` A ) .N ( 2nd ` C ) ) .N ( ( 1st ` C ) .N ( 2nd ` B ) ) ) +N ( ( ( 2nd ` C ) .N ( 2nd ` C ) ) .N ( ( 1st ` B ) .N ( 2nd ` A ) ) ) ) <-> ( ( ( 2nd ` C ) .N ( 2nd ` C ) ) .N ( ( 1st ` A ) .N ( 2nd ` B ) ) ) = ( ( ( 2nd ` C ) .N ( 2nd ` C ) ) .N ( ( 1st ` B ) .N ( 2nd ` A ) ) ) ) )
49 45 47 48 syl2anc 
 |-  ( ( A e. ( N. X. N. ) /\ B e. ( N. X. N. ) /\ C e. ( N. X. N. ) ) -> ( ( ( ( ( 2nd ` A ) .N ( 2nd ` C ) ) .N ( ( 1st ` C ) .N ( 2nd ` B ) ) ) +N ( ( ( 2nd ` C ) .N ( 2nd ` C ) ) .N ( ( 1st ` A ) .N ( 2nd ` B ) ) ) ) = ( ( ( ( 2nd ` A ) .N ( 2nd ` C ) ) .N ( ( 1st ` C ) .N ( 2nd ` B ) ) ) +N ( ( ( 2nd ` C ) .N ( 2nd ` C ) ) .N ( ( 1st ` B ) .N ( 2nd ` A ) ) ) ) <-> ( ( ( 2nd ` C ) .N ( 2nd ` C ) ) .N ( ( 1st ` A ) .N ( 2nd ` B ) ) ) = ( ( ( 2nd ` C ) .N ( 2nd ` C ) ) .N ( ( 1st ` B ) .N ( 2nd ` A ) ) ) ) )
50 mulcompi 
 |-  ( ( ( 2nd ` C ) .N ( 2nd ` C ) ) .N ( ( 1st ` A ) .N ( 2nd ` B ) ) ) = ( ( ( 1st ` A ) .N ( 2nd ` B ) ) .N ( ( 2nd ` C ) .N ( 2nd ` C ) ) )
51 fvex 
 |-  ( 1st ` A ) e. _V
52 fvex 
 |-  ( 2nd ` B ) e. _V
53 fvex 
 |-  ( 2nd ` C ) e. _V
54 mulcompi 
 |-  ( x .N y ) = ( y .N x )
55 mulasspi 
 |-  ( ( x .N y ) .N z ) = ( x .N ( y .N z ) )
56 51 52 53 54 55 53 caov4 
 |-  ( ( ( 1st ` A ) .N ( 2nd ` B ) ) .N ( ( 2nd ` C ) .N ( 2nd ` C ) ) ) = ( ( ( 1st ` A ) .N ( 2nd ` C ) ) .N ( ( 2nd ` B ) .N ( 2nd ` C ) ) )
57 50 56 eqtri 
 |-  ( ( ( 2nd ` C ) .N ( 2nd ` C ) ) .N ( ( 1st ` A ) .N ( 2nd ` B ) ) ) = ( ( ( 1st ` A ) .N ( 2nd ` C ) ) .N ( ( 2nd ` B ) .N ( 2nd ` C ) ) )
58 fvex 
 |-  ( 2nd ` A ) e. _V
59 fvex 
 |-  ( 1st ` C ) e. _V
60 58 53 59 54 55 52 caov4 
 |-  ( ( ( 2nd ` A ) .N ( 2nd ` C ) ) .N ( ( 1st ` C ) .N ( 2nd ` B ) ) ) = ( ( ( 2nd ` A ) .N ( 1st ` C ) ) .N ( ( 2nd ` C ) .N ( 2nd ` B ) ) )
61 mulcompi 
 |-  ( ( 2nd ` A ) .N ( 1st ` C ) ) = ( ( 1st ` C ) .N ( 2nd ` A ) )
62 mulcompi 
 |-  ( ( 2nd ` C ) .N ( 2nd ` B ) ) = ( ( 2nd ` B ) .N ( 2nd ` C ) )
63 61 62 oveq12i 
 |-  ( ( ( 2nd ` A ) .N ( 1st ` C ) ) .N ( ( 2nd ` C ) .N ( 2nd ` B ) ) ) = ( ( ( 1st ` C ) .N ( 2nd ` A ) ) .N ( ( 2nd ` B ) .N ( 2nd ` C ) ) )
64 60 63 eqtri 
 |-  ( ( ( 2nd ` A ) .N ( 2nd ` C ) ) .N ( ( 1st ` C ) .N ( 2nd ` B ) ) ) = ( ( ( 1st ` C ) .N ( 2nd ` A ) ) .N ( ( 2nd ` B ) .N ( 2nd ` C ) ) )
65 57 64 oveq12i 
 |-  ( ( ( ( 2nd ` C ) .N ( 2nd ` C ) ) .N ( ( 1st ` A ) .N ( 2nd ` B ) ) ) +N ( ( ( 2nd ` A ) .N ( 2nd ` C ) ) .N ( ( 1st ` C ) .N ( 2nd ` B ) ) ) ) = ( ( ( ( 1st ` A ) .N ( 2nd ` C ) ) .N ( ( 2nd ` B ) .N ( 2nd ` C ) ) ) +N ( ( ( 1st ` C ) .N ( 2nd ` A ) ) .N ( ( 2nd ` B ) .N ( 2nd ` C ) ) ) )
66 addcompi 
 |-  ( ( ( ( 2nd ` A ) .N ( 2nd ` C ) ) .N ( ( 1st ` C ) .N ( 2nd ` B ) ) ) +N ( ( ( 2nd ` C ) .N ( 2nd ` C ) ) .N ( ( 1st ` A ) .N ( 2nd ` B ) ) ) ) = ( ( ( ( 2nd ` C ) .N ( 2nd ` C ) ) .N ( ( 1st ` A ) .N ( 2nd ` B ) ) ) +N ( ( ( 2nd ` A ) .N ( 2nd ` C ) ) .N ( ( 1st ` C ) .N ( 2nd ` B ) ) ) )
67 ovex 
 |-  ( ( 1st ` A ) .N ( 2nd ` C ) ) e. _V
68 ovex 
 |-  ( ( 1st ` C ) .N ( 2nd ` A ) ) e. _V
69 ovex 
 |-  ( ( 2nd ` B ) .N ( 2nd ` C ) ) e. _V
70 distrpi 
 |-  ( x .N ( y +N z ) ) = ( ( x .N y ) +N ( x .N z ) )
71 67 68 69 54 70 caovdir 
 |-  ( ( ( ( 1st ` A ) .N ( 2nd ` C ) ) +N ( ( 1st ` C ) .N ( 2nd ` A ) ) ) .N ( ( 2nd ` B ) .N ( 2nd ` C ) ) ) = ( ( ( ( 1st ` A ) .N ( 2nd ` C ) ) .N ( ( 2nd ` B ) .N ( 2nd ` C ) ) ) +N ( ( ( 1st ` C ) .N ( 2nd ` A ) ) .N ( ( 2nd ` B ) .N ( 2nd ` C ) ) ) )
72 65 66 71 3eqtr4i 
 |-  ( ( ( ( 2nd ` A ) .N ( 2nd ` C ) ) .N ( ( 1st ` C ) .N ( 2nd ` B ) ) ) +N ( ( ( 2nd ` C ) .N ( 2nd ` C ) ) .N ( ( 1st ` A ) .N ( 2nd ` B ) ) ) ) = ( ( ( ( 1st ` A ) .N ( 2nd ` C ) ) +N ( ( 1st ` C ) .N ( 2nd ` A ) ) ) .N ( ( 2nd ` B ) .N ( 2nd ` C ) ) )
73 addcompi 
 |-  ( ( ( ( 2nd ` A ) .N ( 2nd ` C ) ) .N ( ( 1st ` C ) .N ( 2nd ` B ) ) ) +N ( ( ( 2nd ` A ) .N ( 2nd ` C ) ) .N ( ( 1st ` B ) .N ( 2nd ` C ) ) ) ) = ( ( ( ( 2nd ` A ) .N ( 2nd ` C ) ) .N ( ( 1st ` B ) .N ( 2nd ` C ) ) ) +N ( ( ( 2nd ` A ) .N ( 2nd ` C ) ) .N ( ( 1st ` C ) .N ( 2nd ` B ) ) ) )
74 mulasspi 
 |-  ( ( ( 2nd ` C ) .N ( 2nd ` C ) ) .N ( ( 1st ` B ) .N ( 2nd ` A ) ) ) = ( ( 2nd ` C ) .N ( ( 2nd ` C ) .N ( ( 1st ` B ) .N ( 2nd ` A ) ) ) )
75 mulcompi 
 |-  ( ( 2nd ` C ) .N ( ( 2nd ` C ) .N ( ( 1st ` B ) .N ( 2nd ` A ) ) ) ) = ( ( ( 2nd ` C ) .N ( ( 1st ` B ) .N ( 2nd ` A ) ) ) .N ( 2nd ` C ) )
76 mulasspi 
 |-  ( ( ( 2nd ` A ) .N ( 2nd ` C ) ) .N ( 1st ` B ) ) = ( ( 2nd ` A ) .N ( ( 2nd ` C ) .N ( 1st ` B ) ) )
77 mulcompi 
 |-  ( ( 2nd ` A ) .N ( ( 2nd ` C ) .N ( 1st ` B ) ) ) = ( ( ( 2nd ` C ) .N ( 1st ` B ) ) .N ( 2nd ` A ) )
78 mulasspi 
 |-  ( ( ( 2nd ` C ) .N ( 1st ` B ) ) .N ( 2nd ` A ) ) = ( ( 2nd ` C ) .N ( ( 1st ` B ) .N ( 2nd ` A ) ) )
79 76 77 78 3eqtrri 
 |-  ( ( 2nd ` C ) .N ( ( 1st ` B ) .N ( 2nd ` A ) ) ) = ( ( ( 2nd ` A ) .N ( 2nd ` C ) ) .N ( 1st ` B ) )
80 79 oveq1i 
 |-  ( ( ( 2nd ` C ) .N ( ( 1st ` B ) .N ( 2nd ` A ) ) ) .N ( 2nd ` C ) ) = ( ( ( ( 2nd ` A ) .N ( 2nd ` C ) ) .N ( 1st ` B ) ) .N ( 2nd ` C ) )
81 75 80 eqtri 
 |-  ( ( 2nd ` C ) .N ( ( 2nd ` C ) .N ( ( 1st ` B ) .N ( 2nd ` A ) ) ) ) = ( ( ( ( 2nd ` A ) .N ( 2nd ` C ) ) .N ( 1st ` B ) ) .N ( 2nd ` C ) )
82 mulasspi 
 |-  ( ( ( ( 2nd ` A ) .N ( 2nd ` C ) ) .N ( 1st ` B ) ) .N ( 2nd ` C ) ) = ( ( ( 2nd ` A ) .N ( 2nd ` C ) ) .N ( ( 1st ` B ) .N ( 2nd ` C ) ) )
83 81 82 eqtri 
 |-  ( ( 2nd ` C ) .N ( ( 2nd ` C ) .N ( ( 1st ` B ) .N ( 2nd ` A ) ) ) ) = ( ( ( 2nd ` A ) .N ( 2nd ` C ) ) .N ( ( 1st ` B ) .N ( 2nd ` C ) ) )
84 74 83 eqtri 
 |-  ( ( ( 2nd ` C ) .N ( 2nd ` C ) ) .N ( ( 1st ` B ) .N ( 2nd ` A ) ) ) = ( ( ( 2nd ` A ) .N ( 2nd ` C ) ) .N ( ( 1st ` B ) .N ( 2nd ` C ) ) )
85 84 oveq2i 
 |-  ( ( ( ( 2nd ` A ) .N ( 2nd ` C ) ) .N ( ( 1st ` C ) .N ( 2nd ` B ) ) ) +N ( ( ( 2nd ` C ) .N ( 2nd ` C ) ) .N ( ( 1st ` B ) .N ( 2nd ` A ) ) ) ) = ( ( ( ( 2nd ` A ) .N ( 2nd ` C ) ) .N ( ( 1st ` C ) .N ( 2nd ` B ) ) ) +N ( ( ( 2nd ` A ) .N ( 2nd ` C ) ) .N ( ( 1st ` B ) .N ( 2nd ` C ) ) ) )
86 distrpi 
 |-  ( ( ( 2nd ` A ) .N ( 2nd ` C ) ) .N ( ( ( 1st ` B ) .N ( 2nd ` C ) ) +N ( ( 1st ` C ) .N ( 2nd ` B ) ) ) ) = ( ( ( ( 2nd ` A ) .N ( 2nd ` C ) ) .N ( ( 1st ` B ) .N ( 2nd ` C ) ) ) +N ( ( ( 2nd ` A ) .N ( 2nd ` C ) ) .N ( ( 1st ` C ) .N ( 2nd ` B ) ) ) )
87 73 85 86 3eqtr4i 
 |-  ( ( ( ( 2nd ` A ) .N ( 2nd ` C ) ) .N ( ( 1st ` C ) .N ( 2nd ` B ) ) ) +N ( ( ( 2nd ` C ) .N ( 2nd ` C ) ) .N ( ( 1st ` B ) .N ( 2nd ` A ) ) ) ) = ( ( ( 2nd ` A ) .N ( 2nd ` C ) ) .N ( ( ( 1st ` B ) .N ( 2nd ` C ) ) +N ( ( 1st ` C ) .N ( 2nd ` B ) ) ) )
88 72 87 eqeq12i 
 |-  ( ( ( ( ( 2nd ` A ) .N ( 2nd ` C ) ) .N ( ( 1st ` C ) .N ( 2nd ` B ) ) ) +N ( ( ( 2nd ` C ) .N ( 2nd ` C ) ) .N ( ( 1st ` A ) .N ( 2nd ` B ) ) ) ) = ( ( ( ( 2nd ` A ) .N ( 2nd ` C ) ) .N ( ( 1st ` C ) .N ( 2nd ` B ) ) ) +N ( ( ( 2nd ` C ) .N ( 2nd ` C ) ) .N ( ( 1st ` B ) .N ( 2nd ` A ) ) ) ) <-> ( ( ( ( 1st ` A ) .N ( 2nd ` C ) ) +N ( ( 1st ` C ) .N ( 2nd ` A ) ) ) .N ( ( 2nd ` B ) .N ( 2nd ` C ) ) ) = ( ( ( 2nd ` A ) .N ( 2nd ` C ) ) .N ( ( ( 1st ` B ) .N ( 2nd ` C ) ) +N ( ( 1st ` C ) .N ( 2nd ` B ) ) ) ) )
89 49 88 bitr3di 
 |-  ( ( A e. ( N. X. N. ) /\ B e. ( N. X. N. ) /\ C e. ( N. X. N. ) ) -> ( ( ( ( 2nd ` C ) .N ( 2nd ` C ) ) .N ( ( 1st ` A ) .N ( 2nd ` B ) ) ) = ( ( ( 2nd ` C ) .N ( 2nd ` C ) ) .N ( ( 1st ` B ) .N ( 2nd ` A ) ) ) <-> ( ( ( ( 1st ` A ) .N ( 2nd ` C ) ) +N ( ( 1st ` C ) .N ( 2nd ` A ) ) ) .N ( ( 2nd ` B ) .N ( 2nd ` C ) ) ) = ( ( ( 2nd ` A ) .N ( 2nd ` C ) ) .N ( ( ( 1st ` B ) .N ( 2nd ` C ) ) +N ( ( 1st ` C ) .N ( 2nd ` B ) ) ) ) ) )
90 37 43 89 3bitr2d 
 |-  ( ( A e. ( N. X. N. ) /\ B e. ( N. X. N. ) /\ C e. ( N. X. N. ) ) -> ( A ~Q B <-> ( ( ( ( 1st ` A ) .N ( 2nd ` C ) ) +N ( ( 1st ` C ) .N ( 2nd ` A ) ) ) .N ( ( 2nd ` B ) .N ( 2nd ` C ) ) ) = ( ( ( 2nd ` A ) .N ( 2nd ` C ) ) .N ( ( ( 1st ` B ) .N ( 2nd ` C ) ) +N ( ( 1st ` C ) .N ( 2nd ` B ) ) ) ) ) )
91 30 35 90 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 ) ) )