Step | Hyp | Ref
| Expression |
1 | | mulnqprlemfl 7576 |
. . 3
โข ((๐ด โ Q โง
๐ต โ Q)
โ (1st โโจ{๐ โฃ ๐ <Q (๐ด
ยทQ ๐ต)}, {๐ข โฃ (๐ด ยทQ ๐ต) <Q
๐ข}โฉ) โ
(1st โ(โจ{๐ โฃ ๐ <Q ๐ด}, {๐ข โฃ ๐ด <Q ๐ข}โฉ
ยทP โจ{๐ โฃ ๐ <Q ๐ต}, {๐ข โฃ ๐ต <Q ๐ข}โฉ))) |
2 | | mulnqprlemrl 7574 |
. . 3
โข ((๐ด โ Q โง
๐ต โ Q)
โ (1st โ(โจ{๐ โฃ ๐ <Q ๐ด}, {๐ข โฃ ๐ด <Q ๐ข}โฉ
ยทP โจ{๐ โฃ ๐ <Q ๐ต}, {๐ข โฃ ๐ต <Q ๐ข}โฉ)) โ
(1st โโจ{๐ โฃ ๐ <Q (๐ด
ยทQ ๐ต)}, {๐ข โฃ (๐ด ยทQ ๐ต) <Q
๐ข}โฉ)) |
3 | 1, 2 | eqssd 3174 |
. 2
โข ((๐ด โ Q โง
๐ต โ Q)
โ (1st โโจ{๐ โฃ ๐ <Q (๐ด
ยทQ ๐ต)}, {๐ข โฃ (๐ด ยทQ ๐ต) <Q
๐ข}โฉ) = (1st
โ(โจ{๐ โฃ
๐
<Q ๐ด}, {๐ข โฃ ๐ด <Q ๐ข}โฉ
ยทP โจ{๐ โฃ ๐ <Q ๐ต}, {๐ข โฃ ๐ต <Q ๐ข}โฉ))) |
4 | | mulnqprlemfu 7577 |
. . 3
โข ((๐ด โ Q โง
๐ต โ Q)
โ (2nd โโจ{๐ โฃ ๐ <Q (๐ด
ยทQ ๐ต)}, {๐ข โฃ (๐ด ยทQ ๐ต) <Q
๐ข}โฉ) โ
(2nd โ(โจ{๐ โฃ ๐ <Q ๐ด}, {๐ข โฃ ๐ด <Q ๐ข}โฉ
ยทP โจ{๐ โฃ ๐ <Q ๐ต}, {๐ข โฃ ๐ต <Q ๐ข}โฉ))) |
5 | | mulnqprlemru 7575 |
. . 3
โข ((๐ด โ Q โง
๐ต โ Q)
โ (2nd โ(โจ{๐ โฃ ๐ <Q ๐ด}, {๐ข โฃ ๐ด <Q ๐ข}โฉ
ยทP โจ{๐ โฃ ๐ <Q ๐ต}, {๐ข โฃ ๐ต <Q ๐ข}โฉ)) โ
(2nd โโจ{๐ โฃ ๐ <Q (๐ด
ยทQ ๐ต)}, {๐ข โฃ (๐ด ยทQ ๐ต) <Q
๐ข}โฉ)) |
6 | 4, 5 | eqssd 3174 |
. 2
โข ((๐ด โ Q โง
๐ต โ Q)
โ (2nd โโจ{๐ โฃ ๐ <Q (๐ด
ยทQ ๐ต)}, {๐ข โฃ (๐ด ยทQ ๐ต) <Q
๐ข}โฉ) = (2nd
โ(โจ{๐ โฃ
๐
<Q ๐ด}, {๐ข โฃ ๐ด <Q ๐ข}โฉ
ยทP โจ{๐ โฃ ๐ <Q ๐ต}, {๐ข โฃ ๐ต <Q ๐ข}โฉ))) |
7 | | mulclnq 7377 |
. . . 4
โข ((๐ด โ Q โง
๐ต โ Q)
โ (๐ด
ยทQ ๐ต) โ Q) |
8 | | nqprlu 7548 |
. . . 4
โข ((๐ด
ยทQ ๐ต) โ Q โ โจ{๐ โฃ ๐ <Q (๐ด
ยทQ ๐ต)}, {๐ข โฃ (๐ด ยทQ ๐ต) <Q
๐ข}โฉ โ
P) |
9 | 7, 8 | syl 14 |
. . 3
โข ((๐ด โ Q โง
๐ต โ Q)
โ โจ{๐ โฃ
๐
<Q (๐ด ยทQ ๐ต)}, {๐ข โฃ (๐ด ยทQ ๐ต) <Q
๐ข}โฉ โ
P) |
10 | | nqprlu 7548 |
. . . 4
โข (๐ด โ Q โ
โจ{๐ โฃ ๐ <Q
๐ด}, {๐ข โฃ ๐ด <Q ๐ข}โฉ โ
P) |
11 | | nqprlu 7548 |
. . . 4
โข (๐ต โ Q โ
โจ{๐ โฃ ๐ <Q
๐ต}, {๐ข โฃ ๐ต <Q ๐ข}โฉ โ
P) |
12 | | mulclpr 7573 |
. . . 4
โข
((โจ{๐ โฃ
๐
<Q ๐ด}, {๐ข โฃ ๐ด <Q ๐ข}โฉ โ P
โง โจ{๐ โฃ
๐
<Q ๐ต}, {๐ข โฃ ๐ต <Q ๐ข}โฉ โ P)
โ (โจ{๐ โฃ
๐
<Q ๐ด}, {๐ข โฃ ๐ด <Q ๐ข}โฉ
ยทP โจ{๐ โฃ ๐ <Q ๐ต}, {๐ข โฃ ๐ต <Q ๐ข}โฉ) โ
P) |
13 | 10, 11, 12 | syl2an 289 |
. . 3
โข ((๐ด โ Q โง
๐ต โ Q)
โ (โจ{๐ โฃ
๐
<Q ๐ด}, {๐ข โฃ ๐ด <Q ๐ข}โฉ
ยทP โจ{๐ โฃ ๐ <Q ๐ต}, {๐ข โฃ ๐ต <Q ๐ข}โฉ) โ
P) |
14 | | preqlu 7473 |
. . 3
โข
((โจ{๐ โฃ
๐
<Q (๐ด ยทQ ๐ต)}, {๐ข โฃ (๐ด ยทQ ๐ต) <Q
๐ข}โฉ โ
P โง (โจ{๐ โฃ ๐ <Q ๐ด}, {๐ข โฃ ๐ด <Q ๐ข}โฉ
ยทP โจ{๐ โฃ ๐ <Q ๐ต}, {๐ข โฃ ๐ต <Q ๐ข}โฉ) โ P)
โ (โจ{๐ โฃ
๐
<Q (๐ด ยทQ ๐ต)}, {๐ข โฃ (๐ด ยทQ ๐ต) <Q
๐ข}โฉ = (โจ{๐ โฃ ๐ <Q ๐ด}, {๐ข โฃ ๐ด <Q ๐ข}โฉ
ยทP โจ{๐ โฃ ๐ <Q ๐ต}, {๐ข โฃ ๐ต <Q ๐ข}โฉ) โ ((1st
โโจ{๐ โฃ
๐
<Q (๐ด ยทQ ๐ต)}, {๐ข โฃ (๐ด ยทQ ๐ต) <Q
๐ข}โฉ) = (1st
โ(โจ{๐ โฃ
๐
<Q ๐ด}, {๐ข โฃ ๐ด <Q ๐ข}โฉ
ยทP โจ{๐ โฃ ๐ <Q ๐ต}, {๐ข โฃ ๐ต <Q ๐ข}โฉ)) โง (2nd
โโจ{๐ โฃ
๐
<Q (๐ด ยทQ ๐ต)}, {๐ข โฃ (๐ด ยทQ ๐ต) <Q
๐ข}โฉ) = (2nd
โ(โจ{๐ โฃ
๐
<Q ๐ด}, {๐ข โฃ ๐ด <Q ๐ข}โฉ
ยทP โจ{๐ โฃ ๐ <Q ๐ต}, {๐ข โฃ ๐ต <Q ๐ข}โฉ))))) |
15 | 9, 13, 14 | syl2anc 411 |
. 2
โข ((๐ด โ Q โง
๐ต โ Q)
โ (โจ{๐ โฃ
๐
<Q (๐ด ยทQ ๐ต)}, {๐ข โฃ (๐ด ยทQ ๐ต) <Q
๐ข}โฉ = (โจ{๐ โฃ ๐ <Q ๐ด}, {๐ข โฃ ๐ด <Q ๐ข}โฉ
ยทP โจ{๐ โฃ ๐ <Q ๐ต}, {๐ข โฃ ๐ต <Q ๐ข}โฉ) โ ((1st
โโจ{๐ โฃ
๐
<Q (๐ด ยทQ ๐ต)}, {๐ข โฃ (๐ด ยทQ ๐ต) <Q
๐ข}โฉ) = (1st
โ(โจ{๐ โฃ
๐
<Q ๐ด}, {๐ข โฃ ๐ด <Q ๐ข}โฉ
ยทP โจ{๐ โฃ ๐ <Q ๐ต}, {๐ข โฃ ๐ต <Q ๐ข}โฉ)) โง (2nd
โโจ{๐ โฃ
๐
<Q (๐ด ยทQ ๐ต)}, {๐ข โฃ (๐ด ยทQ ๐ต) <Q
๐ข}โฉ) = (2nd
โ(โจ{๐ โฃ
๐
<Q ๐ด}, {๐ข โฃ ๐ด <Q ๐ข}โฉ
ยทP โจ{๐ โฃ ๐ <Q ๐ต}, {๐ข โฃ ๐ต <Q ๐ข}โฉ))))) |
16 | 3, 6, 15 | mpbir2and 944 |
1
โข ((๐ด โ Q โง
๐ต โ Q)
โ โจ{๐ โฃ
๐
<Q (๐ด ยทQ ๐ต)}, {๐ข โฃ (๐ด ยทQ ๐ต) <Q
๐ข}โฉ = (โจ{๐ โฃ ๐ <Q ๐ด}, {๐ข โฃ ๐ด <Q ๐ข}โฉ
ยทP โจ{๐ โฃ ๐ <Q ๐ต}, {๐ข โฃ ๐ต <Q ๐ข}โฉ)) |