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