Step | Hyp | Ref
| Expression |
1 | | recclnq 7390 |
. . . 4
โข (๐ด โ Q โ
(*Qโ๐ด) โ Q) |
2 | | recclnq 7390 |
. . . 4
โข (๐ต โ Q โ
(*Qโ๐ต) โ Q) |
3 | | mulclnq 7374 |
. . . 4
โข
(((*Qโ๐ด) โ Q โง
(*Qโ๐ต) โ Q) โ
((*Qโ๐ด) ยทQ
(*Qโ๐ต)) โ Q) |
4 | 1, 2, 3 | syl2an 289 |
. . 3
โข ((๐ด โ Q โง
๐ต โ Q)
โ ((*Qโ๐ด) ยทQ
(*Qโ๐ต)) โ Q) |
5 | | ltmnqg 7399 |
. . 3
โข ((๐ด โ Q โง
๐ต โ Q
โง ((*Qโ๐ด) ยทQ
(*Qโ๐ต)) โ Q) โ (๐ด <Q
๐ต โ
(((*Qโ๐ด) ยทQ
(*Qโ๐ต)) ยทQ ๐ด) <Q
(((*Qโ๐ด) ยทQ
(*Qโ๐ต)) ยทQ ๐ต))) |
6 | 4, 5 | mpd3an3 1338 |
. 2
โข ((๐ด โ Q โง
๐ต โ Q)
โ (๐ด
<Q ๐ต โ
(((*Qโ๐ด) ยทQ
(*Qโ๐ต)) ยทQ ๐ด) <Q
(((*Qโ๐ด) ยทQ
(*Qโ๐ต)) ยทQ ๐ต))) |
7 | | simpl 109 |
. . . . . 6
โข ((๐ด โ Q โง
๐ต โ Q)
โ ๐ด โ
Q) |
8 | | mulcomnqg 7381 |
. . . . . 6
โข
((((*Qโ๐ด) ยทQ
(*Qโ๐ต)) โ Q โง ๐ด โ Q) โ
(((*Qโ๐ด) ยทQ
(*Qโ๐ต)) ยทQ ๐ด) = (๐ด ยทQ
((*Qโ๐ด) ยทQ
(*Qโ๐ต)))) |
9 | 4, 7, 8 | syl2anc 411 |
. . . . 5
โข ((๐ด โ Q โง
๐ต โ Q)
โ (((*Qโ๐ด) ยทQ
(*Qโ๐ต)) ยทQ ๐ด) = (๐ด ยทQ
((*Qโ๐ด) ยทQ
(*Qโ๐ต)))) |
10 | 1 | adantr 276 |
. . . . . 6
โข ((๐ด โ Q โง
๐ต โ Q)
โ (*Qโ๐ด) โ Q) |
11 | 2 | adantl 277 |
. . . . . 6
โข ((๐ด โ Q โง
๐ต โ Q)
โ (*Qโ๐ต) โ Q) |
12 | | mulassnqg 7382 |
. . . . . 6
โข ((๐ด โ Q โง
(*Qโ๐ด) โ Q โง
(*Qโ๐ต) โ Q) โ ((๐ด
ยทQ (*Qโ๐ด))
ยทQ (*Qโ๐ต)) = (๐ด ยทQ
((*Qโ๐ด) ยทQ
(*Qโ๐ต)))) |
13 | 7, 10, 11, 12 | syl3anc 1238 |
. . . . 5
โข ((๐ด โ Q โง
๐ต โ Q)
โ ((๐ด
ยทQ (*Qโ๐ด))
ยทQ (*Qโ๐ต)) = (๐ด ยทQ
((*Qโ๐ด) ยทQ
(*Qโ๐ต)))) |
14 | | mulclnq 7374 |
. . . . . . 7
โข ((๐ด โ Q โง
(*Qโ๐ด) โ Q) โ (๐ด
ยทQ (*Qโ๐ด)) โ
Q) |
15 | 7, 10, 14 | syl2anc 411 |
. . . . . 6
โข ((๐ด โ Q โง
๐ต โ Q)
โ (๐ด
ยทQ (*Qโ๐ด)) โ
Q) |
16 | | mulcomnqg 7381 |
. . . . . 6
โข (((๐ด
ยทQ (*Qโ๐ด)) โ Q โง
(*Qโ๐ต) โ Q) โ ((๐ด
ยทQ (*Qโ๐ด))
ยทQ (*Qโ๐ต)) =
((*Qโ๐ต) ยทQ (๐ด
ยทQ (*Qโ๐ด)))) |
17 | 15, 11, 16 | syl2anc 411 |
. . . . 5
โข ((๐ด โ Q โง
๐ต โ Q)
โ ((๐ด
ยทQ (*Qโ๐ด))
ยทQ (*Qโ๐ต)) =
((*Qโ๐ต) ยทQ (๐ด
ยทQ (*Qโ๐ด)))) |
18 | 9, 13, 17 | 3eqtr2d 2216 |
. . . 4
โข ((๐ด โ Q โง
๐ต โ Q)
โ (((*Qโ๐ด) ยทQ
(*Qโ๐ต)) ยทQ ๐ด) =
((*Qโ๐ต) ยทQ (๐ด
ยทQ (*Qโ๐ด)))) |
19 | | recidnq 7391 |
. . . . . 6
โข (๐ด โ Q โ
(๐ด
ยทQ (*Qโ๐ด)) =
1Q) |
20 | 19 | oveq2d 5890 |
. . . . 5
โข (๐ด โ Q โ
((*Qโ๐ต) ยทQ (๐ด
ยทQ (*Qโ๐ด))) =
((*Qโ๐ต) ยทQ
1Q)) |
21 | | mulidnq 7387 |
. . . . . 6
โข
((*Qโ๐ต) โ Q โ
((*Qโ๐ต) ยทQ
1Q) = (*Qโ๐ต)) |
22 | 2, 21 | syl 14 |
. . . . 5
โข (๐ต โ Q โ
((*Qโ๐ต) ยทQ
1Q) = (*Qโ๐ต)) |
23 | 20, 22 | sylan9eq 2230 |
. . . 4
โข ((๐ด โ Q โง
๐ต โ Q)
โ ((*Qโ๐ต) ยทQ (๐ด
ยทQ (*Qโ๐ด))) =
(*Qโ๐ต)) |
24 | 18, 23 | eqtrd 2210 |
. . 3
โข ((๐ด โ Q โง
๐ต โ Q)
โ (((*Qโ๐ด) ยทQ
(*Qโ๐ต)) ยทQ ๐ด) =
(*Qโ๐ต)) |
25 | | simpr 110 |
. . . . 5
โข ((๐ด โ Q โง
๐ต โ Q)
โ ๐ต โ
Q) |
26 | | mulassnqg 7382 |
. . . . 5
โข
(((*Qโ๐ด) โ Q โง
(*Qโ๐ต) โ Q โง ๐ต โ Q) โ
(((*Qโ๐ด) ยทQ
(*Qโ๐ต)) ยทQ ๐ต) =
((*Qโ๐ด) ยทQ
((*Qโ๐ต) ยทQ ๐ต))) |
27 | 10, 11, 25, 26 | syl3anc 1238 |
. . . 4
โข ((๐ด โ Q โง
๐ต โ Q)
โ (((*Qโ๐ด) ยทQ
(*Qโ๐ต)) ยทQ ๐ต) =
((*Qโ๐ด) ยทQ
((*Qโ๐ต) ยทQ ๐ต))) |
28 | | mulcomnqg 7381 |
. . . . . 6
โข
(((*Qโ๐ต) โ Q โง ๐ต โ Q) โ
((*Qโ๐ต) ยทQ ๐ต) = (๐ต ยทQ
(*Qโ๐ต))) |
29 | 11, 25, 28 | syl2anc 411 |
. . . . 5
โข ((๐ด โ Q โง
๐ต โ Q)
โ ((*Qโ๐ต) ยทQ ๐ต) = (๐ต ยทQ
(*Qโ๐ต))) |
30 | 29 | oveq2d 5890 |
. . . 4
โข ((๐ด โ Q โง
๐ต โ Q)
โ ((*Qโ๐ด) ยทQ
((*Qโ๐ต) ยทQ ๐ต)) =
((*Qโ๐ด) ยทQ (๐ต
ยทQ (*Qโ๐ต)))) |
31 | | recidnq 7391 |
. . . . . 6
โข (๐ต โ Q โ
(๐ต
ยทQ (*Qโ๐ต)) =
1Q) |
32 | 31 | oveq2d 5890 |
. . . . 5
โข (๐ต โ Q โ
((*Qโ๐ด) ยทQ (๐ต
ยทQ (*Qโ๐ต))) =
((*Qโ๐ด) ยทQ
1Q)) |
33 | | mulidnq 7387 |
. . . . . 6
โข
((*Qโ๐ด) โ Q โ
((*Qโ๐ด) ยทQ
1Q) = (*Qโ๐ด)) |
34 | 1, 33 | syl 14 |
. . . . 5
โข (๐ด โ Q โ
((*Qโ๐ด) ยทQ
1Q) = (*Qโ๐ด)) |
35 | 32, 34 | sylan9eqr 2232 |
. . . 4
โข ((๐ด โ Q โง
๐ต โ Q)
โ ((*Qโ๐ด) ยทQ (๐ต
ยทQ (*Qโ๐ต))) =
(*Qโ๐ด)) |
36 | 27, 30, 35 | 3eqtrd 2214 |
. . 3
โข ((๐ด โ Q โง
๐ต โ Q)
โ (((*Qโ๐ด) ยทQ
(*Qโ๐ต)) ยทQ ๐ต) =
(*Qโ๐ด)) |
37 | 24, 36 | breq12d 4016 |
. 2
โข ((๐ด โ Q โง
๐ต โ Q)
โ ((((*Qโ๐ด) ยทQ
(*Qโ๐ต)) ยทQ ๐ด) <Q
(((*Qโ๐ด) ยทQ
(*Qโ๐ต)) ยทQ ๐ต) โ
(*Qโ๐ต) <Q
(*Qโ๐ด))) |
38 | 6, 37 | bitrd 188 |
1
โข ((๐ด โ Q โง
๐ต โ Q)
โ (๐ด
<Q ๐ต โ
(*Qโ๐ต) <Q
(*Qโ๐ด))) |