Metamath Proof Explorer

Theorem distrnq

Description: Multiplication of positive fractions is distributive. (Contributed by NM, 2-Sep-1995) (Revised by Mario Carneiro, 28-Apr-2013) (New usage is discouraged.)

Ref Expression
Assertion distrnq 
|- ( A .Q ( B +Q C ) ) = ( ( A .Q B ) +Q ( A .Q C ) )

Proof

Step Hyp Ref Expression
1 mulcompi 
 |-  ( ( 1st ` A ) .N ( 1st ` B ) ) = ( ( 1st ` B ) .N ( 1st ` A ) )
2 1 oveq1i 
 |-  ( ( ( 1st ` A ) .N ( 1st ` B ) ) .N ( ( 2nd ` A ) .N ( 2nd ` C ) ) ) = ( ( ( 1st ` B ) .N ( 1st ` A ) ) .N ( ( 2nd ` A ) .N ( 2nd ` C ) ) )
3 fvex 
 |-  ( 1st ` B ) e. _V
4 fvex 
 |-  ( 1st ` A ) e. _V
5 fvex 
 |-  ( 2nd ` A ) e. _V
6 mulcompi 
 |-  ( x .N y ) = ( y .N x )
7 mulasspi 
 |-  ( ( x .N y ) .N z ) = ( x .N ( y .N z ) )
8 fvex 
 |-  ( 2nd ` C ) e. _V
9 3 4 5 6 7 8 caov411 
 |-  ( ( ( 1st ` B ) .N ( 1st ` A ) ) .N ( ( 2nd ` A ) .N ( 2nd ` C ) ) ) = ( ( ( 2nd ` A ) .N ( 1st ` A ) ) .N ( ( 1st ` B ) .N ( 2nd ` C ) ) )
10 2 9 eqtri 
 |-  ( ( ( 1st ` A ) .N ( 1st ` B ) ) .N ( ( 2nd ` A ) .N ( 2nd ` C ) ) ) = ( ( ( 2nd ` A ) .N ( 1st ` A ) ) .N ( ( 1st ` B ) .N ( 2nd ` C ) ) )
11 mulcompi 
 |-  ( ( 1st ` A ) .N ( 1st ` C ) ) = ( ( 1st ` C ) .N ( 1st ` A ) )
12 11 oveq1i 
 |-  ( ( ( 1st ` A ) .N ( 1st ` C ) ) .N ( ( 2nd ` A ) .N ( 2nd ` B ) ) ) = ( ( ( 1st ` C ) .N ( 1st ` A ) ) .N ( ( 2nd ` A ) .N ( 2nd ` B ) ) )
13 fvex 
 |-  ( 1st ` C ) e. _V
14 fvex 
 |-  ( 2nd ` B ) e. _V
15 13 4 5 6 7 14 caov411 
 |-  ( ( ( 1st ` C ) .N ( 1st ` A ) ) .N ( ( 2nd ` A ) .N ( 2nd ` B ) ) ) = ( ( ( 2nd ` A ) .N ( 1st ` A ) ) .N ( ( 1st ` C ) .N ( 2nd ` B ) ) )
16 12 15 eqtri 
 |-  ( ( ( 1st ` A ) .N ( 1st ` C ) ) .N ( ( 2nd ` A ) .N ( 2nd ` B ) ) ) = ( ( ( 2nd ` A ) .N ( 1st ` A ) ) .N ( ( 1st ` C ) .N ( 2nd ` B ) ) )
17 10 16 oveq12i 
 |-  ( ( ( ( 1st ` A ) .N ( 1st ` B ) ) .N ( ( 2nd ` A ) .N ( 2nd ` C ) ) ) +N ( ( ( 1st ` A ) .N ( 1st ` C ) ) .N ( ( 2nd ` A ) .N ( 2nd ` B ) ) ) ) = ( ( ( ( 2nd ` A ) .N ( 1st ` A ) ) .N ( ( 1st ` B ) .N ( 2nd ` C ) ) ) +N ( ( ( 2nd ` A ) .N ( 1st ` A ) ) .N ( ( 1st ` C ) .N ( 2nd ` B ) ) ) )
