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

Metamath Proof Explorer

Theorem prlem934

Description: Lemma 9-3.4 of Gleason p. 122. (Contributed by NM, 25-Mar-1996) (Revised by Mario Carneiro, 11-May-2013) (New usage is discouraged.)

Ref Expression
Hypothesis prlem934.1 
|- B e. _V
Assertion prlem934 
|- ( A e. P. -> E. x e. A -. ( x +Q B ) e. A )

Proof

Step Hyp Ref Expression
1 prlem934.1 
 |-  B e. _V
2 prn0 
 |-  ( A e. P. -> A =/= (/) )
3 r19.2z 
 |-  ( ( A =/= (/) /\ A. x e. A ( x +Q B ) e. A ) -> E. x e. A ( x +Q B ) e. A )
4 3 ex 
 |-  ( A =/= (/) -> ( A. x e. A ( x +Q B ) e. A -> E. x e. A ( x +Q B ) e. A ) )
5 2 4 syl 
 |-  ( A e. P. -> ( A. x e. A ( x +Q B ) e. A -> E. x e. A ( x +Q B ) e. A ) )
6 prpssnq 
 |-  ( A e. P. -> A C. Q. )
7 6 pssssd 
 |-  ( A e. P. -> A C_ Q. )
8 7 sseld 
 |-  ( A e. P. -> ( ( x +Q B ) e. A -> ( x +Q B ) e. Q. ) )
9 addnqf 
 |-  +Q : ( Q. X. Q. ) --> Q.
10 9 fdmi 
 |-  dom +Q = ( Q. X. Q. )
11 0nnq 
 |-  -. (/) e. Q.
12 10 11 ndmovrcl 
 |-  ( ( x +Q B ) e. Q. -> ( x e. Q. /\ B e. Q. ) )
13 12 simprd 
 |-  ( ( x +Q B ) e. Q. -> B e. Q. )
14 8 13 syl6com 
 |-  ( ( x +Q B ) e. A -> ( A e. P. -> B e. Q. ) )
15 14 rexlimivw 
 |-  ( E. x e. A ( x +Q B ) e. A -> ( A e. P. -> B e. Q. ) )
16 15 com12 
 |-  ( A e. P. -> ( E. x e. A ( x +Q B ) e. A -> B e. Q. ) )
17 oveq2 
 |-  ( b = B -> ( x +Q b ) = ( x +Q B ) )
18 17 eleq1d 
 |-  ( b = B -> ( ( x +Q b ) e. A <-> ( x +Q B ) e. A ) )
19 18 ralbidv 
 |-  ( b = B -> ( A. x e. A ( x +Q b ) e. A <-> A. x e. A ( x +Q B ) e. A ) )
20 19 notbid 
 |-  ( b = B -> ( -. A. x e. A ( x +Q b ) e. A <-> -. A. x e. A ( x +Q B ) e. A ) )
21 20 imbi2d 
 |-  ( b = B -> ( ( A e. P. -> -. A. x e. A ( x +Q b ) e. A ) <-> ( A e. P. -> -. A. x e. A ( x +Q B ) e. A ) ) )
22 dfpss2 
 |-  ( A C. Q. <-> ( A C_ Q. /\ -. A = Q. ) )
23 6 22 sylib 
 |-  ( A e. P. -> ( A C_ Q. /\ -. A = Q. ) )
24 23 simprd 
 |-  ( A e. P. -> -. A = Q. )
25 24 adantr 
 |-  ( ( A e. P. /\ b e. Q. ) -> -. A = Q. )
26 7 3ad2ant1 
 |-  ( ( A e. P. /\ b e. Q. /\ A. x e. A ( x +Q b ) e. A ) -> A C_ Q. )
27 simpl1 
 |-  ( ( ( A e. P. /\ b e. Q. /\ A. x e. A ( x +Q b ) e. A ) /\ w e. Q. ) -> A e. P. )
28 n0 
 |-  ( A =/= (/) <-> E. y y e. A )
29 2 28 sylib 
 |-  ( A e. P. -> E. y y e. A )
