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 imbitrid 
 |-  ( ( ( 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 ) )