Step | Hyp | Ref
| Expression |
1 | | ianor 980 |
. . . . 5
โข (ยฌ
((๐ด โ 0 โง ๐ต = 0) โง ๐ถ = 0) โ (ยฌ (๐ด โ 0 โง ๐ต = 0) โจ ยฌ ๐ถ = 0)) |
2 | | df-ne 2941 |
. . . . . . . . 9
โข (๐ถ โ 0 โ ยฌ ๐ถ = 0) |
3 | | 0re 11215 |
. . . . . . . . . . . 12
โข 0 โ
โ |
4 | | line2ylem.i |
. . . . . . . . . . . . 13
โข ๐ผ = {1, 2} |
5 | | line2ylem.p |
. . . . . . . . . . . . 13
โข ๐ = (โ โm
๐ผ) |
6 | 4, 5 | prelrrx2 47389 |
. . . . . . . . . . . 12
โข ((0
โ โ โง 0 โ โ) โ {โจ1, 0โฉ, โจ2,
0โฉ} โ ๐) |
7 | 3, 3, 6 | mp2an 690 |
. . . . . . . . . . 11
โข {โจ1,
0โฉ, โจ2, 0โฉ} โ ๐ |
8 | | eqneqall 2951 |
. . . . . . . . . . . . . . . 16
โข (๐ถ = 0 โ (๐ถ โ 0 โ ยฌ 0 =
0)) |
9 | 8 | com12 32 |
. . . . . . . . . . . . . . 15
โข (๐ถ โ 0 โ (๐ถ = 0 โ ยฌ 0 =
0)) |
10 | | eqid 2732 |
. . . . . . . . . . . . . . . 16
โข 0 =
0 |
11 | 10 | pm2.24i 150 |
. . . . . . . . . . . . . . 15
โข (ยฌ 0
= 0 โ ๐ถ =
0) |
12 | 9, 11 | impbid1 224 |
. . . . . . . . . . . . . 14
โข (๐ถ โ 0 โ (๐ถ = 0 โ ยฌ 0 =
0)) |
13 | 12 | adantl 482 |
. . . . . . . . . . . . 13
โข (((๐ด โ โ โง ๐ต โ โ โง ๐ถ โ โ) โง ๐ถ โ 0) โ (๐ถ = 0 โ ยฌ 0 =
0)) |
14 | | xor3 383 |
. . . . . . . . . . . . 13
โข (ยฌ
(๐ถ = 0 โ 0 = 0) โ
(๐ถ = 0 โ ยฌ 0 =
0)) |
15 | 13, 14 | sylibr 233 |
. . . . . . . . . . . 12
โข (((๐ด โ โ โง ๐ต โ โ โง ๐ถ โ โ) โง ๐ถ โ 0) โ ยฌ (๐ถ = 0 โ 0 =
0)) |
16 | | simp1 1136 |
. . . . . . . . . . . . . . . . . . . 20
โข ((๐ด โ โ โง ๐ต โ โ โง ๐ถ โ โ) โ ๐ด โ
โ) |
17 | 16 | recnd 11241 |
. . . . . . . . . . . . . . . . . . 19
โข ((๐ด โ โ โง ๐ต โ โ โง ๐ถ โ โ) โ ๐ด โ
โ) |
18 | 17 | mul01d 11412 |
. . . . . . . . . . . . . . . . . 18
โข ((๐ด โ โ โง ๐ต โ โ โง ๐ถ โ โ) โ (๐ด ยท 0) =
0) |
19 | | simp2 1137 |
. . . . . . . . . . . . . . . . . . . 20
โข ((๐ด โ โ โง ๐ต โ โ โง ๐ถ โ โ) โ ๐ต โ
โ) |
20 | 19 | recnd 11241 |
. . . . . . . . . . . . . . . . . . 19
โข ((๐ด โ โ โง ๐ต โ โ โง ๐ถ โ โ) โ ๐ต โ
โ) |
21 | 20 | mul01d 11412 |
. . . . . . . . . . . . . . . . . 18
โข ((๐ด โ โ โง ๐ต โ โ โง ๐ถ โ โ) โ (๐ต ยท 0) =
0) |
22 | 18, 21 | oveq12d 7426 |
. . . . . . . . . . . . . . . . 17
โข ((๐ด โ โ โง ๐ต โ โ โง ๐ถ โ โ) โ ((๐ด ยท 0) + (๐ต ยท 0)) = (0 +
0)) |
23 | | 00id 11388 |
. . . . . . . . . . . . . . . . 17
โข (0 + 0) =
0 |
24 | 22, 23 | eqtrdi 2788 |
. . . . . . . . . . . . . . . 16
โข ((๐ด โ โ โง ๐ต โ โ โง ๐ถ โ โ) โ ((๐ด ยท 0) + (๐ต ยท 0)) =
0) |
25 | 24 | eqeq1d 2734 |
. . . . . . . . . . . . . . 15
โข ((๐ด โ โ โง ๐ต โ โ โง ๐ถ โ โ) โ (((๐ด ยท 0) + (๐ต ยท 0)) = ๐ถ โ 0 = ๐ถ)) |
26 | | eqcom 2739 |
. . . . . . . . . . . . . . 15
โข (0 =
๐ถ โ ๐ถ = 0) |
27 | 25, 26 | bitrdi 286 |
. . . . . . . . . . . . . 14
โข ((๐ด โ โ โง ๐ต โ โ โง ๐ถ โ โ) โ (((๐ด ยท 0) + (๐ต ยท 0)) = ๐ถ โ ๐ถ = 0)) |
28 | 27 | adantr 481 |
. . . . . . . . . . . . 13
โข (((๐ด โ โ โง ๐ต โ โ โง ๐ถ โ โ) โง ๐ถ โ 0) โ (((๐ด ยท 0) + (๐ต ยท 0)) = ๐ถ โ ๐ถ = 0)) |
29 | 28 | bibi1d 343 |
. . . . . . . . . . . 12
โข (((๐ด โ โ โง ๐ต โ โ โง ๐ถ โ โ) โง ๐ถ โ 0) โ ((((๐ด ยท 0) + (๐ต ยท 0)) = ๐ถ โ 0 = 0) โ (๐ถ = 0 โ 0 =
0))) |
30 | 15, 29 | mtbird 324 |
. . . . . . . . . . 11
โข (((๐ด โ โ โง ๐ต โ โ โง ๐ถ โ โ) โง ๐ถ โ 0) โ ยฌ (((๐ด ยท 0) + (๐ต ยท 0)) = ๐ถ โ 0 = 0)) |
31 | | fveq1 6890 |
. . . . . . . . . . . . . . . . . 18
โข (๐ = {โจ1, 0โฉ, โจ2,
0โฉ} โ (๐โ1)
= ({โจ1, 0โฉ, โจ2, 0โฉ}โ1)) |
32 | | 1ex 11209 |
. . . . . . . . . . . . . . . . . . 19
โข 1 โ
V |
33 | | c0ex 11207 |
. . . . . . . . . . . . . . . . . . 19
โข 0 โ
V |
34 | | 1ne2 12419 |
. . . . . . . . . . . . . . . . . . 19
โข 1 โ
2 |
35 | | fvpr1g 7187 |
. . . . . . . . . . . . . . . . . . 19
โข ((1
โ V โง 0 โ V โง 1 โ 2) โ ({โจ1, 0โฉ, โจ2,
0โฉ}โ1) = 0) |
36 | 32, 33, 34, 35 | mp3an 1461 |
. . . . . . . . . . . . . . . . . 18
โข
({โจ1, 0โฉ, โจ2, 0โฉ}โ1) = 0 |
37 | 31, 36 | eqtrdi 2788 |
. . . . . . . . . . . . . . . . 17
โข (๐ = {โจ1, 0โฉ, โจ2,
0โฉ} โ (๐โ1)
= 0) |
38 | 37 | oveq2d 7424 |
. . . . . . . . . . . . . . . 16
โข (๐ = {โจ1, 0โฉ, โจ2,
0โฉ} โ (๐ด ยท
(๐โ1)) = (๐ด ยท 0)) |
39 | | fveq1 6890 |
. . . . . . . . . . . . . . . . . 18
โข (๐ = {โจ1, 0โฉ, โจ2,
0โฉ} โ (๐โ2)
= ({โจ1, 0โฉ, โจ2, 0โฉ}โ2)) |
40 | | 2ex 12288 |
. . . . . . . . . . . . . . . . . . 19
โข 2 โ
V |
41 | | fvpr2g 7188 |
. . . . . . . . . . . . . . . . . . 19
โข ((2
โ V โง 0 โ V โง 1 โ 2) โ ({โจ1, 0โฉ, โจ2,
0โฉ}โ2) = 0) |
42 | 40, 33, 34, 41 | mp3an 1461 |
. . . . . . . . . . . . . . . . . 18
โข
({โจ1, 0โฉ, โจ2, 0โฉ}โ2) = 0 |
43 | 39, 42 | eqtrdi 2788 |
. . . . . . . . . . . . . . . . 17
โข (๐ = {โจ1, 0โฉ, โจ2,
0โฉ} โ (๐โ2)
= 0) |
44 | 43 | oveq2d 7424 |
. . . . . . . . . . . . . . . 16
โข (๐ = {โจ1, 0โฉ, โจ2,
0โฉ} โ (๐ต ยท
(๐โ2)) = (๐ต ยท 0)) |
45 | 38, 44 | oveq12d 7426 |
. . . . . . . . . . . . . . 15
โข (๐ = {โจ1, 0โฉ, โจ2,
0โฉ} โ ((๐ด
ยท (๐โ1)) +
(๐ต ยท (๐โ2))) = ((๐ด ยท 0) + (๐ต ยท 0))) |
46 | 45 | eqeq1d 2734 |
. . . . . . . . . . . . . 14
โข (๐ = {โจ1, 0โฉ, โจ2,
0โฉ} โ (((๐ด
ยท (๐โ1)) +
(๐ต ยท (๐โ2))) = ๐ถ โ ((๐ด ยท 0) + (๐ต ยท 0)) = ๐ถ)) |
47 | 37 | eqeq1d 2734 |
. . . . . . . . . . . . . 14
โข (๐ = {โจ1, 0โฉ, โจ2,
0โฉ} โ ((๐โ1) = 0 โ 0 = 0)) |
48 | 46, 47 | bibi12d 345 |
. . . . . . . . . . . . 13
โข (๐ = {โจ1, 0โฉ, โจ2,
0โฉ} โ ((((๐ด
ยท (๐โ1)) +
(๐ต ยท (๐โ2))) = ๐ถ โ (๐โ1) = 0) โ (((๐ด ยท 0) + (๐ต ยท 0)) = ๐ถ โ 0 = 0))) |
49 | 48 | notbid 317 |
. . . . . . . . . . . 12
โข (๐ = {โจ1, 0โฉ, โจ2,
0โฉ} โ (ยฌ (((๐ด
ยท (๐โ1)) +
(๐ต ยท (๐โ2))) = ๐ถ โ (๐โ1) = 0) โ ยฌ (((๐ด ยท 0) + (๐ต ยท 0)) = ๐ถ โ 0 =
0))) |
50 | 49 | rspcev 3612 |
. . . . . . . . . . 11
โข
(({โจ1, 0โฉ, โจ2, 0โฉ} โ ๐ โง ยฌ (((๐ด ยท 0) + (๐ต ยท 0)) = ๐ถ โ 0 = 0)) โ โ๐ โ ๐ ยฌ (((๐ด ยท (๐โ1)) + (๐ต ยท (๐โ2))) = ๐ถ โ (๐โ1) = 0)) |
51 | 7, 30, 50 | sylancr 587 |
. . . . . . . . . 10
โข (((๐ด โ โ โง ๐ต โ โ โง ๐ถ โ โ) โง ๐ถ โ 0) โ โ๐ โ ๐ ยฌ (((๐ด ยท (๐โ1)) + (๐ต ยท (๐โ2))) = ๐ถ โ (๐โ1) = 0)) |
52 | 51 | expcom 414 |
. . . . . . . . 9
โข (๐ถ โ 0 โ ((๐ด โ โ โง ๐ต โ โ โง ๐ถ โ โ) โ
โ๐ โ ๐ ยฌ (((๐ด ยท (๐โ1)) + (๐ต ยท (๐โ2))) = ๐ถ โ (๐โ1) = 0))) |
53 | 2, 52 | sylbir 234 |
. . . . . . . 8
โข (ยฌ
๐ถ = 0 โ ((๐ด โ โ โง ๐ต โ โ โง ๐ถ โ โ) โ
โ๐ โ ๐ ยฌ (((๐ด ยท (๐โ1)) + (๐ต ยท (๐โ2))) = ๐ถ โ (๐โ1) = 0))) |
54 | | notnotb 314 |
. . . . . . . . . 10
โข (๐ถ = 0 โ ยฌ ยฌ ๐ถ = 0) |
55 | | ianor 980 |
. . . . . . . . . . . 12
โข (ยฌ
(๐ด โ 0 โง ๐ต = 0) โ (ยฌ ๐ด โ 0 โจ ยฌ ๐ต = 0)) |
56 | | df-ne 2941 |
. . . . . . . . . . . . . . 15
โข (๐ต โ 0 โ ยฌ ๐ต = 0) |
57 | | 1red 11214 |
. . . . . . . . . . . . . . . . . . 19
โข (((๐ด โ โ โง ๐ต โ โ โง ๐ถ โ โ) โง (๐ต โ 0 โง ๐ถ = 0)) โ 1 โ
โ) |
58 | 16 | adantr 481 |
. . . . . . . . . . . . . . . . . . . . 21
โข (((๐ด โ โ โง ๐ต โ โ โง ๐ถ โ โ) โง (๐ต โ 0 โง ๐ถ = 0)) โ ๐ด โ โ) |
59 | 58 | renegcld 11640 |
. . . . . . . . . . . . . . . . . . . 20
โข (((๐ด โ โ โง ๐ต โ โ โง ๐ถ โ โ) โง (๐ต โ 0 โง ๐ถ = 0)) โ -๐ด โ โ) |
60 | 19 | adantr 481 |
. . . . . . . . . . . . . . . . . . . 20
โข (((๐ด โ โ โง ๐ต โ โ โง ๐ถ โ โ) โง (๐ต โ 0 โง ๐ถ = 0)) โ ๐ต โ โ) |
61 | | simprl 769 |
. . . . . . . . . . . . . . . . . . . 20
โข (((๐ด โ โ โง ๐ต โ โ โง ๐ถ โ โ) โง (๐ต โ 0 โง ๐ถ = 0)) โ ๐ต โ 0) |
62 | 59, 60, 61 | redivcld 12041 |
. . . . . . . . . . . . . . . . . . 19
โข (((๐ด โ โ โง ๐ต โ โ โง ๐ถ โ โ) โง (๐ต โ 0 โง ๐ถ = 0)) โ (-๐ด / ๐ต) โ โ) |
63 | 4, 5 | prelrrx2 47389 |
. . . . . . . . . . . . . . . . . . 19
โข ((1
โ โ โง (-๐ด /
๐ต) โ โ) โ
{โจ1, 1โฉ, โจ2, (-๐ด / ๐ต)โฉ} โ ๐) |
64 | 57, 62, 63 | syl2anc 584 |
. . . . . . . . . . . . . . . . . 18
โข (((๐ด โ โ โง ๐ต โ โ โง ๐ถ โ โ) โง (๐ต โ 0 โง ๐ถ = 0)) โ {โจ1, 1โฉ, โจ2,
(-๐ด / ๐ต)โฉ} โ ๐) |
65 | | ax-1ne0 11178 |
. . . . . . . . . . . . . . . . . . . . . 22
โข 1 โ
0 |
66 | 65 | neii 2942 |
. . . . . . . . . . . . . . . . . . . . 21
โข ยฌ 1
= 0 |
67 | 10, 66 | 2th 263 |
. . . . . . . . . . . . . . . . . . . 20
โข (0 = 0
โ ยฌ 1 = 0) |
68 | | xor3 383 |
. . . . . . . . . . . . . . . . . . . 20
โข (ยฌ (0
= 0 โ 1 = 0) โ (0 = 0 โ ยฌ 1 = 0)) |
69 | 67, 68 | mpbir 230 |
. . . . . . . . . . . . . . . . . . 19
โข ยฌ (0
= 0 โ 1 = 0) |
70 | 17 | mulridd 11230 |
. . . . . . . . . . . . . . . . . . . . . . . 24
โข ((๐ด โ โ โง ๐ต โ โ โง ๐ถ โ โ) โ (๐ด ยท 1) = ๐ด) |
71 | 70 | adantr 481 |
. . . . . . . . . . . . . . . . . . . . . . 23
โข (((๐ด โ โ โง ๐ต โ โ โง ๐ถ โ โ) โง (๐ต โ 0 โง ๐ถ = 0)) โ (๐ด ยท 1) = ๐ด) |
72 | 17 | negcld 11557 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
โข ((๐ด โ โ โง ๐ต โ โ โง ๐ถ โ โ) โ -๐ด โ
โ) |
73 | 72 | adantr 481 |
. . . . . . . . . . . . . . . . . . . . . . . 24
โข (((๐ด โ โ โง ๐ต โ โ โง ๐ถ โ โ) โง (๐ต โ 0 โง ๐ถ = 0)) โ -๐ด โ โ) |
74 | 20 | adantr 481 |
. . . . . . . . . . . . . . . . . . . . . . . 24
โข (((๐ด โ โ โง ๐ต โ โ โง ๐ถ โ โ) โง (๐ต โ 0 โง ๐ถ = 0)) โ ๐ต โ โ) |
75 | 73, 74, 61 | divcan2d 11991 |
. . . . . . . . . . . . . . . . . . . . . . 23
โข (((๐ด โ โ โง ๐ต โ โ โง ๐ถ โ โ) โง (๐ต โ 0 โง ๐ถ = 0)) โ (๐ต ยท (-๐ด / ๐ต)) = -๐ด) |
76 | 71, 75 | oveq12d 7426 |
. . . . . . . . . . . . . . . . . . . . . 22
โข (((๐ด โ โ โง ๐ต โ โ โง ๐ถ โ โ) โง (๐ต โ 0 โง ๐ถ = 0)) โ ((๐ด ยท 1) + (๐ต ยท (-๐ด / ๐ต))) = (๐ด + -๐ด)) |
77 | 17 | negidd 11560 |
. . . . . . . . . . . . . . . . . . . . . . 23
โข ((๐ด โ โ โง ๐ต โ โ โง ๐ถ โ โ) โ (๐ด + -๐ด) = 0) |
78 | 77 | adantr 481 |
. . . . . . . . . . . . . . . . . . . . . 22
โข (((๐ด โ โ โง ๐ต โ โ โง ๐ถ โ โ) โง (๐ต โ 0 โง ๐ถ = 0)) โ (๐ด + -๐ด) = 0) |
79 | 76, 78 | eqtrd 2772 |
. . . . . . . . . . . . . . . . . . . . 21
โข (((๐ด โ โ โง ๐ต โ โ โง ๐ถ โ โ) โง (๐ต โ 0 โง ๐ถ = 0)) โ ((๐ด ยท 1) + (๐ต ยท (-๐ด / ๐ต))) = 0) |
80 | | simprr 771 |
. . . . . . . . . . . . . . . . . . . . 21
โข (((๐ด โ โ โง ๐ต โ โ โง ๐ถ โ โ) โง (๐ต โ 0 โง ๐ถ = 0)) โ ๐ถ = 0) |
81 | 79, 80 | eqeq12d 2748 |
. . . . . . . . . . . . . . . . . . . 20
โข (((๐ด โ โ โง ๐ต โ โ โง ๐ถ โ โ) โง (๐ต โ 0 โง ๐ถ = 0)) โ (((๐ด ยท 1) + (๐ต ยท (-๐ด / ๐ต))) = ๐ถ โ 0 = 0)) |
82 | 81 | bibi1d 343 |
. . . . . . . . . . . . . . . . . . 19
โข (((๐ด โ โ โง ๐ต โ โ โง ๐ถ โ โ) โง (๐ต โ 0 โง ๐ถ = 0)) โ ((((๐ด ยท 1) + (๐ต ยท (-๐ด / ๐ต))) = ๐ถ โ 1 = 0) โ (0 = 0 โ 1 =
0))) |
83 | 69, 82 | mtbiri 326 |
. . . . . . . . . . . . . . . . . 18
โข (((๐ด โ โ โง ๐ต โ โ โง ๐ถ โ โ) โง (๐ต โ 0 โง ๐ถ = 0)) โ ยฌ (((๐ด ยท 1) + (๐ต ยท (-๐ด / ๐ต))) = ๐ถ โ 1 = 0)) |
84 | | fveq1 6890 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
โข (๐ = {โจ1, 1โฉ, โจ2,
(-๐ด / ๐ต)โฉ} โ (๐โ1) = ({โจ1, 1โฉ, โจ2,
(-๐ด / ๐ต)โฉ}โ1)) |
85 | | fvpr1g 7187 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
โข ((1
โ V โง 1 โ V โง 1 โ 2) โ ({โจ1, 1โฉ, โจ2,
(-๐ด / ๐ต)โฉ}โ1) = 1) |
86 | 32, 32, 34, 85 | mp3an 1461 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
โข
({โจ1, 1โฉ, โจ2, (-๐ด / ๐ต)โฉ}โ1) = 1 |
87 | 84, 86 | eqtrdi 2788 |
. . . . . . . . . . . . . . . . . . . . . . . 24
โข (๐ = {โจ1, 1โฉ, โจ2,
(-๐ด / ๐ต)โฉ} โ (๐โ1) = 1) |
88 | 87 | oveq2d 7424 |
. . . . . . . . . . . . . . . . . . . . . . 23
โข (๐ = {โจ1, 1โฉ, โจ2,
(-๐ด / ๐ต)โฉ} โ (๐ด ยท (๐โ1)) = (๐ด ยท 1)) |
89 | | fveq1 6890 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
โข (๐ = {โจ1, 1โฉ, โจ2,
(-๐ด / ๐ต)โฉ} โ (๐โ2) = ({โจ1, 1โฉ, โจ2,
(-๐ด / ๐ต)โฉ}โ2)) |
90 | | ovex 7441 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
โข (-๐ด / ๐ต) โ V |
91 | | fvpr2g 7188 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
โข ((2
โ V โง (-๐ด / ๐ต) โ V โง 1 โ 2)
โ ({โจ1, 1โฉ, โจ2, (-๐ด / ๐ต)โฉ}โ2) = (-๐ด / ๐ต)) |
92 | 40, 90, 34, 91 | mp3an 1461 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
โข
({โจ1, 1โฉ, โจ2, (-๐ด / ๐ต)โฉ}โ2) = (-๐ด / ๐ต) |
93 | 89, 92 | eqtrdi 2788 |
. . . . . . . . . . . . . . . . . . . . . . . 24
โข (๐ = {โจ1, 1โฉ, โจ2,
(-๐ด / ๐ต)โฉ} โ (๐โ2) = (-๐ด / ๐ต)) |
94 | 93 | oveq2d 7424 |
. . . . . . . . . . . . . . . . . . . . . . 23
โข (๐ = {โจ1, 1โฉ, โจ2,
(-๐ด / ๐ต)โฉ} โ (๐ต ยท (๐โ2)) = (๐ต ยท (-๐ด / ๐ต))) |
95 | 88, 94 | oveq12d 7426 |
. . . . . . . . . . . . . . . . . . . . . 22
โข (๐ = {โจ1, 1โฉ, โจ2,
(-๐ด / ๐ต)โฉ} โ ((๐ด ยท (๐โ1)) + (๐ต ยท (๐โ2))) = ((๐ด ยท 1) + (๐ต ยท (-๐ด / ๐ต)))) |
96 | 95 | eqeq1d 2734 |
. . . . . . . . . . . . . . . . . . . . 21
โข (๐ = {โจ1, 1โฉ, โจ2,
(-๐ด / ๐ต)โฉ} โ (((๐ด ยท (๐โ1)) + (๐ต ยท (๐โ2))) = ๐ถ โ ((๐ด ยท 1) + (๐ต ยท (-๐ด / ๐ต))) = ๐ถ)) |
97 | 87 | eqeq1d 2734 |
. . . . . . . . . . . . . . . . . . . . 21
โข (๐ = {โจ1, 1โฉ, โจ2,
(-๐ด / ๐ต)โฉ} โ ((๐โ1) = 0 โ 1 = 0)) |
98 | 96, 97 | bibi12d 345 |
. . . . . . . . . . . . . . . . . . . 20
โข (๐ = {โจ1, 1โฉ, โจ2,
(-๐ด / ๐ต)โฉ} โ ((((๐ด ยท (๐โ1)) + (๐ต ยท (๐โ2))) = ๐ถ โ (๐โ1) = 0) โ (((๐ด ยท 1) + (๐ต ยท (-๐ด / ๐ต))) = ๐ถ โ 1 = 0))) |
99 | 98 | notbid 317 |
. . . . . . . . . . . . . . . . . . 19
โข (๐ = {โจ1, 1โฉ, โจ2,
(-๐ด / ๐ต)โฉ} โ (ยฌ (((๐ด ยท (๐โ1)) + (๐ต ยท (๐โ2))) = ๐ถ โ (๐โ1) = 0) โ ยฌ (((๐ด ยท 1) + (๐ต ยท (-๐ด / ๐ต))) = ๐ถ โ 1 = 0))) |
100 | 99 | rspcev 3612 |
. . . . . . . . . . . . . . . . . 18
โข
(({โจ1, 1โฉ, โจ2, (-๐ด / ๐ต)โฉ} โ ๐ โง ยฌ (((๐ด ยท 1) + (๐ต ยท (-๐ด / ๐ต))) = ๐ถ โ 1 = 0)) โ โ๐ โ ๐ ยฌ (((๐ด ยท (๐โ1)) + (๐ต ยท (๐โ2))) = ๐ถ โ (๐โ1) = 0)) |
101 | 64, 83, 100 | syl2anc 584 |
. . . . . . . . . . . . . . . . 17
โข (((๐ด โ โ โง ๐ต โ โ โง ๐ถ โ โ) โง (๐ต โ 0 โง ๐ถ = 0)) โ โ๐ โ ๐ ยฌ (((๐ด ยท (๐โ1)) + (๐ต ยท (๐โ2))) = ๐ถ โ (๐โ1) = 0)) |
102 | 101 | expcom 414 |
. . . . . . . . . . . . . . . 16
โข ((๐ต โ 0 โง ๐ถ = 0) โ ((๐ด โ โ โง ๐ต โ โ โง ๐ถ โ โ) โ โ๐ โ ๐ ยฌ (((๐ด ยท (๐โ1)) + (๐ต ยท (๐โ2))) = ๐ถ โ (๐โ1) = 0))) |
103 | 102 | ex 413 |
. . . . . . . . . . . . . . 15
โข (๐ต โ 0 โ (๐ถ = 0 โ ((๐ด โ โ โง ๐ต โ โ โง ๐ถ โ โ) โ โ๐ โ ๐ ยฌ (((๐ด ยท (๐โ1)) + (๐ต ยท (๐โ2))) = ๐ถ โ (๐โ1) = 0)))) |
104 | 56, 103 | sylbir 234 |
. . . . . . . . . . . . . 14
โข (ยฌ
๐ต = 0 โ (๐ถ = 0 โ ((๐ด โ โ โง ๐ต โ โ โง ๐ถ โ โ) โ โ๐ โ ๐ ยฌ (((๐ด ยท (๐โ1)) + (๐ต ยท (๐โ2))) = ๐ถ โ (๐โ1) = 0)))) |
105 | | notnotb 314 |
. . . . . . . . . . . . . . 15
โข (๐ต = 0 โ ยฌ ยฌ ๐ต = 0) |
106 | | nne 2944 |
. . . . . . . . . . . . . . . 16
โข (ยฌ
๐ด โ 0 โ ๐ด = 0) |
107 | 106 | bicomi 223 |
. . . . . . . . . . . . . . 15
โข (๐ด = 0 โ ยฌ ๐ด โ 0) |
108 | | 1re 11213 |
. . . . . . . . . . . . . . . . . . 19
โข 1 โ
โ |
109 | 4, 5 | prelrrx2 47389 |
. . . . . . . . . . . . . . . . . . 19
โข ((1
โ โ โง 1 โ โ) โ {โจ1, 1โฉ, โจ2,
1โฉ} โ ๐) |
110 | 108, 108,
109 | mp2an 690 |
. . . . . . . . . . . . . . . . . 18
โข {โจ1,
1โฉ, โจ2, 1โฉ} โ ๐ |
111 | | oveq1 7415 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
โข (๐ด = 0 โ (๐ด ยท 1) = (0 ยท
1)) |
112 | 111 | adantl 482 |
. . . . . . . . . . . . . . . . . . . . . . . 24
โข ((๐ต = 0 โง ๐ด = 0) โ (๐ด ยท 1) = (0 ยท
1)) |
113 | | ax-1cn 11167 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
โข 1 โ
โ |
114 | 113 | mul02i 11402 |
. . . . . . . . . . . . . . . . . . . . . . . 24
โข (0
ยท 1) = 0 |
115 | 112, 114 | eqtrdi 2788 |
. . . . . . . . . . . . . . . . . . . . . . 23
โข ((๐ต = 0 โง ๐ด = 0) โ (๐ด ยท 1) = 0) |
116 | | oveq1 7415 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
โข (๐ต = 0 โ (๐ต ยท 1) = (0 ยท
1)) |
117 | 116 | adantr 481 |
. . . . . . . . . . . . . . . . . . . . . . . 24
โข ((๐ต = 0 โง ๐ด = 0) โ (๐ต ยท 1) = (0 ยท
1)) |
118 | 117, 114 | eqtrdi 2788 |
. . . . . . . . . . . . . . . . . . . . . . 23
โข ((๐ต = 0 โง ๐ด = 0) โ (๐ต ยท 1) = 0) |
119 | 115, 118 | oveq12d 7426 |
. . . . . . . . . . . . . . . . . . . . . 22
โข ((๐ต = 0 โง ๐ด = 0) โ ((๐ด ยท 1) + (๐ต ยท 1)) = (0 + 0)) |
120 | 119, 23 | eqtrdi 2788 |
. . . . . . . . . . . . . . . . . . . . 21
โข ((๐ต = 0 โง ๐ด = 0) โ ((๐ด ยท 1) + (๐ต ยท 1)) = 0) |
121 | | id 22 |
. . . . . . . . . . . . . . . . . . . . 21
โข (๐ถ = 0 โ ๐ถ = 0) |
122 | 120, 121 | eqeqan12d 2746 |
. . . . . . . . . . . . . . . . . . . 20
โข (((๐ต = 0 โง ๐ด = 0) โง ๐ถ = 0) โ (((๐ด ยท 1) + (๐ต ยท 1)) = ๐ถ โ 0 = 0)) |
123 | 122 | bibi1d 343 |
. . . . . . . . . . . . . . . . . . 19
โข (((๐ต = 0 โง ๐ด = 0) โง ๐ถ = 0) โ ((((๐ด ยท 1) + (๐ต ยท 1)) = ๐ถ โ 1 = 0) โ (0 = 0 โ 1 =
0))) |
124 | 69, 123 | mtbiri 326 |
. . . . . . . . . . . . . . . . . 18
โข (((๐ต = 0 โง ๐ด = 0) โง ๐ถ = 0) โ ยฌ (((๐ด ยท 1) + (๐ต ยท 1)) = ๐ถ โ 1 = 0)) |
125 | | fveq1 6890 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
โข (๐ = {โจ1, 1โฉ, โจ2,
1โฉ} โ (๐โ1)
= ({โจ1, 1โฉ, โจ2, 1โฉ}โ1)) |
126 | | fvpr1g 7187 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
โข ((1
โ V โง 1 โ V โง 1 โ 2) โ ({โจ1, 1โฉ, โจ2,
1โฉ}โ1) = 1) |
127 | 32, 32, 34, 126 | mp3an 1461 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
โข
({โจ1, 1โฉ, โจ2, 1โฉ}โ1) = 1 |
128 | 125, 127 | eqtrdi 2788 |
. . . . . . . . . . . . . . . . . . . . . . . 24
โข (๐ = {โจ1, 1โฉ, โจ2,
1โฉ} โ (๐โ1)
= 1) |
129 | 128 | oveq2d 7424 |
. . . . . . . . . . . . . . . . . . . . . . 23
โข (๐ = {โจ1, 1โฉ, โจ2,
1โฉ} โ (๐ด ยท
(๐โ1)) = (๐ด ยท 1)) |
130 | | fveq1 6890 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
โข (๐ = {โจ1, 1โฉ, โจ2,
1โฉ} โ (๐โ2)
= ({โจ1, 1โฉ, โจ2, 1โฉ}โ2)) |
131 | | fvpr2g 7188 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
โข ((2
โ V โง 1 โ V โง 1 โ 2) โ ({โจ1, 1โฉ, โจ2,
1โฉ}โ2) = 1) |
132 | 40, 32, 34, 131 | mp3an 1461 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
โข
({โจ1, 1โฉ, โจ2, 1โฉ}โ2) = 1 |
133 | 130, 132 | eqtrdi 2788 |
. . . . . . . . . . . . . . . . . . . . . . . 24
โข (๐ = {โจ1, 1โฉ, โจ2,
1โฉ} โ (๐โ2)
= 1) |
134 | 133 | oveq2d 7424 |
. . . . . . . . . . . . . . . . . . . . . . 23
โข (๐ = {โจ1, 1โฉ, โจ2,
1โฉ} โ (๐ต ยท
(๐โ2)) = (๐ต ยท 1)) |
135 | 129, 134 | oveq12d 7426 |
. . . . . . . . . . . . . . . . . . . . . 22
โข (๐ = {โจ1, 1โฉ, โจ2,
1โฉ} โ ((๐ด
ยท (๐โ1)) +
(๐ต ยท (๐โ2))) = ((๐ด ยท 1) + (๐ต ยท 1))) |
136 | 135 | eqeq1d 2734 |
. . . . . . . . . . . . . . . . . . . . 21
โข (๐ = {โจ1, 1โฉ, โจ2,
1โฉ} โ (((๐ด
ยท (๐โ1)) +
(๐ต ยท (๐โ2))) = ๐ถ โ ((๐ด ยท 1) + (๐ต ยท 1)) = ๐ถ)) |
137 | 128 | eqeq1d 2734 |
. . . . . . . . . . . . . . . . . . . . 21
โข (๐ = {โจ1, 1โฉ, โจ2,
1โฉ} โ ((๐โ1) = 0 โ 1 = 0)) |
138 | 136, 137 | bibi12d 345 |
. . . . . . . . . . . . . . . . . . . 20
โข (๐ = {โจ1, 1โฉ, โจ2,
1โฉ} โ ((((๐ด
ยท (๐โ1)) +
(๐ต ยท (๐โ2))) = ๐ถ โ (๐โ1) = 0) โ (((๐ด ยท 1) + (๐ต ยท 1)) = ๐ถ โ 1 = 0))) |
139 | 138 | notbid 317 |
. . . . . . . . . . . . . . . . . . 19
โข (๐ = {โจ1, 1โฉ, โจ2,
1โฉ} โ (ยฌ (((๐ด
ยท (๐โ1)) +
(๐ต ยท (๐โ2))) = ๐ถ โ (๐โ1) = 0) โ ยฌ (((๐ด ยท 1) + (๐ต ยท 1)) = ๐ถ โ 1 =
0))) |
140 | 139 | rspcev 3612 |
. . . . . . . . . . . . . . . . . 18
โข
(({โจ1, 1โฉ, โจ2, 1โฉ} โ ๐ โง ยฌ (((๐ด ยท 1) + (๐ต ยท 1)) = ๐ถ โ 1 = 0)) โ โ๐ โ ๐ ยฌ (((๐ด ยท (๐โ1)) + (๐ต ยท (๐โ2))) = ๐ถ โ (๐โ1) = 0)) |
141 | 110, 124,
140 | sylancr 587 |
. . . . . . . . . . . . . . . . 17
โข (((๐ต = 0 โง ๐ด = 0) โง ๐ถ = 0) โ โ๐ โ ๐ ยฌ (((๐ด ยท (๐โ1)) + (๐ต ยท (๐โ2))) = ๐ถ โ (๐โ1) = 0)) |
142 | 141 | a1d 25 |
. . . . . . . . . . . . . . . 16
โข (((๐ต = 0 โง ๐ด = 0) โง ๐ถ = 0) โ ((๐ด โ โ โง ๐ต โ โ โง ๐ถ โ โ) โ โ๐ โ ๐ ยฌ (((๐ด ยท (๐โ1)) + (๐ต ยท (๐โ2))) = ๐ถ โ (๐โ1) = 0))) |
143 | 142 | ex 413 |
. . . . . . . . . . . . . . 15
โข ((๐ต = 0 โง ๐ด = 0) โ (๐ถ = 0 โ ((๐ด โ โ โง ๐ต โ โ โง ๐ถ โ โ) โ โ๐ โ ๐ ยฌ (((๐ด ยท (๐โ1)) + (๐ต ยท (๐โ2))) = ๐ถ โ (๐โ1) = 0)))) |
144 | 105, 107,
143 | syl2anbr 599 |
. . . . . . . . . . . . . 14
โข ((ยฌ
ยฌ ๐ต = 0 โง ยฌ
๐ด โ 0) โ (๐ถ = 0 โ ((๐ด โ โ โง ๐ต โ โ โง ๐ถ โ โ) โ โ๐ โ ๐ ยฌ (((๐ด ยท (๐โ1)) + (๐ต ยท (๐โ2))) = ๐ถ โ (๐โ1) = 0)))) |
145 | 104, 144 | jaoi3 1059 |
. . . . . . . . . . . . 13
โข ((ยฌ
๐ต = 0 โจ ยฌ ๐ด โ 0) โ (๐ถ = 0 โ ((๐ด โ โ โง ๐ต โ โ โง ๐ถ โ โ) โ โ๐ โ ๐ ยฌ (((๐ด ยท (๐โ1)) + (๐ต ยท (๐โ2))) = ๐ถ โ (๐โ1) = 0)))) |
146 | 145 | orcoms 870 |
. . . . . . . . . . . 12
โข ((ยฌ
๐ด โ 0 โจ ยฌ ๐ต = 0) โ (๐ถ = 0 โ ((๐ด โ โ โง ๐ต โ โ โง ๐ถ โ โ) โ โ๐ โ ๐ ยฌ (((๐ด ยท (๐โ1)) + (๐ต ยท (๐โ2))) = ๐ถ โ (๐โ1) = 0)))) |
147 | 55, 146 | sylbi 216 |
. . . . . . . . . . 11
โข (ยฌ
(๐ด โ 0 โง ๐ต = 0) โ (๐ถ = 0 โ ((๐ด โ โ โง ๐ต โ โ โง ๐ถ โ โ) โ โ๐ โ ๐ ยฌ (((๐ด ยท (๐โ1)) + (๐ต ยท (๐โ2))) = ๐ถ โ (๐โ1) = 0)))) |
148 | 147 | com12 32 |
. . . . . . . . . 10
โข (๐ถ = 0 โ (ยฌ (๐ด โ 0 โง ๐ต = 0) โ ((๐ด โ โ โง ๐ต โ โ โง ๐ถ โ โ) โ โ๐ โ ๐ ยฌ (((๐ด ยท (๐โ1)) + (๐ต ยท (๐โ2))) = ๐ถ โ (๐โ1) = 0)))) |
149 | 54, 148 | sylbir 234 |
. . . . . . . . 9
โข (ยฌ
ยฌ ๐ถ = 0 โ (ยฌ
(๐ด โ 0 โง ๐ต = 0) โ ((๐ด โ โ โง ๐ต โ โ โง ๐ถ โ โ) โ โ๐ โ ๐ ยฌ (((๐ด ยท (๐โ1)) + (๐ต ยท (๐โ2))) = ๐ถ โ (๐โ1) = 0)))) |
150 | 149 | imp 407 |
. . . . . . . 8
โข ((ยฌ
ยฌ ๐ถ = 0 โง ยฌ
(๐ด โ 0 โง ๐ต = 0)) โ ((๐ด โ โ โง ๐ต โ โ โง ๐ถ โ โ) โ
โ๐ โ ๐ ยฌ (((๐ด ยท (๐โ1)) + (๐ต ยท (๐โ2))) = ๐ถ โ (๐โ1) = 0))) |
151 | 53, 150 | jaoi3 1059 |
. . . . . . 7
โข ((ยฌ
๐ถ = 0 โจ ยฌ (๐ด โ 0 โง ๐ต = 0)) โ ((๐ด โ โ โง ๐ต โ โ โง ๐ถ โ โ) โ โ๐ โ ๐ ยฌ (((๐ด ยท (๐โ1)) + (๐ต ยท (๐โ2))) = ๐ถ โ (๐โ1) = 0))) |
152 | 151 | orcoms 870 |
. . . . . 6
โข ((ยฌ
(๐ด โ 0 โง ๐ต = 0) โจ ยฌ ๐ถ = 0) โ ((๐ด โ โ โง ๐ต โ โ โง ๐ถ โ โ) โ โ๐ โ ๐ ยฌ (((๐ด ยท (๐โ1)) + (๐ต ยท (๐โ2))) = ๐ถ โ (๐โ1) = 0))) |
153 | 152 | com12 32 |
. . . . 5
โข ((๐ด โ โ โง ๐ต โ โ โง ๐ถ โ โ) โ ((ยฌ
(๐ด โ 0 โง ๐ต = 0) โจ ยฌ ๐ถ = 0) โ โ๐ โ ๐ ยฌ (((๐ด ยท (๐โ1)) + (๐ต ยท (๐โ2))) = ๐ถ โ (๐โ1) = 0))) |
154 | 1, 153 | biimtrid 241 |
. . . 4
โข ((๐ด โ โ โง ๐ต โ โ โง ๐ถ โ โ) โ (ยฌ
((๐ด โ 0 โง ๐ต = 0) โง ๐ถ = 0) โ โ๐ โ ๐ ยฌ (((๐ด ยท (๐โ1)) + (๐ต ยท (๐โ2))) = ๐ถ โ (๐โ1) = 0))) |
155 | | rexnal 3100 |
. . . 4
โข
(โ๐ โ
๐ ยฌ (((๐ด ยท (๐โ1)) + (๐ต ยท (๐โ2))) = ๐ถ โ (๐โ1) = 0) โ ยฌ โ๐ โ ๐ (((๐ด ยท (๐โ1)) + (๐ต ยท (๐โ2))) = ๐ถ โ (๐โ1) = 0)) |
156 | 154, 155 | imbitrdi 250 |
. . 3
โข ((๐ด โ โ โง ๐ต โ โ โง ๐ถ โ โ) โ (ยฌ
((๐ด โ 0 โง ๐ต = 0) โง ๐ถ = 0) โ ยฌ โ๐ โ ๐ (((๐ด ยท (๐โ1)) + (๐ต ยท (๐โ2))) = ๐ถ โ (๐โ1) = 0))) |
157 | 156 | con4d 115 |
. 2
โข ((๐ด โ โ โง ๐ต โ โ โง ๐ถ โ โ) โ
(โ๐ โ ๐ (((๐ด ยท (๐โ1)) + (๐ต ยท (๐โ2))) = ๐ถ โ (๐โ1) = 0) โ ((๐ด โ 0 โง ๐ต = 0) โง ๐ถ = 0))) |
158 | | df-3an 1089 |
. 2
โข ((๐ด โ 0 โง ๐ต = 0 โง ๐ถ = 0) โ ((๐ด โ 0 โง ๐ต = 0) โง ๐ถ = 0)) |
159 | 157, 158 | syl6ibr 251 |
1
โข ((๐ด โ โ โง ๐ต โ โ โง ๐ถ โ โ) โ
(โ๐ โ ๐ (((๐ด ยท (๐โ1)) + (๐ต ยท (๐โ2))) = ๐ถ โ (๐โ1) = 0) โ (๐ด โ 0 โง ๐ต = 0 โง ๐ถ = 0))) |