Step | Hyp | Ref
| Expression |
1 | | ltrelsr 11060 |
. . . . 5
โข
<R โ (R ร
R) |
2 | 1 | brel 5740 |
. . . 4
โข ((๐ถ +R
-1R) <R ๐ด โ ((๐ถ +R
-1R) โ R โง ๐ด โ R)) |
3 | 2 | simprd 497 |
. . 3
โข ((๐ถ +R
-1R) <R ๐ด โ ๐ด โ R) |
4 | | map2psrpr.2 |
. . . . . 6
โข ๐ถ โ
R |
5 | | ltasr 11092 |
. . . . . 6
โข (๐ถ โ R โ
(-1R <R ((๐ถ
ยทR -1R)
+R ๐ด) โ (๐ถ +R
-1R) <R (๐ถ +R ((๐ถ
ยทR -1R)
+R ๐ด)))) |
6 | 4, 5 | ax-mp 5 |
. . . . 5
โข
(-1R <R ((๐ถ
ยทR -1R)
+R ๐ด) โ (๐ถ +R
-1R) <R (๐ถ +R ((๐ถ
ยทR -1R)
+R ๐ด))) |
7 | | pn0sr 11093 |
. . . . . . . . . 10
โข (๐ถ โ R โ
(๐ถ
+R (๐ถ ยทR
-1R)) = 0R) |
8 | 4, 7 | ax-mp 5 |
. . . . . . . . 9
โข (๐ถ +R
(๐ถ
ยทR -1R)) =
0R |
9 | 8 | oveq1i 7416 |
. . . . . . . 8
โข ((๐ถ +R
(๐ถ
ยทR -1R))
+R ๐ด) = (0R
+R ๐ด) |
10 | | addasssr 11080 |
. . . . . . . 8
โข ((๐ถ +R
(๐ถ
ยทR -1R))
+R ๐ด) = (๐ถ +R ((๐ถ
ยทR -1R)
+R ๐ด)) |
11 | | addcomsr 11079 |
. . . . . . . 8
โข
(0R +R ๐ด) = (๐ด +R
0R) |
12 | 9, 10, 11 | 3eqtr3i 2769 |
. . . . . . 7
โข (๐ถ +R
((๐ถ
ยทR -1R)
+R ๐ด)) = (๐ด +R
0R) |
13 | | 0idsr 11089 |
. . . . . . 7
โข (๐ด โ R โ
(๐ด
+R 0R) = ๐ด) |
14 | 12, 13 | eqtrid 2785 |
. . . . . 6
โข (๐ด โ R โ
(๐ถ
+R ((๐ถ ยทR
-1R) +R ๐ด)) = ๐ด) |
15 | 14 | breq2d 5160 |
. . . . 5
โข (๐ด โ R โ
((๐ถ
+R -1R)
<R (๐ถ +R ((๐ถ
ยทR -1R)
+R ๐ด)) โ (๐ถ +R
-1R) <R ๐ด)) |
16 | 6, 15 | bitrid 283 |
. . . 4
โข (๐ด โ R โ
(-1R <R ((๐ถ
ยทR -1R)
+R ๐ด) โ (๐ถ +R
-1R) <R ๐ด)) |
17 | | m1r 11074 |
. . . . . . . 8
โข
-1R โ R |
18 | | mulclsr 11076 |
. . . . . . . 8
โข ((๐ถ โ R โง
-1R โ R) โ (๐ถ ยทR
-1R) โ R) |
19 | 4, 17, 18 | mp2an 691 |
. . . . . . 7
โข (๐ถ
ยทR -1R) โ
R |
20 | | addclsr 11075 |
. . . . . . 7
โข (((๐ถ
ยทR -1R) โ
R โง ๐ด
โ R) โ ((๐ถ ยทR
-1R) +R ๐ด) โ R) |
21 | 19, 20 | mpan 689 |
. . . . . 6
โข (๐ด โ R โ
((๐ถ
ยทR -1R)
+R ๐ด) โ R) |
22 | | df-nr 11048 |
. . . . . . 7
โข
R = ((P ร P) /
~R ) |
23 | | breq2 5152 |
. . . . . . . 8
โข
([โจ๐ฆ, ๐งโฉ]
~R = ((๐ถ ยทR
-1R) +R ๐ด) โ (-1R
<R [โจ๐ฆ, ๐งโฉ] ~R โ
-1R <R ((๐ถ ยทR
-1R) +R ๐ด))) |
24 | | eqeq2 2745 |
. . . . . . . . 9
โข
([โจ๐ฆ, ๐งโฉ]
~R = ((๐ถ ยทR
-1R) +R ๐ด) โ ([โจ๐ฅ, 1Pโฉ]
~R = [โจ๐ฆ, ๐งโฉ] ~R โ
[โจ๐ฅ,
1Pโฉ] ~R = ((๐ถ
ยทR -1R)
+R ๐ด))) |
25 | 24 | rexbidv 3179 |
. . . . . . . 8
โข
([โจ๐ฆ, ๐งโฉ]
~R = ((๐ถ ยทR
-1R) +R ๐ด) โ (โ๐ฅ โ P [โจ๐ฅ,
1Pโฉ] ~R = [โจ๐ฆ, ๐งโฉ] ~R โ
โ๐ฅ โ
P [โจ๐ฅ,
1Pโฉ] ~R = ((๐ถ
ยทR -1R)
+R ๐ด))) |
26 | 23, 25 | imbi12d 345 |
. . . . . . 7
โข
([โจ๐ฆ, ๐งโฉ]
~R = ((๐ถ ยทR
-1R) +R ๐ด) โ ((-1R
<R [โจ๐ฆ, ๐งโฉ] ~R โ
โ๐ฅ โ
P [โจ๐ฅ,
1Pโฉ] ~R = [โจ๐ฆ, ๐งโฉ] ~R ) โ
(-1R <R ((๐ถ
ยทR -1R)
+R ๐ด) โ โ๐ฅ โ P [โจ๐ฅ,
1Pโฉ] ~R = ((๐ถ
ยทR -1R)
+R ๐ด)))) |
27 | | df-m1r 11054 |
. . . . . . . . . . 11
โข
-1R = [โจ1P,
(1P +P
1P)โฉ]
~R |
28 | 27 | breq1i 5155 |
. . . . . . . . . 10
โข
(-1R <R
[โจ๐ฆ, ๐งโฉ]
~R โ [โจ1P,
(1P +P
1P)โฉ] ~R
<R [โจ๐ฆ, ๐งโฉ] ~R
) |
29 | | addasspr 11014 |
. . . . . . . . . . . 12
โข
((1P +P
1P) +P ๐ฆ) = (1P
+P (1P
+P ๐ฆ)) |
30 | 29 | breq2i 5156 |
. . . . . . . . . . 11
โข
((1P +P ๐ง)<P
((1P +P
1P) +P ๐ฆ) โ (1P
+P ๐ง)<P
(1P +P
(1P +P ๐ฆ))) |
31 | | ltsrpr 11069 |
. . . . . . . . . . 11
โข
([โจ1P, (1P
+P 1P)โฉ]
~R <R [โจ๐ฆ, ๐งโฉ] ~R โ
(1P +P ๐ง)<P
((1P +P
1P) +P ๐ฆ)) |
32 | | 1pr 11007 |
. . . . . . . . . . . 12
โข
1P โ P |
33 | | ltapr 11037 |
. . . . . . . . . . . 12
โข
(1P โ P โ (๐ง<P
(1P +P ๐ฆ) โ (1P
+P ๐ง)<P
(1P +P
(1P +P ๐ฆ)))) |
34 | 32, 33 | ax-mp 5 |
. . . . . . . . . . 11
โข (๐ง<P
(1P +P ๐ฆ) โ (1P
+P ๐ง)<P
(1P +P
(1P +P ๐ฆ))) |
35 | 30, 31, 34 | 3bitr4i 303 |
. . . . . . . . . 10
โข
([โจ1P, (1P
+P 1P)โฉ]
~R <R [โจ๐ฆ, ๐งโฉ] ~R โ
๐ง<P
(1P +P ๐ฆ)) |
36 | 28, 35 | bitri 275 |
. . . . . . . . 9
โข
(-1R <R
[โจ๐ฆ, ๐งโฉ]
~R โ ๐ง<P
(1P +P ๐ฆ)) |
37 | | ltexpri 11035 |
. . . . . . . . 9
โข (๐ง<P
(1P +P ๐ฆ) โ โ๐ฅ โ P (๐ง +P ๐ฅ) = (1P
+P ๐ฆ)) |
38 | 36, 37 | sylbi 216 |
. . . . . . . 8
โข
(-1R <R
[โจ๐ฆ, ๐งโฉ]
~R โ โ๐ฅ โ P (๐ง +P ๐ฅ) = (1P
+P ๐ฆ)) |
39 | | enreceq 11058 |
. . . . . . . . . . . 12
โข (((๐ฅ โ P โง
1P โ P) โง (๐ฆ โ P โง ๐ง โ P)) โ
([โจ๐ฅ,
1Pโฉ] ~R = [โจ๐ฆ, ๐งโฉ] ~R โ
(๐ฅ
+P ๐ง) = (1P
+P ๐ฆ))) |
40 | 32, 39 | mpanl2 700 |
. . . . . . . . . . 11
โข ((๐ฅ โ P โง
(๐ฆ โ P
โง ๐ง โ
P)) โ ([โจ๐ฅ, 1Pโฉ]
~R = [โจ๐ฆ, ๐งโฉ] ~R โ
(๐ฅ
+P ๐ง) = (1P
+P ๐ฆ))) |
41 | | addcompr 11013 |
. . . . . . . . . . . 12
โข (๐ง +P
๐ฅ) = (๐ฅ +P ๐ง) |
42 | 41 | eqeq1i 2738 |
. . . . . . . . . . 11
โข ((๐ง +P
๐ฅ) =
(1P +P ๐ฆ) โ (๐ฅ +P ๐ง) = (1P
+P ๐ฆ)) |
43 | 40, 42 | bitr4di 289 |
. . . . . . . . . 10
โข ((๐ฅ โ P โง
(๐ฆ โ P
โง ๐ง โ
P)) โ ([โจ๐ฅ, 1Pโฉ]
~R = [โจ๐ฆ, ๐งโฉ] ~R โ
(๐ง
+P ๐ฅ) = (1P
+P ๐ฆ))) |
44 | 43 | ancoms 460 |
. . . . . . . . 9
โข (((๐ฆ โ P โง
๐ง โ P)
โง ๐ฅ โ
P) โ ([โจ๐ฅ, 1Pโฉ]
~R = [โจ๐ฆ, ๐งโฉ] ~R โ
(๐ง
+P ๐ฅ) = (1P
+P ๐ฆ))) |
45 | 44 | rexbidva 3177 |
. . . . . . . 8
โข ((๐ฆ โ P โง
๐ง โ P)
โ (โ๐ฅ โ
P [โจ๐ฅ,
1Pโฉ] ~R = [โจ๐ฆ, ๐งโฉ] ~R โ
โ๐ฅ โ
P (๐ง
+P ๐ฅ) = (1P
+P ๐ฆ))) |
46 | 38, 45 | imbitrrid 245 |
. . . . . . 7
โข ((๐ฆ โ P โง
๐ง โ P)
โ (-1R <R
[โจ๐ฆ, ๐งโฉ]
~R โ โ๐ฅ โ P [โจ๐ฅ,
1Pโฉ] ~R = [โจ๐ฆ, ๐งโฉ] ~R
)) |
47 | 22, 26, 46 | ecoptocl 8798 |
. . . . . 6
โข (((๐ถ
ยทR -1R)
+R ๐ด) โ R โ
(-1R <R ((๐ถ
ยทR -1R)
+R ๐ด) โ โ๐ฅ โ P [โจ๐ฅ,
1Pโฉ] ~R = ((๐ถ
ยทR -1R)
+R ๐ด))) |
48 | 21, 47 | syl 17 |
. . . . 5
โข (๐ด โ R โ
(-1R <R ((๐ถ
ยทR -1R)
+R ๐ด) โ โ๐ฅ โ P [โจ๐ฅ,
1Pโฉ] ~R = ((๐ถ
ยทR -1R)
+R ๐ด))) |
49 | | oveq2 7414 |
. . . . . . . 8
โข
([โจ๐ฅ,
1Pโฉ] ~R = ((๐ถ
ยทR -1R)
+R ๐ด) โ (๐ถ +R [โจ๐ฅ,
1Pโฉ] ~R ) = (๐ถ +R
((๐ถ
ยทR -1R)
+R ๐ด))) |
50 | 49, 14 | sylan9eqr 2795 |
. . . . . . 7
โข ((๐ด โ R โง
[โจ๐ฅ,
1Pโฉ] ~R = ((๐ถ
ยทR -1R)
+R ๐ด)) โ (๐ถ +R [โจ๐ฅ,
1Pโฉ] ~R ) = ๐ด) |
51 | 50 | ex 414 |
. . . . . 6
โข (๐ด โ R โ
([โจ๐ฅ,
1Pโฉ] ~R = ((๐ถ
ยทR -1R)
+R ๐ด) โ (๐ถ +R [โจ๐ฅ,
1Pโฉ] ~R ) = ๐ด)) |
52 | 51 | reximdv 3171 |
. . . . 5
โข (๐ด โ R โ
(โ๐ฅ โ
P [โจ๐ฅ,
1Pโฉ] ~R = ((๐ถ
ยทR -1R)
+R ๐ด) โ โ๐ฅ โ P (๐ถ +R [โจ๐ฅ,
1Pโฉ] ~R ) = ๐ด)) |
53 | 48, 52 | syld 47 |
. . . 4
โข (๐ด โ R โ
(-1R <R ((๐ถ
ยทR -1R)
+R ๐ด) โ โ๐ฅ โ P (๐ถ +R [โจ๐ฅ,
1Pโฉ] ~R ) = ๐ด)) |
54 | 16, 53 | sylbird 260 |
. . 3
โข (๐ด โ R โ
((๐ถ
+R -1R)
<R ๐ด โ โ๐ฅ โ P (๐ถ +R [โจ๐ฅ,
1Pโฉ] ~R ) = ๐ด)) |
55 | 3, 54 | mpcom 38 |
. 2
โข ((๐ถ +R
-1R) <R ๐ด โ โ๐ฅ โ P (๐ถ +R [โจ๐ฅ,
1Pโฉ] ~R ) = ๐ด) |
56 | 4 | mappsrpr 11100 |
. . . . 5
โข ((๐ถ +R
-1R) <R (๐ถ +R [โจ๐ฅ,
1Pโฉ] ~R ) โ ๐ฅ โ
P) |
57 | | breq2 5152 |
. . . . 5
โข ((๐ถ +R
[โจ๐ฅ,
1Pโฉ] ~R ) = ๐ด โ ((๐ถ +R
-1R) <R (๐ถ +R [โจ๐ฅ,
1Pโฉ] ~R ) โ (๐ถ +R
-1R) <R ๐ด)) |
58 | 56, 57 | bitr3id 285 |
. . . 4
โข ((๐ถ +R
[โจ๐ฅ,
1Pโฉ] ~R ) = ๐ด โ (๐ฅ โ P โ (๐ถ +R
-1R) <R ๐ด)) |
59 | 58 | biimpac 480 |
. . 3
โข ((๐ฅ โ P โง
(๐ถ
+R [โจ๐ฅ, 1Pโฉ]
~R ) = ๐ด) โ (๐ถ +R
-1R) <R ๐ด) |
60 | 59 | rexlimiva 3148 |
. 2
โข
(โ๐ฅ โ
P (๐ถ
+R [โจ๐ฅ, 1Pโฉ]
~R ) = ๐ด โ (๐ถ +R
-1R) <R ๐ด) |
61 | 55, 60 | impbii 208 |
1
โข ((๐ถ +R
-1R) <R ๐ด โ โ๐ฅ โ P (๐ถ +R [โจ๐ฅ,
1Pโฉ] ~R ) = ๐ด) |