18 distrpi 
 |-  ( ( ( 2nd ` A ) .N ( 1st ` A ) ) .N ( ( ( 1st ` B ) .N ( 2nd ` C ) ) +N ( ( 1st ` C ) .N ( 2nd ` B ) ) ) ) = ( ( ( ( 2nd ` A ) .N ( 1st ` A ) ) .N ( ( 1st ` B ) .N ( 2nd ` C ) ) ) +N ( ( ( 2nd ` A ) .N ( 1st ` A ) ) .N ( ( 1st ` C ) .N ( 2nd ` B ) ) ) )
19 mulasspi 
 |-  ( ( ( 2nd ` A ) .N ( 1st ` A ) ) .N ( ( ( 1st ` B ) .N ( 2nd ` C ) ) +N ( ( 1st ` C ) .N ( 2nd ` B ) ) ) ) = ( ( 2nd ` A ) .N ( ( 1st ` A ) .N ( ( ( 1st ` B ) .N ( 2nd ` C ) ) +N ( ( 1st ` C ) .N ( 2nd ` B ) ) ) ) )
20 17 18 19 3eqtr2i 
 |-  ( ( ( ( 1st ` A ) .N ( 1st ` B ) ) .N ( ( 2nd ` A ) .N ( 2nd ` C ) ) ) +N ( ( ( 1st ` A ) .N ( 1st ` C ) ) .N ( ( 2nd ` A ) .N ( 2nd ` B ) ) ) ) = ( ( 2nd ` A ) .N ( ( 1st ` A ) .N ( ( ( 1st ` B ) .N ( 2nd ` C ) ) +N ( ( 1st ` C ) .N ( 2nd ` B ) ) ) ) )
21 mulasspi 
 |-  ( ( ( 2nd ` A ) .N ( 2nd ` B ) ) .N ( ( 2nd ` A ) .N ( 2nd ` C ) ) ) = ( ( 2nd ` A ) .N ( ( 2nd ` B ) .N ( ( 2nd ` A ) .N ( 2nd ` C ) ) ) )
22 14 5 8 6 7 caov12 
 |-  ( ( 2nd ` B ) .N ( ( 2nd ` A ) .N ( 2nd ` C ) ) ) = ( ( 2nd ` A ) .N ( ( 2nd ` B ) .N ( 2nd ` C ) ) )
23 22 oveq2i 
 |-  ( ( 2nd ` A ) .N ( ( 2nd ` B ) .N ( ( 2nd ` A ) .N ( 2nd ` C ) ) ) ) = ( ( 2nd ` A ) .N ( ( 2nd ` A ) .N ( ( 2nd ` B ) .N ( 2nd ` C ) ) ) )
24 21 23 eqtri 
 |-  ( ( ( 2nd ` A ) .N ( 2nd ` B ) ) .N ( ( 2nd ` A ) .N ( 2nd ` C ) ) ) = ( ( 2nd ` A ) .N ( ( 2nd ` A ) .N ( ( 2nd ` B ) .N ( 2nd ` C ) ) ) )
25 20 24 opeq12i 
 |-  <. ( ( ( ( 1st ` A ) .N ( 1st ` B ) ) .N ( ( 2nd ` A ) .N ( 2nd ` C ) ) ) +N ( ( ( 1st ` A ) .N ( 1st ` C ) ) .N ( ( 2nd ` A ) .N ( 2nd ` B ) ) ) ) , ( ( ( 2nd ` A ) .N ( 2nd ` B ) ) .N ( ( 2nd ` A ) .N ( 2nd ` C ) ) ) >. = <. ( ( 2nd ` A ) .N ( ( 1st ` A ) .N ( ( ( 1st ` B ) .N ( 2nd ` C ) ) +N ( ( 1st ` C ) .N ( 2nd ` B ) ) ) ) ) , ( ( 2nd ` A ) .N ( ( 2nd ` A ) .N ( ( 2nd ` B ) .N ( 2nd ` C ) ) ) ) >.
26 elpqn 
 |-  ( A e. Q. -> A e. ( N. X. N. ) )
27 26 3ad2ant1 
 |-  ( ( A e. Q. /\ B e. Q. /\ C e. Q. ) -> A e. ( N. X. N. ) )
28 xp2nd 
 |-  ( A e. ( N. X. N. ) -> ( 2nd ` A ) e. N. )
29 27 28 syl 
 |-  ( ( A e. Q. /\ B e. Q. /\ C e. Q. ) -> ( 2nd ` A ) e. N. )
