Metamath Proof Explorer


Theorem ltexnq

Description: Ordering on positive fractions in terms of existence of sum. Definition in Proposition 9-2.6 of Gleason p. 119. (Contributed by NM, 24-Apr-1996) (Revised by Mario Carneiro, 10-May-2013) (New usage is discouraged.)

Ref Expression
Assertion ltexnq
|- ( B e. Q. -> ( A  E. x ( A +Q x ) = B ) )

Proof

Step Hyp Ref Expression
1 ltrelnq
 |-  
2 1 brel
 |-  ( A  ( A e. Q. /\ B e. Q. ) )
3 ordpinq
 |-  ( ( A e. Q. /\ B e. Q. ) -> ( A  ( ( 1st ` A ) .N ( 2nd ` B ) ) 
4 elpqn
 |-  ( A e. Q. -> A e. ( N. X. N. ) )
5 4 adantr
 |-  ( ( A e. Q. /\ B e. Q. ) -> A e. ( N. X. N. ) )
6 xp1st
 |-  ( A e. ( N. X. N. ) -> ( 1st ` A ) e. N. )
7 5 6 syl
 |-  ( ( A e. Q. /\ B e. Q. ) -> ( 1st ` A ) e. N. )
8 elpqn
 |-  ( B e. Q. -> B e. ( N. X. N. ) )
9 8 adantl
 |-  ( ( A e. Q. /\ B e. Q. ) -> B e. ( N. X. N. ) )
10 xp2nd
 |-  ( B e. ( N. X. N. ) -> ( 2nd ` B ) e. N. )
11 9 10 syl
 |-  ( ( A e. Q. /\ B e. Q. ) -> ( 2nd ` B ) e. N. )
12 mulclpi
 |-  ( ( ( 1st ` A ) e. N. /\ ( 2nd ` B ) e. N. ) -> ( ( 1st ` A ) .N ( 2nd ` B ) ) e. N. )
13 7 11 12 syl2anc
 |-  ( ( A e. Q. /\ B e. Q. ) -> ( ( 1st ` A ) .N ( 2nd ` B ) ) e. N. )
14 xp1st
 |-  ( B e. ( N. X. N. ) -> ( 1st ` B ) e. N. )
15 9 14 syl
 |-  ( ( A e. Q. /\ B e. Q. ) -> ( 1st ` B ) e. N. )
16 xp2nd
 |-  ( A e. ( N. X. N. ) -> ( 2nd ` A ) e. N. )
17 5 16 syl
 |-  ( ( A e. Q. /\ B e. Q. ) -> ( 2nd ` A ) e. N. )
18 mulclpi
 |-  ( ( ( 1st ` B ) e. N. /\ ( 2nd ` A ) e. N. ) -> ( ( 1st ` B ) .N ( 2nd ` A ) ) e. N. )
19 15 17 18 syl2anc
 |-  ( ( A e. Q. /\ B e. Q. ) -> ( ( 1st ` B ) .N ( 2nd ` A ) ) e. N. )
20 ltexpi
 |-  ( ( ( ( 1st ` A ) .N ( 2nd ` B ) ) e. N. /\ ( ( 1st ` B ) .N ( 2nd ` A ) ) e. N. ) -> ( ( ( 1st ` A ) .N ( 2nd ` B ) )  E. y e. N. ( ( ( 1st ` A ) .N ( 2nd ` B ) ) +N y ) = ( ( 1st ` B ) .N ( 2nd ` A ) ) ) )
21 13 19 20 syl2anc
 |-  ( ( A e. Q. /\ B e. Q. ) -> ( ( ( 1st ` A ) .N ( 2nd ` B ) )  E. y e. N. ( ( ( 1st ` A ) .N ( 2nd ` B ) ) +N y ) = ( ( 1st ` B ) .N ( 2nd ` A ) ) ) )
22 relxp
 |-  Rel ( N. X. N. )
23 4 ad2antrr
 |-  ( ( ( A e. Q. /\ B e. Q. ) /\ y e. N. ) -> A e. ( N. X. N. ) )
24 1st2nd
 |-  ( ( Rel ( N. X. N. ) /\ A e. ( N. X. N. ) ) -> A = <. ( 1st ` A ) , ( 2nd ` A ) >. )
25 22 23 24 sylancr
 |-  ( ( ( A e. Q. /\ B e. Q. ) /\ y e. N. ) -> A = <. ( 1st ` A ) , ( 2nd ` A ) >. )
26 25 oveq1d
 |-  ( ( ( A e. Q. /\ B e. Q. ) /\ y e. N. ) -> ( A +pQ <. y , ( ( 2nd ` A ) .N ( 2nd ` B ) ) >. ) = ( <. ( 1st ` A ) , ( 2nd ` A ) >. +pQ <. y , ( ( 2nd ` A ) .N ( 2nd ` B ) ) >. ) )
27 7 adantr
 |-  ( ( ( A e. Q. /\ B e. Q. ) /\ y e. N. ) -> ( 1st ` A ) e. N. )
28 17 adantr
 |-  ( ( ( A e. Q. /\ B e. Q. ) /\ y e. N. ) -> ( 2nd ` A ) e. N. )
29 simpr
 |-  ( ( ( A e. Q. /\ B e. Q. ) /\ y e. N. ) -> y e. N. )
30 mulclpi
 |-  ( ( ( 2nd ` A ) e. N. /\ ( 2nd ` B ) e. N. ) -> ( ( 2nd ` A ) .N ( 2nd ` B ) ) e. N. )
31 17 11 30 syl2anc
 |-  ( ( A e. Q. /\ B e. Q. ) -> ( ( 2nd ` A ) .N ( 2nd ` B ) ) e. N. )
32 31 adantr
 |-  ( ( ( A e. Q. /\ B e. Q. ) /\ y e. N. ) -> ( ( 2nd ` A ) .N ( 2nd ` B ) ) e. N. )
33 addpipq
 |-  ( ( ( ( 1st ` A ) e. N. /\ ( 2nd ` A ) e. N. ) /\ ( y e. N. /\ ( ( 2nd ` A ) .N ( 2nd ` B ) ) e. N. ) ) -> ( <. ( 1st ` A ) , ( 2nd ` A ) >. +pQ <. y , ( ( 2nd ` A ) .N ( 2nd ` B ) ) >. ) = <. ( ( ( 1st ` A ) .N ( ( 2nd ` A ) .N ( 2nd ` B ) ) ) +N ( y .N ( 2nd ` A ) ) ) , ( ( 2nd ` A ) .N ( ( 2nd ` A ) .N ( 2nd ` B ) ) ) >. )
34 27 28 29 32 33 syl22anc
 |-  ( ( ( A e. Q. /\ B e. Q. ) /\ y e. N. ) -> ( <. ( 1st ` A ) , ( 2nd ` A ) >. +pQ <. y , ( ( 2nd ` A ) .N ( 2nd ` B ) ) >. ) = <. ( ( ( 1st ` A ) .N ( ( 2nd ` A ) .N ( 2nd ` B ) ) ) +N ( y .N ( 2nd ` A ) ) ) , ( ( 2nd ` A ) .N ( ( 2nd ` A ) .N ( 2nd ` B ) ) ) >. )
35 26 34 eqtrd
 |-  ( ( ( A e. Q. /\ B e. Q. ) /\ y e. N. ) -> ( A +pQ <. y , ( ( 2nd ` A ) .N ( 2nd ` B ) ) >. ) = <. ( ( ( 1st ` A ) .N ( ( 2nd ` A ) .N ( 2nd ` B ) ) ) +N ( y .N ( 2nd ` A ) ) ) , ( ( 2nd ` A ) .N ( ( 2nd ` A ) .N ( 2nd ` B ) ) ) >. )
36 oveq2
 |-  ( ( ( ( 1st ` A ) .N ( 2nd ` B ) ) +N y ) = ( ( 1st ` B ) .N ( 2nd ` A ) ) -> ( ( 2nd ` A ) .N ( ( ( 1st ` A ) .N ( 2nd ` B ) ) +N y ) ) = ( ( 2nd ` A ) .N ( ( 1st ` B ) .N ( 2nd ` A ) ) ) )
37 distrpi
 |-  ( ( 2nd ` A ) .N ( ( ( 1st ` A ) .N ( 2nd ` B ) ) +N y ) ) = ( ( ( 2nd ` A ) .N ( ( 1st ` A ) .N ( 2nd ` B ) ) ) +N ( ( 2nd ` A ) .N y ) )
38 fvex
 |-  ( 2nd ` A ) e. _V
39 fvex
 |-  ( 1st ` A ) e. _V
40 fvex
 |-  ( 2nd ` B ) e. _V
41 mulcompi
 |-  ( x .N y ) = ( y .N x )
42 mulasspi
 |-  ( ( x .N y ) .N z ) = ( x .N ( y .N z ) )
43 38 39 40 41 42 caov12
 |-  ( ( 2nd ` A ) .N ( ( 1st ` A ) .N ( 2nd ` B ) ) ) = ( ( 1st ` A ) .N ( ( 2nd ` A ) .N ( 2nd ` B ) ) )
44 mulcompi
 |-  ( ( 2nd ` A ) .N y ) = ( y .N ( 2nd ` A ) )
45 43 44 oveq12i
 |-  ( ( ( 2nd ` A ) .N ( ( 1st ` A ) .N ( 2nd ` B ) ) ) +N ( ( 2nd ` A ) .N y ) ) = ( ( ( 1st ` A ) .N ( ( 2nd ` A ) .N ( 2nd ` B ) ) ) +N ( y .N ( 2nd ` A ) ) )
46 37 45 eqtr2i
 |-  ( ( ( 1st ` A ) .N ( ( 2nd ` A ) .N ( 2nd ` B ) ) ) +N ( y .N ( 2nd ` A ) ) ) = ( ( 2nd ` A ) .N ( ( ( 1st ` A ) .N ( 2nd ` B ) ) +N y ) )
47 mulasspi
 |-  ( ( ( 2nd ` A ) .N ( 2nd ` A ) ) .N ( 1st ` B ) ) = ( ( 2nd ` A ) .N ( ( 2nd ` A ) .N ( 1st ` B ) ) )
48 mulcompi
 |-  ( ( 2nd ` A ) .N ( 1st ` B ) ) = ( ( 1st ` B ) .N ( 2nd ` A ) )
49 48 oveq2i
 |-  ( ( 2nd ` A ) .N ( ( 2nd ` A ) .N ( 1st ` B ) ) ) = ( ( 2nd ` A ) .N ( ( 1st ` B ) .N ( 2nd ` A ) ) )
50 47 49 eqtri
 |-  ( ( ( 2nd ` A ) .N ( 2nd ` A ) ) .N ( 1st ` B ) ) = ( ( 2nd ` A ) .N ( ( 1st ` B ) .N ( 2nd ` A ) ) )
51 36 46 50 3eqtr4g
 |-  ( ( ( ( 1st ` A ) .N ( 2nd ` B ) ) +N y ) = ( ( 1st ` B ) .N ( 2nd ` A ) ) -> ( ( ( 1st ` A ) .N ( ( 2nd ` A ) .N ( 2nd ` B ) ) ) +N ( y .N ( 2nd ` A ) ) ) = ( ( ( 2nd ` A ) .N ( 2nd ` A ) ) .N ( 1st ` B ) ) )
52 mulasspi
 |-  ( ( ( 2nd ` A ) .N ( 2nd ` A ) ) .N ( 2nd ` B ) ) = ( ( 2nd ` A ) .N ( ( 2nd ` A ) .N ( 2nd ` B ) ) )
53 52 eqcomi
 |-  ( ( 2nd ` A ) .N ( ( 2nd ` A ) .N ( 2nd ` B ) ) ) = ( ( ( 2nd ` A ) .N ( 2nd ` A ) ) .N ( 2nd ` B ) )
54 53 a1i
 |-  ( ( ( ( 1st ` A ) .N ( 2nd ` B ) ) +N y ) = ( ( 1st ` B ) .N ( 2nd ` A ) ) -> ( ( 2nd ` A ) .N ( ( 2nd ` A ) .N ( 2nd ` B ) ) ) = ( ( ( 2nd ` A ) .N ( 2nd ` A ) ) .N ( 2nd ` B ) ) )
55 51 54 opeq12d
 |-  ( ( ( ( 1st ` A ) .N ( 2nd ` B ) ) +N y ) = ( ( 1st ` B ) .N ( 2nd ` A ) ) -> <. ( ( ( 1st ` A ) .N ( ( 2nd ` A ) .N ( 2nd ` B ) ) ) +N ( y .N ( 2nd ` A ) ) ) , ( ( 2nd ` A ) .N ( ( 2nd ` A ) .N ( 2nd ` B ) ) ) >. = <. ( ( ( 2nd ` A ) .N ( 2nd ` A ) ) .N ( 1st ` B ) ) , ( ( ( 2nd ` A ) .N ( 2nd ` A ) ) .N ( 2nd ` B ) ) >. )
56 55 eqeq2d
 |-  ( ( ( ( 1st ` A ) .N ( 2nd ` B ) ) +N y ) = ( ( 1st ` B ) .N ( 2nd ` A ) ) -> ( ( A +pQ <. y , ( ( 2nd ` A ) .N ( 2nd ` B ) ) >. ) = <. ( ( ( 1st ` A ) .N ( ( 2nd ` A ) .N ( 2nd ` B ) ) ) +N ( y .N ( 2nd ` A ) ) ) , ( ( 2nd ` A ) .N ( ( 2nd ` A ) .N ( 2nd ` B ) ) ) >. <-> ( A +pQ <. y , ( ( 2nd ` A ) .N ( 2nd ` B ) ) >. ) = <. ( ( ( 2nd ` A ) .N ( 2nd ` A ) ) .N ( 1st ` B ) ) , ( ( ( 2nd ` A ) .N ( 2nd ` A ) ) .N ( 2nd ` B ) ) >. ) )
57 35 56 syl5ibcom
 |-  ( ( ( A e. Q. /\ B e. Q. ) /\ y e. N. ) -> ( ( ( ( 1st ` A ) .N ( 2nd ` B ) ) +N y ) = ( ( 1st ` B ) .N ( 2nd ` A ) ) -> ( A +pQ <. y , ( ( 2nd ` A ) .N ( 2nd ` B ) ) >. ) = <. ( ( ( 2nd ` A ) .N ( 2nd ` A ) ) .N ( 1st ` B ) ) , ( ( ( 2nd ` A ) .N ( 2nd ` A ) ) .N ( 2nd ` B ) ) >. ) )
58 fveq2
 |-  ( ( A +pQ <. y , ( ( 2nd ` A ) .N ( 2nd ` B ) ) >. ) = <. ( ( ( 2nd ` A ) .N ( 2nd ` A ) ) .N ( 1st ` B ) ) , ( ( ( 2nd ` A ) .N ( 2nd ` A ) ) .N ( 2nd ` B ) ) >. -> ( /Q ` ( A +pQ <. y , ( ( 2nd ` A ) .N ( 2nd ` B ) ) >. ) ) = ( /Q ` <. ( ( ( 2nd ` A ) .N ( 2nd ` A ) ) .N ( 1st ` B ) ) , ( ( ( 2nd ` A ) .N ( 2nd ` A ) ) .N ( 2nd ` B ) ) >. ) )
59 adderpq
 |-  ( ( /Q ` A ) +Q ( /Q ` <. y , ( ( 2nd ` A ) .N ( 2nd ` B ) ) >. ) ) = ( /Q ` ( A +pQ <. y , ( ( 2nd ` A ) .N ( 2nd ` B ) ) >. ) )
60 nqerid
 |-  ( A e. Q. -> ( /Q ` A ) = A )
61 60 ad2antrr
 |-  ( ( ( A e. Q. /\ B e. Q. ) /\ y e. N. ) -> ( /Q ` A ) = A )
62 61 oveq1d
 |-  ( ( ( A e. Q. /\ B e. Q. ) /\ y e. N. ) -> ( ( /Q ` A ) +Q ( /Q ` <. y , ( ( 2nd ` A ) .N ( 2nd ` B ) ) >. ) ) = ( A +Q ( /Q ` <. y , ( ( 2nd ` A ) .N ( 2nd ` B ) ) >. ) ) )
63 59 62 eqtr3id
 |-  ( ( ( A e. Q. /\ B e. Q. ) /\ y e. N. ) -> ( /Q ` ( A +pQ <. y , ( ( 2nd ` A ) .N ( 2nd ` B ) ) >. ) ) = ( A +Q ( /Q ` <. y , ( ( 2nd ` A ) .N ( 2nd ` B ) ) >. ) ) )
64 mulclpi
 |-  ( ( ( 2nd ` A ) e. N. /\ ( 2nd ` A ) e. N. ) -> ( ( 2nd ` A ) .N ( 2nd ` A ) ) e. N. )
65 17 17 64 syl2anc
 |-  ( ( A e. Q. /\ B e. Q. ) -> ( ( 2nd ` A ) .N ( 2nd ` A ) ) e. N. )
66 65 adantr
 |-  ( ( ( A e. Q. /\ B e. Q. ) /\ y e. N. ) -> ( ( 2nd ` A ) .N ( 2nd ` A ) ) e. N. )
67 15 adantr
 |-  ( ( ( A e. Q. /\ B e. Q. ) /\ y e. N. ) -> ( 1st ` B ) e. N. )
68 11 adantr
 |-  ( ( ( A e. Q. /\ B e. Q. ) /\ y e. N. ) -> ( 2nd ` B ) e. N. )
69 mulcanenq
 |-  ( ( ( ( 2nd ` A ) .N ( 2nd ` A ) ) e. N. /\ ( 1st ` B ) e. N. /\ ( 2nd ` B ) e. N. ) -> <. ( ( ( 2nd ` A ) .N ( 2nd ` A ) ) .N ( 1st ` B ) ) , ( ( ( 2nd ` A ) .N ( 2nd ` A ) ) .N ( 2nd ` B ) ) >. ~Q <. ( 1st ` B ) , ( 2nd ` B ) >. )
70 66 67 68 69 syl3anc
 |-  ( ( ( A e. Q. /\ B e. Q. ) /\ y e. N. ) -> <. ( ( ( 2nd ` A ) .N ( 2nd ` A ) ) .N ( 1st ` B ) ) , ( ( ( 2nd ` A ) .N ( 2nd ` A ) ) .N ( 2nd ` B ) ) >. ~Q <. ( 1st ` B ) , ( 2nd ` B ) >. )
71 8 ad2antlr
 |-  ( ( ( A e. Q. /\ B e. Q. ) /\ y e. N. ) -> B e. ( N. X. N. ) )
72 1st2nd
 |-  ( ( Rel ( N. X. N. ) /\ B e. ( N. X. N. ) ) -> B = <. ( 1st ` B ) , ( 2nd ` B ) >. )
73 22 71 72 sylancr
 |-  ( ( ( A e. Q. /\ B e. Q. ) /\ y e. N. ) -> B = <. ( 1st ` B ) , ( 2nd ` B ) >. )
74 70 73 breqtrrd
 |-  ( ( ( A e. Q. /\ B e. Q. ) /\ y e. N. ) -> <. ( ( ( 2nd ` A ) .N ( 2nd ` A ) ) .N ( 1st ` B ) ) , ( ( ( 2nd ` A ) .N ( 2nd ` A ) ) .N ( 2nd ` B ) ) >. ~Q B )
75 mulclpi
 |-  ( ( ( ( 2nd ` A ) .N ( 2nd ` A ) ) e. N. /\ ( 1st ` B ) e. N. ) -> ( ( ( 2nd ` A ) .N ( 2nd ` A ) ) .N ( 1st ` B ) ) e. N. )
76 66 67 75 syl2anc
 |-  ( ( ( A e. Q. /\ B e. Q. ) /\ y e. N. ) -> ( ( ( 2nd ` A ) .N ( 2nd ` A ) ) .N ( 1st ` B ) ) e. N. )
77 mulclpi
 |-  ( ( ( ( 2nd ` A ) .N ( 2nd ` A ) ) e. N. /\ ( 2nd ` B ) e. N. ) -> ( ( ( 2nd ` A ) .N ( 2nd ` A ) ) .N ( 2nd ` B ) ) e. N. )
78 66 68 77 syl2anc
 |-  ( ( ( A e. Q. /\ B e. Q. ) /\ y e. N. ) -> ( ( ( 2nd ` A ) .N ( 2nd ` A ) ) .N ( 2nd ` B ) ) e. N. )
79 76 78 opelxpd
 |-  ( ( ( A e. Q. /\ B e. Q. ) /\ y e. N. ) -> <. ( ( ( 2nd ` A ) .N ( 2nd ` A ) ) .N ( 1st ` B ) ) , ( ( ( 2nd ` A ) .N ( 2nd ` A ) ) .N ( 2nd ` B ) ) >. e. ( N. X. N. ) )
80 nqereq
 |-  ( ( <. ( ( ( 2nd ` A ) .N ( 2nd ` A ) ) .N ( 1st ` B ) ) , ( ( ( 2nd ` A ) .N ( 2nd ` A ) ) .N ( 2nd ` B ) ) >. e. ( N. X. N. ) /\ B e. ( N. X. N. ) ) -> ( <. ( ( ( 2nd ` A ) .N ( 2nd ` A ) ) .N ( 1st ` B ) ) , ( ( ( 2nd ` A ) .N ( 2nd ` A ) ) .N ( 2nd ` B ) ) >. ~Q B <-> ( /Q ` <. ( ( ( 2nd ` A ) .N ( 2nd ` A ) ) .N ( 1st ` B ) ) , ( ( ( 2nd ` A ) .N ( 2nd ` A ) ) .N ( 2nd ` B ) ) >. ) = ( /Q ` B ) ) )
81 79 71 80 syl2anc
 |-  ( ( ( A e. Q. /\ B e. Q. ) /\ y e. N. ) -> ( <. ( ( ( 2nd ` A ) .N ( 2nd ` A ) ) .N ( 1st ` B ) ) , ( ( ( 2nd ` A ) .N ( 2nd ` A ) ) .N ( 2nd ` B ) ) >. ~Q B <-> ( /Q ` <. ( ( ( 2nd ` A ) .N ( 2nd ` A ) ) .N ( 1st ` B ) ) , ( ( ( 2nd ` A ) .N ( 2nd ` A ) ) .N ( 2nd ` B ) ) >. ) = ( /Q ` B ) ) )
82 74 81 mpbid
 |-  ( ( ( A e. Q. /\ B e. Q. ) /\ y e. N. ) -> ( /Q ` <. ( ( ( 2nd ` A ) .N ( 2nd ` A ) ) .N ( 1st ` B ) ) , ( ( ( 2nd ` A ) .N ( 2nd ` A ) ) .N ( 2nd ` B ) ) >. ) = ( /Q ` B ) )
83 nqerid
 |-  ( B e. Q. -> ( /Q ` B ) = B )
84 83 ad2antlr
 |-  ( ( ( A e. Q. /\ B e. Q. ) /\ y e. N. ) -> ( /Q ` B ) = B )
85 82 84 eqtrd
 |-  ( ( ( A e. Q. /\ B e. Q. ) /\ y e. N. ) -> ( /Q ` <. ( ( ( 2nd ` A ) .N ( 2nd ` A ) ) .N ( 1st ` B ) ) , ( ( ( 2nd ` A ) .N ( 2nd ` A ) ) .N ( 2nd ` B ) ) >. ) = B )
86 63 85 eqeq12d
 |-  ( ( ( A e. Q. /\ B e. Q. ) /\ y e. N. ) -> ( ( /Q ` ( A +pQ <. y , ( ( 2nd ` A ) .N ( 2nd ` B ) ) >. ) ) = ( /Q ` <. ( ( ( 2nd ` A ) .N ( 2nd ` A ) ) .N ( 1st ` B ) ) , ( ( ( 2nd ` A ) .N ( 2nd ` A ) ) .N ( 2nd ` B ) ) >. ) <-> ( A +Q ( /Q ` <. y , ( ( 2nd ` A ) .N ( 2nd ` B ) ) >. ) ) = B ) )
87 58 86 syl5ib
 |-  ( ( ( A e. Q. /\ B e. Q. ) /\ y e. N. ) -> ( ( A +pQ <. y , ( ( 2nd ` A ) .N ( 2nd ` B ) ) >. ) = <. ( ( ( 2nd ` A ) .N ( 2nd ` A ) ) .N ( 1st ` B ) ) , ( ( ( 2nd ` A ) .N ( 2nd ` A ) ) .N ( 2nd ` B ) ) >. -> ( A +Q ( /Q ` <. y , ( ( 2nd ` A ) .N ( 2nd ` B ) ) >. ) ) = B ) )
88 57 87 syld
 |-  ( ( ( A e. Q. /\ B e. Q. ) /\ y e. N. ) -> ( ( ( ( 1st ` A ) .N ( 2nd ` B ) ) +N y ) = ( ( 1st ` B ) .N ( 2nd ` A ) ) -> ( A +Q ( /Q ` <. y , ( ( 2nd ` A ) .N ( 2nd ` B ) ) >. ) ) = B ) )
89 fvex
 |-  ( /Q ` <. y , ( ( 2nd ` A ) .N ( 2nd ` B ) ) >. ) e. _V
90 oveq2
 |-  ( x = ( /Q ` <. y , ( ( 2nd ` A ) .N ( 2nd ` B ) ) >. ) -> ( A +Q x ) = ( A +Q ( /Q ` <. y , ( ( 2nd ` A ) .N ( 2nd ` B ) ) >. ) ) )
91 90 eqeq1d
 |-  ( x = ( /Q ` <. y , ( ( 2nd ` A ) .N ( 2nd ` B ) ) >. ) -> ( ( A +Q x ) = B <-> ( A +Q ( /Q ` <. y , ( ( 2nd ` A ) .N ( 2nd ` B ) ) >. ) ) = B ) )
92 89 91 spcev
 |-  ( ( A +Q ( /Q ` <. y , ( ( 2nd ` A ) .N ( 2nd ` B ) ) >. ) ) = B -> E. x ( A +Q x ) = B )
93 88 92 syl6
 |-  ( ( ( A e. Q. /\ B e. Q. ) /\ y e. N. ) -> ( ( ( ( 1st ` A ) .N ( 2nd ` B ) ) +N y ) = ( ( 1st ` B ) .N ( 2nd ` A ) ) -> E. x ( A +Q x ) = B ) )
94 93 rexlimdva
 |-  ( ( A e. Q. /\ B e. Q. ) -> ( E. y e. N. ( ( ( 1st ` A ) .N ( 2nd ` B ) ) +N y ) = ( ( 1st ` B ) .N ( 2nd ` A ) ) -> E. x ( A +Q x ) = B ) )
95 21 94 sylbid
 |-  ( ( A e. Q. /\ B e. Q. ) -> ( ( ( 1st ` A ) .N ( 2nd ` B ) )  E. x ( A +Q x ) = B ) )
96 3 95 sylbid
 |-  ( ( A e. Q. /\ B e. Q. ) -> ( A  E. x ( A +Q x ) = B ) )
97 2 96 mpcom
 |-  ( A  E. x ( A +Q x ) = B )
98 eleq1
 |-  ( ( A +Q x ) = B -> ( ( A +Q x ) e. Q. <-> B e. Q. ) )
99 98 biimparc
 |-  ( ( B e. Q. /\ ( A +Q x ) = B ) -> ( A +Q x ) e. Q. )
100 addnqf
 |-  +Q : ( Q. X. Q. ) --> Q.
101 100 fdmi
 |-  dom +Q = ( Q. X. Q. )
102 0nnq
 |-  -. (/) e. Q.
103 101 102 ndmovrcl
 |-  ( ( A +Q x ) e. Q. -> ( A e. Q. /\ x e. Q. ) )
104 ltaddnq
 |-  ( ( A e. Q. /\ x e. Q. ) -> A 
105 99 103 104 3syl
 |-  ( ( B e. Q. /\ ( A +Q x ) = B ) -> A 
106 simpr
 |-  ( ( B e. Q. /\ ( A +Q x ) = B ) -> ( A +Q x ) = B )
107 105 106 breqtrd
 |-  ( ( B e. Q. /\ ( A +Q x ) = B ) -> A 
108 107 ex
 |-  ( B e. Q. -> ( ( A +Q x ) = B -> A 
109 108 exlimdv
 |-  ( B e. Q. -> ( E. x ( A +Q x ) = B -> A 
110 97 109 impbid2
 |-  ( B e. Q. -> ( A  E. x ( A +Q x ) = B ) )