Step | Hyp | Ref
| Expression |
1 | | mullocprlem.uqedu |
. . . . . . 7
โข (๐ โ (๐ ยทQ ๐) <Q
(๐ธ
ยทQ (๐ท ยทQ ๐))) |
2 | | mullocprlem.et |
. . . . . . . . 9
โข (๐ โ (๐ธ โ Q โง ๐ โ
Q)) |
3 | 2 | simpld 112 |
. . . . . . . 8
โข (๐ โ ๐ธ โ Q) |
4 | | mullocprlem.duq |
. . . . . . . . 9
โข (๐ โ (๐ท โ Q โง ๐ โ
Q)) |
5 | 4 | simpld 112 |
. . . . . . . 8
โข (๐ โ ๐ท โ Q) |
6 | 4 | simprd 114 |
. . . . . . . 8
โข (๐ โ ๐ โ Q) |
7 | | mulcomnqg 7384 |
. . . . . . . . 9
โข ((๐ฅ โ Q โง
๐ฆ โ Q)
โ (๐ฅ
ยทQ ๐ฆ) = (๐ฆ ยทQ ๐ฅ)) |
8 | 7 | adantl 277 |
. . . . . . . 8
โข ((๐ โง (๐ฅ โ Q โง ๐ฆ โ Q)) โ
(๐ฅ
ยทQ ๐ฆ) = (๐ฆ ยทQ ๐ฅ)) |
9 | | mulassnqg 7385 |
. . . . . . . . 9
โข ((๐ฅ โ Q โง
๐ฆ โ Q
โง ๐ง โ
Q) โ ((๐ฅ
ยทQ ๐ฆ) ยทQ ๐ง) = (๐ฅ ยทQ (๐ฆ
ยทQ ๐ง))) |
10 | 9 | adantl 277 |
. . . . . . . 8
โข ((๐ โง (๐ฅ โ Q โง ๐ฆ โ Q โง
๐ง โ Q))
โ ((๐ฅ
ยทQ ๐ฆ) ยทQ ๐ง) = (๐ฅ ยทQ (๐ฆ
ยทQ ๐ง))) |
11 | 3, 5, 6, 8, 10 | caov13d 6060 |
. . . . . . 7
โข (๐ โ (๐ธ ยทQ (๐ท
ยทQ ๐)) = (๐ ยทQ (๐ท
ยทQ ๐ธ))) |
12 | 1, 11 | breqtrd 4031 |
. . . . . 6
โข (๐ โ (๐ ยทQ ๐) <Q
(๐
ยทQ (๐ท ยทQ ๐ธ))) |
13 | | mullocprlem.qr |
. . . . . . . 8
โข (๐ โ (๐ โ Q โง ๐
โ
Q)) |
14 | 13 | simpld 112 |
. . . . . . 7
โข (๐ โ ๐ โ Q) |
15 | | mulclnq 7377 |
. . . . . . . 8
โข ((๐ท โ Q โง
๐ธ โ Q)
โ (๐ท
ยทQ ๐ธ) โ Q) |
16 | 5, 3, 15 | syl2anc 411 |
. . . . . . 7
โข (๐ โ (๐ท ยทQ ๐ธ) โ
Q) |
17 | | ltmnqg 7402 |
. . . . . . 7
โข ((๐ โ Q โง
(๐ท
ยทQ ๐ธ) โ Q โง ๐ โ Q) โ
(๐
<Q (๐ท ยทQ ๐ธ) โ (๐ ยทQ ๐) <Q
(๐
ยทQ (๐ท ยทQ ๐ธ)))) |
18 | 14, 16, 6, 17 | syl3anc 1238 |
. . . . . 6
โข (๐ โ (๐ <Q (๐ท
ยทQ ๐ธ) โ (๐ ยทQ ๐) <Q
(๐
ยทQ (๐ท ยทQ ๐ธ)))) |
19 | 12, 18 | mpbird 167 |
. . . . 5
โข (๐ โ ๐ <Q (๐ท
ยทQ ๐ธ)) |
20 | 19 | adantr 276 |
. . . 4
โข ((๐ โง ๐ธ โ (1st โ๐ต)) โ ๐ <Q (๐ท
ยทQ ๐ธ)) |
21 | | mullocprlem.ab |
. . . . . . . 8
โข (๐ โ (๐ด โ P โง ๐ต โ
P)) |
22 | 21 | simpld 112 |
. . . . . . 7
โข (๐ โ ๐ด โ P) |
23 | | mullocprlem.du |
. . . . . . . 8
โข (๐ โ (๐ท โ (1st โ๐ด) โง ๐ โ (2nd โ๐ด))) |
24 | 23 | simpld 112 |
. . . . . . 7
โข (๐ โ ๐ท โ (1st โ๐ด)) |
25 | 22, 24 | jca 306 |
. . . . . 6
โข (๐ โ (๐ด โ P โง ๐ท โ (1st
โ๐ด))) |
26 | 25 | adantr 276 |
. . . . 5
โข ((๐ โง ๐ธ โ (1st โ๐ต)) โ (๐ด โ P โง ๐ท โ (1st
โ๐ด))) |
27 | 21 | simprd 114 |
. . . . . 6
โข (๐ โ ๐ต โ P) |
28 | 27 | anim1i 340 |
. . . . 5
โข ((๐ โง ๐ธ โ (1st โ๐ต)) โ (๐ต โ P โง ๐ธ โ (1st
โ๐ต))) |
29 | 14 | adantr 276 |
. . . . 5
โข ((๐ โง ๐ธ โ (1st โ๐ต)) โ ๐ โ Q) |
30 | | mulnqprl 7569 |
. . . . 5
โข ((((๐ด โ P โง
๐ท โ (1st
โ๐ด)) โง (๐ต โ P โง
๐ธ โ (1st
โ๐ต))) โง ๐ โ Q) โ
(๐
<Q (๐ท ยทQ ๐ธ) โ ๐ โ (1st โ(๐ด
ยทP ๐ต)))) |
31 | 26, 28, 29, 30 | syl21anc 1237 |
. . . 4
โข ((๐ โง ๐ธ โ (1st โ๐ต)) โ (๐ <Q (๐ท
ยทQ ๐ธ) โ ๐ โ (1st โ(๐ด
ยทP ๐ต)))) |
32 | 20, 31 | mpd 13 |
. . 3
โข ((๐ โง ๐ธ โ (1st โ๐ต)) โ ๐ โ (1st โ(๐ด
ยทP ๐ต))) |
33 | 32 | orcd 733 |
. 2
โข ((๐ โง ๐ธ โ (1st โ๐ต)) โ (๐ โ (1st โ(๐ด
ยทP ๐ต)) โจ ๐
โ (2nd โ(๐ด
ยทP ๐ต)))) |
34 | 2 | simprd 114 |
. . . . . . 7
โข (๐ โ ๐ โ Q) |
35 | | mulcomnqg 7384 |
. . . . . . 7
โข ((๐ โ Q โง
๐ โ Q)
โ (๐
ยทQ ๐) = (๐ ยทQ ๐)) |
36 | 34, 6, 35 | syl2anc 411 |
. . . . . 6
โข (๐ โ (๐ ยทQ ๐) = (๐ ยทQ ๐)) |
37 | | mullocprlem.tdudr |
. . . . . . 7
โข (๐ โ (๐ ยทQ (๐ท
ยทQ ๐)) <Q (๐ท
ยทQ ๐
)) |
38 | | mulclnq 7377 |
. . . . . . . . . 10
โข ((๐ โ Q โง
๐ โ Q)
โ (๐
ยทQ ๐) โ Q) |
39 | 34, 6, 38 | syl2anc 411 |
. . . . . . . . 9
โข (๐ โ (๐ ยทQ ๐) โ
Q) |
40 | 13 | simprd 114 |
. . . . . . . . 9
โข (๐ โ ๐
โ Q) |
41 | | ltmnqg 7402 |
. . . . . . . . 9
โข (((๐
ยทQ ๐) โ Q โง ๐
โ Q โง
๐ท โ Q)
โ ((๐
ยทQ ๐) <Q ๐
โ (๐ท ยทQ (๐
ยทQ ๐)) <Q (๐ท
ยทQ ๐
))) |
42 | 39, 40, 5, 41 | syl3anc 1238 |
. . . . . . . 8
โข (๐ โ ((๐ ยทQ ๐) <Q
๐
โ (๐ท ยทQ (๐
ยทQ ๐)) <Q (๐ท
ยทQ ๐
))) |
43 | 34, 5, 6, 8, 10 | caov12d 6058 |
. . . . . . . . 9
โข (๐ โ (๐ ยทQ (๐ท
ยทQ ๐)) = (๐ท ยทQ (๐
ยทQ ๐))) |
44 | 43 | breq1d 4015 |
. . . . . . . 8
โข (๐ โ ((๐ ยทQ (๐ท
ยทQ ๐)) <Q (๐ท
ยทQ ๐
) โ (๐ท ยทQ (๐
ยทQ ๐)) <Q (๐ท
ยทQ ๐
))) |
45 | 42, 44 | bitr4d 191 |
. . . . . . 7
โข (๐ โ ((๐ ยทQ ๐) <Q
๐
โ (๐ ยทQ (๐ท
ยทQ ๐)) <Q (๐ท
ยทQ ๐
))) |
46 | 37, 45 | mpbird 167 |
. . . . . 6
โข (๐ โ (๐ ยทQ ๐) <Q
๐
) |
47 | 36, 46 | eqbrtrrd 4029 |
. . . . 5
โข (๐ โ (๐ ยทQ ๐) <Q
๐
) |
48 | 47 | adantr 276 |
. . . 4
โข ((๐ โง ๐ โ (2nd โ๐ต)) โ (๐ ยทQ ๐) <Q
๐
) |
49 | 23 | simprd 114 |
. . . . . . 7
โข (๐ โ ๐ โ (2nd โ๐ด)) |
50 | 22, 49 | jca 306 |
. . . . . 6
โข (๐ โ (๐ด โ P โง ๐ โ (2nd
โ๐ด))) |
51 | 50 | adantr 276 |
. . . . 5
โข ((๐ โง ๐ โ (2nd โ๐ต)) โ (๐ด โ P โง ๐ โ (2nd
โ๐ด))) |
52 | 27 | anim1i 340 |
. . . . 5
โข ((๐ โง ๐ โ (2nd โ๐ต)) โ (๐ต โ P โง ๐ โ (2nd
โ๐ต))) |
53 | 40 | adantr 276 |
. . . . 5
โข ((๐ โง ๐ โ (2nd โ๐ต)) โ ๐
โ Q) |
54 | | mulnqpru 7570 |
. . . . 5
โข ((((๐ด โ P โง
๐ โ (2nd
โ๐ด)) โง (๐ต โ P โง
๐ โ (2nd
โ๐ต))) โง ๐
โ Q) โ
((๐
ยทQ ๐) <Q ๐
โ ๐
โ (2nd โ(๐ด
ยทP ๐ต)))) |
55 | 51, 52, 53, 54 | syl21anc 1237 |
. . . 4
โข ((๐ โง ๐ โ (2nd โ๐ต)) โ ((๐ ยทQ ๐) <Q
๐
โ ๐
โ (2nd โ(๐ด
ยทP ๐ต)))) |
56 | 48, 55 | mpd 13 |
. . 3
โข ((๐ โง ๐ โ (2nd โ๐ต)) โ ๐
โ (2nd โ(๐ด
ยทP ๐ต))) |
57 | 56 | olcd 734 |
. 2
โข ((๐ โง ๐ โ (2nd โ๐ต)) โ (๐ โ (1st โ(๐ด
ยทP ๐ต)) โจ ๐
โ (2nd โ(๐ด
ยทP ๐ต)))) |
58 | | mullocprlem.edutdu |
. . . 4
โข (๐ โ (๐ธ ยทQ (๐ท
ยทQ ๐)) <Q (๐
ยทQ (๐ท ยทQ ๐))) |
59 | | mulclnq 7377 |
. . . . . . 7
โข ((๐ท โ Q โง
๐ โ Q)
โ (๐ท
ยทQ ๐) โ Q) |
60 | 4, 59 | syl 14 |
. . . . . 6
โข (๐ โ (๐ท ยทQ ๐) โ
Q) |
61 | | ltmnqg 7402 |
. . . . . 6
โข ((๐ธ โ Q โง
๐ โ Q
โง (๐ท
ยทQ ๐) โ Q) โ (๐ธ <Q
๐ โ ((๐ท
ยทQ ๐) ยทQ ๐ธ) <Q
((๐ท
ยทQ ๐) ยทQ ๐))) |
62 | 3, 34, 60, 61 | syl3anc 1238 |
. . . . 5
โข (๐ โ (๐ธ <Q ๐ โ ((๐ท ยทQ ๐)
ยทQ ๐ธ) <Q ((๐ท
ยทQ ๐) ยทQ ๐))) |
63 | | mulcomnqg 7384 |
. . . . . . 7
โข (((๐ท
ยทQ ๐) โ Q โง ๐ธ โ Q) โ
((๐ท
ยทQ ๐) ยทQ ๐ธ) = (๐ธ ยทQ (๐ท
ยทQ ๐))) |
64 | 60, 3, 63 | syl2anc 411 |
. . . . . 6
โข (๐ โ ((๐ท ยทQ ๐)
ยทQ ๐ธ) = (๐ธ ยทQ (๐ท
ยทQ ๐))) |
65 | | mulcomnqg 7384 |
. . . . . . 7
โข (((๐ท
ยทQ ๐) โ Q โง ๐ โ Q) โ
((๐ท
ยทQ ๐) ยทQ ๐) = (๐ ยทQ (๐ท
ยทQ ๐))) |
66 | 60, 34, 65 | syl2anc 411 |
. . . . . 6
โข (๐ โ ((๐ท ยทQ ๐)
ยทQ ๐) = (๐ ยทQ (๐ท
ยทQ ๐))) |
67 | 64, 66 | breq12d 4018 |
. . . . 5
โข (๐ โ (((๐ท ยทQ ๐)
ยทQ ๐ธ) <Q ((๐ท
ยทQ ๐) ยทQ ๐) โ (๐ธ ยทQ (๐ท
ยทQ ๐)) <Q (๐
ยทQ (๐ท ยทQ ๐)))) |
68 | 62, 67 | bitrd 188 |
. . . 4
โข (๐ โ (๐ธ <Q ๐ โ (๐ธ ยทQ (๐ท
ยทQ ๐)) <Q (๐
ยทQ (๐ท ยทQ ๐)))) |
69 | 58, 68 | mpbird 167 |
. . 3
โข (๐ โ ๐ธ <Q ๐) |
70 | | prop 7476 |
. . . 4
โข (๐ต โ P โ
โจ(1st โ๐ต), (2nd โ๐ต)โฉ โ
P) |
71 | | prloc 7492 |
. . . 4
โข
((โจ(1st โ๐ต), (2nd โ๐ต)โฉ โ P โง ๐ธ <Q
๐) โ (๐ธ โ (1st
โ๐ต) โจ ๐ โ (2nd
โ๐ต))) |
72 | 70, 71 | sylan 283 |
. . 3
โข ((๐ต โ P โง
๐ธ
<Q ๐) โ (๐ธ โ (1st โ๐ต) โจ ๐ โ (2nd โ๐ต))) |
73 | 27, 69, 72 | syl2anc 411 |
. 2
โข (๐ โ (๐ธ โ (1st โ๐ต) โจ ๐ โ (2nd โ๐ต))) |
74 | 33, 57, 73 | mpjaodan 798 |
1
โข (๐ โ (๐ โ (1st โ(๐ด
ยทP ๐ต)) โจ ๐
โ (2nd โ(๐ด
ยทP ๐ต)))) |