Step | Hyp | Ref
| Expression |
1 | | rrx2linest2.i |
. . 3
โข ๐ผ = {1, 2} |
2 | | rrx2linest2.e |
. . 3
โข ๐ธ = (โ^โ๐ผ) |
3 | | rrx2linest2.p |
. . 3
โข ๐ = (โ โm
๐ผ) |
4 | | rrx2linest2.l |
. . 3
โข ๐ฟ = (LineMโ๐ธ) |
5 | | rrx2linest2.b |
. . 3
โข ๐ต = ((๐โ1) โ (๐โ1)) |
6 | | eqid 2733 |
. . 3
โข ((๐โ2) โ (๐โ2)) = ((๐โ2) โ (๐โ2)) |
7 | | rrx2linest2.c |
. . 3
โข ๐ถ = (((๐โ2) ยท (๐โ1)) โ ((๐โ1) ยท (๐โ2))) |
8 | 1, 2, 3, 4, 5, 6, 7 | rrx2linest 46918 |
. 2
โข ((๐ โ ๐ โง ๐ โ ๐ โง ๐ โ ๐) โ (๐๐ฟ๐) = {๐ โ ๐ โฃ (๐ต ยท (๐โ2)) = ((((๐โ2) โ (๐โ2)) ยท (๐โ1)) + ๐ถ)}) |
9 | | eqcom 2740 |
. . . 4
โข ((๐ต ยท (๐โ2)) = ((((๐โ2) โ (๐โ2)) ยท (๐โ1)) + ๐ถ) โ ((((๐โ2) โ (๐โ2)) ยท (๐โ1)) + ๐ถ) = (๐ต ยท (๐โ2))) |
10 | 1, 3 | rrx2pyel 46888 |
. . . . . . . . . . 11
โข (๐ โ ๐ โ (๐โ2) โ โ) |
11 | 10 | 3ad2ant2 1135 |
. . . . . . . . . 10
โข ((๐ โ ๐ โง ๐ โ ๐ โง ๐ โ ๐) โ (๐โ2) โ โ) |
12 | 1, 3 | rrx2pyel 46888 |
. . . . . . . . . . 11
โข (๐ โ ๐ โ (๐โ2) โ โ) |
13 | 12 | 3ad2ant1 1134 |
. . . . . . . . . 10
โข ((๐ โ ๐ โง ๐ โ ๐ โง ๐ โ ๐) โ (๐โ2) โ โ) |
14 | 11, 13 | resubcld 11591 |
. . . . . . . . 9
โข ((๐ โ ๐ โง ๐ โ ๐ โง ๐ โ ๐) โ ((๐โ2) โ (๐โ2)) โ โ) |
15 | 14 | adantr 482 |
. . . . . . . 8
โข (((๐ โ ๐ โง ๐ โ ๐ โง ๐ โ ๐) โง ๐ โ ๐) โ ((๐โ2) โ (๐โ2)) โ โ) |
16 | 1, 3 | rrx2pxel 46887 |
. . . . . . . . 9
โข (๐ โ ๐ โ (๐โ1) โ โ) |
17 | 16 | adantl 483 |
. . . . . . . 8
โข (((๐ โ ๐ โง ๐ โ ๐ โง ๐ โ ๐) โง ๐ โ ๐) โ (๐โ1) โ โ) |
18 | 15, 17 | remulcld 11193 |
. . . . . . 7
โข (((๐ โ ๐ โง ๐ โ ๐ โง ๐ โ ๐) โง ๐ โ ๐) โ (((๐โ2) โ (๐โ2)) ยท (๐โ1)) โ โ) |
19 | 18 | recnd 11191 |
. . . . . 6
โข (((๐ โ ๐ โง ๐ โ ๐ โง ๐ โ ๐) โง ๐ โ ๐) โ (((๐โ2) โ (๐โ2)) ยท (๐โ1)) โ โ) |
20 | 1, 3 | rrx2pxel 46887 |
. . . . . . . . . . . 12
โข (๐ โ ๐ โ (๐โ1) โ โ) |
21 | 20 | 3ad2ant2 1135 |
. . . . . . . . . . 11
โข ((๐ โ ๐ โง ๐ โ ๐ โง ๐ โ ๐) โ (๐โ1) โ โ) |
22 | 13, 21 | remulcld 11193 |
. . . . . . . . . 10
โข ((๐ โ ๐ โง ๐ โ ๐ โง ๐ โ ๐) โ ((๐โ2) ยท (๐โ1)) โ โ) |
23 | 1, 3 | rrx2pxel 46887 |
. . . . . . . . . . . 12
โข (๐ โ ๐ โ (๐โ1) โ โ) |
24 | 23 | 3ad2ant1 1134 |
. . . . . . . . . . 11
โข ((๐ โ ๐ โง ๐ โ ๐ โง ๐ โ ๐) โ (๐โ1) โ โ) |
25 | 24, 11 | remulcld 11193 |
. . . . . . . . . 10
โข ((๐ โ ๐ โง ๐ โ ๐ โง ๐ โ ๐) โ ((๐โ1) ยท (๐โ2)) โ โ) |
26 | 22, 25 | resubcld 11591 |
. . . . . . . . 9
โข ((๐ โ ๐ โง ๐ โ ๐ โง ๐ โ ๐) โ (((๐โ2) ยท (๐โ1)) โ ((๐โ1) ยท (๐โ2))) โ โ) |
27 | 7, 26 | eqeltrid 2838 |
. . . . . . . 8
โข ((๐ โ ๐ โง ๐ โ ๐ โง ๐ โ ๐) โ ๐ถ โ โ) |
28 | 27 | adantr 482 |
. . . . . . 7
โข (((๐ โ ๐ โง ๐ โ ๐ โง ๐ โ ๐) โง ๐ โ ๐) โ ๐ถ โ โ) |
29 | 28 | recnd 11191 |
. . . . . 6
โข (((๐ โ ๐ โง ๐ โ ๐ โง ๐ โ ๐) โง ๐ โ ๐) โ ๐ถ โ โ) |
30 | 21, 24 | resubcld 11591 |
. . . . . . . . . 10
โข ((๐ โ ๐ โง ๐ โ ๐ โง ๐ โ ๐) โ ((๐โ1) โ (๐โ1)) โ โ) |
31 | 5, 30 | eqeltrid 2838 |
. . . . . . . . 9
โข ((๐ โ ๐ โง ๐ โ ๐ โง ๐ โ ๐) โ ๐ต โ โ) |
32 | 31 | adantr 482 |
. . . . . . . 8
โข (((๐ โ ๐ โง ๐ โ ๐ โง ๐ โ ๐) โง ๐ โ ๐) โ ๐ต โ โ) |
33 | 1, 3 | rrx2pyel 46888 |
. . . . . . . . 9
โข (๐ โ ๐ โ (๐โ2) โ โ) |
34 | 33 | adantl 483 |
. . . . . . . 8
โข (((๐ โ ๐ โง ๐ โ ๐ โง ๐ โ ๐) โง ๐ โ ๐) โ (๐โ2) โ โ) |
35 | 32, 34 | remulcld 11193 |
. . . . . . 7
โข (((๐ โ ๐ โง ๐ โ ๐ โง ๐ โ ๐) โง ๐ โ ๐) โ (๐ต ยท (๐โ2)) โ โ) |
36 | 35 | recnd 11191 |
. . . . . 6
โข (((๐ โ ๐ โง ๐ โ ๐ โง ๐ โ ๐) โง ๐ โ ๐) โ (๐ต ยท (๐โ2)) โ โ) |
37 | 19, 29, 36 | addrsub 11580 |
. . . . 5
โข (((๐ โ ๐ โง ๐ โ ๐ โง ๐ โ ๐) โง ๐ โ ๐) โ (((((๐โ2) โ (๐โ2)) ยท (๐โ1)) + ๐ถ) = (๐ต ยท (๐โ2)) โ ๐ถ = ((๐ต ยท (๐โ2)) โ (((๐โ2) โ (๐โ2)) ยท (๐โ1))))) |
38 | | eqcom 2740 |
. . . . . 6
โข (๐ถ = ((๐ต ยท (๐โ2)) โ (((๐โ2) โ (๐โ2)) ยท (๐โ1))) โ ((๐ต ยท (๐โ2)) โ (((๐โ2) โ (๐โ2)) ยท (๐โ1))) = ๐ถ) |
39 | | rrx2linest2.a |
. . . . . . . . . . . . 13
โข ๐ด = ((๐โ2) โ (๐โ2)) |
40 | 13, 11 | resubcld 11591 |
. . . . . . . . . . . . 13
โข ((๐ โ ๐ โง ๐ โ ๐ โง ๐ โ ๐) โ ((๐โ2) โ (๐โ2)) โ โ) |
41 | 39, 40 | eqeltrid 2838 |
. . . . . . . . . . . 12
โข ((๐ โ ๐ โง ๐ โ ๐ โง ๐ โ ๐) โ ๐ด โ โ) |
42 | 41 | adantr 482 |
. . . . . . . . . . 11
โข (((๐ โ ๐ โง ๐ โ ๐ โง ๐ โ ๐) โง ๐ โ ๐) โ ๐ด โ โ) |
43 | 42, 17 | remulcld 11193 |
. . . . . . . . . 10
โข (((๐ โ ๐ โง ๐ โ ๐ โง ๐ โ ๐) โง ๐ โ ๐) โ (๐ด ยท (๐โ1)) โ โ) |
44 | 43 | recnd 11191 |
. . . . . . . . 9
โข (((๐ โ ๐ โง ๐ โ ๐ โง ๐ โ ๐) โง ๐ โ ๐) โ (๐ด ยท (๐โ1)) โ โ) |
45 | 44, 36 | addcomd 11365 |
. . . . . . . 8
โข (((๐ โ ๐ โง ๐ โ ๐ โง ๐ โ ๐) โง ๐ โ ๐) โ ((๐ด ยท (๐โ1)) + (๐ต ยท (๐โ2))) = ((๐ต ยท (๐โ2)) + (๐ด ยท (๐โ1)))) |
46 | 11 | adantr 482 |
. . . . . . . . . . . . . 14
โข (((๐ โ ๐ โง ๐ โ ๐ โง ๐ โ ๐) โง ๐ โ ๐) โ (๐โ2) โ โ) |
47 | 46 | recnd 11191 |
. . . . . . . . . . . . 13
โข (((๐ โ ๐ โง ๐ โ ๐ โง ๐ โ ๐) โง ๐ โ ๐) โ (๐โ2) โ โ) |
48 | 13 | adantr 482 |
. . . . . . . . . . . . . 14
โข (((๐ โ ๐ โง ๐ โ ๐ โง ๐ โ ๐) โง ๐ โ ๐) โ (๐โ2) โ โ) |
49 | 48 | recnd 11191 |
. . . . . . . . . . . . 13
โข (((๐ โ ๐ โง ๐ โ ๐ โง ๐ โ ๐) โง ๐ โ ๐) โ (๐โ2) โ โ) |
50 | 47, 49 | negsubdi2d 11536 |
. . . . . . . . . . . 12
โข (((๐ โ ๐ โง ๐ โ ๐ โง ๐ โ ๐) โง ๐ โ ๐) โ -((๐โ2) โ (๐โ2)) = ((๐โ2) โ (๐โ2))) |
51 | 39, 50 | eqtr4id 2792 |
. . . . . . . . . . 11
โข (((๐ โ ๐ โง ๐ โ ๐ โง ๐ โ ๐) โง ๐ โ ๐) โ ๐ด = -((๐โ2) โ (๐โ2))) |
52 | 51 | oveq1d 7376 |
. . . . . . . . . 10
โข (((๐ โ ๐ โง ๐ โ ๐ โง ๐ โ ๐) โง ๐ โ ๐) โ (๐ด ยท (๐โ1)) = (-((๐โ2) โ (๐โ2)) ยท (๐โ1))) |
53 | 15 | recnd 11191 |
. . . . . . . . . . 11
โข (((๐ โ ๐ โง ๐ โ ๐ โง ๐ โ ๐) โง ๐ โ ๐) โ ((๐โ2) โ (๐โ2)) โ โ) |
54 | 17 | recnd 11191 |
. . . . . . . . . . 11
โข (((๐ โ ๐ โง ๐ โ ๐ โง ๐ โ ๐) โง ๐ โ ๐) โ (๐โ1) โ โ) |
55 | 53, 54 | mulneg1d 11616 |
. . . . . . . . . 10
โข (((๐ โ ๐ โง ๐ โ ๐ โง ๐ โ ๐) โง ๐ โ ๐) โ (-((๐โ2) โ (๐โ2)) ยท (๐โ1)) = -(((๐โ2) โ (๐โ2)) ยท (๐โ1))) |
56 | 52, 55 | eqtrd 2773 |
. . . . . . . . 9
โข (((๐ โ ๐ โง ๐ โ ๐ โง ๐ โ ๐) โง ๐ โ ๐) โ (๐ด ยท (๐โ1)) = -(((๐โ2) โ (๐โ2)) ยท (๐โ1))) |
57 | 56 | oveq2d 7377 |
. . . . . . . 8
โข (((๐ โ ๐ โง ๐ โ ๐ โง ๐ โ ๐) โง ๐ โ ๐) โ ((๐ต ยท (๐โ2)) + (๐ด ยท (๐โ1))) = ((๐ต ยท (๐โ2)) + -(((๐โ2) โ (๐โ2)) ยท (๐โ1)))) |
58 | 36, 19 | negsubd 11526 |
. . . . . . . 8
โข (((๐ โ ๐ โง ๐ โ ๐ โง ๐ โ ๐) โง ๐ โ ๐) โ ((๐ต ยท (๐โ2)) + -(((๐โ2) โ (๐โ2)) ยท (๐โ1))) = ((๐ต ยท (๐โ2)) โ (((๐โ2) โ (๐โ2)) ยท (๐โ1)))) |
59 | 45, 57, 58 | 3eqtrd 2777 |
. . . . . . 7
โข (((๐ โ ๐ โง ๐ โ ๐ โง ๐ โ ๐) โง ๐ โ ๐) โ ((๐ด ยท (๐โ1)) + (๐ต ยท (๐โ2))) = ((๐ต ยท (๐โ2)) โ (((๐โ2) โ (๐โ2)) ยท (๐โ1)))) |
60 | 59 | eqeq1d 2735 |
. . . . . 6
โข (((๐ โ ๐ โง ๐ โ ๐ โง ๐ โ ๐) โง ๐ โ ๐) โ (((๐ด ยท (๐โ1)) + (๐ต ยท (๐โ2))) = ๐ถ โ ((๐ต ยท (๐โ2)) โ (((๐โ2) โ (๐โ2)) ยท (๐โ1))) = ๐ถ)) |
61 | 38, 60 | bitr4id 290 |
. . . . 5
โข (((๐ โ ๐ โง ๐ โ ๐ โง ๐ โ ๐) โง ๐ โ ๐) โ (๐ถ = ((๐ต ยท (๐โ2)) โ (((๐โ2) โ (๐โ2)) ยท (๐โ1))) โ ((๐ด ยท (๐โ1)) + (๐ต ยท (๐โ2))) = ๐ถ)) |
62 | 37, 61 | bitrd 279 |
. . . 4
โข (((๐ โ ๐ โง ๐ โ ๐ โง ๐ โ ๐) โง ๐ โ ๐) โ (((((๐โ2) โ (๐โ2)) ยท (๐โ1)) + ๐ถ) = (๐ต ยท (๐โ2)) โ ((๐ด ยท (๐โ1)) + (๐ต ยท (๐โ2))) = ๐ถ)) |
63 | 9, 62 | bitrid 283 |
. . 3
โข (((๐ โ ๐ โง ๐ โ ๐ โง ๐ โ ๐) โง ๐ โ ๐) โ ((๐ต ยท (๐โ2)) = ((((๐โ2) โ (๐โ2)) ยท (๐โ1)) + ๐ถ) โ ((๐ด ยท (๐โ1)) + (๐ต ยท (๐โ2))) = ๐ถ)) |
64 | 63 | rabbidva 3413 |
. 2
โข ((๐ โ ๐ โง ๐ โ ๐ โง ๐ โ ๐) โ {๐ โ ๐ โฃ (๐ต ยท (๐โ2)) = ((((๐โ2) โ (๐โ2)) ยท (๐โ1)) + ๐ถ)} = {๐ โ ๐ โฃ ((๐ด ยท (๐โ1)) + (๐ต ยท (๐โ2))) = ๐ถ}) |
65 | 8, 64 | eqtrd 2773 |
1
โข ((๐ โ ๐ โง ๐ โ ๐ โง ๐ โ ๐) โ (๐๐ฟ๐) = {๐ โ ๐ โฃ ((๐ด ยท (๐โ1)) + (๐ต ยท (๐โ2))) = ๐ถ}) |