30 27 29 syl 
 |-  ( ( ( A e. P. /\ b e. Q. /\ A. x e. A ( x +Q b ) e. A ) /\ w e. Q. ) -> E. y y e. A )
31 simprl 
 |-  ( ( ( A e. P. /\ b e. Q. /\ A. x e. A ( x +Q b ) e. A ) /\ ( w e. Q. /\ y e. A ) ) -> w e. Q. )
32 simpl2 
 |-  ( ( ( A e. P. /\ b e. Q. /\ A. x e. A ( x +Q b ) e. A ) /\ ( w e. Q. /\ y e. A ) ) -> b e. Q. )
33 recclnq 
 |-  ( b e. Q. -> ( *Q ` b ) e. Q. )
34 mulclnq 
 |-  ( ( w e. Q. /\ ( *Q ` b ) e. Q. ) -> ( w .Q ( *Q ` b ) ) e. Q. )
35 archnq 
 |-  ( ( w .Q ( *Q ` b ) ) e. Q. -> E. z e. N. ( w .Q ( *Q ` b ) ) . )
36 34 35 syl 
 |-  ( ( w e. Q. /\ ( *Q ` b ) e. Q. ) -> E. z e. N. ( w .Q ( *Q ` b ) ) . )
37 33 36 sylan2 
 |-  ( ( w e. Q. /\ b e. Q. ) -> E. z e. N. ( w .Q ( *Q ` b ) ) . )
38 31 32 37 syl2anc 
 |-  ( ( ( A e. P. /\ b e. Q. /\ A. x e. A ( x +Q b ) e. A ) /\ ( w e. Q. /\ y e. A ) ) -> E. z e. N. ( w .Q ( *Q ` b ) ) . )
39 simpll2 
 |-  ( ( ( ( A e. P. /\ b e. Q. /\ A. x e. A ( x +Q b ) e. A ) /\ ( w e. Q. /\ y e. A ) ) /\ ( z e. N. /\ ( w .Q ( *Q ` b ) ) . ) ) -> b e. Q. )
40 simplrl 
 |-  ( ( ( ( A e. P. /\ b e. Q. /\ A. x e. A ( x +Q b ) e. A ) /\ ( w e. Q. /\ y e. A ) ) /\ ( z e. N. /\ ( w .Q ( *Q ` b ) ) . ) ) -> w e. Q. )
41 simprr 
 |-  ( ( ( ( A e. P. /\ b e. Q. /\ A. x e. A ( x +Q b ) e. A ) /\ ( w e. Q. /\ y e. A ) ) /\ ( z e. N. /\ ( w .Q ( *Q ` b ) ) . ) ) -> ( w .Q ( *Q ` b ) ) . )
42 ltmnq 
 |-  ( b e. Q. -> ( ( w .Q ( *Q ` b ) ) . <-> ( b .Q ( w .Q ( *Q ` b ) ) ) . ) ) )
43 vex 
 |-  b e. _V
44 vex 
 |-  w e. _V
45 fvex 
 |-  ( *Q ` b ) e. _V
46 mulcomnq 
 |-  ( v .Q x ) = ( x .Q v )
47 mulassnq 
 |-  ( ( v .Q x ) .Q y ) = ( v .Q ( x .Q y ) )
48 43 44 45 46 47 caov12 
 |-  ( b .Q ( w .Q ( *Q ` b ) ) ) = ( w .Q ( b .Q ( *Q ` b ) ) )
49 mulcomnq 
 |-  ( b .Q <. z , 1o >. ) = ( <. z , 1o >. .Q b )
50 48 49 breq12i 
 |-  ( ( b .Q ( w .Q ( *Q ` b ) ) ) . ) <-> ( w .Q ( b .Q ( *Q ` b ) ) ) . .Q b ) )
51 42 50 bitrdi 
 |-  ( b e. Q. -> ( ( w .Q ( *Q ` b ) ) . <-> ( w .Q ( b .Q ( *Q ` b ) ) ) . .Q b ) ) )
52 51 adantr 
 |-  ( ( b e. Q. /\ w e. Q. ) -> ( ( w .Q ( *Q ` b ) ) . <-> ( w .Q ( b .Q ( *Q ` b ) ) ) . .Q b ) ) )
