Step | Hyp | Ref
| Expression |
1 | | simpr 110 |
. . . . 5
โข
((((โจ๐ฟ, ๐โฉ โ P
โง ๐บ โ ๐ฟ) โง ๐ โ Q) โง ๐ <Q
๐) โ ๐ <Q ๐) |
2 | | ltrnqi 7422 |
. . . . . 6
โข (๐ <Q
๐ โ
(*Qโ๐) <Q
(*Qโ๐)) |
3 | | ltrelnq 7366 |
. . . . . . . . . . . 12
โข
<Q โ (Q ร
Q) |
4 | 3 | brel 4680 |
. . . . . . . . . . 11
โข (๐ <Q
๐ โ (๐ โ Q โง ๐ โ
Q)) |
5 | 4 | adantl 277 |
. . . . . . . . . 10
โข
((((โจ๐ฟ, ๐โฉ โ P
โง ๐บ โ ๐ฟ) โง ๐ โ Q) โง ๐ <Q
๐) โ (๐ โ Q โง
๐ โ
Q)) |
6 | 5 | simprd 114 |
. . . . . . . . 9
โข
((((โจ๐ฟ, ๐โฉ โ P
โง ๐บ โ ๐ฟ) โง ๐ โ Q) โง ๐ <Q
๐) โ ๐ โ Q) |
7 | | recclnq 7393 |
. . . . . . . . 9
โข (๐ โ Q โ
(*Qโ๐) โ Q) |
8 | 6, 7 | syl 14 |
. . . . . . . 8
โข
((((โจ๐ฟ, ๐โฉ โ P
โง ๐บ โ ๐ฟ) โง ๐ โ Q) โง ๐ <Q
๐) โ
(*Qโ๐) โ Q) |
9 | | simplr 528 |
. . . . . . . . 9
โข
((((โจ๐ฟ, ๐โฉ โ P
โง ๐บ โ ๐ฟ) โง ๐ โ Q) โง ๐ <Q
๐) โ ๐ โ Q) |
10 | | recclnq 7393 |
. . . . . . . . 9
โข (๐ โ Q โ
(*Qโ๐) โ Q) |
11 | 9, 10 | syl 14 |
. . . . . . . 8
โข
((((โจ๐ฟ, ๐โฉ โ P
โง ๐บ โ ๐ฟ) โง ๐ โ Q) โง ๐ <Q
๐) โ
(*Qโ๐) โ Q) |
12 | | ltmnqg 7402 |
. . . . . . . 8
โข
(((*Qโ๐) โ Q โง
(*Qโ๐) โ Q โง ๐ โ Q) โ
((*Qโ๐) <Q
(*Qโ๐) โ (๐ ยทQ
(*Qโ๐)) <Q (๐
ยทQ (*Qโ๐)))) |
13 | 8, 11, 9, 12 | syl3anc 1238 |
. . . . . . 7
โข
((((โจ๐ฟ, ๐โฉ โ P
โง ๐บ โ ๐ฟ) โง ๐ โ Q) โง ๐ <Q
๐) โ
((*Qโ๐) <Q
(*Qโ๐) โ (๐ ยทQ
(*Qโ๐)) <Q (๐
ยทQ (*Qโ๐)))) |
14 | | ltmnqg 7402 |
. . . . . . . . 9
โข ((๐ฆ โ Q โง
๐ง โ Q
โง ๐ค โ
Q) โ (๐ฆ
<Q ๐ง โ (๐ค ยทQ ๐ฆ) <Q
(๐ค
ยทQ ๐ง))) |
15 | 14 | adantl 277 |
. . . . . . . 8
โข
(((((โจ๐ฟ, ๐โฉ โ P
โง ๐บ โ ๐ฟ) โง ๐ โ Q) โง ๐ <Q
๐) โง (๐ฆ โ Q โง
๐ง โ Q
โง ๐ค โ
Q)) โ (๐ฆ
<Q ๐ง โ (๐ค ยทQ ๐ฆ) <Q
(๐ค
ยทQ ๐ง))) |
16 | | mulclnq 7377 |
. . . . . . . . 9
โข ((๐ โ Q โง
(*Qโ๐) โ Q) โ (๐
ยทQ (*Qโ๐)) โ
Q) |
17 | 9, 8, 16 | syl2anc 411 |
. . . . . . . 8
โข
((((โจ๐ฟ, ๐โฉ โ P
โง ๐บ โ ๐ฟ) โง ๐ โ Q) โง ๐ <Q
๐) โ (๐
ยทQ (*Qโ๐)) โ
Q) |
18 | | mulclnq 7377 |
. . . . . . . . 9
โข ((๐ โ Q โง
(*Qโ๐) โ Q) โ (๐
ยทQ (*Qโ๐)) โ
Q) |
19 | 9, 11, 18 | syl2anc 411 |
. . . . . . . 8
โข
((((โจ๐ฟ, ๐โฉ โ P
โง ๐บ โ ๐ฟ) โง ๐ โ Q) โง ๐ <Q
๐) โ (๐
ยทQ (*Qโ๐)) โ
Q) |
20 | | elprnql 7482 |
. . . . . . . . 9
โข
((โจ๐ฟ, ๐โฉ โ P
โง ๐บ โ ๐ฟ) โ ๐บ โ Q) |
21 | 20 | ad2antrr 488 |
. . . . . . . 8
โข
((((โจ๐ฟ, ๐โฉ โ P
โง ๐บ โ ๐ฟ) โง ๐ โ Q) โง ๐ <Q
๐) โ ๐บ โ Q) |
22 | | mulcomnqg 7384 |
. . . . . . . . 9
โข ((๐ฆ โ Q โง
๐ง โ Q)
โ (๐ฆ
ยทQ ๐ง) = (๐ง ยทQ ๐ฆ)) |
23 | 22 | adantl 277 |
. . . . . . . 8
โข
(((((โจ๐ฟ, ๐โฉ โ P
โง ๐บ โ ๐ฟ) โง ๐ โ Q) โง ๐ <Q
๐) โง (๐ฆ โ Q โง
๐ง โ Q))
โ (๐ฆ
ยทQ ๐ง) = (๐ง ยทQ ๐ฆ)) |
24 | 15, 17, 19, 21, 23 | caovord2d 6046 |
. . . . . . 7
โข
((((โจ๐ฟ, ๐โฉ โ P
โง ๐บ โ ๐ฟ) โง ๐ โ Q) โง ๐ <Q
๐) โ ((๐
ยทQ (*Qโ๐))
<Q (๐ ยทQ
(*Qโ๐)) โ ((๐ ยทQ
(*Qโ๐)) ยทQ ๐บ) <Q
((๐
ยทQ (*Qโ๐))
ยทQ ๐บ))) |
25 | 13, 24 | bitrd 188 |
. . . . . 6
โข
((((โจ๐ฟ, ๐โฉ โ P
โง ๐บ โ ๐ฟ) โง ๐ โ Q) โง ๐ <Q
๐) โ
((*Qโ๐) <Q
(*Qโ๐) โ ((๐ ยทQ
(*Qโ๐)) ยทQ ๐บ) <Q
((๐
ยทQ (*Qโ๐))
ยทQ ๐บ))) |
26 | 2, 25 | imbitrid 154 |
. . . . 5
โข
((((โจ๐ฟ, ๐โฉ โ P
โง ๐บ โ ๐ฟ) โง ๐ โ Q) โง ๐ <Q
๐) โ (๐ <Q
๐ โ ((๐
ยทQ (*Qโ๐))
ยทQ ๐บ) <Q ((๐
ยทQ (*Qโ๐))
ยทQ ๐บ))) |
27 | 1, 26 | mpd 13 |
. . . 4
โข
((((โจ๐ฟ, ๐โฉ โ P
โง ๐บ โ ๐ฟ) โง ๐ โ Q) โง ๐ <Q
๐) โ ((๐
ยทQ (*Qโ๐))
ยทQ ๐บ) <Q ((๐
ยทQ (*Qโ๐))
ยทQ ๐บ)) |
28 | | recidnq 7394 |
. . . . . . . 8
โข (๐ โ Q โ
(๐
ยทQ (*Qโ๐)) =
1Q) |
29 | 28 | oveq1d 5892 |
. . . . . . 7
โข (๐ โ Q โ
((๐
ยทQ (*Qโ๐))
ยทQ ๐บ) = (1Q
ยทQ ๐บ)) |
30 | | 1nq 7367 |
. . . . . . . . 9
โข
1Q โ Q |
31 | | mulcomnqg 7384 |
. . . . . . . . 9
โข
((1Q โ Q โง ๐บ โ Q) โ
(1Q ยทQ ๐บ) = (๐บ ยทQ
1Q)) |
32 | 30, 31 | mpan 424 |
. . . . . . . 8
โข (๐บ โ Q โ
(1Q ยทQ ๐บ) = (๐บ ยทQ
1Q)) |
33 | | mulidnq 7390 |
. . . . . . . 8
โข (๐บ โ Q โ
(๐บ
ยทQ 1Q) = ๐บ) |
34 | 32, 33 | eqtrd 2210 |
. . . . . . 7
โข (๐บ โ Q โ
(1Q ยทQ ๐บ) = ๐บ) |
35 | 29, 34 | sylan9eqr 2232 |
. . . . . 6
โข ((๐บ โ Q โง
๐ โ Q)
โ ((๐
ยทQ (*Qโ๐))
ยทQ ๐บ) = ๐บ) |
36 | 35 | breq2d 4017 |
. . . . 5
โข ((๐บ โ Q โง
๐ โ Q)
โ (((๐
ยทQ (*Qโ๐))
ยทQ ๐บ) <Q ((๐
ยทQ (*Qโ๐))
ยทQ ๐บ) โ ((๐ ยทQ
(*Qโ๐)) ยทQ ๐บ) <Q
๐บ)) |
37 | 21, 9, 36 | syl2anc 411 |
. . . 4
โข
((((โจ๐ฟ, ๐โฉ โ P
โง ๐บ โ ๐ฟ) โง ๐ โ Q) โง ๐ <Q
๐) โ (((๐
ยทQ (*Qโ๐))
ยทQ ๐บ) <Q ((๐
ยทQ (*Qโ๐))
ยทQ ๐บ) โ ((๐ ยทQ
(*Qโ๐)) ยทQ ๐บ) <Q
๐บ)) |
38 | 27, 37 | mpbid 147 |
. . 3
โข
((((โจ๐ฟ, ๐โฉ โ P
โง ๐บ โ ๐ฟ) โง ๐ โ Q) โง ๐ <Q
๐) โ ((๐
ยทQ (*Qโ๐))
ยทQ ๐บ) <Q ๐บ) |
39 | | prcdnql 7485 |
. . . 4
โข
((โจ๐ฟ, ๐โฉ โ P
โง ๐บ โ ๐ฟ) โ (((๐ ยทQ
(*Qโ๐)) ยทQ ๐บ) <Q
๐บ โ ((๐
ยทQ (*Qโ๐))
ยทQ ๐บ) โ ๐ฟ)) |
40 | 39 | ad2antrr 488 |
. . 3
โข
((((โจ๐ฟ, ๐โฉ โ P
โง ๐บ โ ๐ฟ) โง ๐ โ Q) โง ๐ <Q
๐) โ (((๐
ยทQ (*Qโ๐))
ยทQ ๐บ) <Q ๐บ โ ((๐ ยทQ
(*Qโ๐)) ยทQ ๐บ) โ ๐ฟ)) |
41 | 38, 40 | mpd 13 |
. 2
โข
((((โจ๐ฟ, ๐โฉ โ P
โง ๐บ โ ๐ฟ) โง ๐ โ Q) โง ๐ <Q
๐) โ ((๐
ยทQ (*Qโ๐))
ยทQ ๐บ) โ ๐ฟ) |
42 | 41 | ex 115 |
1
โข
(((โจ๐ฟ, ๐โฉ โ P
โง ๐บ โ ๐ฟ) โง ๐ โ Q) โ (๐ <Q
๐ โ ((๐
ยทQ (*Qโ๐))
ยทQ ๐บ) โ ๐ฟ)) |