Metamath Proof Explorer


Theorem prlem936

Description: Lemma 9-3.6 of Gleason p. 124. (Contributed by NM, 26-Apr-1996) (Revised by Mario Carneiro, 12-Jun-2013) (New usage is discouraged.)

Ref Expression
Assertion prlem936
|- ( ( A e. P. /\ 1Q  E. x e. A -. ( x .Q B ) e. A )

Proof

Step Hyp Ref Expression
1 ltrelnq
 |-  
2 1 brel
 |-  ( 1Q  ( 1Q e. Q. /\ B e. Q. ) )
3 2 simprd
 |-  ( 1Q  B e. Q. )
4 3 adantl
 |-  ( ( A e. P. /\ 1Q  B e. Q. )
5 breq2
 |-  ( b = B -> ( 1Q  1Q 
6 5 anbi2d
 |-  ( b = B -> ( ( A e. P. /\ 1Q  ( A e. P. /\ 1Q 
7 oveq2
 |-  ( b = B -> ( x .Q b ) = ( x .Q B ) )
8 7 eleq1d
 |-  ( b = B -> ( ( x .Q b ) e. A <-> ( x .Q B ) e. A ) )
9 8 notbid
 |-  ( b = B -> ( -. ( x .Q b ) e. A <-> -. ( x .Q B ) e. A ) )
10 9 rexbidv
 |-  ( b = B -> ( E. x e. A -. ( x .Q b ) e. A <-> E. x e. A -. ( x .Q B ) e. A ) )
11 6 10 imbi12d
 |-  ( b = B -> ( ( ( A e. P. /\ 1Q  E. x e. A -. ( x .Q b ) e. A ) <-> ( ( A e. P. /\ 1Q  E. x e. A -. ( x .Q B ) e. A ) ) )
12 prn0
 |-  ( A e. P. -> A =/= (/) )
13 n0
 |-  ( A =/= (/) <-> E. y y e. A )
14 12 13 sylib
 |-  ( A e. P. -> E. y y e. A )
15 14 adantr
 |-  ( ( A e. P. /\ 1Q  E. y y e. A )
16 elprnq
 |-  ( ( A e. P. /\ y e. A ) -> y e. Q. )
17 16 ad2ant2r
 |-  ( ( ( A e. P. /\ 1Q  y e. Q. )
18 mulidnq
 |-  ( y e. Q. -> ( y .Q 1Q ) = y )
19 17 18 syl
 |-  ( ( ( A e. P. /\ 1Q  ( y .Q 1Q ) = y )
20 simplr
 |-  ( ( ( A e. P. /\ 1Q  1Q 
21 ltmnq
 |-  ( y e. Q. -> ( 1Q  ( y .Q 1Q ) 
22 21 biimpa
 |-  ( ( y e. Q. /\ 1Q  ( y .Q 1Q ) 
23 17 20 22 syl2anc
 |-  ( ( ( A e. P. /\ 1Q  ( y .Q 1Q ) 
24 19 23 eqbrtrrd
 |-  ( ( ( A e. P. /\ 1Q  y 
25 1 brel
 |-  ( 1Q  ( 1Q e. Q. /\ b e. Q. ) )
26 25 simprd
 |-  ( 1Q  b e. Q. )
27 26 ad2antlr
 |-  ( ( ( A e. P. /\ 1Q  b e. Q. )
28 mulclnq
 |-  ( ( y e. Q. /\ b e. Q. ) -> ( y .Q b ) e. Q. )
29 17 27 28 syl2anc
 |-  ( ( ( A e. P. /\ 1Q  ( y .Q b ) e. Q. )
30 ltexnq
 |-  ( ( y .Q b ) e. Q. -> ( y  E. z ( y +Q z ) = ( y .Q b ) ) )
31 29 30 syl
 |-  ( ( ( A e. P. /\ 1Q  ( y  E. z ( y +Q z ) = ( y .Q b ) ) )
32 24 31 mpbid
 |-  ( ( ( A e. P. /\ 1Q  E. z ( y +Q z ) = ( y .Q b ) )
33 simplll
 |-  ( ( ( ( A e. P. /\ 1Q  A e. P. )
34 vex
 |-  z e. _V
35 34 prlem934
 |-  ( A e. P. -> E. x e. A -. ( x +Q z ) e. A )
36 33 35 syl
 |-  ( ( ( ( A e. P. /\ 1Q  E. x e. A -. ( x +Q z ) e. A )
37 33 adantr
 |-  ( ( ( ( ( A e. P. /\ 1Q  A e. P. )
38 simprr
 |-  ( ( ( A e. P. /\ 1Q  ( y .Q b ) e. A )
39 eleq1
 |-  ( ( y +Q z ) = ( y .Q b ) -> ( ( y +Q z ) e. A <-> ( y .Q b ) e. A ) )
40 39 biimparc
 |-  ( ( ( y .Q b ) e. A /\ ( y +Q z ) = ( y .Q b ) ) -> ( y +Q z ) e. A )
41 38 40 sylan
 |-  ( ( ( ( A e. P. /\ 1Q  ( y +Q z ) e. A )
42 41 adantr
 |-  ( ( ( ( ( A e. P. /\ 1Q  ( y +Q z ) e. A )
43 elprnq
 |-  ( ( A e. P. /\ x e. A ) -> x e. Q. )
44 33 43 sylan
 |-  ( ( ( ( ( A e. P. /\ 1Q  x e. Q. )
45 elprnq
 |-  ( ( A e. P. /\ ( y +Q z ) e. A ) -> ( y +Q z ) e. Q. )
46 addnqf
 |-  +Q : ( Q. X. Q. ) --> Q.
47 46 fdmi
 |-  dom +Q = ( Q. X. Q. )
48 0nnq
 |-  -. (/) e. Q.
49 47 48 ndmovrcl
 |-  ( ( y +Q z ) e. Q. -> ( y e. Q. /\ z e. Q. ) )
50 49 simprd
 |-  ( ( y +Q z ) e. Q. -> z e. Q. )
51 45 50 syl
 |-  ( ( A e. P. /\ ( y +Q z ) e. A ) -> z e. Q. )
52 33 41 51 syl2anc
 |-  ( ( ( ( A e. P. /\ 1Q  z e. Q. )
53 52 adantr
 |-  ( ( ( ( ( A e. P. /\ 1Q  z e. Q. )
54 addclnq
 |-  ( ( x e. Q. /\ z e. Q. ) -> ( x +Q z ) e. Q. )
55 44 53 54 syl2anc
 |-  ( ( ( ( ( A e. P. /\ 1Q  ( x +Q z ) e. Q. )
56 prub
 |-  ( ( ( A e. P. /\ ( y +Q z ) e. A ) /\ ( x +Q z ) e. Q. ) -> ( -. ( x +Q z ) e. A -> ( y +Q z ) 
57 37 42 55 56 syl21anc
 |-  ( ( ( ( ( A e. P. /\ 1Q  ( -. ( x +Q z ) e. A -> ( y +Q z ) 
58 27 ad2antrr
 |-  ( ( ( ( ( A e. P. /\ 1Q  b e. Q. )
59 mulclnq
 |-  ( ( x e. Q. /\ b e. Q. ) -> ( x .Q b ) e. Q. )
60 44 58 59 syl2anc
 |-  ( ( ( ( ( A e. P. /\ 1Q  ( x .Q b ) e. Q. )
61 17 ad2antrr
 |-  ( ( ( ( ( A e. P. /\ 1Q  y e. Q. )
62 simplr
 |-  ( ( ( ( ( A e. P. /\ 1Q  ( y +Q z ) = ( y .Q b ) )
63 recclnq
 |-  ( y e. Q. -> ( *Q ` y ) e. Q. )
64 mulclnq
 |-  ( ( z e. Q. /\ ( *Q ` y ) e. Q. ) -> ( z .Q ( *Q ` y ) ) e. Q. )
65 63 64 sylan2
 |-  ( ( z e. Q. /\ y e. Q. ) -> ( z .Q ( *Q ` y ) ) e. Q. )
66 65 ancoms
 |-  ( ( y e. Q. /\ z e. Q. ) -> ( z .Q ( *Q ` y ) ) e. Q. )
67 ltmnq
 |-  ( ( z .Q ( *Q ` y ) ) e. Q. -> ( y  ( ( z .Q ( *Q ` y ) ) .Q y ) 
68 66 67 syl
 |-  ( ( y e. Q. /\ z e. Q. ) -> ( y  ( ( z .Q ( *Q ` y ) ) .Q y ) 
69 mulassnq
 |-  ( ( z .Q ( *Q ` y ) ) .Q y ) = ( z .Q ( ( *Q ` y ) .Q y ) )
70 mulcomnq
 |-  ( ( *Q ` y ) .Q y ) = ( y .Q ( *Q ` y ) )
71 70 oveq2i
 |-  ( z .Q ( ( *Q ` y ) .Q y ) ) = ( z .Q ( y .Q ( *Q ` y ) ) )
72 69 71 eqtri
 |-  ( ( z .Q ( *Q ` y ) ) .Q y ) = ( z .Q ( y .Q ( *Q ` y ) ) )
73 recidnq
 |-  ( y e. Q. -> ( y .Q ( *Q ` y ) ) = 1Q )
74 73 oveq2d
 |-  ( y e. Q. -> ( z .Q ( y .Q ( *Q ` y ) ) ) = ( z .Q 1Q ) )
75 mulidnq
 |-  ( z e. Q. -> ( z .Q 1Q ) = z )
76 74 75 sylan9eq
 |-  ( ( y e. Q. /\ z e. Q. ) -> ( z .Q ( y .Q ( *Q ` y ) ) ) = z )
77 72 76 eqtrid
 |-  ( ( y e. Q. /\ z e. Q. ) -> ( ( z .Q ( *Q ` y ) ) .Q y ) = z )
78 77 breq1d
 |-  ( ( y e. Q. /\ z e. Q. ) -> ( ( ( z .Q ( *Q ` y ) ) .Q y )  z 
79 68 78 bitrd
 |-  ( ( y e. Q. /\ z e. Q. ) -> ( y  z 
80 79 adantll
 |-  ( ( ( ( x .Q b ) e. Q. /\ y e. Q. ) /\ z e. Q. ) -> ( y  z 
81 mulnqf
 |-  .Q : ( Q. X. Q. ) --> Q.
82 81 fdmi
 |-  dom .Q = ( Q. X. Q. )
83 82 48 ndmovrcl
 |-  ( ( x .Q b ) e. Q. -> ( x e. Q. /\ b e. Q. ) )
84 83 simpld
 |-  ( ( x .Q b ) e. Q. -> x e. Q. )
85 ltanq
 |-  ( x e. Q. -> ( z  ( x +Q z ) 
86 84 85 syl
 |-  ( ( x .Q b ) e. Q. -> ( z  ( x +Q z ) 
87 86 adantr
 |-  ( ( ( x .Q b ) e. Q. /\ y e. Q. ) -> ( z  ( x +Q z ) 
88 vex
 |-  y e. _V
89 ovex
 |-  ( x .Q ( *Q ` y ) ) e. _V
90 mulcomnq
 |-  ( u .Q w ) = ( w .Q u )
91 distrnq
 |-  ( u .Q ( w +Q v ) ) = ( ( u .Q w ) +Q ( u .Q v ) )
92 88 34 89 90 91 caovdir
 |-  ( ( y +Q z ) .Q ( x .Q ( *Q ` y ) ) ) = ( ( y .Q ( x .Q ( *Q ` y ) ) ) +Q ( z .Q ( x .Q ( *Q ` y ) ) ) )
93 vex
 |-  x e. _V
94 fvex
 |-  ( *Q ` y ) e. _V
95 mulassnq
 |-  ( ( u .Q w ) .Q v ) = ( u .Q ( w .Q v ) )
96 88 93 94 90 95 caov12
 |-  ( y .Q ( x .Q ( *Q ` y ) ) ) = ( x .Q ( y .Q ( *Q ` y ) ) )
97 73 oveq2d
 |-  ( y e. Q. -> ( x .Q ( y .Q ( *Q ` y ) ) ) = ( x .Q 1Q ) )
98 mulidnq
 |-  ( x e. Q. -> ( x .Q 1Q ) = x )
99 84 98 syl
 |-  ( ( x .Q b ) e. Q. -> ( x .Q 1Q ) = x )
100 97 99 sylan9eqr
 |-  ( ( ( x .Q b ) e. Q. /\ y e. Q. ) -> ( x .Q ( y .Q ( *Q ` y ) ) ) = x )
101 96 100 eqtrid
 |-  ( ( ( x .Q b ) e. Q. /\ y e. Q. ) -> ( y .Q ( x .Q ( *Q ` y ) ) ) = x )
102 mulcomnq
 |-  ( x .Q ( *Q ` y ) ) = ( ( *Q ` y ) .Q x )
103 102 oveq2i
 |-  ( z .Q ( x .Q ( *Q ` y ) ) ) = ( z .Q ( ( *Q ` y ) .Q x ) )
104 mulassnq
 |-  ( ( z .Q ( *Q ` y ) ) .Q x ) = ( z .Q ( ( *Q ` y ) .Q x ) )
105 103 104 eqtr4i
 |-  ( z .Q ( x .Q ( *Q ` y ) ) ) = ( ( z .Q ( *Q ` y ) ) .Q x )
106 105 a1i
 |-  ( ( ( x .Q b ) e. Q. /\ y e. Q. ) -> ( z .Q ( x .Q ( *Q ` y ) ) ) = ( ( z .Q ( *Q ` y ) ) .Q x ) )
107 101 106 oveq12d
 |-  ( ( ( x .Q b ) e. Q. /\ y e. Q. ) -> ( ( y .Q ( x .Q ( *Q ` y ) ) ) +Q ( z .Q ( x .Q ( *Q ` y ) ) ) ) = ( x +Q ( ( z .Q ( *Q ` y ) ) .Q x ) ) )
108 92 107 eqtrid
 |-  ( ( ( x .Q b ) e. Q. /\ y e. Q. ) -> ( ( y +Q z ) .Q ( x .Q ( *Q ` y ) ) ) = ( x +Q ( ( z .Q ( *Q ` y ) ) .Q x ) ) )
109 108 breq2d
 |-  ( ( ( x .Q b ) e. Q. /\ y e. Q. ) -> ( ( x +Q z )  ( x +Q z ) 
110 87 109 bitr4d
 |-  ( ( ( x .Q b ) e. Q. /\ y e. Q. ) -> ( z  ( x +Q z ) 
111 110 adantr
 |-  ( ( ( ( x .Q b ) e. Q. /\ y e. Q. ) /\ z e. Q. ) -> ( z  ( x +Q z ) 
112 80 111 bitrd
 |-  ( ( ( ( x .Q b ) e. Q. /\ y e. Q. ) /\ z e. Q. ) -> ( y  ( x +Q z ) 
113 112 adantrr
 |-  ( ( ( ( x .Q b ) e. Q. /\ y e. Q. ) /\ ( z e. Q. /\ ( y +Q z ) = ( y .Q b ) ) ) -> ( y  ( x +Q z ) 
114 ltanq
 |-  ( z e. Q. -> ( y  ( z +Q y ) 
115 addcomnq
 |-  ( z +Q y ) = ( y +Q z )
116 addcomnq
 |-  ( z +Q x ) = ( x +Q z )
117 115 116 breq12i
 |-  ( ( z +Q y )  ( y +Q z ) 
118 114 117 bitrdi
 |-  ( z e. Q. -> ( y  ( y +Q z ) 
119 118 ad2antrl
 |-  ( ( ( ( x .Q b ) e. Q. /\ y e. Q. ) /\ ( z e. Q. /\ ( y +Q z ) = ( y .Q b ) ) ) -> ( y  ( y +Q z ) 
120 oveq1
 |-  ( ( y +Q z ) = ( y .Q b ) -> ( ( y +Q z ) .Q ( x .Q ( *Q ` y ) ) ) = ( ( y .Q b ) .Q ( x .Q ( *Q ` y ) ) ) )
121 vex
 |-  b e. _V
122 88 121 93 90 95 94 caov411
 |-  ( ( y .Q b ) .Q ( x .Q ( *Q ` y ) ) ) = ( ( x .Q b ) .Q ( y .Q ( *Q ` y ) ) )
123 73 oveq2d
 |-  ( y e. Q. -> ( ( x .Q b ) .Q ( y .Q ( *Q ` y ) ) ) = ( ( x .Q b ) .Q 1Q ) )
124 mulidnq
 |-  ( ( x .Q b ) e. Q. -> ( ( x .Q b ) .Q 1Q ) = ( x .Q b ) )
125 123 124 sylan9eqr
 |-  ( ( ( x .Q b ) e. Q. /\ y e. Q. ) -> ( ( x .Q b ) .Q ( y .Q ( *Q ` y ) ) ) = ( x .Q b ) )
126 122 125 eqtrid
 |-  ( ( ( x .Q b ) e. Q. /\ y e. Q. ) -> ( ( y .Q b ) .Q ( x .Q ( *Q ` y ) ) ) = ( x .Q b ) )
127 120 126 sylan9eqr
 |-  ( ( ( ( x .Q b ) e. Q. /\ y e. Q. ) /\ ( y +Q z ) = ( y .Q b ) ) -> ( ( y +Q z ) .Q ( x .Q ( *Q ` y ) ) ) = ( x .Q b ) )
128 127 breq2d
 |-  ( ( ( ( x .Q b ) e. Q. /\ y e. Q. ) /\ ( y +Q z ) = ( y .Q b ) ) -> ( ( x +Q z )  ( x +Q z ) 
129 128 adantrl
 |-  ( ( ( ( x .Q b ) e. Q. /\ y e. Q. ) /\ ( z e. Q. /\ ( y +Q z ) = ( y .Q b ) ) ) -> ( ( x +Q z )  ( x +Q z ) 
130 113 119 129 3bitr3d
 |-  ( ( ( ( x .Q b ) e. Q. /\ y e. Q. ) /\ ( z e. Q. /\ ( y +Q z ) = ( y .Q b ) ) ) -> ( ( y +Q z )  ( x +Q z ) 
131 60 61 53 62 130 syl22anc
 |-  ( ( ( ( ( A e. P. /\ 1Q  ( ( y +Q z )  ( x +Q z ) 
132 57 131 sylibd
 |-  ( ( ( ( ( A e. P. /\ 1Q  ( -. ( x +Q z ) e. A -> ( x +Q z ) 
133 prcdnq
 |-  ( ( A e. P. /\ ( x .Q b ) e. A ) -> ( ( x +Q z )  ( x +Q z ) e. A ) )
134 133 impancom
 |-  ( ( A e. P. /\ ( x +Q z )  ( ( x .Q b ) e. A -> ( x +Q z ) e. A ) )
135 134 con3d
 |-  ( ( A e. P. /\ ( x +Q z )  ( -. ( x +Q z ) e. A -> -. ( x .Q b ) e. A ) )
136 135 ex
 |-  ( A e. P. -> ( ( x +Q z )  ( -. ( x +Q z ) e. A -> -. ( x .Q b ) e. A ) ) )
137 136 com23
 |-  ( A e. P. -> ( -. ( x +Q z ) e. A -> ( ( x +Q z )  -. ( x .Q b ) e. A ) ) )
138 37 137 syl
 |-  ( ( ( ( ( A e. P. /\ 1Q  ( -. ( x +Q z ) e. A -> ( ( x +Q z )  -. ( x .Q b ) e. A ) ) )
139 132 138 mpdd
 |-  ( ( ( ( ( A e. P. /\ 1Q  ( -. ( x +Q z ) e. A -> -. ( x .Q b ) e. A ) )
140 139 reximdva
 |-  ( ( ( ( A e. P. /\ 1Q  ( E. x e. A -. ( x +Q z ) e. A -> E. x e. A -. ( x .Q b ) e. A ) )
141 36 140 mpd
 |-  ( ( ( ( A e. P. /\ 1Q  E. x e. A -. ( x .Q b ) e. A )
142 32 141 exlimddv
 |-  ( ( ( A e. P. /\ 1Q  E. x e. A -. ( x .Q b ) e. A )
143 142 expr
 |-  ( ( ( A e. P. /\ 1Q  ( ( y .Q b ) e. A -> E. x e. A -. ( x .Q b ) e. A ) )
144 oveq1
 |-  ( x = y -> ( x .Q b ) = ( y .Q b ) )
145 144 eleq1d
 |-  ( x = y -> ( ( x .Q b ) e. A <-> ( y .Q b ) e. A ) )
146 145 notbid
 |-  ( x = y -> ( -. ( x .Q b ) e. A <-> -. ( y .Q b ) e. A ) )
147 146 rspcev
 |-  ( ( y e. A /\ -. ( y .Q b ) e. A ) -> E. x e. A -. ( x .Q b ) e. A )
148 147 ex
 |-  ( y e. A -> ( -. ( y .Q b ) e. A -> E. x e. A -. ( x .Q b ) e. A ) )
149 148 adantl
 |-  ( ( ( A e. P. /\ 1Q  ( -. ( y .Q b ) e. A -> E. x e. A -. ( x .Q b ) e. A ) )
150 143 149 pm2.61d
 |-  ( ( ( A e. P. /\ 1Q  E. x e. A -. ( x .Q b ) e. A )
151 15 150 exlimddv
 |-  ( ( A e. P. /\ 1Q  E. x e. A -. ( x .Q b ) e. A )
152 11 151 vtoclg
 |-  ( B e. Q. -> ( ( A e. P. /\ 1Q  E. x e. A -. ( x .Q B ) e. A ) )
153 4 152 mpcom
 |-  ( ( A e. P. /\ 1Q  E. x e. A -. ( x .Q B ) e. A )