53 recidnq 
 |-  ( b e. Q. -> ( b .Q ( *Q ` b ) ) = 1Q )
54 53 oveq2d 
 |-  ( b e. Q. -> ( w .Q ( b .Q ( *Q ` b ) ) ) = ( w .Q 1Q ) )
55 mulidnq 
 |-  ( w e. Q. -> ( w .Q 1Q ) = w )
56 54 55 sylan9eq 
 |-  ( ( b e. Q. /\ w e. Q. ) -> ( w .Q ( b .Q ( *Q ` b ) ) ) = w )
57 56 breq1d 
 |-  ( ( b e. Q. /\ w e. Q. ) -> ( ( w .Q ( b .Q ( *Q ` b ) ) ) . .Q b ) <-> w . .Q b ) ) )
58 52 57 bitrd 
 |-  ( ( b e. Q. /\ w e. Q. ) -> ( ( w .Q ( *Q ` b ) ) . <-> w . .Q b ) ) )
59 58 biimpa 
 |-  ( ( ( b e. Q. /\ w e. Q. ) /\ ( w .Q ( *Q ` b ) ) . ) -> w . .Q b ) )
60 39 40 41 59 syl21anc 
 |-  ( ( ( ( A e. P. /\ b e. Q. /\ A. x e. A ( x +Q b ) e. A ) /\ ( w e. Q. /\ y e. A ) ) /\ ( z e. N. /\ ( w .Q ( *Q ` b ) ) . ) ) -> w . .Q b ) )
61 simprl 
 |-  ( ( ( ( A e. P. /\ b e. Q. /\ A. x e. A ( x +Q b ) e. A ) /\ ( w e. Q. /\ y e. A ) ) /\ ( z e. N. /\ ( w .Q ( *Q ` b ) ) . ) ) -> z e. N. )
62 pinq 
 |-  ( z e. N. -> <. z , 1o >. e. Q. )
63 mulclnq 
 |-  ( ( <. z , 1o >. e. Q. /\ b e. Q. ) -> ( <. z , 1o >. .Q b ) e. Q. )
64 62 63 sylan 
 |-  ( ( z e. N. /\ b e. Q. ) -> ( <. z , 1o >. .Q b ) e. Q. )
65 61 39 64 syl2anc 
 |-  ( ( ( ( A e. P. /\ b e. Q. /\ A. x e. A ( x +Q b ) e. A ) /\ ( w e. Q. /\ y e. A ) ) /\ ( z e. N. /\ ( w .Q ( *Q ` b ) ) . ) ) -> ( <. z , 1o >. .Q b ) e. Q. )
66 simpll1 
 |-  ( ( ( ( A e. P. /\ b e. Q. /\ A. x e. A ( x +Q b ) e. A ) /\ ( w e. Q. /\ y e. A ) ) /\ ( z e. N. /\ ( w .Q ( *Q ` b ) ) . ) ) -> A e. P. )
67 simplrr 
 |-  ( ( ( ( A e. P. /\ b e. Q. /\ A. x e. A ( x +Q b ) e. A ) /\ ( w e. Q. /\ y e. A ) ) /\ ( z e. N. /\ ( w .Q ( *Q ` b ) ) . ) ) -> y e. A )
68 elprnq 
 |-  ( ( A e. P. /\ y e. A ) -> y e. Q. )
69 66 67 68 syl2anc 
 |-  ( ( ( ( A e. P. /\ b e. Q. /\ A. x e. A ( x +Q b ) e. A ) /\ ( w e. Q. /\ y e. A ) ) /\ ( z e. N. /\ ( w .Q ( *Q ` b ) ) . ) ) -> y e. Q. )
70 ltaddnq 
 |-  ( ( ( <. z , 1o >. .Q b ) e. Q. /\ y e. Q. ) -> ( <. z , 1o >. .Q b ) . .Q b ) +Q y ) )
71 addcomnq 
 |-  ( ( <. z , 1o >. .Q b ) +Q y ) = ( y +Q ( <. z , 1o >. .Q b ) )
