Step | Hyp | Ref
| Expression |
1 | | df-rex 3075 |
. . . . 5
โข
(โ๐ โ
1P ๐ฅ = (๐ ยทQ ๐) โ โ๐(๐ โ 1P โง
๐ฅ = (๐ ยทQ ๐))) |
2 | | elprnq 10934 |
. . . . . . . . . 10
โข ((๐ด โ P โง
๐ โ ๐ด) โ ๐ โ Q) |
3 | | breq1 5113 |
. . . . . . . . . . 11
โข (๐ฅ = (๐ ยทQ ๐) โ (๐ฅ <Q ๐ โ (๐ ยทQ ๐) <Q
๐)) |
4 | | df-1p 10925 |
. . . . . . . . . . . . 13
โข
1P = {๐ โฃ ๐ <Q
1Q} |
5 | 4 | eqabi 2882 |
. . . . . . . . . . . 12
โข (๐ โ
1P โ ๐ <Q
1Q) |
6 | | ltmnq 10915 |
. . . . . . . . . . . . 13
โข (๐ โ Q โ
(๐
<Q 1Q โ (๐
ยทQ ๐) <Q (๐
ยทQ
1Q))) |
7 | | mulidnq 10906 |
. . . . . . . . . . . . . 14
โข (๐ โ Q โ
(๐
ยทQ 1Q) = ๐) |
8 | 7 | breq2d 5122 |
. . . . . . . . . . . . 13
โข (๐ โ Q โ
((๐
ยทQ ๐) <Q (๐
ยทQ 1Q) โ (๐
ยทQ ๐) <Q ๐)) |
9 | 6, 8 | bitrd 279 |
. . . . . . . . . . . 12
โข (๐ โ Q โ
(๐
<Q 1Q โ (๐
ยทQ ๐) <Q ๐)) |
10 | 5, 9 | bitr2id 284 |
. . . . . . . . . . 11
โข (๐ โ Q โ
((๐
ยทQ ๐) <Q ๐ โ ๐ โ
1P)) |
11 | 3, 10 | sylan9bbr 512 |
. . . . . . . . . 10
โข ((๐ โ Q โง
๐ฅ = (๐ ยทQ ๐)) โ (๐ฅ <Q ๐ โ ๐ โ
1P)) |
12 | 2, 11 | sylan 581 |
. . . . . . . . 9
โข (((๐ด โ P โง
๐ โ ๐ด) โง ๐ฅ = (๐ ยทQ ๐)) โ (๐ฅ <Q ๐ โ ๐ โ
1P)) |
13 | 12 | ex 414 |
. . . . . . . 8
โข ((๐ด โ P โง
๐ โ ๐ด) โ (๐ฅ = (๐ ยทQ ๐) โ (๐ฅ <Q ๐ โ ๐ โ
1P))) |
14 | 13 | pm5.32rd 579 |
. . . . . . 7
โข ((๐ด โ P โง
๐ โ ๐ด) โ ((๐ฅ <Q ๐ โง ๐ฅ = (๐ ยทQ ๐)) โ (๐ โ 1P โง
๐ฅ = (๐ ยทQ ๐)))) |
15 | 14 | exbidv 1925 |
. . . . . 6
โข ((๐ด โ P โง
๐ โ ๐ด) โ (โ๐(๐ฅ <Q ๐ โง ๐ฅ = (๐ ยทQ ๐)) โ โ๐(๐ โ 1P โง
๐ฅ = (๐ ยทQ ๐)))) |
16 | | 19.42v 1958 |
. . . . . 6
โข
(โ๐(๐ฅ <Q
๐ โง ๐ฅ = (๐ ยทQ ๐)) โ (๐ฅ <Q ๐ โง โ๐ ๐ฅ = (๐ ยทQ ๐))) |
17 | 15, 16 | bitr3di 286 |
. . . . 5
โข ((๐ด โ P โง
๐ โ ๐ด) โ (โ๐(๐ โ 1P โง
๐ฅ = (๐ ยทQ ๐)) โ (๐ฅ <Q ๐ โง โ๐ ๐ฅ = (๐ ยทQ ๐)))) |
18 | 1, 17 | bitrid 283 |
. . . 4
โข ((๐ด โ P โง
๐ โ ๐ด) โ (โ๐ โ 1P ๐ฅ = (๐ ยทQ ๐) โ (๐ฅ <Q ๐ โง โ๐ ๐ฅ = (๐ ยทQ ๐)))) |
19 | 18 | rexbidva 3174 |
. . 3
โข (๐ด โ P โ
(โ๐ โ ๐ด โ๐ โ 1P ๐ฅ = (๐ ยทQ ๐) โ โ๐ โ ๐ด (๐ฅ <Q ๐ โง โ๐ ๐ฅ = (๐ ยทQ ๐)))) |
20 | | 1pr 10958 |
. . . 4
โข
1P โ P |
21 | | df-mp 10927 |
. . . . 5
โข
ยทP = (๐ฆ โ P, ๐ง โ P โฆ {๐ค โฃ โ๐ข โ ๐ฆ โ๐ฃ โ ๐ง ๐ค = (๐ข ยทQ ๐ฃ)}) |
22 | | mulclnq 10890 |
. . . . 5
โข ((๐ข โ Q โง
๐ฃ โ Q)
โ (๐ข
ยทQ ๐ฃ) โ Q) |
23 | 21, 22 | genpelv 10943 |
. . . 4
โข ((๐ด โ P โง
1P โ P) โ (๐ฅ โ (๐ด ยทP
1P) โ โ๐ โ ๐ด โ๐ โ 1P ๐ฅ = (๐ ยทQ ๐))) |
24 | 20, 23 | mpan2 690 |
. . 3
โข (๐ด โ P โ
(๐ฅ โ (๐ด
ยทP 1P) โ
โ๐ โ ๐ด โ๐ โ 1P ๐ฅ = (๐ ยทQ ๐))) |
25 | | prnmax 10938 |
. . . . . 6
โข ((๐ด โ P โง
๐ฅ โ ๐ด) โ โ๐ โ ๐ด ๐ฅ <Q ๐) |
26 | | ltrelnq 10869 |
. . . . . . . . . . 11
โข
<Q โ (Q ร
Q) |
27 | 26 | brel 5702 |
. . . . . . . . . 10
โข (๐ฅ <Q
๐ โ (๐ฅ โ Q โง
๐ โ
Q)) |
28 | | vex 3452 |
. . . . . . . . . . . . . 14
โข ๐ โ V |
29 | | vex 3452 |
. . . . . . . . . . . . . 14
โข ๐ฅ โ V |
30 | | fvex 6860 |
. . . . . . . . . . . . . 14
โข
(*Qโ๐) โ V |
31 | | mulcomnq 10896 |
. . . . . . . . . . . . . 14
โข (๐ฆ
ยทQ ๐ง) = (๐ง ยทQ ๐ฆ) |
32 | | mulassnq 10902 |
. . . . . . . . . . . . . 14
โข ((๐ฆ
ยทQ ๐ง) ยทQ ๐ค) = (๐ฆ ยทQ (๐ง
ยทQ ๐ค)) |
33 | 28, 29, 30, 31, 32 | caov12 7587 |
. . . . . . . . . . . . 13
โข (๐
ยทQ (๐ฅ ยทQ
(*Qโ๐))) = (๐ฅ ยทQ (๐
ยทQ (*Qโ๐))) |
34 | | recidnq 10908 |
. . . . . . . . . . . . . 14
โข (๐ โ Q โ
(๐
ยทQ (*Qโ๐)) =
1Q) |
35 | 34 | oveq2d 7378 |
. . . . . . . . . . . . 13
โข (๐ โ Q โ
(๐ฅ
ยทQ (๐ ยทQ
(*Qโ๐))) = (๐ฅ ยทQ
1Q)) |
36 | 33, 35 | eqtrid 2789 |
. . . . . . . . . . . 12
โข (๐ โ Q โ
(๐
ยทQ (๐ฅ ยทQ
(*Qโ๐))) = (๐ฅ ยทQ
1Q)) |
37 | | mulidnq 10906 |
. . . . . . . . . . . 12
โข (๐ฅ โ Q โ
(๐ฅ
ยทQ 1Q) = ๐ฅ) |
38 | 36, 37 | sylan9eqr 2799 |
. . . . . . . . . . 11
โข ((๐ฅ โ Q โง
๐ โ Q)
โ (๐
ยทQ (๐ฅ ยทQ
(*Qโ๐))) = ๐ฅ) |
39 | 38 | eqcomd 2743 |
. . . . . . . . . 10
โข ((๐ฅ โ Q โง
๐ โ Q)
โ ๐ฅ = (๐
ยทQ (๐ฅ ยทQ
(*Qโ๐)))) |
40 | | ovex 7395 |
. . . . . . . . . . 11
โข (๐ฅ
ยทQ (*Qโ๐)) โ V |
41 | | oveq2 7370 |
. . . . . . . . . . . 12
โข (๐ = (๐ฅ ยทQ
(*Qโ๐)) โ (๐ ยทQ ๐) = (๐ ยทQ (๐ฅ
ยทQ (*Qโ๐)))) |
42 | 41 | eqeq2d 2748 |
. . . . . . . . . . 11
โข (๐ = (๐ฅ ยทQ
(*Qโ๐)) โ (๐ฅ = (๐ ยทQ ๐) โ ๐ฅ = (๐ ยทQ (๐ฅ
ยทQ (*Qโ๐))))) |
43 | 40, 42 | spcev 3568 |
. . . . . . . . . 10
โข (๐ฅ = (๐ ยทQ (๐ฅ
ยทQ (*Qโ๐))) โ โ๐ ๐ฅ = (๐ ยทQ ๐)) |
44 | 27, 39, 43 | 3syl 18 |
. . . . . . . . 9
โข (๐ฅ <Q
๐ โ โ๐ ๐ฅ = (๐ ยทQ ๐)) |
45 | 44 | a1i 11 |
. . . . . . . 8
โข (๐ โ ๐ด โ (๐ฅ <Q ๐ โ โ๐ ๐ฅ = (๐ ยทQ ๐))) |
46 | 45 | ancld 552 |
. . . . . . 7
โข (๐ โ ๐ด โ (๐ฅ <Q ๐ โ (๐ฅ <Q ๐ โง โ๐ ๐ฅ = (๐ ยทQ ๐)))) |
47 | 46 | reximia 3085 |
. . . . . 6
โข
(โ๐ โ
๐ด ๐ฅ <Q ๐ โ โ๐ โ ๐ด (๐ฅ <Q ๐ โง โ๐ ๐ฅ = (๐ ยทQ ๐))) |
48 | 25, 47 | syl 17 |
. . . . 5
โข ((๐ด โ P โง
๐ฅ โ ๐ด) โ โ๐ โ ๐ด (๐ฅ <Q ๐ โง โ๐ ๐ฅ = (๐ ยทQ ๐))) |
49 | 48 | ex 414 |
. . . 4
โข (๐ด โ P โ
(๐ฅ โ ๐ด โ โ๐ โ ๐ด (๐ฅ <Q ๐ โง โ๐ ๐ฅ = (๐ ยทQ ๐)))) |
50 | | prcdnq 10936 |
. . . . . 6
โข ((๐ด โ P โง
๐ โ ๐ด) โ (๐ฅ <Q ๐ โ ๐ฅ โ ๐ด)) |
51 | 50 | adantrd 493 |
. . . . 5
โข ((๐ด โ P โง
๐ โ ๐ด) โ ((๐ฅ <Q ๐ โง โ๐ ๐ฅ = (๐ ยทQ ๐)) โ ๐ฅ โ ๐ด)) |
52 | 51 | rexlimdva 3153 |
. . . 4
โข (๐ด โ P โ
(โ๐ โ ๐ด (๐ฅ <Q ๐ โง โ๐ ๐ฅ = (๐ ยทQ ๐)) โ ๐ฅ โ ๐ด)) |
53 | 49, 52 | impbid 211 |
. . 3
โข (๐ด โ P โ
(๐ฅ โ ๐ด โ โ๐ โ ๐ด (๐ฅ <Q ๐ โง โ๐ ๐ฅ = (๐ ยทQ ๐)))) |
54 | 19, 24, 53 | 3bitr4d 311 |
. 2
โข (๐ด โ P โ
(๐ฅ โ (๐ด
ยทP 1P) โ ๐ฅ โ ๐ด)) |
55 | 54 | eqrdv 2735 |
1
โข (๐ด โ P โ
(๐ด
ยทP 1P) = ๐ด) |