Step | Hyp | Ref
| Expression |
1 | | simpl 109 |
. . . 4
โข ((๐ด <Q
๐ต โง ๐ถ โ Q) โ ๐ด <Q
๐ต) |
2 | | ltrelnq 7363 |
. . . . . . . 8
โข
<Q โ (Q ร
Q) |
3 | 2 | brel 4678 |
. . . . . . 7
โข (๐ด <Q
๐ต โ (๐ด โ Q โง ๐ต โ
Q)) |
4 | 3 | adantr 276 |
. . . . . 6
โข ((๐ด <Q
๐ต โง ๐ถ โ Q) โ (๐ด โ Q โง
๐ต โ
Q)) |
5 | 4 | simpld 112 |
. . . . 5
โข ((๐ด <Q
๐ต โง ๐ถ โ Q) โ ๐ด โ
Q) |
6 | 4 | simprd 114 |
. . . . 5
โข ((๐ด <Q
๐ต โง ๐ถ โ Q) โ ๐ต โ
Q) |
7 | | recclnq 7390 |
. . . . . 6
โข (๐ถ โ Q โ
(*Qโ๐ถ) โ Q) |
8 | 7 | adantl 277 |
. . . . 5
โข ((๐ด <Q
๐ต โง ๐ถ โ Q) โ
(*Qโ๐ถ) โ Q) |
9 | | ltmnqg 7399 |
. . . . 5
โข ((๐ด โ Q โง
๐ต โ Q
โง (*Qโ๐ถ) โ Q) โ (๐ด <Q
๐ต โ
((*Qโ๐ถ) ยทQ ๐ด) <Q
((*Qโ๐ถ) ยทQ ๐ต))) |
10 | 5, 6, 8, 9 | syl3anc 1238 |
. . . 4
โข ((๐ด <Q
๐ต โง ๐ถ โ Q) โ (๐ด <Q
๐ต โ
((*Qโ๐ถ) ยทQ ๐ด) <Q
((*Qโ๐ถ) ยทQ ๐ต))) |
11 | 1, 10 | mpbid 147 |
. . 3
โข ((๐ด <Q
๐ต โง ๐ถ โ Q) โ
((*Qโ๐ถ) ยทQ ๐ด) <Q
((*Qโ๐ถ) ยทQ ๐ต)) |
12 | | ltbtwnnqq 7413 |
. . 3
โข
(((*Qโ๐ถ) ยทQ ๐ด) <Q
((*Qโ๐ถ) ยทQ ๐ต) โ โ๐ โ Q
(((*Qโ๐ถ) ยทQ ๐ด) <Q
๐ โง ๐ <Q
((*Qโ๐ถ) ยทQ ๐ต))) |
13 | 11, 12 | sylib 122 |
. 2
โข ((๐ด <Q
๐ต โง ๐ถ โ Q) โ โ๐ โ Q
(((*Qโ๐ถ) ยทQ ๐ด) <Q
๐ โง ๐ <Q
((*Qโ๐ถ) ยทQ ๐ต))) |
14 | 8 | adantr 276 |
. . . . . . . . 9
โข (((๐ด <Q
๐ต โง ๐ถ โ Q) โง ๐ โ Q) โ
(*Qโ๐ถ) โ Q) |
15 | 5 | adantr 276 |
. . . . . . . . 9
โข (((๐ด <Q
๐ต โง ๐ถ โ Q) โง ๐ โ Q) โ
๐ด โ
Q) |
16 | | mulclnq 7374 |
. . . . . . . . 9
โข
(((*Qโ๐ถ) โ Q โง ๐ด โ Q) โ
((*Qโ๐ถ) ยทQ ๐ด) โ
Q) |
17 | 14, 15, 16 | syl2anc 411 |
. . . . . . . 8
โข (((๐ด <Q
๐ต โง ๐ถ โ Q) โง ๐ โ Q) โ
((*Qโ๐ถ) ยทQ ๐ด) โ
Q) |
18 | | simpr 110 |
. . . . . . . 8
โข (((๐ด <Q
๐ต โง ๐ถ โ Q) โง ๐ โ Q) โ
๐ โ
Q) |
19 | | simplr 528 |
. . . . . . . 8
โข (((๐ด <Q
๐ต โง ๐ถ โ Q) โง ๐ โ Q) โ
๐ถ โ
Q) |
20 | | ltmnqg 7399 |
. . . . . . . 8
โข
((((*Qโ๐ถ) ยทQ ๐ด) โ Q โง
๐ โ Q
โง ๐ถ โ
Q) โ (((*Qโ๐ถ) ยทQ ๐ด) <Q
๐ โ (๐ถ ยทQ
((*Qโ๐ถ) ยทQ ๐ด))
<Q (๐ถ ยทQ ๐))) |
21 | 17, 18, 19, 20 | syl3anc 1238 |
. . . . . . 7
โข (((๐ด <Q
๐ต โง ๐ถ โ Q) โง ๐ โ Q) โ
(((*Qโ๐ถ) ยทQ ๐ด) <Q
๐ โ (๐ถ ยทQ
((*Qโ๐ถ) ยทQ ๐ด))
<Q (๐ถ ยทQ ๐))) |
22 | | recidnq 7391 |
. . . . . . . . . . 11
โข (๐ถ โ Q โ
(๐ถ
ยทQ (*Qโ๐ถ)) =
1Q) |
23 | 22 | oveq1d 5889 |
. . . . . . . . . 10
โข (๐ถ โ Q โ
((๐ถ
ยทQ (*Qโ๐ถ))
ยทQ ๐ด) = (1Q
ยทQ ๐ด)) |
24 | 23 | ad2antlr 489 |
. . . . . . . . 9
โข (((๐ด <Q
๐ต โง ๐ถ โ Q) โง ๐ โ Q) โ
((๐ถ
ยทQ (*Qโ๐ถ))
ยทQ ๐ด) = (1Q
ยทQ ๐ด)) |
25 | | mulassnqg 7382 |
. . . . . . . . . 10
โข ((๐ถ โ Q โง
(*Qโ๐ถ) โ Q โง ๐ด โ Q) โ
((๐ถ
ยทQ (*Qโ๐ถ))
ยทQ ๐ด) = (๐ถ ยทQ
((*Qโ๐ถ) ยทQ ๐ด))) |
26 | 19, 14, 15, 25 | syl3anc 1238 |
. . . . . . . . 9
โข (((๐ด <Q
๐ต โง ๐ถ โ Q) โง ๐ โ Q) โ
((๐ถ
ยทQ (*Qโ๐ถ))
ยทQ ๐ด) = (๐ถ ยทQ
((*Qโ๐ถ) ยทQ ๐ด))) |
27 | | 1nq 7364 |
. . . . . . . . . . . 12
โข
1Q โ Q |
28 | | mulcomnqg 7381 |
. . . . . . . . . . . 12
โข
((1Q โ Q โง ๐ด โ Q) โ
(1Q ยทQ ๐ด) = (๐ด ยทQ
1Q)) |
29 | 27, 28 | mpan 424 |
. . . . . . . . . . 11
โข (๐ด โ Q โ
(1Q ยทQ ๐ด) = (๐ด ยทQ
1Q)) |
30 | | mulidnq 7387 |
. . . . . . . . . . 11
โข (๐ด โ Q โ
(๐ด
ยทQ 1Q) = ๐ด) |
31 | 29, 30 | eqtrd 2210 |
. . . . . . . . . 10
โข (๐ด โ Q โ
(1Q ยทQ ๐ด) = ๐ด) |
32 | 15, 31 | syl 14 |
. . . . . . . . 9
โข (((๐ด <Q
๐ต โง ๐ถ โ Q) โง ๐ โ Q) โ
(1Q ยทQ ๐ด) = ๐ด) |
33 | 24, 26, 32 | 3eqtr3d 2218 |
. . . . . . . 8
โข (((๐ด <Q
๐ต โง ๐ถ โ Q) โง ๐ โ Q) โ
(๐ถ
ยทQ ((*Qโ๐ถ)
ยทQ ๐ด)) = ๐ด) |
34 | 33 | breq1d 4013 |
. . . . . . 7
โข (((๐ด <Q
๐ต โง ๐ถ โ Q) โง ๐ โ Q) โ
((๐ถ
ยทQ ((*Qโ๐ถ)
ยทQ ๐ด)) <Q (๐ถ
ยทQ ๐) โ ๐ด <Q (๐ถ
ยทQ ๐))) |
35 | 21, 34 | bitrd 188 |
. . . . . 6
โข (((๐ด <Q
๐ต โง ๐ถ โ Q) โง ๐ โ Q) โ
(((*Qโ๐ถ) ยทQ ๐ด) <Q
๐ โ ๐ด <Q (๐ถ
ยทQ ๐))) |
36 | 6 | adantr 276 |
. . . . . . . . 9
โข (((๐ด <Q
๐ต โง ๐ถ โ Q) โง ๐ โ Q) โ
๐ต โ
Q) |
37 | | mulclnq 7374 |
. . . . . . . . 9
โข
(((*Qโ๐ถ) โ Q โง ๐ต โ Q) โ
((*Qโ๐ถ) ยทQ ๐ต) โ
Q) |
38 | 14, 36, 37 | syl2anc 411 |
. . . . . . . 8
โข (((๐ด <Q
๐ต โง ๐ถ โ Q) โง ๐ โ Q) โ
((*Qโ๐ถ) ยทQ ๐ต) โ
Q) |
39 | | ltmnqg 7399 |
. . . . . . . 8
โข ((๐ โ Q โง
((*Qโ๐ถ) ยทQ ๐ต) โ Q โง
๐ถ โ Q)
โ (๐
<Q ((*Qโ๐ถ)
ยทQ ๐ต) โ (๐ถ ยทQ ๐) <Q
(๐ถ
ยทQ ((*Qโ๐ถ)
ยทQ ๐ต)))) |
40 | 18, 38, 19, 39 | syl3anc 1238 |
. . . . . . 7
โข (((๐ด <Q
๐ต โง ๐ถ โ Q) โง ๐ โ Q) โ
(๐
<Q ((*Qโ๐ถ)
ยทQ ๐ต) โ (๐ถ ยทQ ๐) <Q
(๐ถ
ยทQ ((*Qโ๐ถ)
ยทQ ๐ต)))) |
41 | 22 | oveq1d 5889 |
. . . . . . . . . 10
โข (๐ถ โ Q โ
((๐ถ
ยทQ (*Qโ๐ถ))
ยทQ ๐ต) = (1Q
ยทQ ๐ต)) |
42 | 41 | ad2antlr 489 |
. . . . . . . . 9
โข (((๐ด <Q
๐ต โง ๐ถ โ Q) โง ๐ โ Q) โ
((๐ถ
ยทQ (*Qโ๐ถ))
ยทQ ๐ต) = (1Q
ยทQ ๐ต)) |
43 | | mulassnqg 7382 |
. . . . . . . . . 10
โข ((๐ถ โ Q โง
(*Qโ๐ถ) โ Q โง ๐ต โ Q) โ
((๐ถ
ยทQ (*Qโ๐ถ))
ยทQ ๐ต) = (๐ถ ยทQ
((*Qโ๐ถ) ยทQ ๐ต))) |
44 | 19, 14, 36, 43 | syl3anc 1238 |
. . . . . . . . 9
โข (((๐ด <Q
๐ต โง ๐ถ โ Q) โง ๐ โ Q) โ
((๐ถ
ยทQ (*Qโ๐ถ))
ยทQ ๐ต) = (๐ถ ยทQ
((*Qโ๐ถ) ยทQ ๐ต))) |
45 | | mulcomnqg 7381 |
. . . . . . . . . . . 12
โข
((1Q โ Q โง ๐ต โ Q) โ
(1Q ยทQ ๐ต) = (๐ต ยทQ
1Q)) |
46 | 27, 45 | mpan 424 |
. . . . . . . . . . 11
โข (๐ต โ Q โ
(1Q ยทQ ๐ต) = (๐ต ยทQ
1Q)) |
47 | | mulidnq 7387 |
. . . . . . . . . . 11
โข (๐ต โ Q โ
(๐ต
ยทQ 1Q) = ๐ต) |
48 | 46, 47 | eqtrd 2210 |
. . . . . . . . . 10
โข (๐ต โ Q โ
(1Q ยทQ ๐ต) = ๐ต) |
49 | 36, 48 | syl 14 |
. . . . . . . . 9
โข (((๐ด <Q
๐ต โง ๐ถ โ Q) โง ๐ โ Q) โ
(1Q ยทQ ๐ต) = ๐ต) |
50 | 42, 44, 49 | 3eqtr3d 2218 |
. . . . . . . 8
โข (((๐ด <Q
๐ต โง ๐ถ โ Q) โง ๐ โ Q) โ
(๐ถ
ยทQ ((*Qโ๐ถ)
ยทQ ๐ต)) = ๐ต) |
51 | 50 | breq2d 4015 |
. . . . . . 7
โข (((๐ด <Q
๐ต โง ๐ถ โ Q) โง ๐ โ Q) โ
((๐ถ
ยทQ ๐) <Q (๐ถ
ยทQ ((*Qโ๐ถ)
ยทQ ๐ต)) โ (๐ถ ยทQ ๐) <Q
๐ต)) |
52 | 40, 51 | bitrd 188 |
. . . . . 6
โข (((๐ด <Q
๐ต โง ๐ถ โ Q) โง ๐ โ Q) โ
(๐
<Q ((*Qโ๐ถ)
ยทQ ๐ต) โ (๐ถ ยทQ ๐) <Q
๐ต)) |
53 | 35, 52 | anbi12d 473 |
. . . . 5
โข (((๐ด <Q
๐ต โง ๐ถ โ Q) โง ๐ โ Q) โ
((((*Qโ๐ถ) ยทQ ๐ด) <Q
๐ โง ๐ <Q
((*Qโ๐ถ) ยทQ ๐ต)) โ (๐ด <Q (๐ถ
ยทQ ๐) โง (๐ถ ยทQ ๐) <Q
๐ต))) |
54 | | mulcomnqg 7381 |
. . . . . . . 8
โข ((๐ถ โ Q โง
๐ โ Q)
โ (๐ถ
ยทQ ๐) = (๐ ยทQ ๐ถ)) |
55 | 19, 18, 54 | syl2anc 411 |
. . . . . . 7
โข (((๐ด <Q
๐ต โง ๐ถ โ Q) โง ๐ โ Q) โ
(๐ถ
ยทQ ๐) = (๐ ยทQ ๐ถ)) |
56 | 55 | breq2d 4015 |
. . . . . 6
โข (((๐ด <Q
๐ต โง ๐ถ โ Q) โง ๐ โ Q) โ
(๐ด
<Q (๐ถ ยทQ ๐) โ ๐ด <Q (๐
ยทQ ๐ถ))) |
57 | 55 | breq1d 4013 |
. . . . . 6
โข (((๐ด <Q
๐ต โง ๐ถ โ Q) โง ๐ โ Q) โ
((๐ถ
ยทQ ๐) <Q ๐ต โ (๐ ยทQ ๐ถ) <Q
๐ต)) |
58 | 56, 57 | anbi12d 473 |
. . . . 5
โข (((๐ด <Q
๐ต โง ๐ถ โ Q) โง ๐ โ Q) โ
((๐ด
<Q (๐ถ ยทQ ๐) โง (๐ถ ยทQ ๐) <Q
๐ต) โ (๐ด <Q
(๐
ยทQ ๐ถ) โง (๐ ยทQ ๐ถ) <Q
๐ต))) |
59 | 53, 58 | bitrd 188 |
. . . 4
โข (((๐ด <Q
๐ต โง ๐ถ โ Q) โง ๐ โ Q) โ
((((*Qโ๐ถ) ยทQ ๐ด) <Q
๐ โง ๐ <Q
((*Qโ๐ถ) ยทQ ๐ต)) โ (๐ด <Q (๐
ยทQ ๐ถ) โง (๐ ยทQ ๐ถ) <Q
๐ต))) |
60 | 59 | biimpd 144 |
. . 3
โข (((๐ด <Q
๐ต โง ๐ถ โ Q) โง ๐ โ Q) โ
((((*Qโ๐ถ) ยทQ ๐ด) <Q
๐ โง ๐ <Q
((*Qโ๐ถ) ยทQ ๐ต)) โ (๐ด <Q (๐
ยทQ ๐ถ) โง (๐ ยทQ ๐ถ) <Q
๐ต))) |
61 | 60 | reximdva 2579 |
. 2
โข ((๐ด <Q
๐ต โง ๐ถ โ Q) โ
(โ๐ โ
Q (((*Qโ๐ถ) ยทQ ๐ด) <Q
๐ โง ๐ <Q
((*Qโ๐ถ) ยทQ ๐ต)) โ โ๐ โ Q (๐ด <Q
(๐
ยทQ ๐ถ) โง (๐ ยทQ ๐ถ) <Q
๐ต))) |
62 | 13, 61 | mpd 13 |
1
โข ((๐ด <Q
๐ต โง ๐ถ โ Q) โ โ๐ โ Q (๐ด <Q
(๐
ยทQ ๐ถ) โง (๐ ยทQ ๐ถ) <Q
๐ต)) |