Step | Hyp | Ref
| Expression |
1 | | ssid 2958 |
. . . . . 6
⊢
(1st ‘1P) ⊆
(1st ‘1P) |
2 | | rexss 3001 |
. . . . . 6
⊢
((1st ‘1P) ⊆
(1st ‘1P) → (∃g ∈ (1st
‘1P)x =
(f ·Q
g) ↔ ∃g ∈ (1st
‘1P)(g ∈ (1st
‘1P) ∧ x = (f
·Q g)))) |
3 | 1, 2 | ax-mp 7 |
. . . . 5
⊢ (∃g ∈ (1st
‘1P)x =
(f ·Q
g) ↔ ∃g ∈ (1st
‘1P)(g ∈ (1st
‘1P) ∧ x = (f
·Q g))) |
4 | | r19.42v 2461 |
. . . . . 6
⊢ (∃g ∈ (1st
‘1P)(x
<Q f ∧ x = (f ·Q g)) ↔ (x
<Q f ∧ ∃g ∈
(1st ‘1P)x = (f
·Q g))) |
5 | | 1pr 6535 |
. . . . . . . . . . 11
⊢
1P ∈
P |
6 | | prop 6458 |
. . . . . . . . . . . 12
⊢
(1P ∈
P → 〈(1st
‘1P), (2nd
‘1P)〉 ∈
P) |
7 | | elprnql 6464 |
. . . . . . . . . . . 12
⊢
((〈(1st ‘1P),
(2nd ‘1P)〉 ∈ P ∧ g ∈ (1st
‘1P)) → g ∈
Q) |
8 | 6, 7 | sylan 267 |
. . . . . . . . . . 11
⊢
((1P ∈
P ∧ g ∈
(1st ‘1P)) → g ∈
Q) |
9 | 5, 8 | mpan 400 |
. . . . . . . . . 10
⊢ (g ∈
(1st ‘1P) → g ∈
Q) |
10 | | prop 6458 |
. . . . . . . . . . . 12
⊢ (A ∈
P → 〈(1st ‘A), (2nd ‘A)〉 ∈
P) |
11 | | elprnql 6464 |
. . . . . . . . . . . 12
⊢
((〈(1st ‘A),
(2nd ‘A)〉 ∈ P ∧ f ∈ (1st ‘A)) → f
∈ Q) |
12 | 10, 11 | sylan 267 |
. . . . . . . . . . 11
⊢
((A ∈ P ∧ f ∈ (1st ‘A)) → f
∈ Q) |
13 | | breq1 3758 |
. . . . . . . . . . . . 13
⊢ (x = (f
·Q g)
→ (x <Q
f ↔ (f ·Q g) <Q f)) |
14 | 13 | 3ad2ant3 926 |
. . . . . . . . . . . 12
⊢
((f ∈ Q ∧ g ∈ Q ∧ x = (f ·Q g)) → (x
<Q f ↔
(f ·Q
g) <Q f)) |
15 | | 1prl 6536 |
. . . . . . . . . . . . . . 15
⊢
(1st ‘1P) = {g ∣ g
<Q 1Q} |
16 | 15 | abeq2i 2145 |
. . . . . . . . . . . . . 14
⊢ (g ∈
(1st ‘1P) ↔ g <Q
1Q) |
17 | | 1nq 6350 |
. . . . . . . . . . . . . . . . 17
⊢
1Q ∈
Q |
18 | | ltmnqg 6385 |
. . . . . . . . . . . . . . . . 17
⊢
((g ∈ Q ∧ 1Q ∈ Q ∧ f ∈ Q) → (g <Q
1Q ↔ (f
·Q g)
<Q (f
·Q
1Q))) |
19 | 17, 18 | mp3an2 1219 |
. . . . . . . . . . . . . . . 16
⊢
((g ∈ Q ∧ f ∈ Q) → (g <Q
1Q ↔ (f
·Q g)
<Q (f
·Q
1Q))) |
20 | 19 | ancoms 255 |
. . . . . . . . . . . . . . 15
⊢
((f ∈ Q ∧ g ∈ Q) → (g <Q
1Q ↔ (f
·Q g)
<Q (f
·Q
1Q))) |
21 | | mulidnq 6373 |
. . . . . . . . . . . . . . . . 17
⊢ (f ∈
Q → (f
·Q 1Q) = f) |
22 | 21 | breq2d 3767 |
. . . . . . . . . . . . . . . 16
⊢ (f ∈
Q → ((f
·Q g)
<Q (f
·Q 1Q) ↔
(f ·Q
g) <Q f)) |
23 | 22 | adantr 261 |
. . . . . . . . . . . . . . 15
⊢
((f ∈ Q ∧ g ∈ Q) → ((f ·Q g) <Q (f ·Q
1Q) ↔ (f
·Q g)
<Q f)) |
24 | 20, 23 | bitrd 177 |
. . . . . . . . . . . . . 14
⊢
((f ∈ Q ∧ g ∈ Q) → (g <Q
1Q ↔ (f
·Q g)
<Q f)) |
25 | 16, 24 | syl5rbb 182 |
. . . . . . . . . . . . 13
⊢
((f ∈ Q ∧ g ∈ Q) → ((f ·Q g) <Q f ↔ g ∈ (1st
‘1P))) |
26 | 25 | 3adant3 923 |
. . . . . . . . . . . 12
⊢
((f ∈ Q ∧ g ∈ Q ∧ x = (f ·Q g)) → ((f
·Q g)
<Q f ↔
g ∈
(1st ‘1P))) |
27 | 14, 26 | bitrd 177 |
. . . . . . . . . . 11
⊢
((f ∈ Q ∧ g ∈ Q ∧ x = (f ·Q g)) → (x
<Q f ↔
g ∈
(1st ‘1P))) |
28 | 12, 27 | syl3an1 1167 |
. . . . . . . . . 10
⊢
(((A ∈ P ∧ f ∈ (1st ‘A)) ∧ g ∈
Q ∧ x = (f
·Q g))
→ (x <Q
f ↔ g ∈
(1st ‘1P))) |
29 | 9, 28 | syl3an2 1168 |
. . . . . . . . 9
⊢
(((A ∈ P ∧ f ∈ (1st ‘A)) ∧ g ∈
(1st ‘1P) ∧ x = (f ·Q g)) → (x
<Q f ↔
g ∈
(1st ‘1P))) |
30 | 29 | 3expia 1105 |
. . . . . . . 8
⊢
(((A ∈ P ∧ f ∈ (1st ‘A)) ∧ g ∈
(1st ‘1P)) → (x = (f
·Q g)
→ (x <Q
f ↔ g ∈
(1st ‘1P)))) |
31 | 30 | pm5.32rd 424 |
. . . . . . 7
⊢
(((A ∈ P ∧ f ∈ (1st ‘A)) ∧ g ∈
(1st ‘1P)) → ((x <Q f ∧ x = (f
·Q g))
↔ (g ∈ (1st
‘1P) ∧ x = (f
·Q g)))) |
32 | 31 | rexbidva 2317 |
. . . . . 6
⊢
((A ∈ P ∧ f ∈ (1st ‘A)) → (∃g ∈ (1st
‘1P)(x
<Q f ∧ x = (f ·Q g)) ↔ ∃g ∈ (1st
‘1P)(g ∈ (1st
‘1P) ∧ x = (f
·Q g)))) |
33 | 4, 32 | syl5rbbr 184 |
. . . . 5
⊢
((A ∈ P ∧ f ∈ (1st ‘A)) → (∃g ∈ (1st
‘1P)(g ∈ (1st
‘1P) ∧ x = (f
·Q g))
↔ (x <Q
f ∧ ∃g ∈ (1st
‘1P)x =
(f ·Q
g)))) |
34 | 3, 33 | syl5bb 181 |
. . . 4
⊢
((A ∈ P ∧ f ∈ (1st ‘A)) → (∃g ∈ (1st
‘1P)x =
(f ·Q
g) ↔ (x <Q f ∧ ∃g ∈ (1st
‘1P)x =
(f ·Q
g)))) |
35 | 34 | rexbidva 2317 |
. . 3
⊢ (A ∈
P → (∃f ∈
(1st ‘A)∃g ∈ (1st
‘1P)x =
(f ·Q
g) ↔ ∃f ∈ (1st ‘A)(x
<Q f ∧ ∃g ∈
(1st ‘1P)x = (f
·Q g)))) |
36 | | df-imp 6452 |
. . . . 5
⊢
·P = (y
∈ P, z ∈
P ↦ 〈{w ∈ Q ∣ ∃u ∈ Q ∃v ∈ Q (u ∈
(1st ‘y) ∧ v ∈ (1st ‘z) ∧ w = (u
·Q v))},
{w ∈
Q ∣ ∃u ∈
Q ∃v ∈
Q (u ∈ (2nd ‘y) ∧ v ∈
(2nd ‘z) ∧ w = (u ·Q v))}〉) |
37 | | mulclnq 6360 |
. . . . 5
⊢
((u ∈ Q ∧ v ∈ Q) → (u ·Q v) ∈
Q) |
38 | 36, 37 | genpelvl 6495 |
. . . 4
⊢
((A ∈ P ∧ 1P ∈ P) → (x ∈
(1st ‘(A
·P 1P)) ↔ ∃f ∈ (1st ‘A)∃g ∈
(1st ‘1P)x = (f
·Q g))) |
39 | 5, 38 | mpan2 401 |
. . 3
⊢ (A ∈
P → (x ∈ (1st ‘(A ·P
1P)) ↔ ∃f ∈ (1st ‘A)∃g ∈
(1st ‘1P)x = (f
·Q g))) |
40 | | prnmaxl 6471 |
. . . . . . 7
⊢
((〈(1st ‘A),
(2nd ‘A)〉 ∈ P ∧ x ∈ (1st ‘A)) → ∃f ∈ (1st ‘A)x
<Q f) |
41 | 10, 40 | sylan 267 |
. . . . . 6
⊢
((A ∈ P ∧ x ∈ (1st ‘A)) → ∃f ∈ (1st ‘A)x
<Q f) |
42 | | ltrelnq 6349 |
. . . . . . . . . . . . 13
⊢
<Q ⊆ (Q ×
Q) |
43 | 42 | brel 4335 |
. . . . . . . . . . . 12
⊢ (x <Q f → (x
∈ Q ∧ f ∈ Q)) |
44 | | ltmnqg 6385 |
. . . . . . . . . . . . . . . 16
⊢
((y ∈ Q ∧ z ∈ Q ∧ w ∈ Q) → (y <Q z ↔ (w
·Q y)
<Q (w
·Q z))) |
45 | 44 | adantl 262 |
. . . . . . . . . . . . . . 15
⊢
(((x ∈ Q ∧ f ∈ Q) ∧ (y ∈ Q ∧ z ∈ Q ∧ w ∈ Q)) → (y <Q z ↔ (w
·Q y)
<Q (w
·Q z))) |
46 | | simpl 102 |
. . . . . . . . . . . . . . 15
⊢
((x ∈ Q ∧ f ∈ Q) → x ∈
Q) |
47 | | simpr 103 |
. . . . . . . . . . . . . . 15
⊢
((x ∈ Q ∧ f ∈ Q) → f ∈
Q) |
48 | | recclnq 6376 |
. . . . . . . . . . . . . . . 16
⊢ (f ∈
Q → (*Q‘f) ∈
Q) |
49 | 48 | adantl 262 |
. . . . . . . . . . . . . . 15
⊢
((x ∈ Q ∧ f ∈ Q) →
(*Q‘f) ∈ Q) |
50 | | mulcomnqg 6367 |
. . . . . . . . . . . . . . . 16
⊢
((y ∈ Q ∧ z ∈ Q) → (y ·Q z) = (z
·Q y)) |
51 | 50 | adantl 262 |
. . . . . . . . . . . . . . 15
⊢
(((x ∈ Q ∧ f ∈ Q) ∧ (y ∈ Q ∧ z ∈ Q)) → (y ·Q z) = (z
·Q y)) |
52 | 45, 46, 47, 49, 51 | caovord2d 5612 |
. . . . . . . . . . . . . 14
⊢
((x ∈ Q ∧ f ∈ Q) → (x <Q f ↔ (x
·Q (*Q‘f)) <Q (f ·Q
(*Q‘f)))) |
53 | | recidnq 6377 |
. . . . . . . . . . . . . . . 16
⊢ (f ∈
Q → (f
·Q (*Q‘f)) = 1Q) |
54 | 53 | breq2d 3767 |
. . . . . . . . . . . . . . 15
⊢ (f ∈
Q → ((x
·Q (*Q‘f)) <Q (f ·Q
(*Q‘f))
↔ (x
·Q (*Q‘f)) <Q
1Q)) |
55 | 54 | adantl 262 |
. . . . . . . . . . . . . 14
⊢
((x ∈ Q ∧ f ∈ Q) → ((x ·Q
(*Q‘f))
<Q (f
·Q (*Q‘f)) ↔ (x
·Q (*Q‘f)) <Q
1Q)) |
56 | 52, 55 | bitrd 177 |
. . . . . . . . . . . . 13
⊢
((x ∈ Q ∧ f ∈ Q) → (x <Q f ↔ (x
·Q (*Q‘f)) <Q
1Q)) |
57 | 56 | biimpd 132 |
. . . . . . . . . . . 12
⊢
((x ∈ Q ∧ f ∈ Q) → (x <Q f → (x
·Q (*Q‘f)) <Q
1Q)) |
58 | 43, 57 | mpcom 32 |
. . . . . . . . . . 11
⊢ (x <Q f → (x
·Q (*Q‘f)) <Q
1Q) |
59 | | mulclnq 6360 |
. . . . . . . . . . . . . 14
⊢
((x ∈ Q ∧ (*Q‘f) ∈
Q) → (x
·Q (*Q‘f)) ∈
Q) |
60 | 48, 59 | sylan2 270 |
. . . . . . . . . . . . 13
⊢
((x ∈ Q ∧ f ∈ Q) → (x ·Q
(*Q‘f))
∈ Q) |
61 | 43, 60 | syl 14 |
. . . . . . . . . . . 12
⊢ (x <Q f → (x
·Q (*Q‘f)) ∈
Q) |
62 | | breq1 3758 |
. . . . . . . . . . . . 13
⊢ (g = (x
·Q (*Q‘f)) → (g
<Q 1Q ↔ (x ·Q
(*Q‘f))
<Q 1Q)) |
63 | 62, 15 | elab2g 2683 |
. . . . . . . . . . . 12
⊢
((x
·Q (*Q‘f)) ∈
Q → ((x
·Q (*Q‘f)) ∈
(1st ‘1P) ↔ (x ·Q
(*Q‘f))
<Q 1Q)) |
64 | 61, 63 | syl 14 |
. . . . . . . . . . 11
⊢ (x <Q f → ((x
·Q (*Q‘f)) ∈
(1st ‘1P) ↔ (x ·Q
(*Q‘f))
<Q 1Q)) |
65 | 58, 64 | mpbird 156 |
. . . . . . . . . 10
⊢ (x <Q f → (x
·Q (*Q‘f)) ∈
(1st ‘1P)) |
66 | | mulassnqg 6368 |
. . . . . . . . . . . . . 14
⊢
((y ∈ Q ∧ z ∈ Q ∧ w ∈ Q) → ((y ·Q z) ·Q w) = (y
·Q (z
·Q w))) |
67 | 66 | adantl 262 |
. . . . . . . . . . . . 13
⊢
(((x ∈ Q ∧ f ∈ Q) ∧ (y ∈ Q ∧ z ∈ Q ∧ w ∈ Q)) → ((y ·Q z) ·Q w) = (y
·Q (z
·Q w))) |
68 | 47, 46, 49, 51, 67 | caov12d 5624 |
. . . . . . . . . . . 12
⊢
((x ∈ Q ∧ f ∈ Q) → (f ·Q (x ·Q
(*Q‘f))) =
(x ·Q
(f ·Q
(*Q‘f)))) |
69 | 53 | oveq2d 5471 |
. . . . . . . . . . . . 13
⊢ (f ∈
Q → (x
·Q (f
·Q (*Q‘f))) = (x
·Q
1Q)) |
70 | 69 | adantl 262 |
. . . . . . . . . . . 12
⊢
((x ∈ Q ∧ f ∈ Q) → (x ·Q (f ·Q
(*Q‘f))) =
(x ·Q
1Q)) |
71 | | mulidnq 6373 |
. . . . . . . . . . . . 13
⊢ (x ∈
Q → (x
·Q 1Q) = x) |
72 | 71 | adantr 261 |
. . . . . . . . . . . 12
⊢
((x ∈ Q ∧ f ∈ Q) → (x ·Q
1Q) = x) |
73 | 68, 70, 72 | 3eqtrrd 2074 |
. . . . . . . . . . 11
⊢
((x ∈ Q ∧ f ∈ Q) → x = (f
·Q (x
·Q (*Q‘f)))) |
74 | 43, 73 | syl 14 |
. . . . . . . . . 10
⊢ (x <Q f → x =
(f ·Q
(x ·Q
(*Q‘f)))) |
75 | | oveq2 5463 |
. . . . . . . . . . . 12
⊢ (g = (x
·Q (*Q‘f)) → (f
·Q g) =
(f ·Q
(x ·Q
(*Q‘f)))) |
76 | 75 | eqeq2d 2048 |
. . . . . . . . . . 11
⊢ (g = (x
·Q (*Q‘f)) → (x =
(f ·Q
g) ↔ x = (f
·Q (x
·Q (*Q‘f))))) |
77 | 76 | rspcev 2650 |
. . . . . . . . . 10
⊢
(((x
·Q (*Q‘f)) ∈
(1st ‘1P) ∧ x = (f ·Q (x ·Q
(*Q‘f))))
→ ∃g ∈
(1st ‘1P)x = (f
·Q g)) |
78 | 65, 74, 77 | syl2anc 391 |
. . . . . . . . 9
⊢ (x <Q f → ∃g ∈ (1st
‘1P)x =
(f ·Q
g)) |
79 | 78 | a1i 9 |
. . . . . . . 8
⊢ (f ∈
(1st ‘A) → (x <Q f → ∃g ∈ (1st
‘1P)x =
(f ·Q
g))) |
80 | 79 | ancld 308 |
. . . . . . 7
⊢ (f ∈
(1st ‘A) → (x <Q f → (x
<Q f ∧ ∃g ∈
(1st ‘1P)x = (f
·Q g)))) |
81 | 80 | reximia 2408 |
. . . . . 6
⊢ (∃f ∈ (1st ‘A)x
<Q f →
∃f ∈ (1st ‘A)(x
<Q f ∧ ∃g ∈
(1st ‘1P)x = (f
·Q g))) |
82 | 41, 81 | syl 14 |
. . . . 5
⊢
((A ∈ P ∧ x ∈ (1st ‘A)) → ∃f ∈ (1st ‘A)(x
<Q f ∧ ∃g ∈
(1st ‘1P)x = (f
·Q g))) |
83 | 82 | ex 108 |
. . . 4
⊢ (A ∈
P → (x ∈ (1st ‘A) → ∃f ∈ (1st ‘A)(x
<Q f ∧ ∃g ∈
(1st ‘1P)x = (f
·Q g)))) |
84 | | prcdnql 6467 |
. . . . . . 7
⊢
((〈(1st ‘A),
(2nd ‘A)〉 ∈ P ∧ f ∈ (1st ‘A)) → (x
<Q f →
x ∈
(1st ‘A))) |
85 | 10, 84 | sylan 267 |
. . . . . 6
⊢
((A ∈ P ∧ f ∈ (1st ‘A)) → (x
<Q f →
x ∈
(1st ‘A))) |
86 | 85 | adantrd 264 |
. . . . 5
⊢
((A ∈ P ∧ f ∈ (1st ‘A)) → ((x
<Q f ∧ ∃g ∈
(1st ‘1P)x = (f
·Q g))
→ x ∈ (1st ‘A))) |
87 | 86 | rexlimdva 2427 |
. . . 4
⊢ (A ∈
P → (∃f ∈
(1st ‘A)(x <Q f ∧ ∃g ∈ (1st
‘1P)x =
(f ·Q
g)) → x ∈
(1st ‘A))) |
88 | 83, 87 | impbid 120 |
. . 3
⊢ (A ∈
P → (x ∈ (1st ‘A) ↔ ∃f ∈ (1st ‘A)(x
<Q f ∧ ∃g ∈
(1st ‘1P)x = (f
·Q g)))) |
89 | 35, 39, 88 | 3bitr4d 209 |
. 2
⊢ (A ∈
P → (x ∈ (1st ‘(A ·P
1P)) ↔ x
∈ (1st ‘A))) |
90 | 89 | eqrdv 2035 |
1
⊢ (A ∈
P → (1st ‘(A ·P
1P)) = (1st ‘A)) |