72 70 71 breqtrdi 
 |-  ( ( ( <. z , 1o >. .Q b ) e. Q. /\ y e. Q. ) -> ( <. z , 1o >. .Q b ) . .Q b ) ) )
73 65 69 72 syl2anc 
 |-  ( ( ( ( A e. P. /\ b e. Q. /\ A. x e. A ( x +Q b ) e. A ) /\ ( w e. Q. /\ y e. A ) ) /\ ( z e. N. /\ ( w .Q ( *Q ` b ) ) . ) ) -> ( <. z , 1o >. .Q b ) . .Q b ) ) )
74 ltsonq 
 |-
75 ltrelnq 
 |-
76 74 75 sotri 
 |-  ( ( w . .Q b ) /\ ( <. z , 1o >. .Q b ) . .Q b ) ) ) -> w . .Q b ) ) )
77 60 73 76 syl2anc 
 |-  ( ( ( ( A e. P. /\ b e. Q. /\ A. x e. A ( x +Q b ) e. A ) /\ ( w e. Q. /\ y e. A ) ) /\ ( z e. N. /\ ( w .Q ( *Q ` b ) ) . ) ) -> w . .Q b ) ) )
78 simpll3 
 |-  ( ( ( ( A e. P. /\ b e. Q. /\ A. x e. A ( x +Q b ) e. A ) /\ ( w e. Q. /\ y e. A ) ) /\ ( z e. N. /\ ( w .Q ( *Q ` b ) ) . ) ) -> A. x e. A ( x +Q b ) e. A )
79 opeq1 
 |-  ( w = 1o -> <. w , 1o >. = <. 1o , 1o >. )
80 df-1nq 
 |-  1Q = <. 1o , 1o >.
81 79 80 eqtr4di 
 |-  ( w = 1o -> <. w , 1o >. = 1Q )
82 81 oveq1d 
 |-  ( w = 1o -> ( <. w , 1o >. .Q b ) = ( 1Q .Q b ) )
83 82 oveq2d 
 |-  ( w = 1o -> ( y +Q ( <. w , 1o >. .Q b ) ) = ( y +Q ( 1Q .Q b ) ) )
84 83 eleq1d 
 |-  ( w = 1o -> ( ( y +Q ( <. w , 1o >. .Q b ) ) e. A <-> ( y +Q ( 1Q .Q b ) ) e. A ) )
85 84 imbi2d 
 |-  ( w = 1o -> ( ( ( b e. Q. /\ A. x e. A ( x +Q b ) e. A /\ y e. A ) -> ( y +Q ( <. w , 1o >. .Q b ) ) e. A ) <-> ( ( b e. Q. /\ A. x e. A ( x +Q b ) e. A /\ y e. A ) -> ( y +Q ( 1Q .Q b ) ) e. A ) ) )
86 opeq1 
 |-  ( w = z -> <. w , 1o >. = <. z , 1o >. )
87 86 oveq1d 
 |-  ( w = z -> ( <. w , 1o >. .Q b ) = ( <. z , 1o >. .Q b ) )
88 87 oveq2d 
 |-  ( w = z -> ( y +Q ( <. w , 1o >. .Q b ) ) = ( y +Q ( <. z , 1o >. .Q b ) ) )
89 88 eleq1d 
 |-  ( w = z -> ( ( y +Q ( <. w , 1o >. .Q b ) ) e. A <-> ( y +Q ( <. z , 1o >. .Q b ) ) e. A ) )
90 89 imbi2d 
 |-  ( w = z -> ( ( ( b e. Q. /\ A. x e. A ( x +Q b ) e. A /\ y e. A ) -> ( y +Q ( <. w , 1o >. .Q b ) ) e. A ) <-> ( ( b e. Q. /\ A. x e. A ( x +Q b ) e. A /\ y e. A ) -> ( y +Q ( <. z , 1o >. .Q b ) ) e. A ) ) )
91 opeq1 
 |-  ( w = ( z +N 1o ) -> <. w , 1o >. = <. ( z +N 1o ) , 1o >. )
92 91 oveq1d 
 |-  ( w = ( z +N 1o ) -> ( <. w , 1o >. .Q b ) = ( <. ( z +N 1o ) , 1o >. .Q b ) )
93 92 oveq2d 
 |-  ( w = ( z +N 1o ) -> ( y +Q ( <. w , 1o >. .Q b ) ) = ( y +Q ( <. ( z +N 1o ) , 1o >. .Q b ) ) )
94 93 eleq1d 
 |-  ( w = ( z +N 1o ) -> ( ( y +Q ( <. w , 1o >. .Q b ) ) e. A <-> ( y +Q ( <. ( z +N 1o ) , 1o >. .Q b ) ) e. A ) )
95 94 imbi2d 
 |-  ( w = ( z +N 1o ) -> ( ( ( b e. Q. /\ A. x e. A ( x +Q b ) e. A /\ y e. A ) -> ( y +Q ( <. w , 1o >. .Q b ) ) e. A ) <-> ( ( b e. Q. /\ A. x e. A ( x +Q b ) e. A /\ y e. A ) -> ( y +Q ( <. ( z +N 1o ) , 1o >. .Q b ) ) e. A ) ) )
96 mulcomnq 
 |-  ( 1Q .Q b ) = ( b .Q 1Q )
97 mulidnq 
 |-  ( b e. Q. -> ( b .Q 1Q ) = b )
98 96 97 eqtrid 
 |-  ( b e. Q. -> ( 1Q .Q b ) = b )
99 oveq1 
 |-  ( x = y -> ( x +Q b ) = ( y +Q b ) )
100 99 eleq1d 
 |-  ( x = y -> ( ( x +Q b ) e. A <-> ( y +Q b ) e. A ) )
101 100 rspccva 
 |-  ( ( A. x e. A ( x +Q b ) e. A /\ y e. A ) -> ( y +Q b ) e. A )
102 oveq2 
 |-  ( ( 1Q .Q b ) = b -> ( y +Q ( 1Q .Q b ) ) = ( y +Q b ) )
103 102 eleq1d 
 |-  ( ( 1Q .Q b ) = b -> ( ( y +Q ( 1Q .Q b ) ) e. A <-> ( y +Q b ) e. A ) )
104 103 biimpar 
 |-  ( ( ( 1Q .Q b ) = b /\ ( y +Q b ) e. A ) -> ( y +Q ( 1Q .Q b ) ) e. A )
105 98 101 104 syl2an 
 |-  ( ( b e. Q. /\ ( A. x e. A ( x +Q b ) e. A /\ y e. A ) ) -> ( y +Q ( 1Q .Q b ) ) e. A )
106 105 3impb 
 |-  ( ( b e. Q. /\ A. x e. A ( x +Q b ) e. A /\ y e. A ) -> ( y +Q ( 1Q .Q b ) ) e. A )
107 3simpa 
 |-  ( ( b e. Q. /\ A. x e. A ( x +Q b ) e. A /\ y e. A ) -> ( b e. Q. /\ A. x e. A ( x +Q b ) e. A ) )
108 oveq1 
 |-  ( x = ( y +Q ( <. z , 1o >. .Q b ) ) -> ( x +Q b ) = ( ( y +Q ( <. z , 1o >. .Q b ) ) +Q b ) )
109 108 eleq1d 
 |-  ( x = ( y +Q ( <. z , 1o >. .Q b ) ) -> ( ( x +Q b ) e. A <-> ( ( y +Q ( <. z , 1o >. .Q b ) ) +Q b ) e. A ) )
110 109 rspccva 
 |-  ( ( A. x e. A ( x +Q b ) e. A /\ ( y +Q ( <. z , 1o >. .Q b ) ) e. A ) -> ( ( y +Q ( <. z , 1o >. .Q b ) ) +Q b ) e. A )
111 addassnq 
 |-  ( ( y +Q ( <. z , 1o >. .Q b ) ) +Q b ) = ( y +Q ( ( <. z , 1o >. .Q b ) +Q b ) )
112 opex 
 |-  <. z , 1o >. e. _V
113 1nq 
 |-  1Q e. Q.
114 113 elexi 
 |-  1Q e. _V
115 distrnq 
 |-  ( v .Q ( x +Q y ) ) = ( ( v .Q x ) +Q ( v .Q y ) )
116 112 114 43 46 115 caovdir 
 |-  ( ( <. z , 1o >. +Q 1Q ) .Q b ) = ( ( <. z , 1o >. .Q b ) +Q ( 1Q .Q b ) )
117 116 a1i 
 |-  ( ( z e. N. /\ b e. Q. ) -> ( ( <. z , 1o >. +Q 1Q ) .Q b ) = ( ( <. z , 1o >. .Q b ) +Q ( 1Q .Q b ) ) )
118 addpqnq 
 |-  ( ( <. z , 1o >. e. Q. /\ 1Q e. Q. ) -> ( <. z , 1o >. +Q 1Q ) = ( /Q ` ( <. z , 1o >. +pQ 1Q ) ) )
119 62 113 118 sylancl 
 |-  ( z e. N. -> ( <. z , 1o >. +Q 1Q ) = ( /Q ` ( <. z , 1o >. +pQ 1Q ) ) )
120 80 oveq2i 
 |-  ( <. z , 1o >. +pQ 1Q ) = ( <. z , 1o >. +pQ <. 1o , 1o >. )
121 1pi 
 |-  1o e. N.
122 addpipq 
 |-  ( ( ( z e. N. /\ 1o e. N. ) /\ ( 1o e. N. /\ 1o e. N. ) ) -> ( <. z , 1o >. +pQ <. 1o , 1o >. ) = <. ( ( z .N 1o ) +N ( 1o .N 1o ) ) , ( 1o .N 1o ) >. )
123 121 121 122 mpanr12 
 |-  ( ( z e. N. /\ 1o e. N. ) -> ( <. z , 1o >. +pQ <. 1o , 1o >. ) = <. ( ( z .N 1o ) +N ( 1o .N 1o ) ) , ( 1o .N 1o ) >. )
124 121 123 mpan2 
 |-  ( z e. N. -> ( <. z , 1o >. +pQ <. 1o , 1o >. ) = <. ( ( z .N 1o ) +N ( 1o .N 1o ) ) , ( 1o .N 1o ) >. )
125 120 124 eqtrid 
 |-  ( z e. N. -> ( <. z , 1o >. +pQ 1Q ) = <. ( ( z .N 1o ) +N ( 1o .N 1o ) ) , ( 1o .N 1o ) >. )
126 mulidpi 
 |-  ( z e. N. -> ( z .N 1o ) = z )
127 mulidpi 
 |-  ( 1o e. N. -> ( 1o .N 1o ) = 1o )
128 121 127 mp1i 
 |-  ( z e. N. -> ( 1o .N 1o ) = 1o )
129 126 128 oveq12d 
 |-  ( z e. N. -> ( ( z .N 1o ) +N ( 1o .N 1o ) ) = ( z +N 1o ) )
130 129 128 opeq12d 
 |-  ( z e. N. -> <. ( ( z .N 1o ) +N ( 1o .N 1o ) ) , ( 1o .N 1o ) >. = <. ( z +N 1o ) , 1o >. )
131 125 130 eqtrd 
 |-  ( z e. N. -> ( <. z , 1o >. +pQ 1Q ) = <. ( z +N 1o ) , 1o >. )
132 131 fveq2d 
 |-  ( z e. N. -> ( /Q ` ( <. z , 1o >. +pQ 1Q ) ) = ( /Q ` <. ( z +N 1o ) , 1o >. ) )
133 addclpi 
 |-  ( ( z e. N. /\ 1o e. N. ) -> ( z +N 1o ) e. N. )
134 121 133 mpan2 
 |-  ( z e. N. -> ( z +N 1o ) e. N. )
135 pinq 
 |-  ( ( z +N 1o ) e. N. -> <. ( z +N 1o ) , 1o >. e. Q. )
136 nqerid 
 |-  ( <. ( z +N 1o ) , 1o >. e. Q. -> ( /Q ` <. ( z +N 1o ) , 1o >. ) = <. ( z +N 1o ) , 1o >. )
137 134 135 136 3syl 
 |-  ( z e. N. -> ( /Q ` <. ( z +N 1o ) , 1o >. ) = <. ( z +N 1o ) , 1o >. )
138 119 132 137 3eqtrd 
 |-  ( z e. N. -> ( <. z , 1o >. +Q 1Q ) = <. ( z +N 1o ) , 1o >. )
139 138 adantr 
 |-  ( ( z e. N. /\ b e. Q. ) -> ( <. z , 1o >. +Q 1Q ) = <. ( z +N 1o ) , 1o >. )
140 139 oveq1d 
 |-  ( ( z e. N. /\ b e. Q. ) -> ( ( <. z , 1o >. +Q 1Q ) .Q b ) = ( <. ( z +N 1o ) , 1o >. .Q b ) )
141 98 adantl 
 |-  ( ( z e. N. /\ b e. Q. ) -> ( 1Q .Q b ) = b )
142 141 oveq2d 
 |-  ( ( z e. N. /\ b e. Q. ) -> ( ( <. z , 1o >. .Q b ) +Q ( 1Q .Q b ) ) = ( ( <. z , 1o >. .Q b ) +Q b ) )
143 117 140 142 3eqtr3rd 
 |-  ( ( z e. N. /\ b e. Q. ) -> ( ( <. z , 1o >. .Q b ) +Q b ) = ( <. ( z +N 1o ) , 1o >. .Q b ) )
144 143 oveq2d 
 |-  ( ( z e. N. /\ b e. Q. ) -> ( y +Q ( ( <. z , 1o >. .Q b ) +Q b ) ) = ( y +Q ( <. ( z +N 1o ) , 1o >. .Q b ) ) )
145 111 144 eqtrid 
 |-  ( ( z e. N. /\ b e. Q. ) -> ( ( y +Q ( <. z , 1o >. .Q b ) ) +Q b ) = ( y +Q ( <. ( z +N 1o ) , 1o >. .Q b ) ) )
146 145 eleq1d 
 |-  ( ( z e. N. /\ b e. Q. ) -> ( ( ( y +Q ( <. z , 1o >. .Q b ) ) +Q b ) e. A <-> ( y +Q ( <. ( z +N 1o ) , 1o >. .Q b ) ) e. A ) )
147 110 146 imbitrid 
 |-  ( ( z e. N. /\ b e. Q. ) -> ( ( A. x e. A ( x +Q b ) e. A /\ ( y +Q ( <. z , 1o >. .Q b ) ) e. A ) -> ( y +Q ( <. ( z +N 1o ) , 1o >. .Q b ) ) e. A ) )
148 147 expd 
 |-  ( ( z e. N. /\ b e. Q. ) -> ( A. x e. A ( x +Q b ) e. A -> ( ( y +Q ( <. z , 1o >. .Q b ) ) e. A -> ( y +Q ( <. ( z +N 1o ) , 1o >. .Q b ) ) e. A ) ) )
149 148 expimpd 
 |-  ( z e. N. -> ( ( b e. Q. /\ A. x e. A ( x +Q b ) e. A ) -> ( ( y +Q ( <. z , 1o >. .Q b ) ) e. A -> ( y +Q ( <. ( z +N 1o ) , 1o >. .Q b ) ) e. A ) ) )
150 107 149 syl5 
 |-  ( z e. N. -> ( ( b e. Q. /\ A. x e. A ( x +Q b ) e. A /\ y e. A ) -> ( ( y +Q ( <. z , 1o >. .Q b ) ) e. A -> ( y +Q ( <. ( z +N 1o ) , 1o >. .Q b ) ) e. A ) ) )
151 150 a2d 
 |-  ( z e. N. -> ( ( ( b e. Q. /\ A. x e. A ( x +Q b ) e. A /\ y e. A ) -> ( y +Q ( <. z , 1o >. .Q b ) ) e. A ) -> ( ( b e. Q. /\ A. x e. A ( x +Q b ) e. A /\ y e. A ) -> ( y +Q ( <. ( z +N 1o ) , 1o >. .Q b ) ) e. A ) ) )
152 85 90 95 90 106 151 indpi 
 |-  ( z e. N. -> ( ( b e. Q. /\ A. x e. A ( x +Q b ) e. A /\ y e. A ) -> ( y +Q ( <. z , 1o >. .Q b ) ) e. A ) )
153 152 imp 
 |-  ( ( z e. N. /\ ( b e. Q. /\ A. x e. A ( x +Q b ) e. A /\ y e. A ) ) -> ( y +Q ( <. z , 1o >. .Q b ) ) e. A )
154 61 39 78 67 153 syl13anc 
 |-  ( ( ( ( A e. P. /\ b e. Q. /\ A. x e. A ( x +Q b ) e. A ) /\ ( w e. Q. /\ y e. A ) ) /\ ( z e. N. /\ ( w .Q ( *Q ` b ) ) . ) ) -> ( y +Q ( <. z , 1o >. .Q b ) ) e. A )
