Step | Hyp | Ref
| Expression |
1 | | elprnq 10934 |
. . . . . 6
โข ((๐ด โ P โง
๐ โ ๐ด) โ ๐ โ Q) |
2 | | elprnq 10934 |
. . . . . 6
โข ((๐ต โ P โง
โ โ ๐ต) โ โ โ Q) |
3 | | recclnq 10909 |
. . . . . . . . 9
โข (โ โ Q โ
(*Qโโ) โ Q) |
4 | 3 | adantl 483 |
. . . . . . . 8
โข ((๐ โ Q โง
โ โ Q)
โ (*Qโโ) โ Q) |
5 | | vex 3452 |
. . . . . . . . 9
โข ๐ฅ โ V |
6 | | ovex 7395 |
. . . . . . . . 9
โข (๐
ยทQ โ) โ V |
7 | | ltmnq 10915 |
. . . . . . . . 9
โข (๐ค โ Q โ
(๐ฆ
<Q ๐ง โ (๐ค ยทQ ๐ฆ) <Q
(๐ค
ยทQ ๐ง))) |
8 | | fvex 6860 |
. . . . . . . . 9
โข
(*Qโโ) โ V |
9 | | mulcomnq 10896 |
. . . . . . . . 9
โข (๐ฆ
ยทQ ๐ง) = (๐ง ยทQ ๐ฆ) |
10 | 5, 6, 7, 8, 9 | caovord2 7571 |
. . . . . . . 8
โข
((*Qโโ) โ Q โ (๐ฅ <Q
(๐
ยทQ โ) โ (๐ฅ ยทQ
(*Qโโ)) <Q ((๐
ยทQ โ) ยทQ
(*Qโโ)))) |
11 | 4, 10 | syl 17 |
. . . . . . 7
โข ((๐ โ Q โง
โ โ Q)
โ (๐ฅ
<Q (๐ ยทQ โ) โ (๐ฅ ยทQ
(*Qโโ)) <Q ((๐
ยทQ โ) ยทQ
(*Qโโ)))) |
12 | | mulassnq 10902 |
. . . . . . . . . 10
โข ((๐
ยทQ โ) ยทQ
(*Qโโ)) = (๐ ยทQ (โ
ยทQ (*Qโโ))) |
13 | | recidnq 10908 |
. . . . . . . . . . 11
โข (โ โ Q โ
(โ
ยทQ (*Qโโ)) =
1Q) |
14 | 13 | oveq2d 7378 |
. . . . . . . . . 10
โข (โ โ Q โ
(๐
ยทQ (โ ยทQ
(*Qโโ))) = (๐ ยทQ
1Q)) |
15 | 12, 14 | eqtrid 2789 |
. . . . . . . . 9
โข (โ โ Q โ
((๐
ยทQ โ) ยทQ
(*Qโโ)) = (๐ ยทQ
1Q)) |
16 | | mulidnq 10906 |
. . . . . . . . 9
โข (๐ โ Q โ
(๐
ยทQ 1Q) = ๐) |
17 | 15, 16 | sylan9eqr 2799 |
. . . . . . . 8
โข ((๐ โ Q โง
โ โ Q)
โ ((๐
ยทQ โ) ยทQ
(*Qโโ)) = ๐) |
18 | 17 | breq2d 5122 |
. . . . . . 7
โข ((๐ โ Q โง
โ โ Q)
โ ((๐ฅ
ยทQ (*Qโโ)) <Q
((๐
ยทQ โ) ยทQ
(*Qโโ)) โ (๐ฅ ยทQ
(*Qโโ)) <Q ๐)) |
19 | 11, 18 | bitrd 279 |
. . . . . 6
โข ((๐ โ Q โง
โ โ Q)
โ (๐ฅ
<Q (๐ ยทQ โ) โ (๐ฅ ยทQ
(*Qโโ)) <Q ๐)) |
20 | 1, 2, 19 | syl2an 597 |
. . . . 5
โข (((๐ด โ P โง
๐ โ ๐ด) โง (๐ต โ P โง โ โ ๐ต)) โ (๐ฅ <Q (๐
ยทQ โ) โ (๐ฅ ยทQ
(*Qโโ)) <Q ๐)) |
21 | | prcdnq 10936 |
. . . . . 6
โข ((๐ด โ P โง
๐ โ ๐ด) โ ((๐ฅ ยทQ
(*Qโโ)) <Q ๐ โ (๐ฅ ยทQ
(*Qโโ)) โ ๐ด)) |
22 | 21 | adantr 482 |
. . . . 5
โข (((๐ด โ P โง
๐ โ ๐ด) โง (๐ต โ P โง โ โ ๐ต)) โ ((๐ฅ ยทQ
(*Qโโ)) <Q ๐ โ (๐ฅ ยทQ
(*Qโโ)) โ ๐ด)) |
23 | 20, 22 | sylbid 239 |
. . . 4
โข (((๐ด โ P โง
๐ โ ๐ด) โง (๐ต โ P โง โ โ ๐ต)) โ (๐ฅ <Q (๐
ยทQ โ) โ (๐ฅ ยทQ
(*Qโโ)) โ ๐ด)) |
24 | | df-mp 10927 |
. . . . . . . . 9
โข
ยทP = (๐ค โ P, ๐ฃ โ P โฆ {๐ฅ โฃ โ๐ฆ โ ๐ค โ๐ง โ ๐ฃ ๐ฅ = (๐ฆ ยทQ ๐ง)}) |
25 | | mulclnq 10890 |
. . . . . . . . 9
โข ((๐ฆ โ Q โง
๐ง โ Q)
โ (๐ฆ
ยทQ ๐ง) โ Q) |
26 | 24, 25 | genpprecl 10944 |
. . . . . . . 8
โข ((๐ด โ P โง
๐ต โ P)
โ (((๐ฅ
ยทQ (*Qโโ)) โ ๐ด โง โ โ ๐ต) โ ((๐ฅ ยทQ
(*Qโโ)) ยทQ โ) โ (๐ด ยทP ๐ต))) |
27 | 26 | exp4b 432 |
. . . . . . 7
โข (๐ด โ P โ
(๐ต โ P
โ ((๐ฅ
ยทQ (*Qโโ)) โ ๐ด โ (โ โ ๐ต โ ((๐ฅ ยทQ
(*Qโโ)) ยทQ โ) โ (๐ด ยทP ๐ต))))) |
28 | 27 | com34 91 |
. . . . . 6
โข (๐ด โ P โ
(๐ต โ P
โ (โ โ ๐ต โ ((๐ฅ ยทQ
(*Qโโ)) โ ๐ด โ ((๐ฅ ยทQ
(*Qโโ)) ยทQ โ) โ (๐ด ยทP ๐ต))))) |
29 | 28 | imp32 420 |
. . . . 5
โข ((๐ด โ P โง
(๐ต โ P
โง โ โ ๐ต)) โ ((๐ฅ ยทQ
(*Qโโ)) โ ๐ด โ ((๐ฅ ยทQ
(*Qโโ)) ยทQ โ) โ (๐ด ยทP ๐ต))) |
30 | 29 | adantlr 714 |
. . . 4
โข (((๐ด โ P โง
๐ โ ๐ด) โง (๐ต โ P โง โ โ ๐ต)) โ ((๐ฅ ยทQ
(*Qโโ)) โ ๐ด โ ((๐ฅ ยทQ
(*Qโโ)) ยทQ โ) โ (๐ด ยทP ๐ต))) |
31 | 23, 30 | syld 47 |
. . 3
โข (((๐ด โ P โง
๐ โ ๐ด) โง (๐ต โ P โง โ โ ๐ต)) โ (๐ฅ <Q (๐
ยทQ โ) โ ((๐ฅ ยทQ
(*Qโโ)) ยทQ โ) โ (๐ด ยทP ๐ต))) |
32 | 31 | adantr 482 |
. 2
โข ((((๐ด โ P โง
๐ โ ๐ด) โง (๐ต โ P โง โ โ ๐ต)) โง ๐ฅ โ Q) โ (๐ฅ <Q
(๐
ยทQ โ) โ ((๐ฅ ยทQ
(*Qโโ)) ยทQ โ) โ (๐ด ยทP ๐ต))) |
33 | 2 | adantl 483 |
. . 3
โข (((๐ด โ P โง
๐ โ ๐ด) โง (๐ต โ P โง โ โ ๐ต)) โ โ โ Q) |
34 | | mulassnq 10902 |
. . . . . 6
โข ((๐ฅ
ยทQ (*Qโโ))
ยทQ โ) = (๐ฅ ยทQ
((*Qโโ) ยทQ โ)) |
35 | | mulcomnq 10896 |
. . . . . . . 8
โข
((*Qโโ) ยทQ โ) = (โ ยทQ
(*Qโโ)) |
36 | 35, 13 | eqtrid 2789 |
. . . . . . 7
โข (โ โ Q โ
((*Qโโ) ยทQ โ) =
1Q) |
37 | 36 | oveq2d 7378 |
. . . . . 6
โข (โ โ Q โ
(๐ฅ
ยทQ ((*Qโโ)
ยทQ โ)) = (๐ฅ ยทQ
1Q)) |
38 | 34, 37 | eqtrid 2789 |
. . . . 5
โข (โ โ Q โ
((๐ฅ
ยทQ (*Qโโ))
ยทQ โ) = (๐ฅ ยทQ
1Q)) |
39 | | mulidnq 10906 |
. . . . 5
โข (๐ฅ โ Q โ
(๐ฅ
ยทQ 1Q) = ๐ฅ) |
40 | 38, 39 | sylan9eq 2797 |
. . . 4
โข ((โ โ Q โง
๐ฅ โ Q)
โ ((๐ฅ
ยทQ (*Qโโ))
ยทQ โ) = ๐ฅ) |
41 | 40 | eleq1d 2823 |
. . 3
โข ((โ โ Q โง
๐ฅ โ Q)
โ (((๐ฅ
ยทQ (*Qโโ))
ยทQ โ) โ (๐ด ยทP ๐ต) โ ๐ฅ โ (๐ด ยทP ๐ต))) |
42 | 33, 41 | sylan 581 |
. 2
โข ((((๐ด โ P โง
๐ โ ๐ด) โง (๐ต โ P โง โ โ ๐ต)) โง ๐ฅ โ Q) โ (((๐ฅ
ยทQ (*Qโโ))
ยทQ โ) โ (๐ด ยทP ๐ต) โ ๐ฅ โ (๐ด ยทP ๐ต))) |
43 | 32, 42 | sylibd 238 |
1
โข ((((๐ด โ P โง
๐ โ ๐ด) โง (๐ต โ P โง โ โ ๐ต)) โง ๐ฅ โ Q) โ (๐ฅ <Q
(๐
ยทQ โ) โ ๐ฅ โ (๐ด ยทP ๐ต))) |