Step | Hyp | Ref
| Expression |
1 | | 1pru 7554 |
. . . 4
โข
(2nd โ1P) = {๐ค โฃ
1Q <Q ๐ค} |
2 | 1 | abeq2i 2288 |
. . 3
โข (๐ค โ (2nd
โ1P) โ 1Q
<Q ๐ค) |
3 | | prop 7473 |
. . . . . 6
โข (๐ด โ P โ
โจ(1st โ๐ด), (2nd โ๐ด)โฉ โ
P) |
4 | | prmuloc2 7565 |
. . . . . 6
โข
((โจ(1st โ๐ด), (2nd โ๐ด)โฉ โ P โง
1Q <Q ๐ค) โ โ๐ฃ โ (1st โ๐ด)(๐ฃ ยทQ ๐ค) โ (2nd
โ๐ด)) |
5 | 3, 4 | sylan 283 |
. . . . 5
โข ((๐ด โ P โง
1Q <Q ๐ค) โ โ๐ฃ โ (1st โ๐ด)(๐ฃ ยทQ ๐ค) โ (2nd
โ๐ด)) |
6 | | prnminu 7487 |
. . . . . . . 8
โข
((โจ(1st โ๐ด), (2nd โ๐ด)โฉ โ P โง (๐ฃ
ยทQ ๐ค) โ (2nd โ๐ด)) โ โ๐ง โ (2nd
โ๐ด)๐ง <Q (๐ฃ
ยทQ ๐ค)) |
7 | 3, 6 | sylan 283 |
. . . . . . 7
โข ((๐ด โ P โง
(๐ฃ
ยทQ ๐ค) โ (2nd โ๐ด)) โ โ๐ง โ (2nd
โ๐ด)๐ง <Q (๐ฃ
ยทQ ๐ค)) |
8 | 7 | ad2ant2rl 511 |
. . . . . 6
โข (((๐ด โ P โง
1Q <Q ๐ค) โง (๐ฃ โ (1st โ๐ด) โง (๐ฃ ยทQ ๐ค) โ (2nd
โ๐ด))) โ
โ๐ง โ
(2nd โ๐ด)๐ง <Q (๐ฃ
ยทQ ๐ค)) |
9 | | simp3 999 |
. . . . . . . . . . 11
โข (((๐ด โ P โง
1Q <Q ๐ค) โง (๐ฃ โ (1st โ๐ด) โง (๐ฃ ยทQ ๐ค) โ (2nd
โ๐ด)) โง ๐ง <Q
(๐ฃ
ยทQ ๐ค)) โ ๐ง <Q (๐ฃ
ยทQ ๐ค)) |
10 | | simp2l 1023 |
. . . . . . . . . . . 12
โข (((๐ด โ P โง
1Q <Q ๐ค) โง (๐ฃ โ (1st โ๐ด) โง (๐ฃ ยทQ ๐ค) โ (2nd
โ๐ด)) โง ๐ง <Q
(๐ฃ
ยทQ ๐ค)) โ ๐ฃ โ (1st โ๐ด)) |
11 | | elprnql 7479 |
. . . . . . . . . . . . . . . . . 18
โข
((โจ(1st โ๐ด), (2nd โ๐ด)โฉ โ P โง ๐ฃ โ (1st
โ๐ด)) โ ๐ฃ โ
Q) |
12 | 3, 11 | sylan 283 |
. . . . . . . . . . . . . . . . 17
โข ((๐ด โ P โง
๐ฃ โ (1st
โ๐ด)) โ ๐ฃ โ
Q) |
13 | 12 | ad2ant2r 509 |
. . . . . . . . . . . . . . . 16
โข (((๐ด โ P โง
1Q <Q ๐ค) โง (๐ฃ โ (1st โ๐ด) โง (๐ฃ ยทQ ๐ค) โ (2nd
โ๐ด))) โ ๐ฃ โ
Q) |
14 | 13 | 3adant3 1017 |
. . . . . . . . . . . . . . 15
โข (((๐ด โ P โง
1Q <Q ๐ค) โง (๐ฃ โ (1st โ๐ด) โง (๐ฃ ยทQ ๐ค) โ (2nd
โ๐ด)) โง ๐ง <Q
(๐ฃ
ยทQ ๐ค)) โ ๐ฃ โ Q) |
15 | | simp1r 1022 |
. . . . . . . . . . . . . . . 16
โข (((๐ด โ P โง
1Q <Q ๐ค) โง (๐ฃ โ (1st โ๐ด) โง (๐ฃ ยทQ ๐ค) โ (2nd
โ๐ด)) โง ๐ง <Q
(๐ฃ
ยทQ ๐ค)) โ 1Q
<Q ๐ค) |
16 | | ltrelnq 7363 |
. . . . . . . . . . . . . . . . . 18
โข
<Q โ (Q ร
Q) |
17 | 16 | brel 4678 |
. . . . . . . . . . . . . . . . 17
โข
(1Q <Q ๐ค โ
(1Q โ Q โง ๐ค โ Q)) |
18 | 17 | simprd 114 |
. . . . . . . . . . . . . . . 16
โข
(1Q <Q ๐ค โ ๐ค โ Q) |
19 | 15, 18 | syl 14 |
. . . . . . . . . . . . . . 15
โข (((๐ด โ P โง
1Q <Q ๐ค) โง (๐ฃ โ (1st โ๐ด) โง (๐ฃ ยทQ ๐ค) โ (2nd
โ๐ด)) โง ๐ง <Q
(๐ฃ
ยทQ ๐ค)) โ ๐ค โ Q) |
20 | | recclnq 7390 |
. . . . . . . . . . . . . . . 16
โข (๐ค โ Q โ
(*Qโ๐ค) โ Q) |
21 | 19, 20 | syl 14 |
. . . . . . . . . . . . . . 15
โข (((๐ด โ P โง
1Q <Q ๐ค) โง (๐ฃ โ (1st โ๐ด) โง (๐ฃ ยทQ ๐ค) โ (2nd
โ๐ด)) โง ๐ง <Q
(๐ฃ
ยทQ ๐ค)) โ
(*Qโ๐ค) โ Q) |
22 | | mulassnqg 7382 |
. . . . . . . . . . . . . . 15
โข ((๐ฃ โ Q โง
๐ค โ Q
โง (*Qโ๐ค) โ Q) โ ((๐ฃ
ยทQ ๐ค) ยทQ
(*Qโ๐ค)) = (๐ฃ ยทQ (๐ค
ยทQ (*Qโ๐ค)))) |
23 | 14, 19, 21, 22 | syl3anc 1238 |
. . . . . . . . . . . . . 14
โข (((๐ด โ P โง
1Q <Q ๐ค) โง (๐ฃ โ (1st โ๐ด) โง (๐ฃ ยทQ ๐ค) โ (2nd
โ๐ด)) โง ๐ง <Q
(๐ฃ
ยทQ ๐ค)) โ ((๐ฃ ยทQ ๐ค)
ยทQ (*Qโ๐ค)) = (๐ฃ ยทQ (๐ค
ยทQ (*Qโ๐ค)))) |
24 | | recidnq 7391 |
. . . . . . . . . . . . . . . 16
โข (๐ค โ Q โ
(๐ค
ยทQ (*Qโ๐ค)) =
1Q) |
25 | 19, 24 | syl 14 |
. . . . . . . . . . . . . . 15
โข (((๐ด โ P โง
1Q <Q ๐ค) โง (๐ฃ โ (1st โ๐ด) โง (๐ฃ ยทQ ๐ค) โ (2nd
โ๐ด)) โง ๐ง <Q
(๐ฃ
ยทQ ๐ค)) โ (๐ค ยทQ
(*Qโ๐ค)) =
1Q) |
26 | 25 | oveq2d 5890 |
. . . . . . . . . . . . . 14
โข (((๐ด โ P โง
1Q <Q ๐ค) โง (๐ฃ โ (1st โ๐ด) โง (๐ฃ ยทQ ๐ค) โ (2nd
โ๐ด)) โง ๐ง <Q
(๐ฃ
ยทQ ๐ค)) โ (๐ฃ ยทQ (๐ค
ยทQ (*Qโ๐ค))) = (๐ฃ ยทQ
1Q)) |
27 | | mulidnq 7387 |
. . . . . . . . . . . . . . 15
โข (๐ฃ โ Q โ
(๐ฃ
ยทQ 1Q) = ๐ฃ) |
28 | 14, 27 | syl 14 |
. . . . . . . . . . . . . 14
โข (((๐ด โ P โง
1Q <Q ๐ค) โง (๐ฃ โ (1st โ๐ด) โง (๐ฃ ยทQ ๐ค) โ (2nd
โ๐ด)) โง ๐ง <Q
(๐ฃ
ยทQ ๐ค)) โ (๐ฃ ยทQ
1Q) = ๐ฃ) |
29 | 23, 26, 28 | 3eqtrd 2214 |
. . . . . . . . . . . . 13
โข (((๐ด โ P โง
1Q <Q ๐ค) โง (๐ฃ โ (1st โ๐ด) โง (๐ฃ ยทQ ๐ค) โ (2nd
โ๐ด)) โง ๐ง <Q
(๐ฃ
ยทQ ๐ค)) โ ((๐ฃ ยทQ ๐ค)
ยทQ (*Qโ๐ค)) = ๐ฃ) |
30 | 29 | eleq1d 2246 |
. . . . . . . . . . . 12
โข (((๐ด โ P โง
1Q <Q ๐ค) โง (๐ฃ โ (1st โ๐ด) โง (๐ฃ ยทQ ๐ค) โ (2nd
โ๐ด)) โง ๐ง <Q
(๐ฃ
ยทQ ๐ค)) โ (((๐ฃ ยทQ ๐ค)
ยทQ (*Qโ๐ค)) โ (1st
โ๐ด) โ ๐ฃ โ (1st
โ๐ด))) |
31 | 10, 30 | mpbird 167 |
. . . . . . . . . . 11
โข (((๐ด โ P โง
1Q <Q ๐ค) โง (๐ฃ โ (1st โ๐ด) โง (๐ฃ ยทQ ๐ค) โ (2nd
โ๐ด)) โง ๐ง <Q
(๐ฃ
ยทQ ๐ค)) โ ((๐ฃ ยทQ ๐ค)
ยทQ (*Qโ๐ค)) โ (1st
โ๐ด)) |
32 | | ltrnqi 7419 |
. . . . . . . . . . . . 13
โข (๐ง <Q
(๐ฃ
ยทQ ๐ค) โ
(*Qโ(๐ฃ ยทQ ๐ค))
<Q (*Qโ๐ง)) |
33 | | ltmnqg 7399 |
. . . . . . . . . . . . . . 15
โข ((๐ โ Q โง
๐ โ Q
โง โ โ
Q) โ (๐
<Q ๐ โ (โ ยทQ ๐) <Q
(โ
ยทQ ๐))) |
34 | 33 | adantl 277 |
. . . . . . . . . . . . . 14
โข ((((๐ด โ P โง
1Q <Q ๐ค) โง (๐ฃ โ (1st โ๐ด) โง (๐ฃ ยทQ ๐ค) โ (2nd
โ๐ด)) โง ๐ง <Q
(๐ฃ
ยทQ ๐ค)) โง (๐ โ Q โง ๐ โ Q โง
โ โ Q))
โ (๐
<Q ๐ โ (โ ยทQ ๐) <Q
(โ
ยทQ ๐))) |
35 | | mulclnq 7374 |
. . . . . . . . . . . . . . . 16
โข ((๐ฃ โ Q โง
๐ค โ Q)
โ (๐ฃ
ยทQ ๐ค) โ Q) |
36 | 14, 19, 35 | syl2anc 411 |
. . . . . . . . . . . . . . 15
โข (((๐ด โ P โง
1Q <Q ๐ค) โง (๐ฃ โ (1st โ๐ด) โง (๐ฃ ยทQ ๐ค) โ (2nd
โ๐ด)) โง ๐ง <Q
(๐ฃ
ยทQ ๐ค)) โ (๐ฃ ยทQ ๐ค) โ
Q) |
37 | | recclnq 7390 |
. . . . . . . . . . . . . . 15
โข ((๐ฃ
ยทQ ๐ค) โ Q โ
(*Qโ(๐ฃ ยทQ ๐ค)) โ
Q) |
38 | 36, 37 | syl 14 |
. . . . . . . . . . . . . 14
โข (((๐ด โ P โง
1Q <Q ๐ค) โง (๐ฃ โ (1st โ๐ด) โง (๐ฃ ยทQ ๐ค) โ (2nd
โ๐ด)) โง ๐ง <Q
(๐ฃ
ยทQ ๐ค)) โ
(*Qโ(๐ฃ ยทQ ๐ค)) โ
Q) |
39 | 16 | brel 4678 |
. . . . . . . . . . . . . . . . 17
โข (๐ง <Q
(๐ฃ
ยทQ ๐ค) โ (๐ง โ Q โง (๐ฃ
ยทQ ๐ค) โ Q)) |
40 | 39 | simpld 112 |
. . . . . . . . . . . . . . . 16
โข (๐ง <Q
(๐ฃ
ยทQ ๐ค) โ ๐ง โ Q) |
41 | 9, 40 | syl 14 |
. . . . . . . . . . . . . . 15
โข (((๐ด โ P โง
1Q <Q ๐ค) โง (๐ฃ โ (1st โ๐ด) โง (๐ฃ ยทQ ๐ค) โ (2nd
โ๐ด)) โง ๐ง <Q
(๐ฃ
ยทQ ๐ค)) โ ๐ง โ Q) |
42 | | recclnq 7390 |
. . . . . . . . . . . . . . 15
โข (๐ง โ Q โ
(*Qโ๐ง) โ Q) |
43 | 41, 42 | syl 14 |
. . . . . . . . . . . . . 14
โข (((๐ด โ P โง
1Q <Q ๐ค) โง (๐ฃ โ (1st โ๐ด) โง (๐ฃ ยทQ ๐ค) โ (2nd
โ๐ด)) โง ๐ง <Q
(๐ฃ
ยทQ ๐ค)) โ
(*Qโ๐ง) โ Q) |
44 | | mulcomnqg 7381 |
. . . . . . . . . . . . . . 15
โข ((๐ โ Q โง
๐ โ Q)
โ (๐
ยทQ ๐) = (๐ ยทQ ๐)) |
45 | 44 | adantl 277 |
. . . . . . . . . . . . . 14
โข ((((๐ด โ P โง
1Q <Q ๐ค) โง (๐ฃ โ (1st โ๐ด) โง (๐ฃ ยทQ ๐ค) โ (2nd
โ๐ด)) โง ๐ง <Q
(๐ฃ
ยทQ ๐ค)) โง (๐ โ Q โง ๐ โ Q)) โ
(๐
ยทQ ๐) = (๐ ยทQ ๐)) |
46 | 34, 38, 43, 19, 45 | caovord2d 6043 |
. . . . . . . . . . . . 13
โข (((๐ด โ P โง
1Q <Q ๐ค) โง (๐ฃ โ (1st โ๐ด) โง (๐ฃ ยทQ ๐ค) โ (2nd
โ๐ด)) โง ๐ง <Q
(๐ฃ
ยทQ ๐ค)) โ
((*Qโ(๐ฃ ยทQ ๐ค))
<Q (*Qโ๐ง) โ
((*Qโ(๐ฃ ยทQ ๐ค))
ยทQ ๐ค) <Q
((*Qโ๐ง) ยทQ ๐ค))) |
47 | 32, 46 | imbitrid 154 |
. . . . . . . . . . . 12
โข (((๐ด โ P โง
1Q <Q ๐ค) โง (๐ฃ โ (1st โ๐ด) โง (๐ฃ ยทQ ๐ค) โ (2nd
โ๐ด)) โง ๐ง <Q
(๐ฃ
ยทQ ๐ค)) โ (๐ง <Q (๐ฃ
ยทQ ๐ค) โ
((*Qโ(๐ฃ ยทQ ๐ค))
ยทQ ๐ค) <Q
((*Qโ๐ง) ยทQ ๐ค))) |
48 | | mulcomnqg 7381 |
. . . . . . . . . . . . . . . . . . . . 21
โข (((๐ฃ
ยทQ ๐ค) โ Q โง
(*Qโ(๐ฃ ยทQ ๐ค)) โ Q)
โ ((๐ฃ
ยทQ ๐ค) ยทQ
(*Qโ(๐ฃ ยทQ ๐ค))) =
((*Qโ(๐ฃ ยทQ ๐ค))
ยทQ (๐ฃ ยทQ ๐ค))) |
49 | 37, 48 | mpdan 421 |
. . . . . . . . . . . . . . . . . . . 20
โข ((๐ฃ
ยทQ ๐ค) โ Q โ ((๐ฃ
ยทQ ๐ค) ยทQ
(*Qโ(๐ฃ ยทQ ๐ค))) =
((*Qโ(๐ฃ ยทQ ๐ค))
ยทQ (๐ฃ ยทQ ๐ค))) |
50 | | recidnq 7391 |
. . . . . . . . . . . . . . . . . . . 20
โข ((๐ฃ
ยทQ ๐ค) โ Q โ ((๐ฃ
ยทQ ๐ค) ยทQ
(*Qโ(๐ฃ ยทQ ๐ค))) =
1Q) |
51 | 49, 50 | eqtr3d 2212 |
. . . . . . . . . . . . . . . . . . 19
โข ((๐ฃ
ยทQ ๐ค) โ Q โ
((*Qโ(๐ฃ ยทQ ๐ค))
ยทQ (๐ฃ ยทQ ๐ค)) =
1Q) |
52 | 51, 24 | oveqan12d 5893 |
. . . . . . . . . . . . . . . . . 18
โข (((๐ฃ
ยทQ ๐ค) โ Q โง ๐ค โ Q) โ
(((*Qโ(๐ฃ ยทQ ๐ค))
ยทQ (๐ฃ ยทQ ๐ค))
ยทQ (๐ค ยทQ
(*Qโ๐ค))) = (1Q
ยทQ
1Q)) |
53 | 36, 19, 52 | syl2anc 411 |
. . . . . . . . . . . . . . . . 17
โข (((๐ด โ P โง
1Q <Q ๐ค) โง (๐ฃ โ (1st โ๐ด) โง (๐ฃ ยทQ ๐ค) โ (2nd
โ๐ด)) โง ๐ง <Q
(๐ฃ
ยทQ ๐ค)) โ
(((*Qโ(๐ฃ ยทQ ๐ค))
ยทQ (๐ฃ ยทQ ๐ค))
ยทQ (๐ค ยทQ
(*Qโ๐ค))) = (1Q
ยทQ
1Q)) |
54 | | mulassnqg 7382 |
. . . . . . . . . . . . . . . . . . 19
โข ((๐ โ Q โง
๐ โ Q
โง โ โ
Q) โ ((๐
ยทQ ๐) ยทQ โ) = (๐ ยทQ (๐
ยทQ โ))) |
55 | 54 | adantl 277 |
. . . . . . . . . . . . . . . . . 18
โข ((((๐ด โ P โง
1Q <Q ๐ค) โง (๐ฃ โ (1st โ๐ด) โง (๐ฃ ยทQ ๐ค) โ (2nd
โ๐ด)) โง ๐ง <Q
(๐ฃ
ยทQ ๐ค)) โง (๐ โ Q โง ๐ โ Q โง
โ โ Q))
โ ((๐
ยทQ ๐) ยทQ โ) = (๐ ยทQ (๐
ยทQ โ))) |
56 | | mulclnq 7374 |
. . . . . . . . . . . . . . . . . . 19
โข ((๐ โ Q โง
๐ โ Q)
โ (๐
ยทQ ๐) โ Q) |
57 | 56 | adantl 277 |
. . . . . . . . . . . . . . . . . 18
โข ((((๐ด โ P โง
1Q <Q ๐ค) โง (๐ฃ โ (1st โ๐ด) โง (๐ฃ ยทQ ๐ค) โ (2nd
โ๐ด)) โง ๐ง <Q
(๐ฃ
ยทQ ๐ค)) โง (๐ โ Q โง ๐ โ Q)) โ
(๐
ยทQ ๐) โ Q) |
58 | 38, 36, 19, 45, 55, 21, 57 | caov4d 6058 |
. . . . . . . . . . . . . . . . 17
โข (((๐ด โ P โง
1Q <Q ๐ค) โง (๐ฃ โ (1st โ๐ด) โง (๐ฃ ยทQ ๐ค) โ (2nd
โ๐ด)) โง ๐ง <Q
(๐ฃ
ยทQ ๐ค)) โ
(((*Qโ(๐ฃ ยทQ ๐ค))
ยทQ (๐ฃ ยทQ ๐ค))
ยทQ (๐ค ยทQ
(*Qโ๐ค))) =
(((*Qโ(๐ฃ ยทQ ๐ค))
ยทQ ๐ค) ยทQ ((๐ฃ
ยทQ ๐ค) ยทQ
(*Qโ๐ค)))) |
59 | 53, 58 | eqtr3d 2212 |
. . . . . . . . . . . . . . . 16
โข (((๐ด โ P โง
1Q <Q ๐ค) โง (๐ฃ โ (1st โ๐ด) โง (๐ฃ ยทQ ๐ค) โ (2nd
โ๐ด)) โง ๐ง <Q
(๐ฃ
ยทQ ๐ค)) โ (1Q
ยทQ 1Q) =
(((*Qโ(๐ฃ ยทQ ๐ค))
ยทQ ๐ค) ยทQ ((๐ฃ
ยทQ ๐ค) ยทQ
(*Qโ๐ค)))) |
60 | | 1nq 7364 |
. . . . . . . . . . . . . . . . 17
โข
1Q โ Q |
61 | | mulidnq 7387 |
. . . . . . . . . . . . . . . . 17
โข
(1Q โ Q โ
(1Q ยทQ
1Q) = 1Q) |
62 | 60, 61 | ax-mp 5 |
. . . . . . . . . . . . . . . 16
โข
(1Q ยทQ
1Q) = 1Q |
63 | 59, 62 | eqtr3di 2225 |
. . . . . . . . . . . . . . 15
โข (((๐ด โ P โง
1Q <Q ๐ค) โง (๐ฃ โ (1st โ๐ด) โง (๐ฃ ยทQ ๐ค) โ (2nd
โ๐ด)) โง ๐ง <Q
(๐ฃ
ยทQ ๐ค)) โ
(((*Qโ(๐ฃ ยทQ ๐ค))
ยทQ ๐ค) ยทQ ((๐ฃ
ยทQ ๐ค) ยทQ
(*Qโ๐ค))) =
1Q) |
64 | 57, 38, 19 | caovcld 6027 |
. . . . . . . . . . . . . . . 16
โข (((๐ด โ P โง
1Q <Q ๐ค) โง (๐ฃ โ (1st โ๐ด) โง (๐ฃ ยทQ ๐ค) โ (2nd
โ๐ด)) โง ๐ง <Q
(๐ฃ
ยทQ ๐ค)) โ
((*Qโ(๐ฃ ยทQ ๐ค))
ยทQ ๐ค) โ Q) |
65 | 57, 36, 21 | caovcld 6027 |
. . . . . . . . . . . . . . . 16
โข (((๐ด โ P โง
1Q <Q ๐ค) โง (๐ฃ โ (1st โ๐ด) โง (๐ฃ ยทQ ๐ค) โ (2nd
โ๐ด)) โง ๐ง <Q
(๐ฃ
ยทQ ๐ค)) โ ((๐ฃ ยทQ ๐ค)
ยทQ (*Qโ๐ค)) โ
Q) |
66 | | recmulnqg 7389 |
. . . . . . . . . . . . . . . 16
โข
((((*Qโ(๐ฃ ยทQ ๐ค))
ยทQ ๐ค) โ Q โง ((๐ฃ
ยทQ ๐ค) ยทQ
(*Qโ๐ค)) โ Q) โ
((*Qโ((*Qโ(๐ฃ
ยทQ ๐ค)) ยทQ ๐ค)) = ((๐ฃ ยทQ ๐ค)
ยทQ (*Qโ๐ค)) โ
(((*Qโ(๐ฃ ยทQ ๐ค))
ยทQ ๐ค) ยทQ ((๐ฃ
ยทQ ๐ค) ยทQ
(*Qโ๐ค))) =
1Q)) |
67 | 64, 65, 66 | syl2anc 411 |
. . . . . . . . . . . . . . 15
โข (((๐ด โ P โง
1Q <Q ๐ค) โง (๐ฃ โ (1st โ๐ด) โง (๐ฃ ยทQ ๐ค) โ (2nd
โ๐ด)) โง ๐ง <Q
(๐ฃ
ยทQ ๐ค)) โ
((*Qโ((*Qโ(๐ฃ
ยทQ ๐ค)) ยทQ ๐ค)) = ((๐ฃ ยทQ ๐ค)
ยทQ (*Qโ๐ค)) โ
(((*Qโ(๐ฃ ยทQ ๐ค))
ยทQ ๐ค) ยทQ ((๐ฃ
ยทQ ๐ค) ยทQ
(*Qโ๐ค))) =
1Q)) |
68 | 63, 67 | mpbird 167 |
. . . . . . . . . . . . . 14
โข (((๐ด โ P โง
1Q <Q ๐ค) โง (๐ฃ โ (1st โ๐ด) โง (๐ฃ ยทQ ๐ค) โ (2nd
โ๐ด)) โง ๐ง <Q
(๐ฃ
ยทQ ๐ค)) โ
(*Qโ((*Qโ(๐ฃ
ยทQ ๐ค)) ยทQ ๐ค)) = ((๐ฃ ยทQ ๐ค)
ยทQ (*Qโ๐ค))) |
69 | 68 | eleq1d 2246 |
. . . . . . . . . . . . 13
โข (((๐ด โ P โง
1Q <Q ๐ค) โง (๐ฃ โ (1st โ๐ด) โง (๐ฃ ยทQ ๐ค) โ (2nd
โ๐ด)) โง ๐ง <Q
(๐ฃ
ยทQ ๐ค)) โ
((*Qโ((*Qโ(๐ฃ
ยทQ ๐ค)) ยทQ ๐ค)) โ (1st
โ๐ด) โ ((๐ฃ
ยทQ ๐ค) ยทQ
(*Qโ๐ค)) โ (1st โ๐ด))) |
70 | 69 | biimprd 158 |
. . . . . . . . . . . 12
โข (((๐ด โ P โง
1Q <Q ๐ค) โง (๐ฃ โ (1st โ๐ด) โง (๐ฃ ยทQ ๐ค) โ (2nd
โ๐ด)) โง ๐ง <Q
(๐ฃ
ยทQ ๐ค)) โ (((๐ฃ ยทQ ๐ค)
ยทQ (*Qโ๐ค)) โ (1st
โ๐ด) โ
(*Qโ((*Qโ(๐ฃ
ยทQ ๐ค)) ยทQ ๐ค)) โ (1st
โ๐ด))) |
71 | | breq1 4006 |
. . . . . . . . . . . . . . . 16
โข (๐ฆ =
((*Qโ(๐ฃ ยทQ ๐ค))
ยทQ ๐ค) โ (๐ฆ <Q
((*Qโ๐ง) ยทQ ๐ค) โ
((*Qโ(๐ฃ ยทQ ๐ค))
ยทQ ๐ค) <Q
((*Qโ๐ง) ยทQ ๐ค))) |
72 | | fveq2 5515 |
. . . . . . . . . . . . . . . . 17
โข (๐ฆ =
((*Qโ(๐ฃ ยทQ ๐ค))
ยทQ ๐ค) โ
(*Qโ๐ฆ) =
(*Qโ((*Qโ(๐ฃ
ยทQ ๐ค)) ยทQ ๐ค))) |
73 | 72 | eleq1d 2246 |
. . . . . . . . . . . . . . . 16
โข (๐ฆ =
((*Qโ(๐ฃ ยทQ ๐ค))
ยทQ ๐ค) โ
((*Qโ๐ฆ) โ (1st โ๐ด) โ
(*Qโ((*Qโ(๐ฃ
ยทQ ๐ค)) ยทQ ๐ค)) โ (1st
โ๐ด))) |
74 | 71, 73 | anbi12d 473 |
. . . . . . . . . . . . . . 15
โข (๐ฆ =
((*Qโ(๐ฃ ยทQ ๐ค))
ยทQ ๐ค) โ ((๐ฆ <Q
((*Qโ๐ง) ยทQ ๐ค) โง
(*Qโ๐ฆ) โ (1st โ๐ด)) โ
(((*Qโ(๐ฃ ยทQ ๐ค))
ยทQ ๐ค) <Q
((*Qโ๐ง) ยทQ ๐ค) โง
(*Qโ((*Qโ(๐ฃ
ยทQ ๐ค)) ยทQ ๐ค)) โ (1st
โ๐ด)))) |
75 | 74 | spcegv 2825 |
. . . . . . . . . . . . . 14
โข
(((*Qโ(๐ฃ ยทQ ๐ค))
ยทQ ๐ค) โ Q โ
((((*Qโ(๐ฃ ยทQ ๐ค))
ยทQ ๐ค) <Q
((*Qโ๐ง) ยทQ ๐ค) โง
(*Qโ((*Qโ(๐ฃ
ยทQ ๐ค)) ยทQ ๐ค)) โ (1st
โ๐ด)) โ
โ๐ฆ(๐ฆ <Q
((*Qโ๐ง) ยทQ ๐ค) โง
(*Qโ๐ฆ) โ (1st โ๐ด)))) |
76 | 64, 75 | syl 14 |
. . . . . . . . . . . . 13
โข (((๐ด โ P โง
1Q <Q ๐ค) โง (๐ฃ โ (1st โ๐ด) โง (๐ฃ ยทQ ๐ค) โ (2nd
โ๐ด)) โง ๐ง <Q
(๐ฃ
ยทQ ๐ค)) โ
((((*Qโ(๐ฃ ยทQ ๐ค))
ยทQ ๐ค) <Q
((*Qโ๐ง) ยทQ ๐ค) โง
(*Qโ((*Qโ(๐ฃ
ยทQ ๐ค)) ยทQ ๐ค)) โ (1st
โ๐ด)) โ
โ๐ฆ(๐ฆ <Q
((*Qโ๐ง) ยทQ ๐ค) โง
(*Qโ๐ฆ) โ (1st โ๐ด)))) |
77 | | recexpr.1 |
. . . . . . . . . . . . . 14
โข ๐ต = โจ{๐ฅ โฃ โ๐ฆ(๐ฅ <Q ๐ฆ โง
(*Qโ๐ฆ) โ (2nd โ๐ด))}, {๐ฅ โฃ โ๐ฆ(๐ฆ <Q ๐ฅ โง
(*Qโ๐ฆ) โ (1st โ๐ด))}โฉ |
78 | 77 | recexprlemelu 7621 |
. . . . . . . . . . . . 13
โข
(((*Qโ๐ง) ยทQ ๐ค) โ (2nd
โ๐ต) โ
โ๐ฆ(๐ฆ <Q
((*Qโ๐ง) ยทQ ๐ค) โง
(*Qโ๐ฆ) โ (1st โ๐ด))) |
79 | 76, 78 | imbitrrdi 162 |
. . . . . . . . . . . 12
โข (((๐ด โ P โง
1Q <Q ๐ค) โง (๐ฃ โ (1st โ๐ด) โง (๐ฃ ยทQ ๐ค) โ (2nd
โ๐ด)) โง ๐ง <Q
(๐ฃ
ยทQ ๐ค)) โ
((((*Qโ(๐ฃ ยทQ ๐ค))
ยทQ ๐ค) <Q
((*Qโ๐ง) ยทQ ๐ค) โง
(*Qโ((*Qโ(๐ฃ
ยทQ ๐ค)) ยทQ ๐ค)) โ (1st
โ๐ด)) โ
((*Qโ๐ง) ยทQ ๐ค) โ (2nd
โ๐ต))) |
80 | 47, 70, 79 | syl2and 295 |
. . . . . . . . . . 11
โข (((๐ด โ P โง
1Q <Q ๐ค) โง (๐ฃ โ (1st โ๐ด) โง (๐ฃ ยทQ ๐ค) โ (2nd
โ๐ด)) โง ๐ง <Q
(๐ฃ
ยทQ ๐ค)) โ ((๐ง <Q (๐ฃ
ยทQ ๐ค) โง ((๐ฃ ยทQ ๐ค)
ยทQ (*Qโ๐ค)) โ (1st
โ๐ด)) โ
((*Qโ๐ง) ยทQ ๐ค) โ (2nd
โ๐ต))) |
81 | 9, 31, 80 | mp2and 433 |
. . . . . . . . . 10
โข (((๐ด โ P โง
1Q <Q ๐ค) โง (๐ฃ โ (1st โ๐ด) โง (๐ฃ ยทQ ๐ค) โ (2nd
โ๐ด)) โง ๐ง <Q
(๐ฃ
ยทQ ๐ค)) โ
((*Qโ๐ง) ยทQ ๐ค) โ (2nd
โ๐ต)) |
82 | | mulidnq 7387 |
. . . . . . . . . . . . . 14
โข (๐ค โ Q โ
(๐ค
ยทQ 1Q) = ๐ค) |
83 | | mulcomnqg 7381 |
. . . . . . . . . . . . . . 15
โข ((๐ค โ Q โง
1Q โ Q) โ (๐ค ยทQ
1Q) = (1Q
ยทQ ๐ค)) |
84 | 60, 83 | mpan2 425 |
. . . . . . . . . . . . . 14
โข (๐ค โ Q โ
(๐ค
ยทQ 1Q) =
(1Q ยทQ ๐ค)) |
85 | 82, 84 | eqtr3d 2212 |
. . . . . . . . . . . . 13
โข (๐ค โ Q โ
๐ค =
(1Q ยทQ ๐ค)) |
86 | 85 | adantl 277 |
. . . . . . . . . . . 12
โข ((๐ง โ Q โง
๐ค โ Q)
โ ๐ค =
(1Q ยทQ ๐ค)) |
87 | | recidnq 7391 |
. . . . . . . . . . . . . 14
โข (๐ง โ Q โ
(๐ง
ยทQ (*Qโ๐ง)) =
1Q) |
88 | 87 | oveq1d 5889 |
. . . . . . . . . . . . 13
โข (๐ง โ Q โ
((๐ง
ยทQ (*Qโ๐ง))
ยทQ ๐ค) = (1Q
ยทQ ๐ค)) |
89 | 88 | adantr 276 |
. . . . . . . . . . . 12
โข ((๐ง โ Q โง
๐ค โ Q)
โ ((๐ง
ยทQ (*Qโ๐ง))
ยทQ ๐ค) = (1Q
ยทQ ๐ค)) |
90 | | mulassnqg 7382 |
. . . . . . . . . . . . . 14
โข ((๐ง โ Q โง
(*Qโ๐ง) โ Q โง ๐ค โ Q) โ
((๐ง
ยทQ (*Qโ๐ง))
ยทQ ๐ค) = (๐ง ยทQ
((*Qโ๐ง) ยทQ ๐ค))) |
91 | 42, 90 | syl3an2 1272 |
. . . . . . . . . . . . 13
โข ((๐ง โ Q โง
๐ง โ Q
โง ๐ค โ
Q) โ ((๐ง
ยทQ (*Qโ๐ง))
ยทQ ๐ค) = (๐ง ยทQ
((*Qโ๐ง) ยทQ ๐ค))) |
92 | 91 | 3anidm12 1295 |
. . . . . . . . . . . 12
โข ((๐ง โ Q โง
๐ค โ Q)
โ ((๐ง
ยทQ (*Qโ๐ง))
ยทQ ๐ค) = (๐ง ยทQ
((*Qโ๐ง) ยทQ ๐ค))) |
93 | 86, 89, 92 | 3eqtr2d 2216 |
. . . . . . . . . . 11
โข ((๐ง โ Q โง
๐ค โ Q)
โ ๐ค = (๐ง
ยทQ ((*Qโ๐ง)
ยทQ ๐ค))) |
94 | 41, 19, 93 | syl2anc 411 |
. . . . . . . . . 10
โข (((๐ด โ P โง
1Q <Q ๐ค) โง (๐ฃ โ (1st โ๐ด) โง (๐ฃ ยทQ ๐ค) โ (2nd
โ๐ด)) โง ๐ง <Q
(๐ฃ
ยทQ ๐ค)) โ ๐ค = (๐ง ยทQ
((*Qโ๐ง) ยทQ ๐ค))) |
95 | | oveq2 5882 |
. . . . . . . . . . . 12
โข (๐ฅ =
((*Qโ๐ง) ยทQ ๐ค) โ (๐ง ยทQ ๐ฅ) = (๐ง ยทQ
((*Qโ๐ง) ยทQ ๐ค))) |
96 | 95 | eqeq2d 2189 |
. . . . . . . . . . 11
โข (๐ฅ =
((*Qโ๐ง) ยทQ ๐ค) โ (๐ค = (๐ง ยทQ ๐ฅ) โ ๐ค = (๐ง ยทQ
((*Qโ๐ง) ยทQ ๐ค)))) |
97 | 96 | rspcev 2841 |
. . . . . . . . . 10
โข
((((*Qโ๐ง) ยทQ ๐ค) โ (2nd
โ๐ต) โง ๐ค = (๐ง ยทQ
((*Qโ๐ง) ยทQ ๐ค))) โ โ๐ฅ โ (2nd
โ๐ต)๐ค = (๐ง ยทQ ๐ฅ)) |
98 | 81, 94, 97 | syl2anc 411 |
. . . . . . . . 9
โข (((๐ด โ P โง
1Q <Q ๐ค) โง (๐ฃ โ (1st โ๐ด) โง (๐ฃ ยทQ ๐ค) โ (2nd
โ๐ด)) โง ๐ง <Q
(๐ฃ
ยทQ ๐ค)) โ โ๐ฅ โ (2nd โ๐ต)๐ค = (๐ง ยทQ ๐ฅ)) |
99 | 98 | 3expia 1205 |
. . . . . . . 8
โข (((๐ด โ P โง
1Q <Q ๐ค) โง (๐ฃ โ (1st โ๐ด) โง (๐ฃ ยทQ ๐ค) โ (2nd
โ๐ด))) โ (๐ง <Q
(๐ฃ
ยทQ ๐ค) โ โ๐ฅ โ (2nd โ๐ต)๐ค = (๐ง ยทQ ๐ฅ))) |
100 | 99 | reximdv 2578 |
. . . . . . 7
โข (((๐ด โ P โง
1Q <Q ๐ค) โง (๐ฃ โ (1st โ๐ด) โง (๐ฃ ยทQ ๐ค) โ (2nd
โ๐ด))) โ
(โ๐ง โ
(2nd โ๐ด)๐ง <Q (๐ฃ
ยทQ ๐ค) โ โ๐ง โ (2nd โ๐ด)โ๐ฅ โ (2nd โ๐ต)๐ค = (๐ง ยทQ ๐ฅ))) |
101 | 77 | recexprlempr 7630 |
. . . . . . . . 9
โข (๐ด โ P โ
๐ต โ
P) |
102 | | df-imp 7467 |
. . . . . . . . . 10
โข
ยทP = (๐ฆ โ P, ๐ค โ P โฆ โจ{๐ข โ Q โฃ
โ๐ โ
Q โ๐
โ Q (๐
โ (1st โ๐ฆ) โง ๐ โ (1st โ๐ค) โง ๐ข = (๐ ยทQ ๐))}, {๐ข โ Q โฃ โ๐ โ Q
โ๐ โ
Q (๐ โ
(2nd โ๐ฆ)
โง ๐ โ
(2nd โ๐ค)
โง ๐ข = (๐
ยทQ ๐))}โฉ) |
103 | 102, 56 | genpelvu 7511 |
. . . . . . . . 9
โข ((๐ด โ P โง
๐ต โ P)
โ (๐ค โ
(2nd โ(๐ด
ยทP ๐ต)) โ โ๐ง โ (2nd โ๐ด)โ๐ฅ โ (2nd โ๐ต)๐ค = (๐ง ยทQ ๐ฅ))) |
104 | 101, 103 | mpdan 421 |
. . . . . . . 8
โข (๐ด โ P โ
(๐ค โ (2nd
โ(๐ด
ยทP ๐ต)) โ โ๐ง โ (2nd โ๐ด)โ๐ฅ โ (2nd โ๐ต)๐ค = (๐ง ยทQ ๐ฅ))) |
105 | 104 | ad2antrr 488 |
. . . . . . 7
โข (((๐ด โ P โง
1Q <Q ๐ค) โง (๐ฃ โ (1st โ๐ด) โง (๐ฃ ยทQ ๐ค) โ (2nd
โ๐ด))) โ (๐ค โ (2nd
โ(๐ด
ยทP ๐ต)) โ โ๐ง โ (2nd โ๐ด)โ๐ฅ โ (2nd โ๐ต)๐ค = (๐ง ยทQ ๐ฅ))) |
106 | 100, 105 | sylibrd 169 |
. . . . . 6
โข (((๐ด โ P โง
1Q <Q ๐ค) โง (๐ฃ โ (1st โ๐ด) โง (๐ฃ ยทQ ๐ค) โ (2nd
โ๐ด))) โ
(โ๐ง โ
(2nd โ๐ด)๐ง <Q (๐ฃ
ยทQ ๐ค) โ ๐ค โ (2nd โ(๐ด
ยทP ๐ต)))) |
107 | 8, 106 | mpd 13 |
. . . . 5
โข (((๐ด โ P โง
1Q <Q ๐ค) โง (๐ฃ โ (1st โ๐ด) โง (๐ฃ ยทQ ๐ค) โ (2nd
โ๐ด))) โ ๐ค โ (2nd
โ(๐ด
ยทP ๐ต))) |
108 | 5, 107 | rexlimddv 2599 |
. . . 4
โข ((๐ด โ P โง
1Q <Q ๐ค) โ ๐ค โ (2nd โ(๐ด
ยทP ๐ต))) |
109 | 108 | ex 115 |
. . 3
โข (๐ด โ P โ
(1Q <Q ๐ค โ ๐ค โ (2nd โ(๐ด
ยทP ๐ต)))) |
110 | 2, 109 | biimtrid 152 |
. 2
โข (๐ด โ P โ
(๐ค โ (2nd
โ1P) โ ๐ค โ (2nd โ(๐ด
ยทP ๐ต)))) |
111 | 110 | ssrdv 3161 |
1
โข (๐ด โ P โ
(2nd โ1P) โ (2nd
โ(๐ด
ยทP ๐ต))) |