155 prcdnq 
 |-  ( ( A e. P. /\ ( y +Q ( <. z , 1o >. .Q b ) ) e. A ) -> ( w . .Q b ) ) -> w e. A ) )
156 66 154 155 syl2anc 
 |-  ( ( ( ( A e. P. /\ b e. Q. /\ A. x e. A ( x +Q b ) e. A ) /\ ( w e. Q. /\ y e. A ) ) /\ ( z e. N. /\ ( w .Q ( *Q ` b ) ) . ) ) -> ( w . .Q b ) ) -> w e. A ) )
157 77 156 mpd 
 |-  ( ( ( ( A e. P. /\ b e. Q. /\ A. x e. A ( x +Q b ) e. A ) /\ ( w e. Q. /\ y e. A ) ) /\ ( z e. N. /\ ( w .Q ( *Q ` b ) ) . ) ) -> w e. A )
158 38 157 rexlimddv 
 |-  ( ( ( A e. P. /\ b e. Q. /\ A. x e. A ( x +Q b ) e. A ) /\ ( w e. Q. /\ y e. A ) ) -> w e. A )
159 158 expr 
 |-  ( ( ( A e. P. /\ b e. Q. /\ A. x e. A ( x +Q b ) e. A ) /\ w e. Q. ) -> ( y e. A -> w e. A ) )