30 xp1st 
 |-  ( A e. ( N. X. N. ) -> ( 1st ` A ) e. N. )
31 27 30 syl 
 |-  ( ( A e. Q. /\ B e. Q. /\ C e. Q. ) -> ( 1st ` A ) e. N. )
32 elpqn 
 |-  ( B e. Q. -> B e. ( N. X. N. ) )
33 32 3ad2ant2 
 |-  ( ( A e. Q. /\ B e. Q. /\ C e. Q. ) -> B e. ( N. X. N. ) )
34 xp1st 
 |-  ( B e. ( N. X. N. ) -> ( 1st ` B ) e. N. )
35 33 34 syl 
 |-  ( ( A e. Q. /\ B e. Q. /\ C e. Q. ) -> ( 1st ` B ) e. N. )
36 elpqn 
 |-  ( C e. Q. -> C e. ( N. X. N. ) )
37 36 3ad2ant3 
 |-  ( ( A e. Q. /\ B e. Q. /\ C e. Q. ) -> C e. ( N. X. N. ) )
38 xp2nd 
 |-  ( C e. ( N. X. N. ) -> ( 2nd ` C ) e. N. )
39 37 38 syl 
 |-  ( ( A e. Q. /\ B e. Q. /\ C e. Q. ) -> ( 2nd ` C ) e. N. )
40 mulclpi 
 |-  ( ( ( 1st ` B ) e. N. /\ ( 2nd ` C ) e. N. ) -> ( ( 1st ` B ) .N ( 2nd ` C ) ) e. N. )
41 35 39 40 syl2anc 
 |-  ( ( A e. Q. /\ B e. Q. /\ C e. Q. ) -> ( ( 1st ` B ) .N ( 2nd ` C ) ) e. N. )
42 xp1st 
 |-  ( C e. ( N. X. N. ) -> ( 1st ` C ) e. N. )
43 37 42 syl 
 |-  ( ( A e. Q. /\ B e. Q. /\ C e. Q. ) -> ( 1st ` C ) e. N. )
44 xp2nd 
 |-  ( B e. ( N. X. N. ) -> ( 2nd ` B ) e. N. )
45 33 44 syl 
 |-  ( ( A e. Q. /\ B e. Q. /\ C e. Q. ) -> ( 2nd ` B ) e. N. )
46 mulclpi 
 |-  ( ( ( 1st ` C ) e. N. /\ ( 2nd ` B ) e. N. ) -> ( ( 1st ` C ) .N ( 2nd ` B ) ) e. N. )
47 43 45 46 syl2anc 
 |-  ( ( A e. Q. /\ B e. Q. /\ C e. Q. ) -> ( ( 1st ` C ) .N ( 2nd ` B ) ) e. N. )
48 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. )
49 41 47 48 syl2anc 
 |-  ( ( A e. Q. /\ B e. Q. /\ C e. Q. ) -> ( ( ( 1st ` B ) .N ( 2nd ` C ) ) +N ( ( 1st ` C ) .N ( 2nd ` B ) ) ) e. N. )
50 mulclpi 
 |-  ( ( ( 1st ` A ) e. N. /\ ( ( ( 1st ` B ) .N ( 2nd ` C ) ) +N ( ( 1st ` C ) .N ( 2nd ` B ) ) ) e. N. ) -> ( ( 1st ` A ) .N ( ( ( 1st ` B ) .N ( 2nd ` C ) ) +N ( ( 1st ` C ) .N ( 2nd ` B ) ) ) ) e. N. )
51 31 49 50 syl2anc 
 |-  ( ( A e. Q. /\ B e. Q. /\ C e. Q. ) -> ( ( 1st ` A ) .N ( ( ( 1st ` B ) .N ( 2nd ` C ) ) +N ( ( 1st ` C ) .N ( 2nd ` B ) ) ) ) e. N. )
52 mulclpi 
 |-  ( ( ( 2nd ` B ) e. N. /\ ( 2nd ` C ) e. N. ) -> ( ( 2nd ` B ) .N ( 2nd ` C ) ) e. N. )
53 45 39 52 syl2anc 
 |-  ( ( A e. Q. /\ B e. Q. /\ C e. Q. ) -> ( ( 2nd ` B ) .N ( 2nd ` C ) ) e. N. )
54 mulclpi 
 |-  ( ( ( 2nd ` A ) e. N. /\ ( ( 2nd ` B ) .N ( 2nd ` C ) ) e. N. ) -> ( ( 2nd ` A ) .N ( ( 2nd ` B ) .N ( 2nd ` C ) ) ) e. N. )
55 29 53 54 syl2anc 
 |-  ( ( A e. Q. /\ B e. Q. /\ C e. Q. ) -> ( ( 2nd ` A ) .N ( ( 2nd ` B ) .N ( 2nd ` C ) ) ) e. N. )
