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