160 159 exlimdv 
 |-  ( ( ( A e. P. /\ b e. Q. /\ A. x e. A ( x +Q b ) e. A ) /\ w e. Q. ) -> ( E. y y e. A -> w e. A ) )
161 30 160 mpd 
 |-  ( ( ( A e. P. /\ b e. Q. /\ A. x e. A ( x +Q b ) e. A ) /\ w e. Q. ) -> w e. A )
162 26 161 eqelssd 
 |-  ( ( A e. P. /\ b e. Q. /\ A. x e. A ( x +Q b ) e. A ) -> A = Q. )
163 162 3expia 
 |-  ( ( A e. P. /\ b e. Q. ) -> ( A. x e. A ( x +Q b ) e. A -> A = Q. ) )
164 25 163 mtod 
 |-  ( ( A e. P. /\ b e. Q. ) -> -. A. x e. A ( x +Q b ) e. A )
165 164 expcom 
 |-  ( b e. Q. -> ( A e. P. -> -. A. x e. A ( x +Q b ) e. A ) )
166 21 165 vtoclga 
 |-  ( B e. Q. -> ( A e. P. -> -. A. x e. A ( x +Q B ) e. A ) )
167 166 com12 
 |-  ( A e. P. -> ( B e. Q. -> -. A. x e. A ( x +Q B ) e. A ) )
168 5 16 167 3syld 
 |-  ( A e. P. -> ( A. x e. A ( x +Q B ) e. A -> -. A. x e. A ( x +Q B ) e. A ) )
169 168 pm2.01d 
 |-  ( A e. P. -> -. A. x e. A ( x +Q B ) e. A )
170 rexnal 
 |-  ( E. x e. A -. ( x +Q B ) e. A <-> -. A. x e. A ( x +Q B ) e. A )
171 169 170 sylibr 
 |-  ( A e. P. -> E. x e. A -. ( x +Q B ) e. A )