Step | Hyp | Ref
| Expression |
1 | | itscnhlc0yqe.t |
. . . . 5
โข ๐ = -(2 ยท (๐ต ยท ๐ถ)) |
2 | 1 | oveq1i 7371 |
. . . 4
โข (๐โ2) = (-(2 ยท (๐ต ยท ๐ถ))โ2) |
3 | | 2cnd 12239 |
. . . . . . 7
โข (((๐ด โ โ โง ๐ต โ โ โง ๐ถ โ โ) โง ๐
โ โ) โ 2 โ
โ) |
4 | | simpl2 1193 |
. . . . . . . 8
โข (((๐ด โ โ โง ๐ต โ โ โง ๐ถ โ โ) โง ๐
โ โ) โ ๐ต โ
โ) |
5 | | simpl3 1194 |
. . . . . . . 8
โข (((๐ด โ โ โง ๐ต โ โ โง ๐ถ โ โ) โง ๐
โ โ) โ ๐ถ โ
โ) |
6 | 4, 5 | mulcld 11183 |
. . . . . . 7
โข (((๐ด โ โ โง ๐ต โ โ โง ๐ถ โ โ) โง ๐
โ โ) โ (๐ต ยท ๐ถ) โ โ) |
7 | 3, 6 | mulcld 11183 |
. . . . . 6
โข (((๐ด โ โ โง ๐ต โ โ โง ๐ถ โ โ) โง ๐
โ โ) โ (2
ยท (๐ต ยท ๐ถ)) โ
โ) |
8 | | sqneg 14030 |
. . . . . 6
โข ((2
ยท (๐ต ยท ๐ถ)) โ โ โ (-(2
ยท (๐ต ยท ๐ถ))โ2) = ((2 ยท (๐ต ยท ๐ถ))โ2)) |
9 | 7, 8 | syl 17 |
. . . . 5
โข (((๐ด โ โ โง ๐ต โ โ โง ๐ถ โ โ) โง ๐
โ โ) โ (-(2
ยท (๐ต ยท ๐ถ))โ2) = ((2 ยท (๐ต ยท ๐ถ))โ2)) |
10 | 3, 6 | sqmuld 14072 |
. . . . 5
โข (((๐ด โ โ โง ๐ต โ โ โง ๐ถ โ โ) โง ๐
โ โ) โ ((2
ยท (๐ต ยท ๐ถ))โ2) = ((2โ2)
ยท ((๐ต ยท ๐ถ)โ2))) |
11 | | sq2 14110 |
. . . . . . 7
โข
(2โ2) = 4 |
12 | 11 | a1i 11 |
. . . . . 6
โข (((๐ด โ โ โง ๐ต โ โ โง ๐ถ โ โ) โง ๐
โ โ) โ
(2โ2) = 4) |
13 | 4, 5 | sqmuld 14072 |
. . . . . 6
โข (((๐ด โ โ โง ๐ต โ โ โง ๐ถ โ โ) โง ๐
โ โ) โ ((๐ต ยท ๐ถ)โ2) = ((๐ตโ2) ยท (๐ถโ2))) |
14 | 12, 13 | oveq12d 7379 |
. . . . 5
โข (((๐ด โ โ โง ๐ต โ โ โง ๐ถ โ โ) โง ๐
โ โ) โ
((2โ2) ยท ((๐ต
ยท ๐ถ)โ2)) = (4
ยท ((๐ตโ2)
ยท (๐ถโ2)))) |
15 | 9, 10, 14 | 3eqtrd 2777 |
. . . 4
โข (((๐ด โ โ โง ๐ต โ โ โง ๐ถ โ โ) โง ๐
โ โ) โ (-(2
ยท (๐ต ยท ๐ถ))โ2) = (4 ยท ((๐ตโ2) ยท (๐ถโ2)))) |
16 | 2, 15 | eqtrid 2785 |
. . 3
โข (((๐ด โ โ โง ๐ต โ โ โง ๐ถ โ โ) โง ๐
โ โ) โ (๐โ2) = (4 ยท ((๐ตโ2) ยท (๐ถโ2)))) |
17 | | itscnhlc0yqe.q |
. . . . . 6
โข ๐ = ((๐ดโ2) + (๐ตโ2)) |
18 | | itscnhlc0yqe.u |
. . . . . 6
โข ๐ = ((๐ถโ2) โ ((๐ดโ2) ยท (๐
โ2))) |
19 | 17, 18 | oveq12i 7373 |
. . . . 5
โข (๐ ยท ๐) = (((๐ดโ2) + (๐ตโ2)) ยท ((๐ถโ2) โ ((๐ดโ2) ยท (๐
โ2)))) |
20 | | simpl1 1192 |
. . . . . . . . 9
โข (((๐ด โ โ โง ๐ต โ โ โง ๐ถ โ โ) โง ๐
โ โ) โ ๐ด โ
โ) |
21 | 20 | sqcld 14058 |
. . . . . . . 8
โข (((๐ด โ โ โง ๐ต โ โ โง ๐ถ โ โ) โง ๐
โ โ) โ (๐ดโ2) โ
โ) |
22 | 4 | sqcld 14058 |
. . . . . . . 8
โข (((๐ด โ โ โง ๐ต โ โ โง ๐ถ โ โ) โง ๐
โ โ) โ (๐ตโ2) โ
โ) |
23 | 21, 22 | addcld 11182 |
. . . . . . 7
โข (((๐ด โ โ โง ๐ต โ โ โง ๐ถ โ โ) โง ๐
โ โ) โ ((๐ดโ2) + (๐ตโ2)) โ โ) |
24 | 5 | sqcld 14058 |
. . . . . . 7
โข (((๐ด โ โ โง ๐ต โ โ โง ๐ถ โ โ) โง ๐
โ โ) โ (๐ถโ2) โ
โ) |
25 | | simpr 486 |
. . . . . . . . 9
โข (((๐ด โ โ โง ๐ต โ โ โง ๐ถ โ โ) โง ๐
โ โ) โ ๐
โ
โ) |
26 | 25 | sqcld 14058 |
. . . . . . . 8
โข (((๐ด โ โ โง ๐ต โ โ โง ๐ถ โ โ) โง ๐
โ โ) โ (๐
โ2) โ
โ) |
27 | 21, 26 | mulcld 11183 |
. . . . . . 7
โข (((๐ด โ โ โง ๐ต โ โ โง ๐ถ โ โ) โง ๐
โ โ) โ ((๐ดโ2) ยท (๐
โ2)) โ
โ) |
28 | 23, 24, 27 | subdid 11619 |
. . . . . 6
โข (((๐ด โ โ โง ๐ต โ โ โง ๐ถ โ โ) โง ๐
โ โ) โ (((๐ดโ2) + (๐ตโ2)) ยท ((๐ถโ2) โ ((๐ดโ2) ยท (๐
โ2)))) = ((((๐ดโ2) + (๐ตโ2)) ยท (๐ถโ2)) โ (((๐ดโ2) + (๐ตโ2)) ยท ((๐ดโ2) ยท (๐
โ2))))) |
29 | 21, 22, 24 | adddird 11188 |
. . . . . . 7
โข (((๐ด โ โ โง ๐ต โ โ โง ๐ถ โ โ) โง ๐
โ โ) โ (((๐ดโ2) + (๐ตโ2)) ยท (๐ถโ2)) = (((๐ดโ2) ยท (๐ถโ2)) + ((๐ตโ2) ยท (๐ถโ2)))) |
30 | 21, 22, 27 | adddird 11188 |
. . . . . . 7
โข (((๐ด โ โ โง ๐ต โ โ โง ๐ถ โ โ) โง ๐
โ โ) โ (((๐ดโ2) + (๐ตโ2)) ยท ((๐ดโ2) ยท (๐
โ2))) = (((๐ดโ2) ยท ((๐ดโ2) ยท (๐
โ2))) + ((๐ตโ2) ยท ((๐ดโ2) ยท (๐
โ2))))) |
31 | 29, 30 | oveq12d 7379 |
. . . . . 6
โข (((๐ด โ โ โง ๐ต โ โ โง ๐ถ โ โ) โง ๐
โ โ) โ
((((๐ดโ2) + (๐ตโ2)) ยท (๐ถโ2)) โ (((๐ดโ2) + (๐ตโ2)) ยท ((๐ดโ2) ยท (๐
โ2)))) = ((((๐ดโ2) ยท (๐ถโ2)) + ((๐ตโ2) ยท (๐ถโ2))) โ (((๐ดโ2) ยท ((๐ดโ2) ยท (๐
โ2))) + ((๐ตโ2) ยท ((๐ดโ2) ยท (๐
โ2)))))) |
32 | 22, 24 | mulcld 11183 |
. . . . . . 7
โข (((๐ด โ โ โง ๐ต โ โ โง ๐ถ โ โ) โง ๐
โ โ) โ ((๐ตโ2) ยท (๐ถโ2)) โ
โ) |
33 | 21, 24 | mulcld 11183 |
. . . . . . 7
โข (((๐ด โ โ โง ๐ต โ โ โง ๐ถ โ โ) โง ๐
โ โ) โ ((๐ดโ2) ยท (๐ถโ2)) โ
โ) |
34 | 21, 27 | mulcld 11183 |
. . . . . . . 8
โข (((๐ด โ โ โง ๐ต โ โ โง ๐ถ โ โ) โง ๐
โ โ) โ ((๐ดโ2) ยท ((๐ดโ2) ยท (๐
โ2))) โ
โ) |
35 | 22, 26 | mulcld 11183 |
. . . . . . . . 9
โข (((๐ด โ โ โง ๐ต โ โ โง ๐ถ โ โ) โง ๐
โ โ) โ ((๐ตโ2) ยท (๐
โ2)) โ
โ) |
36 | 21, 35 | mulcld 11183 |
. . . . . . . 8
โข (((๐ด โ โ โง ๐ต โ โ โง ๐ถ โ โ) โง ๐
โ โ) โ ((๐ดโ2) ยท ((๐ตโ2) ยท (๐
โ2))) โ
โ) |
37 | 34, 36 | addcld 11182 |
. . . . . . 7
โข (((๐ด โ โ โง ๐ต โ โ โง ๐ถ โ โ) โง ๐
โ โ) โ (((๐ดโ2) ยท ((๐ดโ2) ยท (๐
โ2))) + ((๐ดโ2) ยท ((๐ตโ2) ยท (๐
โ2)))) โ โ) |
38 | 33, 32 | addcomd 11365 |
. . . . . . . 8
โข (((๐ด โ โ โง ๐ต โ โ โง ๐ถ โ โ) โง ๐
โ โ) โ (((๐ดโ2) ยท (๐ถโ2)) + ((๐ตโ2) ยท (๐ถโ2))) = (((๐ตโ2) ยท (๐ถโ2)) + ((๐ดโ2) ยท (๐ถโ2)))) |
39 | 22, 21, 26 | mul12d 11372 |
. . . . . . . . 9
โข (((๐ด โ โ โง ๐ต โ โ โง ๐ถ โ โ) โง ๐
โ โ) โ ((๐ตโ2) ยท ((๐ดโ2) ยท (๐
โ2))) = ((๐ดโ2) ยท ((๐ตโ2) ยท (๐
โ2)))) |
40 | 39 | oveq2d 7377 |
. . . . . . . 8
โข (((๐ด โ โ โง ๐ต โ โ โง ๐ถ โ โ) โง ๐
โ โ) โ (((๐ดโ2) ยท ((๐ดโ2) ยท (๐
โ2))) + ((๐ตโ2) ยท ((๐ดโ2) ยท (๐
โ2)))) = (((๐ดโ2) ยท ((๐ดโ2) ยท (๐
โ2))) + ((๐ดโ2) ยท ((๐ตโ2) ยท (๐
โ2))))) |
41 | 38, 40 | oveq12d 7379 |
. . . . . . 7
โข (((๐ด โ โ โง ๐ต โ โ โง ๐ถ โ โ) โง ๐
โ โ) โ
((((๐ดโ2) ยท
(๐ถโ2)) + ((๐ตโ2) ยท (๐ถโ2))) โ (((๐ดโ2) ยท ((๐ดโ2) ยท (๐
โ2))) + ((๐ตโ2) ยท ((๐ดโ2) ยท (๐
โ2))))) = ((((๐ตโ2) ยท (๐ถโ2)) + ((๐ดโ2) ยท (๐ถโ2))) โ (((๐ดโ2) ยท ((๐ดโ2) ยท (๐
โ2))) + ((๐ดโ2) ยท ((๐ตโ2) ยท (๐
โ2)))))) |
42 | 32, 33, 37, 41 | assraddsubd 11577 |
. . . . . 6
โข (((๐ด โ โ โง ๐ต โ โ โง ๐ถ โ โ) โง ๐
โ โ) โ
((((๐ดโ2) ยท
(๐ถโ2)) + ((๐ตโ2) ยท (๐ถโ2))) โ (((๐ดโ2) ยท ((๐ดโ2) ยท (๐
โ2))) + ((๐ตโ2) ยท ((๐ดโ2) ยท (๐
โ2))))) = (((๐ตโ2) ยท (๐ถโ2)) + (((๐ดโ2) ยท (๐ถโ2)) โ (((๐ดโ2) ยท ((๐ดโ2) ยท (๐
โ2))) + ((๐ดโ2) ยท ((๐ตโ2) ยท (๐
โ2))))))) |
43 | 28, 31, 42 | 3eqtrd 2777 |
. . . . 5
โข (((๐ด โ โ โง ๐ต โ โ โง ๐ถ โ โ) โง ๐
โ โ) โ (((๐ดโ2) + (๐ตโ2)) ยท ((๐ถโ2) โ ((๐ดโ2) ยท (๐
โ2)))) = (((๐ตโ2) ยท (๐ถโ2)) + (((๐ดโ2) ยท (๐ถโ2)) โ (((๐ดโ2) ยท ((๐ดโ2) ยท (๐
โ2))) + ((๐ดโ2) ยท ((๐ตโ2) ยท (๐
โ2))))))) |
44 | 19, 43 | eqtrid 2785 |
. . . 4
โข (((๐ด โ โ โง ๐ต โ โ โง ๐ถ โ โ) โง ๐
โ โ) โ (๐ ยท ๐) = (((๐ตโ2) ยท (๐ถโ2)) + (((๐ดโ2) ยท (๐ถโ2)) โ (((๐ดโ2) ยท ((๐ดโ2) ยท (๐
โ2))) + ((๐ดโ2) ยท ((๐ตโ2) ยท (๐
โ2))))))) |
45 | 44 | oveq2d 7377 |
. . 3
โข (((๐ด โ โ โง ๐ต โ โ โง ๐ถ โ โ) โง ๐
โ โ) โ (4
ยท (๐ ยท ๐)) = (4 ยท (((๐ตโ2) ยท (๐ถโ2)) + (((๐ดโ2) ยท (๐ถโ2)) โ (((๐ดโ2) ยท ((๐ดโ2) ยท (๐
โ2))) + ((๐ดโ2) ยท ((๐ตโ2) ยท (๐
โ2)))))))) |
46 | 16, 45 | oveq12d 7379 |
. 2
โข (((๐ด โ โ โง ๐ต โ โ โง ๐ถ โ โ) โง ๐
โ โ) โ ((๐โ2) โ (4 ยท
(๐ ยท ๐))) = ((4 ยท ((๐ตโ2) ยท (๐ถโ2))) โ (4 ยท
(((๐ตโ2) ยท
(๐ถโ2)) + (((๐ดโ2) ยท (๐ถโ2)) โ (((๐ดโ2) ยท ((๐ดโ2) ยท (๐
โ2))) + ((๐ดโ2) ยท ((๐ตโ2) ยท (๐
โ2))))))))) |
47 | | 4cn 12246 |
. . . . 5
โข 4 โ
โ |
48 | 47 | a1i 11 |
. . . 4
โข (((๐ด โ โ โง ๐ต โ โ โง ๐ถ โ โ) โง ๐
โ โ) โ 4 โ
โ) |
49 | | simp1 1137 |
. . . . . 6
โข ((๐ด โ โ โง ๐ต โ โ โง ๐ถ โ โ) โ ๐ด โ
โ) |
50 | 49 | sqcld 14058 |
. . . . 5
โข ((๐ด โ โ โง ๐ต โ โ โง ๐ถ โ โ) โ (๐ดโ2) โ
โ) |
51 | 50 | adantr 482 |
. . . 4
โข (((๐ด โ โ โง ๐ต โ โ โง ๐ถ โ โ) โง ๐
โ โ) โ (๐ดโ2) โ
โ) |
52 | | itsclc0yqsollem1.d |
. . . . 5
โข ๐ท = (((๐
โ2) ยท ๐) โ (๐ถโ2)) |
53 | 17, 23 | eqeltrid 2838 |
. . . . . . 7
โข (((๐ด โ โ โง ๐ต โ โ โง ๐ถ โ โ) โง ๐
โ โ) โ ๐ โ
โ) |
54 | 26, 53 | mulcld 11183 |
. . . . . 6
โข (((๐ด โ โ โง ๐ต โ โ โง ๐ถ โ โ) โง ๐
โ โ) โ ((๐
โ2) ยท ๐) โ
โ) |
55 | 54, 24 | subcld 11520 |
. . . . 5
โข (((๐ด โ โ โง ๐ต โ โ โง ๐ถ โ โ) โง ๐
โ โ) โ (((๐
โ2) ยท ๐) โ (๐ถโ2)) โ โ) |
56 | 52, 55 | eqeltrid 2838 |
. . . 4
โข (((๐ด โ โ โง ๐ต โ โ โง ๐ถ โ โ) โง ๐
โ โ) โ ๐ท โ
โ) |
57 | 48, 51, 56 | mulassd 11186 |
. . 3
โข (((๐ด โ โ โง ๐ต โ โ โง ๐ถ โ โ) โง ๐
โ โ) โ ((4
ยท (๐ดโ2))
ยท ๐ท) = (4 ยท
((๐ดโ2) ยท ๐ท))) |
58 | 33, 37 | subcld 11520 |
. . . . . . 7
โข (((๐ด โ โ โง ๐ต โ โ โง ๐ถ โ โ) โง ๐
โ โ) โ (((๐ดโ2) ยท (๐ถโ2)) โ (((๐ดโ2) ยท ((๐ดโ2) ยท (๐
โ2))) + ((๐ดโ2) ยท ((๐ตโ2) ยท (๐
โ2))))) โ
โ) |
59 | 32, 32, 58 | subsub4d 11551 |
. . . . . 6
โข (((๐ด โ โ โง ๐ต โ โ โง ๐ถ โ โ) โง ๐
โ โ) โ
((((๐ตโ2) ยท
(๐ถโ2)) โ ((๐ตโ2) ยท (๐ถโ2))) โ (((๐ดโ2) ยท (๐ถโ2)) โ (((๐ดโ2) ยท ((๐ดโ2) ยท (๐
โ2))) + ((๐ดโ2) ยท ((๐ตโ2) ยท (๐
โ2)))))) = (((๐ตโ2) ยท (๐ถโ2)) โ (((๐ตโ2) ยท (๐ถโ2)) + (((๐ดโ2) ยท (๐ถโ2)) โ (((๐ดโ2) ยท ((๐ดโ2) ยท (๐
โ2))) + ((๐ดโ2) ยท ((๐ตโ2) ยท (๐
โ2)))))))) |
60 | 32 | subidd 11508 |
. . . . . . . 8
โข (((๐ด โ โ โง ๐ต โ โ โง ๐ถ โ โ) โง ๐
โ โ) โ (((๐ตโ2) ยท (๐ถโ2)) โ ((๐ตโ2) ยท (๐ถโ2))) = 0) |
61 | 60 | oveq1d 7376 |
. . . . . . 7
โข (((๐ด โ โ โง ๐ต โ โ โง ๐ถ โ โ) โง ๐
โ โ) โ
((((๐ตโ2) ยท
(๐ถโ2)) โ ((๐ตโ2) ยท (๐ถโ2))) โ (((๐ดโ2) ยท (๐ถโ2)) โ (((๐ดโ2) ยท ((๐ดโ2) ยท (๐
โ2))) + ((๐ดโ2) ยท ((๐ตโ2) ยท (๐
โ2)))))) = (0 โ (((๐ดโ2) ยท (๐ถโ2)) โ (((๐ดโ2) ยท ((๐ดโ2) ยท (๐
โ2))) + ((๐ดโ2) ยท ((๐ตโ2) ยท (๐
โ2))))))) |
62 | | 0cnd 11156 |
. . . . . . . 8
โข (((๐ด โ โ โง ๐ต โ โ โง ๐ถ โ โ) โง ๐
โ โ) โ 0 โ
โ) |
63 | 62, 33, 37 | subsub2d 11549 |
. . . . . . 7
โข (((๐ด โ โ โง ๐ต โ โ โง ๐ถ โ โ) โง ๐
โ โ) โ (0
โ (((๐ดโ2)
ยท (๐ถโ2))
โ (((๐ดโ2)
ยท ((๐ดโ2)
ยท (๐
โ2))) +
((๐ดโ2) ยท
((๐ตโ2) ยท (๐
โ2)))))) = (0 + ((((๐ดโ2) ยท ((๐ดโ2) ยท (๐
โ2))) + ((๐ดโ2) ยท ((๐ตโ2) ยท (๐
โ2)))) โ ((๐ดโ2) ยท (๐ถโ2))))) |
64 | 37, 33 | subcld 11520 |
. . . . . . . 8
โข (((๐ด โ โ โง ๐ต โ โ โง ๐ถ โ โ) โง ๐
โ โ) โ
((((๐ดโ2) ยท
((๐ดโ2) ยท (๐
โ2))) + ((๐ดโ2) ยท ((๐ตโ2) ยท (๐
โ2)))) โ ((๐ดโ2) ยท (๐ถโ2))) โ โ) |
65 | 64 | addlidd 11364 |
. . . . . . 7
โข (((๐ด โ โ โง ๐ต โ โ โง ๐ถ โ โ) โง ๐
โ โ) โ (0 +
((((๐ดโ2) ยท
((๐ดโ2) ยท (๐
โ2))) + ((๐ดโ2) ยท ((๐ตโ2) ยท (๐
โ2)))) โ ((๐ดโ2) ยท (๐ถโ2)))) = ((((๐ดโ2) ยท ((๐ดโ2) ยท (๐
โ2))) + ((๐ดโ2) ยท ((๐ตโ2) ยท (๐
โ2)))) โ ((๐ดโ2) ยท (๐ถโ2)))) |
66 | 61, 63, 65 | 3eqtrd 2777 |
. . . . . 6
โข (((๐ด โ โ โง ๐ต โ โ โง ๐ถ โ โ) โง ๐
โ โ) โ
((((๐ตโ2) ยท
(๐ถโ2)) โ ((๐ตโ2) ยท (๐ถโ2))) โ (((๐ดโ2) ยท (๐ถโ2)) โ (((๐ดโ2) ยท ((๐ดโ2) ยท (๐
โ2))) + ((๐ดโ2) ยท ((๐ตโ2) ยท (๐
โ2)))))) = ((((๐ดโ2) ยท ((๐ดโ2) ยท (๐
โ2))) + ((๐ดโ2) ยท ((๐ตโ2) ยท (๐
โ2)))) โ ((๐ดโ2) ยท (๐ถโ2)))) |
67 | 59, 66 | eqtr3d 2775 |
. . . . 5
โข (((๐ด โ โ โง ๐ต โ โ โง ๐ถ โ โ) โง ๐
โ โ) โ (((๐ตโ2) ยท (๐ถโ2)) โ (((๐ตโ2) ยท (๐ถโ2)) + (((๐ดโ2) ยท (๐ถโ2)) โ (((๐ดโ2) ยท ((๐ดโ2) ยท (๐
โ2))) + ((๐ดโ2) ยท ((๐ตโ2) ยท (๐
โ2))))))) = ((((๐ดโ2) ยท ((๐ดโ2) ยท (๐
โ2))) + ((๐ดโ2) ยท ((๐ตโ2) ยท (๐
โ2)))) โ ((๐ดโ2) ยท (๐ถโ2)))) |
68 | 21, 27, 35 | adddid 11187 |
. . . . . . . 8
โข (((๐ด โ โ โง ๐ต โ โ โง ๐ถ โ โ) โง ๐
โ โ) โ ((๐ดโ2) ยท (((๐ดโ2) ยท (๐
โ2)) + ((๐ตโ2) ยท (๐
โ2)))) = (((๐ดโ2) ยท ((๐ดโ2) ยท (๐
โ2))) + ((๐ดโ2) ยท ((๐ตโ2) ยท (๐
โ2))))) |
69 | 21, 22, 26 | adddird 11188 |
. . . . . . . . . 10
โข (((๐ด โ โ โง ๐ต โ โ โง ๐ถ โ โ) โง ๐
โ โ) โ (((๐ดโ2) + (๐ตโ2)) ยท (๐
โ2)) = (((๐ดโ2) ยท (๐
โ2)) + ((๐ตโ2) ยท (๐
โ2)))) |
70 | 69 | eqcomd 2739 |
. . . . . . . . 9
โข (((๐ด โ โ โง ๐ต โ โ โง ๐ถ โ โ) โง ๐
โ โ) โ (((๐ดโ2) ยท (๐
โ2)) + ((๐ตโ2) ยท (๐
โ2))) = (((๐ดโ2) + (๐ตโ2)) ยท (๐
โ2))) |
71 | 70 | oveq2d 7377 |
. . . . . . . 8
โข (((๐ด โ โ โง ๐ต โ โ โง ๐ถ โ โ) โง ๐
โ โ) โ ((๐ดโ2) ยท (((๐ดโ2) ยท (๐
โ2)) + ((๐ตโ2) ยท (๐
โ2)))) = ((๐ดโ2) ยท (((๐ดโ2) + (๐ตโ2)) ยท (๐
โ2)))) |
72 | 68, 71 | eqtr3d 2775 |
. . . . . . 7
โข (((๐ด โ โ โง ๐ต โ โ โง ๐ถ โ โ) โง ๐
โ โ) โ (((๐ดโ2) ยท ((๐ดโ2) ยท (๐
โ2))) + ((๐ดโ2) ยท ((๐ตโ2) ยท (๐
โ2)))) = ((๐ดโ2) ยท (((๐ดโ2) + (๐ตโ2)) ยท (๐
โ2)))) |
73 | 72 | oveq1d 7376 |
. . . . . 6
โข (((๐ด โ โ โง ๐ต โ โ โง ๐ถ โ โ) โง ๐
โ โ) โ
((((๐ดโ2) ยท
((๐ดโ2) ยท (๐
โ2))) + ((๐ดโ2) ยท ((๐ตโ2) ยท (๐
โ2)))) โ ((๐ดโ2) ยท (๐ถโ2))) = (((๐ดโ2) ยท (((๐ดโ2) + (๐ตโ2)) ยท (๐
โ2))) โ ((๐ดโ2) ยท (๐ถโ2)))) |
74 | 23, 26 | mulcld 11183 |
. . . . . . 7
โข (((๐ด โ โ โง ๐ต โ โ โง ๐ถ โ โ) โง ๐
โ โ) โ (((๐ดโ2) + (๐ตโ2)) ยท (๐
โ2)) โ โ) |
75 | 21, 74, 24 | subdid 11619 |
. . . . . 6
โข (((๐ด โ โ โง ๐ต โ โ โง ๐ถ โ โ) โง ๐
โ โ) โ ((๐ดโ2) ยท ((((๐ดโ2) + (๐ตโ2)) ยท (๐
โ2)) โ (๐ถโ2))) = (((๐ดโ2) ยท (((๐ดโ2) + (๐ตโ2)) ยท (๐
โ2))) โ ((๐ดโ2) ยท (๐ถโ2)))) |
76 | 73, 75 | eqtr4d 2776 |
. . . . 5
โข (((๐ด โ โ โง ๐ต โ โ โง ๐ถ โ โ) โง ๐
โ โ) โ
((((๐ดโ2) ยท
((๐ดโ2) ยท (๐
โ2))) + ((๐ดโ2) ยท ((๐ตโ2) ยท (๐
โ2)))) โ ((๐ดโ2) ยท (๐ถโ2))) = ((๐ดโ2) ยท ((((๐ดโ2) + (๐ตโ2)) ยท (๐
โ2)) โ (๐ถโ2)))) |
77 | 17 | a1i 11 |
. . . . . . . . . . 11
โข (((๐ด โ โ โง ๐ต โ โ โง ๐ถ โ โ) โง ๐
โ โ) โ ๐ = ((๐ดโ2) + (๐ตโ2))) |
78 | 77 | oveq2d 7377 |
. . . . . . . . . 10
โข (((๐ด โ โ โง ๐ต โ โ โง ๐ถ โ โ) โง ๐
โ โ) โ ((๐
โ2) ยท ๐) = ((๐
โ2) ยท ((๐ดโ2) + (๐ตโ2)))) |
79 | 26, 23 | mulcomd 11184 |
. . . . . . . . . 10
โข (((๐ด โ โ โง ๐ต โ โ โง ๐ถ โ โ) โง ๐
โ โ) โ ((๐
โ2) ยท ((๐ดโ2) + (๐ตโ2))) = (((๐ดโ2) + (๐ตโ2)) ยท (๐
โ2))) |
80 | 78, 79 | eqtrd 2773 |
. . . . . . . . 9
โข (((๐ด โ โ โง ๐ต โ โ โง ๐ถ โ โ) โง ๐
โ โ) โ ((๐
โ2) ยท ๐) = (((๐ดโ2) + (๐ตโ2)) ยท (๐
โ2))) |
81 | 80 | oveq1d 7376 |
. . . . . . . 8
โข (((๐ด โ โ โง ๐ต โ โ โง ๐ถ โ โ) โง ๐
โ โ) โ (((๐
โ2) ยท ๐) โ (๐ถโ2)) = ((((๐ดโ2) + (๐ตโ2)) ยท (๐
โ2)) โ (๐ถโ2))) |
82 | 52, 81 | eqtrid 2785 |
. . . . . . 7
โข (((๐ด โ โ โง ๐ต โ โ โง ๐ถ โ โ) โง ๐
โ โ) โ ๐ท = ((((๐ดโ2) + (๐ตโ2)) ยท (๐
โ2)) โ (๐ถโ2))) |
83 | 82 | eqcomd 2739 |
. . . . . 6
โข (((๐ด โ โ โง ๐ต โ โ โง ๐ถ โ โ) โง ๐
โ โ) โ
((((๐ดโ2) + (๐ตโ2)) ยท (๐
โ2)) โ (๐ถโ2)) = ๐ท) |
84 | 83 | oveq2d 7377 |
. . . . 5
โข (((๐ด โ โ โง ๐ต โ โ โง ๐ถ โ โ) โง ๐
โ โ) โ ((๐ดโ2) ยท ((((๐ดโ2) + (๐ตโ2)) ยท (๐
โ2)) โ (๐ถโ2))) = ((๐ดโ2) ยท ๐ท)) |
85 | 67, 76, 84 | 3eqtrd 2777 |
. . . 4
โข (((๐ด โ โ โง ๐ต โ โ โง ๐ถ โ โ) โง ๐
โ โ) โ (((๐ตโ2) ยท (๐ถโ2)) โ (((๐ตโ2) ยท (๐ถโ2)) + (((๐ดโ2) ยท (๐ถโ2)) โ (((๐ดโ2) ยท ((๐ดโ2) ยท (๐
โ2))) + ((๐ดโ2) ยท ((๐ตโ2) ยท (๐
โ2))))))) = ((๐ดโ2) ยท ๐ท)) |
86 | 85 | oveq2d 7377 |
. . 3
โข (((๐ด โ โ โง ๐ต โ โ โง ๐ถ โ โ) โง ๐
โ โ) โ (4
ยท (((๐ตโ2)
ยท (๐ถโ2))
โ (((๐ตโ2)
ยท (๐ถโ2)) +
(((๐ดโ2) ยท
(๐ถโ2)) โ
(((๐ดโ2) ยท
((๐ดโ2) ยท (๐
โ2))) + ((๐ดโ2) ยท ((๐ตโ2) ยท (๐
โ2)))))))) = (4 ยท ((๐ดโ2) ยท ๐ท))) |
87 | 32, 58 | addcld 11182 |
. . . 4
โข (((๐ด โ โ โง ๐ต โ โ โง ๐ถ โ โ) โง ๐
โ โ) โ (((๐ตโ2) ยท (๐ถโ2)) + (((๐ดโ2) ยท (๐ถโ2)) โ (((๐ดโ2) ยท ((๐ดโ2) ยท (๐
โ2))) + ((๐ดโ2) ยท ((๐ตโ2) ยท (๐
โ2)))))) โ
โ) |
88 | 48, 32, 87 | subdid 11619 |
. . 3
โข (((๐ด โ โ โง ๐ต โ โ โง ๐ถ โ โ) โง ๐
โ โ) โ (4
ยท (((๐ตโ2)
ยท (๐ถโ2))
โ (((๐ตโ2)
ยท (๐ถโ2)) +
(((๐ดโ2) ยท
(๐ถโ2)) โ
(((๐ดโ2) ยท
((๐ดโ2) ยท (๐
โ2))) + ((๐ดโ2) ยท ((๐ตโ2) ยท (๐
โ2)))))))) = ((4 ยท ((๐ตโ2) ยท (๐ถโ2))) โ (4 ยท
(((๐ตโ2) ยท
(๐ถโ2)) + (((๐ดโ2) ยท (๐ถโ2)) โ (((๐ดโ2) ยท ((๐ดโ2) ยท (๐
โ2))) + ((๐ดโ2) ยท ((๐ตโ2) ยท (๐
โ2))))))))) |
89 | 57, 86, 88 | 3eqtr2rd 2780 |
. 2
โข (((๐ด โ โ โง ๐ต โ โ โง ๐ถ โ โ) โง ๐
โ โ) โ ((4
ยท ((๐ตโ2)
ยท (๐ถโ2)))
โ (4 ยท (((๐ตโ2) ยท (๐ถโ2)) + (((๐ดโ2) ยท (๐ถโ2)) โ (((๐ดโ2) ยท ((๐ดโ2) ยท (๐
โ2))) + ((๐ดโ2) ยท ((๐ตโ2) ยท (๐
โ2)))))))) = ((4 ยท (๐ดโ2)) ยท ๐ท)) |
90 | 46, 89 | eqtrd 2773 |
1
โข (((๐ด โ โ โง ๐ต โ โ โง ๐ถ โ โ) โง ๐
โ โ) โ ((๐โ2) โ (4 ยท
(๐ ยท ๐))) = ((4 ยท (๐ดโ2)) ยท ๐ท)) |