56 mulcanenq 
 |-  ( ( ( 2nd ` A ) e. N. /\ ( ( 1st ` A ) .N ( ( ( 1st ` B ) .N ( 2nd ` C ) ) +N ( ( 1st ` C ) .N ( 2nd ` B ) ) ) ) e. N. /\ ( ( 2nd ` A ) .N ( ( 2nd ` B ) .N ( 2nd ` C ) ) ) e. N. ) -> <. ( ( 2nd ` A ) .N ( ( 1st ` A ) .N ( ( ( 1st ` B ) .N ( 2nd ` C ) ) +N ( ( 1st ` C ) .N ( 2nd ` B ) ) ) ) ) , ( ( 2nd ` A ) .N ( ( 2nd ` A ) .N ( ( 2nd ` B ) .N ( 2nd ` C ) ) ) ) >. ~Q <. ( ( 1st ` A ) .N ( ( ( 1st ` B ) .N ( 2nd ` C ) ) +N ( ( 1st ` C ) .N ( 2nd ` B ) ) ) ) , ( ( 2nd ` A ) .N ( ( 2nd ` B ) .N ( 2nd ` C ) ) ) >. )
57 29 51 55 56 syl3anc 
 |-  ( ( A e. Q. /\ B e. Q. /\ C e. Q. ) -> <. ( ( 2nd ` A ) .N ( ( 1st ` A ) .N ( ( ( 1st ` B ) .N ( 2nd ` C ) ) +N ( ( 1st ` C ) .N ( 2nd ` B ) ) ) ) ) , ( ( 2nd ` A ) .N ( ( 2nd ` A ) .N ( ( 2nd ` B ) .N ( 2nd ` C ) ) ) ) >. ~Q <. ( ( 1st ` A ) .N ( ( ( 1st ` B ) .N ( 2nd ` C ) ) +N ( ( 1st ` C ) .N ( 2nd ` B ) ) ) ) , ( ( 2nd ` A ) .N ( ( 2nd ` B ) .N ( 2nd ` C ) ) ) >. )
58 25 57 eqbrtrid 
 |-  ( ( A e. Q. /\ B e. Q. /\ C e. Q. ) -> <. ( ( ( ( 1st ` A ) .N ( 1st ` B ) ) .N ( ( 2nd ` A ) .N ( 2nd ` C ) ) ) +N ( ( ( 1st ` A ) .N ( 1st ` C ) ) .N ( ( 2nd ` A ) .N ( 2nd ` B ) ) ) ) , ( ( ( 2nd ` A ) .N ( 2nd ` B ) ) .N ( ( 2nd ` A ) .N ( 2nd ` C ) ) ) >. ~Q <. ( ( 1st ` A ) .N ( ( ( 1st ` B ) .N ( 2nd ` C ) ) +N ( ( 1st ` C ) .N ( 2nd ` B ) ) ) ) , ( ( 2nd ` A ) .N ( ( 2nd ` B ) .N ( 2nd ` C ) ) ) >. )
59 mulpipq2 
 |-  ( ( A e. ( N. X. N. ) /\ B e. ( N. X. N. ) ) -> ( A .pQ B ) = <. ( ( 1st ` A ) .N ( 1st ` B ) ) , ( ( 2nd ` A ) .N ( 2nd ` B ) ) >. )
60 27 33 59 syl2anc 
 |-  ( ( A e. Q. /\ B e. Q. /\ C e. Q. ) -> ( A .pQ B ) = <. ( ( 1st ` A ) .N ( 1st ` B ) ) , ( ( 2nd ` A ) .N ( 2nd ` B ) ) >. )
61 mulpipq2 
 |-  ( ( A e. ( N. X. N. ) /\ C e. ( N. X. N. ) ) -> ( A .pQ C ) = <. ( ( 1st ` A ) .N ( 1st ` C ) ) , ( ( 2nd ` A ) .N ( 2nd ` C ) ) >. )
62 27 37 61 syl2anc 
 |-  ( ( A e. Q. /\ B e. Q. /\ C e. Q. ) -> ( A .pQ C ) = <. ( ( 1st ` A ) .N ( 1st ` C ) ) , ( ( 2nd ` A ) .N ( 2nd ` C ) ) >. )
63 60 62 oveq12d 
 |-  ( ( A e. Q. /\ B e. Q. /\ C e. Q. ) -> ( ( A .pQ B ) +pQ ( A .pQ C ) ) = ( <. ( ( 1st ` A ) .N ( 1st ` B ) ) , ( ( 2nd ` A ) .N ( 2nd ` B ) ) >. +pQ <. ( ( 1st ` A ) .N ( 1st ` C ) ) , ( ( 2nd ` A ) .N ( 2nd ` C ) ) >. ) )
64 mulclpi 
 |-  ( ( ( 1st ` A ) e. N. /\ ( 1st ` B ) e. N. ) -> ( ( 1st ` A ) .N ( 1st ` B ) ) e. N. )
65 31 35 64 syl2anc 
 |-  ( ( A e. Q. /\ B e. Q. /\ C e. Q. ) -> ( ( 1st ` A ) .N ( 1st ` B ) ) e. N. )
66 mulclpi 
 |-  ( ( ( 2nd ` A ) e. N. /\ ( 2nd ` B ) e. N. ) -> ( ( 2nd ` A ) .N ( 2nd ` B ) ) e. N. )
67 29 45 66 syl2anc 
 |-  ( ( A e. Q. /\ B e. Q. /\ C e. Q. ) -> ( ( 2nd ` A ) .N ( 2nd ` B ) ) e. N. )
68 mulclpi 
 |-  ( ( ( 1st ` A ) e. N. /\ ( 1st ` C ) e. N. ) -> ( ( 1st ` A ) .N ( 1st ` C ) ) e. N. )
69 31 43 68 syl2anc 
 |-  ( ( A e. Q. /\ B e. Q. /\ C e. Q. ) -> ( ( 1st ` A ) .N ( 1st ` C ) ) e. N. )
70 mulclpi 
 |-  ( ( ( 2nd ` A ) e. N. /\ ( 2nd ` C ) e. N. ) -> ( ( 2nd ` A ) .N ( 2nd ` C ) ) e. N. )
71 29 39 70 syl2anc 
 |-  ( ( A e. Q. /\ B e. Q. /\ C e. Q. ) -> ( ( 2nd ` A ) .N ( 2nd ` C ) ) e. N. )
72 addpipq 
 |-  ( ( ( ( ( 1st ` A ) .N ( 1st ` B ) ) e. N. /\ ( ( 2nd ` A ) .N ( 2nd ` B ) ) e. N. ) /\ ( ( ( 1st ` A ) .N ( 1st ` C ) ) e. N. /\ ( ( 2nd ` A ) .N ( 2nd ` C ) ) e. N. ) ) -> ( <. ( ( 1st ` A ) .N ( 1st ` B ) ) , ( ( 2nd ` A ) .N ( 2nd ` B ) ) >. +pQ <. ( ( 1st ` A ) .N ( 1st ` C ) ) , ( ( 2nd ` A ) .N ( 2nd ` C ) ) >. ) = <. ( ( ( ( 1st ` A ) .N ( 1st ` B ) ) .N ( ( 2nd ` A ) .N ( 2nd ` C ) ) ) +N ( ( ( 1st ` A ) .N ( 1st ` C ) ) .N ( ( 2nd ` A ) .N ( 2nd ` B ) ) ) ) , ( ( ( 2nd ` A ) .N ( 2nd ` B ) ) .N ( ( 2nd ` A ) .N ( 2nd ` C ) ) ) >. )
73 65 67 69 71 72 syl22anc 
 |-  ( ( A e. Q. /\ B e. Q. /\ C e. Q. ) -> ( <. ( ( 1st ` A ) .N ( 1st ` B ) ) , ( ( 2nd ` A ) .N ( 2nd ` B ) ) >. +pQ <. ( ( 1st ` A ) .N ( 1st ` C ) ) , ( ( 2nd ` A ) .N ( 2nd ` C ) ) >. ) = <. ( ( ( ( 1st ` A ) .N ( 1st ` B ) ) .N ( ( 2nd ` A ) .N ( 2nd ` C ) ) ) +N ( ( ( 1st ` A ) .N ( 1st ` C ) ) .N ( ( 2nd ` A ) .N ( 2nd ` B ) ) ) ) , ( ( ( 2nd ` A ) .N ( 2nd ` B ) ) .N ( ( 2nd ` A ) .N ( 2nd ` C ) ) ) >. )
74 63 73 eqtrd 
 |-  ( ( A e. Q. /\ B e. Q. /\ C e. Q. ) -> ( ( A .pQ B ) +pQ ( A .pQ C ) ) = <. ( ( ( ( 1st ` A ) .N ( 1st ` B ) ) .N ( ( 2nd ` A ) .N ( 2nd ` C ) ) ) +N ( ( ( 1st ` A ) .N ( 1st ` C ) ) .N ( ( 2nd ` A ) .N ( 2nd ` B ) ) ) ) , ( ( ( 2nd ` A ) .N ( 2nd ` B ) ) .N ( ( 2nd ` A ) .N ( 2nd ` C ) ) ) >. )
75 relxp 
 |-  Rel ( N. X. N. )
76 1st2nd 
 |-  ( ( Rel ( N. X. N. ) /\ A e. ( N. X. N. ) ) -> A = <. ( 1st ` A ) , ( 2nd ` A ) >. )
77 75 27 76 sylancr 
 |-  ( ( A e. Q. /\ B e. Q. /\ C e. Q. ) -> A = <. ( 1st ` A ) , ( 2nd ` A ) >. )
78 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 ) ) >. )
79 33 37 78 syl2anc 
 |-  ( ( A e. Q. /\ B e. Q. /\ C e. Q. ) -> ( B +pQ C ) = <. ( ( ( 1st ` B ) .N ( 2nd ` C ) ) +N ( ( 1st ` C ) .N ( 2nd ` B ) ) ) , ( ( 2nd ` B ) .N ( 2nd ` C ) ) >. )
80 77 79 oveq12d 
 |-  ( ( A e. Q. /\ B e. Q. /\ C e. Q. ) -> ( A .pQ ( B +pQ C ) ) = ( <. ( 1st ` A ) , ( 2nd ` A ) >. .pQ <. ( ( ( 1st ` B ) .N ( 2nd ` C ) ) +N ( ( 1st ` C ) .N ( 2nd ` B ) ) ) , ( ( 2nd ` B ) .N ( 2nd ` C ) ) >. ) )
81 mulpipq 
 |-  ( ( ( ( 1st ` A ) e. N. /\ ( 2nd ` A ) e. N. ) /\ ( ( ( ( 1st ` B ) .N ( 2nd ` C ) ) +N ( ( 1st ` C ) .N ( 2nd ` B ) ) ) e. N. /\ ( ( 2nd ` B ) .N ( 2nd ` C ) ) e. N. ) ) -> ( <. ( 1st ` A ) , ( 2nd ` A ) >. .pQ <. ( ( ( 1st ` B ) .N ( 2nd ` C ) ) +N ( ( 1st ` C ) .N ( 2nd ` B ) ) ) , ( ( 2nd ` B ) .N ( 2nd ` C ) ) >. ) = <. ( ( 1st ` A ) .N ( ( ( 1st ` B ) .N ( 2nd ` C ) ) +N ( ( 1st ` C ) .N ( 2nd ` B ) ) ) ) , ( ( 2nd ` A ) .N ( ( 2nd ` B ) .N ( 2nd ` C ) ) ) >. )
82 31 29 49 53 81 syl22anc 
 |-  ( ( A e. Q. /\ B e. Q. /\ C e. Q. ) -> ( <. ( 1st ` A ) , ( 2nd ` A ) >. .pQ <. ( ( ( 1st ` B ) .N ( 2nd ` C ) ) +N ( ( 1st ` C ) .N ( 2nd ` B ) ) ) , ( ( 2nd ` B ) .N ( 2nd ` C ) ) >. ) = <. ( ( 1st ` A ) .N ( ( ( 1st ` B ) .N ( 2nd ` C ) ) +N ( ( 1st ` C ) .N ( 2nd ` B ) ) ) ) , ( ( 2nd ` A ) .N ( ( 2nd ` B ) .N ( 2nd ` C ) ) ) >. )
83 80 82 eqtrd 
 |-  ( ( A e. Q. /\ B e. Q. /\ C e. Q. ) -> ( A .pQ ( B +pQ C ) ) = <. ( ( 1st ` A ) .N ( ( ( 1st ` B ) .N ( 2nd ` C ) ) +N ( ( 1st ` C ) .N ( 2nd ` B ) ) ) ) , ( ( 2nd ` A ) .N ( ( 2nd ` B ) .N ( 2nd ` C ) ) ) >. )
84 58 74 83 3brtr4d 
 |-  ( ( A e. Q. /\ B e. Q. /\ C e. Q. ) -> ( ( A .pQ B ) +pQ ( A .pQ C ) ) ~Q ( A .pQ ( B +pQ C ) ) )
85 mulpqf 
 |-  .pQ : ( ( N. X. N. ) X. ( N. X. N. ) ) --> ( N. X. N. )
86 85 fovcl 
 |-  ( ( A e. ( N. X. N. ) /\ B e. ( N. X. N. ) ) -> ( A .pQ B ) e. ( N. X. N. ) )
87 27 33 86 syl2anc 
 |-  ( ( A e. Q. /\ B e. Q. /\ C e. Q. ) -> ( A .pQ B ) e. ( N. X. N. ) )
88 85 fovcl 
 |-  ( ( A e. ( N. X. N. ) /\ C e. ( N. X. N. ) ) -> ( A .pQ C ) e. ( N. X. N. ) )
89 27 37 88 syl2anc 
 |-  ( ( A e. Q. /\ B e. Q. /\ C e. Q. ) -> ( A .pQ C ) e. ( N. X. N. ) )
90 addpqf 
 |-  +pQ : ( ( N. X. N. ) X. ( N. X. N. ) ) --> ( N. X. N. )
91 90 fovcl 
 |-  ( ( ( A .pQ B ) e. ( N. X. N. ) /\ ( A .pQ C ) e. ( N. X. N. ) ) -> ( ( A .pQ B ) +pQ ( A .pQ C ) ) e. ( N. X. N. ) )
92 87 89 91 syl2anc 
 |-  ( ( A e. Q. /\ B e. Q. /\ C e. Q. ) -> ( ( A .pQ B ) +pQ ( A .pQ C ) ) e. ( N. X. N. ) )
93 90 fovcl 
 |-  ( ( B e. ( N. X. N. ) /\ C e. ( N. X. N. ) ) -> ( B +pQ C ) e. ( N. X. N. ) )
94 33 37 93 syl2anc 
 |-  ( ( A e. Q. /\ B e. Q. /\ C e. Q. ) -> ( B +pQ C ) e. ( N. X. N. ) )
95 85 fovcl 
 |-  ( ( A e. ( N. X. N. ) /\ ( B +pQ C ) e. ( N. X. N. ) ) -> ( A .pQ ( B +pQ C ) ) e. ( N. X. N. ) )
96 27 94 95 syl2anc 
 |-  ( ( A e. Q. /\ B e. Q. /\ C e. Q. ) -> ( A .pQ ( B +pQ C ) ) e. ( N. X. N. ) )
97 nqereq 
 |-  ( ( ( ( A .pQ B ) +pQ ( A .pQ C ) ) e. ( N. X. N. ) /\ ( A .pQ ( B +pQ C ) ) e. ( N. X. N. ) ) -> ( ( ( A .pQ B ) +pQ ( A .pQ C ) ) ~Q ( A .pQ ( B +pQ C ) ) <-> ( /Q ` ( ( A .pQ B ) +pQ ( A .pQ C ) ) ) = ( /Q ` ( A .pQ ( B +pQ C ) ) ) ) )
98 92 96 97 syl2anc 
 |-  ( ( A e. Q. /\ B e. Q. /\ C e. Q. ) -> ( ( ( A .pQ B ) +pQ ( A .pQ C ) ) ~Q ( A .pQ ( B +pQ C ) ) <-> ( /Q ` ( ( A .pQ B ) +pQ ( A .pQ C ) ) ) = ( /Q ` ( A .pQ ( B +pQ C ) ) ) ) )
99 84 98 mpbid 
 |-  ( ( A e. Q. /\ B e. Q. /\ C e. Q. ) -> ( /Q ` ( ( A .pQ B ) +pQ ( A .pQ C ) ) ) = ( /Q ` ( A .pQ ( B +pQ C ) ) ) )
100 99 eqcomd 
 |-  ( ( A e. Q. /\ B e. Q. /\ C e. Q. ) -> ( /Q ` ( A .pQ ( B +pQ C ) ) ) = ( /Q ` ( ( A .pQ B ) +pQ ( A .pQ C ) ) ) )
101 mulerpq 
 |-  ( ( /Q ` A ) .Q ( /Q ` ( B +pQ C ) ) ) = ( /Q ` ( A .pQ ( B +pQ C ) ) )
102 adderpq 
 |-  ( ( /Q ` ( A .pQ B ) ) +Q ( /Q ` ( A .pQ C ) ) ) = ( /Q ` ( ( A .pQ B ) +pQ ( A .pQ C ) ) )
103 100 101 102 3eqtr4g 
 |-  ( ( A e. Q. /\ B e. Q. /\ C e. Q. ) -> ( ( /Q ` A ) .Q ( /Q ` ( B +pQ C ) ) ) = ( ( /Q ` ( A .pQ B ) ) +Q ( /Q ` ( A .pQ C ) ) ) )
104 nqerid 
 |-  ( A e. Q. -> ( /Q ` A ) = A )
105 104 eqcomd 
 |-  ( A e. Q. -> A = ( /Q ` A ) )
106 105 3ad2ant1 
 |-  ( ( A e. Q. /\ B e. Q. /\ C e. Q. ) -> A = ( /Q ` A ) )
107 addpqnq 
 |-  ( ( B e. Q. /\ C e. Q. ) -> ( B +Q C ) = ( /Q ` ( B +pQ C ) ) )
108 107 3adant1 
 |-  ( ( A e. Q. /\ B e. Q. /\ C e. Q. ) -> ( B +Q C ) = ( /Q ` ( B +pQ C ) ) )
109 106 108 oveq12d 
 |-  ( ( A e. Q. /\ B e. Q. /\ C e. Q. ) -> ( A .Q ( B +Q C ) ) = ( ( /Q ` A ) .Q ( /Q ` ( B +pQ C ) ) ) )
110 mulpqnq 
 |-  ( ( A e. Q. /\ B e. Q. ) -> ( A .Q B ) = ( /Q ` ( A .pQ B ) ) )
111 110 3adant3 
 |-  ( ( A e. Q. /\ B e. Q. /\ C e. Q. ) -> ( A .Q B ) = ( /Q ` ( A .pQ B ) ) )
112 mulpqnq 
 |-  ( ( A e. Q. /\ C e. Q. ) -> ( A .Q C ) = ( /Q ` ( A .pQ C ) ) )
113 112 3adant2 
 |-  ( ( A e. Q. /\ B e. Q. /\ C e. Q. ) -> ( A .Q C ) = ( /Q ` ( A .pQ C ) ) )
114 111 113 oveq12d 
 |-  ( ( A e. Q. /\ B e. Q. /\ C e. Q. ) -> ( ( A .Q B ) +Q ( A .Q C ) ) = ( ( /Q ` ( A .pQ B ) ) +Q ( /Q ` ( A .pQ C ) ) ) )
115 103 109 114 3eqtr4d 
 |-  ( ( A e. Q. /\ B e. Q. /\ C e. Q. ) -> ( A .Q ( B +Q C ) ) = ( ( A .Q B ) +Q ( A .Q C ) ) )
116 addnqf 
 |-  +Q : ( Q. X. Q. ) --> Q.
117 116 fdmi 
 |-  dom +Q = ( Q. X. Q. )
118 0nnq 
 |-  -. (/) e. Q.
119 mulnqf 
 |-  .Q : ( Q. X. Q. ) --> Q.
120 119 fdmi 
 |-  dom .Q = ( Q. X. Q. )
121 117 118 120 ndmovdistr 
 |-  ( -. ( A e. Q. /\ B e. Q. /\ C e. Q. ) -> ( A .Q ( B +Q C ) ) = ( ( A .Q B ) +Q ( A .Q C ) ) )
122 115 121 pm2.61i 
 |-  ( A .Q ( B +Q C ) ) = ( ( A .Q B ) +Q ( A .Q C ) )