Step | Hyp | Ref
| Expression |
1 | | addclprlem1 11011 |
. . . . 5
โข (((๐ด โ P โง
๐ โ ๐ด) โง ๐ฅ โ Q) โ (๐ฅ <Q
(๐
+Q โ) โ ((๐ฅ ยทQ
(*Qโ(๐ +Q โ)))
ยทQ ๐) โ ๐ด)) |
2 | 1 | adantlr 714 |
. . . 4
โข ((((๐ด โ P โง
๐ โ ๐ด) โง (๐ต โ P โง โ โ ๐ต)) โง ๐ฅ โ Q) โ (๐ฅ <Q
(๐
+Q โ) โ ((๐ฅ ยทQ
(*Qโ(๐ +Q โ)))
ยทQ ๐) โ ๐ด)) |
3 | | addclprlem1 11011 |
. . . . . 6
โข (((๐ต โ P โง
โ โ ๐ต) โง ๐ฅ โ Q) โ (๐ฅ <Q
(โ
+Q ๐) โ ((๐ฅ ยทQ
(*Qโ(โ +Q ๐)))
ยทQ โ) โ ๐ต)) |
4 | | addcomnq 10946 |
. . . . . . 7
โข (๐ +Q
โ) = (โ +Q ๐) |
5 | 4 | breq2i 5157 |
. . . . . 6
โข (๐ฅ <Q
(๐
+Q โ) โ ๐ฅ <Q (โ +Q
๐)) |
6 | 4 | fveq2i 6895 |
. . . . . . . . 9
โข
(*Qโ(๐ +Q โ)) =
(*Qโ(โ +Q ๐)) |
7 | 6 | oveq2i 7420 |
. . . . . . . 8
โข (๐ฅ
ยทQ (*Qโ(๐ +Q
โ))) = (๐ฅ ยทQ
(*Qโ(โ +Q ๐))) |
8 | 7 | oveq1i 7419 |
. . . . . . 7
โข ((๐ฅ
ยทQ (*Qโ(๐ +Q
โ)))
ยทQ โ) = ((๐ฅ ยทQ
(*Qโ(โ +Q ๐)))
ยทQ โ) |
9 | 8 | eleq1i 2825 |
. . . . . 6
โข (((๐ฅ
ยทQ (*Qโ(๐ +Q
โ)))
ยทQ โ) โ ๐ต โ ((๐ฅ ยทQ
(*Qโ(โ +Q ๐)))
ยทQ โ) โ ๐ต) |
10 | 3, 5, 9 | 3imtr4g 296 |
. . . . 5
โข (((๐ต โ P โง
โ โ ๐ต) โง ๐ฅ โ Q) โ (๐ฅ <Q
(๐
+Q โ) โ ((๐ฅ ยทQ
(*Qโ(๐ +Q โ)))
ยทQ โ) โ ๐ต)) |
11 | 10 | adantll 713 |
. . . 4
โข ((((๐ด โ P โง
๐ โ ๐ด) โง (๐ต โ P โง โ โ ๐ต)) โง ๐ฅ โ Q) โ (๐ฅ <Q
(๐
+Q โ) โ ((๐ฅ ยทQ
(*Qโ(๐ +Q โ)))
ยทQ โ) โ ๐ต)) |
12 | 2, 11 | jcad 514 |
. . 3
โข ((((๐ด โ P โง
๐ โ ๐ด) โง (๐ต โ P โง โ โ ๐ต)) โง ๐ฅ โ Q) โ (๐ฅ <Q
(๐
+Q โ) โ (((๐ฅ ยทQ
(*Qโ(๐ +Q โ)))
ยทQ ๐) โ ๐ด โง ((๐ฅ ยทQ
(*Qโ(๐ +Q โ)))
ยทQ โ) โ ๐ต))) |
13 | | simpl 484 |
. . . 4
โข ((((๐ด โ P โง
๐ โ ๐ด) โง (๐ต โ P โง โ โ ๐ต)) โง ๐ฅ โ Q) โ ((๐ด โ P โง
๐ โ ๐ด) โง (๐ต โ P โง โ โ ๐ต))) |
14 | | simpl 484 |
. . . . 5
โข ((๐ด โ P โง
๐ โ ๐ด) โ ๐ด โ P) |
15 | | simpl 484 |
. . . . 5
โข ((๐ต โ P โง
โ โ ๐ต) โ ๐ต โ P) |
16 | 14, 15 | anim12i 614 |
. . . 4
โข (((๐ด โ P โง
๐ โ ๐ด) โง (๐ต โ P โง โ โ ๐ต)) โ (๐ด โ P โง ๐ต โ
P)) |
17 | | df-plp 10978 |
. . . . 5
โข
+P = (๐ค โ P, ๐ฃ โ P โฆ {๐ฅ โฃ โ๐ฆ โ ๐ค โ๐ง โ ๐ฃ ๐ฅ = (๐ฆ +Q ๐ง)}) |
18 | | addclnq 10940 |
. . . . 5
โข ((๐ฆ โ Q โง
๐ง โ Q)
โ (๐ฆ
+Q ๐ง) โ Q) |
19 | 17, 18 | genpprecl 10996 |
. . . 4
โข ((๐ด โ P โง
๐ต โ P)
โ ((((๐ฅ
ยทQ (*Qโ(๐ +Q
โ)))
ยทQ ๐) โ ๐ด โง ((๐ฅ ยทQ
(*Qโ(๐ +Q โ)))
ยทQ โ) โ ๐ต) โ (((๐ฅ ยทQ
(*Qโ(๐ +Q โ)))
ยทQ ๐) +Q ((๐ฅ
ยทQ (*Qโ(๐ +Q
โ)))
ยทQ โ)) โ (๐ด +P ๐ต))) |
20 | 13, 16, 19 | 3syl 18 |
. . 3
โข ((((๐ด โ P โง
๐ โ ๐ด) โง (๐ต โ P โง โ โ ๐ต)) โง ๐ฅ โ Q) โ ((((๐ฅ
ยทQ (*Qโ(๐ +Q
โ)))
ยทQ ๐) โ ๐ด โง ((๐ฅ ยทQ
(*Qโ(๐ +Q โ)))
ยทQ โ) โ ๐ต) โ (((๐ฅ ยทQ
(*Qโ(๐ +Q โ)))
ยทQ ๐) +Q ((๐ฅ
ยทQ (*Qโ(๐ +Q
โ)))
ยทQ โ)) โ (๐ด +P ๐ต))) |
21 | 12, 20 | syld 47 |
. 2
โข ((((๐ด โ P โง
๐ โ ๐ด) โง (๐ต โ P โง โ โ ๐ต)) โง ๐ฅ โ Q) โ (๐ฅ <Q
(๐
+Q โ) โ (((๐ฅ ยทQ
(*Qโ(๐ +Q โ)))
ยทQ ๐) +Q ((๐ฅ
ยทQ (*Qโ(๐ +Q
โ)))
ยทQ โ)) โ (๐ด +P ๐ต))) |
22 | | distrnq 10956 |
. . . . 5
โข ((๐ฅ
ยทQ (*Qโ(๐ +Q
โ)))
ยทQ (๐ +Q โ)) = (((๐ฅ ยทQ
(*Qโ(๐ +Q โ)))
ยทQ ๐) +Q ((๐ฅ
ยทQ (*Qโ(๐ +Q
โ)))
ยทQ โ)) |
23 | | mulassnq 10954 |
. . . . 5
โข ((๐ฅ
ยทQ (*Qโ(๐ +Q
โ)))
ยทQ (๐ +Q โ)) = (๐ฅ ยทQ
((*Qโ(๐ +Q โ))
ยทQ (๐ +Q โ))) |
24 | 22, 23 | eqtr3i 2763 |
. . . 4
โข (((๐ฅ
ยทQ (*Qโ(๐ +Q
โ)))
ยทQ ๐) +Q ((๐ฅ
ยทQ (*Qโ(๐ +Q
โ)))
ยทQ โ)) = (๐ฅ ยทQ
((*Qโ(๐ +Q โ))
ยทQ (๐ +Q โ))) |
25 | | mulcomnq 10948 |
. . . . . . 7
โข
((*Qโ(๐ +Q โ))
ยทQ (๐ +Q โ)) = ((๐ +Q โ)
ยทQ (*Qโ(๐ +Q
โ))) |
26 | | elprnq 10986 |
. . . . . . . . 9
โข ((๐ด โ P โง
๐ โ ๐ด) โ ๐ โ Q) |
27 | | elprnq 10986 |
. . . . . . . . 9
โข ((๐ต โ P โง
โ โ ๐ต) โ โ โ Q) |
28 | 26, 27 | anim12i 614 |
. . . . . . . 8
โข (((๐ด โ P โง
๐ โ ๐ด) โง (๐ต โ P โง โ โ ๐ต)) โ (๐ โ Q โง โ โ
Q)) |
29 | | addclnq 10940 |
. . . . . . . 8
โข ((๐ โ Q โง
โ โ Q)
โ (๐
+Q โ) โ Q) |
30 | | recidnq 10960 |
. . . . . . . 8
โข ((๐ +Q
โ) โ Q
โ ((๐
+Q โ) ยทQ
(*Qโ(๐ +Q โ))) =
1Q) |
31 | 28, 29, 30 | 3syl 18 |
. . . . . . 7
โข (((๐ด โ P โง
๐ โ ๐ด) โง (๐ต โ P โง โ โ ๐ต)) โ ((๐ +Q โ)
ยทQ (*Qโ(๐ +Q
โ))) =
1Q) |
32 | 25, 31 | eqtrid 2785 |
. . . . . 6
โข (((๐ด โ P โง
๐ โ ๐ด) โง (๐ต โ P โง โ โ ๐ต)) โ
((*Qโ(๐ +Q โ))
ยทQ (๐ +Q โ)) =
1Q) |
33 | 32 | oveq2d 7425 |
. . . . 5
โข (((๐ด โ P โง
๐ โ ๐ด) โง (๐ต โ P โง โ โ ๐ต)) โ (๐ฅ ยทQ
((*Qโ(๐ +Q โ))
ยทQ (๐ +Q โ))) = (๐ฅ ยทQ
1Q)) |
34 | | mulidnq 10958 |
. . . . 5
โข (๐ฅ โ Q โ
(๐ฅ
ยทQ 1Q) = ๐ฅ) |
35 | 33, 34 | sylan9eq 2793 |
. . . 4
โข ((((๐ด โ P โง
๐ โ ๐ด) โง (๐ต โ P โง โ โ ๐ต)) โง ๐ฅ โ Q) โ (๐ฅ
ยทQ ((*Qโ(๐ +Q
โ))
ยทQ (๐ +Q โ))) = ๐ฅ) |
36 | 24, 35 | eqtrid 2785 |
. . 3
โข ((((๐ด โ P โง
๐ โ ๐ด) โง (๐ต โ P โง โ โ ๐ต)) โง ๐ฅ โ Q) โ (((๐ฅ
ยทQ (*Qโ(๐ +Q
โ)))
ยทQ ๐) +Q ((๐ฅ
ยทQ (*Qโ(๐ +Q
โ)))
ยทQ โ)) = ๐ฅ) |
37 | 36 | eleq1d 2819 |
. 2
โข ((((๐ด โ P โง
๐ โ ๐ด) โง (๐ต โ P โง โ โ ๐ต)) โง ๐ฅ โ Q) โ ((((๐ฅ
ยทQ (*Qโ(๐ +Q
โ)))
ยทQ ๐) +Q ((๐ฅ
ยทQ (*Qโ(๐ +Q
โ)))
ยทQ โ)) โ (๐ด +P ๐ต) โ ๐ฅ โ (๐ด +P ๐ต))) |
38 | 21, 37 | sylibd 238 |
1
โข ((((๐ด โ P โง
๐ โ ๐ด) โง (๐ต โ P โง โ โ ๐ต)) โง ๐ฅ โ Q) โ (๐ฅ <Q
(๐
+Q โ) โ ๐ฅ โ (๐ด +P ๐ต))) |