Step | Hyp | Ref
| Expression |
1 | | cyccom.y |
. 2
โข (๐ โ ๐ โ ๐ถ) |
2 | | cyccom.x |
. 2
โข (๐ โ ๐ โ ๐ถ) |
3 | | cyccom.c |
. . . 4
โข (๐ โ โ๐ โ ๐ถ โ๐ฅ โ ๐ ๐ = (๐ฅ ยท ๐ด)) |
4 | | eqeq1 2741 |
. . . . . 6
โข (๐ = ๐ โ (๐ = (๐ฅ ยท ๐ด) โ ๐ = (๐ฅ ยท ๐ด))) |
5 | 4 | rexbidv 3176 |
. . . . 5
โข (๐ = ๐ โ (โ๐ฅ โ ๐ ๐ = (๐ฅ ยท ๐ด) โ โ๐ฅ โ ๐ ๐ = (๐ฅ ยท ๐ด))) |
6 | 5 | rspccv 3579 |
. . . 4
โข
(โ๐ โ
๐ถ โ๐ฅ โ ๐ ๐ = (๐ฅ ยท ๐ด) โ (๐ โ ๐ถ โ โ๐ฅ โ ๐ ๐ = (๐ฅ ยท ๐ด))) |
7 | 3, 6 | syl 17 |
. . 3
โข (๐ โ (๐ โ ๐ถ โ โ๐ฅ โ ๐ ๐ = (๐ฅ ยท ๐ด))) |
8 | | eqeq1 2741 |
. . . . . . . 8
โข (๐ = ๐ โ (๐ = (๐ฅ ยท ๐ด) โ ๐ = (๐ฅ ยท ๐ด))) |
9 | 8 | rexbidv 3176 |
. . . . . . 7
โข (๐ = ๐ โ (โ๐ฅ โ ๐ ๐ = (๐ฅ ยท ๐ด) โ โ๐ฅ โ ๐ ๐ = (๐ฅ ยท ๐ด))) |
10 | 9 | rspccv 3579 |
. . . . . 6
โข
(โ๐ โ
๐ถ โ๐ฅ โ ๐ ๐ = (๐ฅ ยท ๐ด) โ (๐ โ ๐ถ โ โ๐ฅ โ ๐ ๐ = (๐ฅ ยท ๐ด))) |
11 | 3, 10 | syl 17 |
. . . . 5
โข (๐ โ (๐ โ ๐ถ โ โ๐ฅ โ ๐ ๐ = (๐ฅ ยท ๐ด))) |
12 | | oveq1 7365 |
. . . . . . . 8
โข (๐ฅ = ๐ฆ โ (๐ฅ ยท ๐ด) = (๐ฆ ยท ๐ด)) |
13 | 12 | eqeq2d 2748 |
. . . . . . 7
โข (๐ฅ = ๐ฆ โ (๐ = (๐ฅ ยท ๐ด) โ ๐ = (๐ฆ ยท ๐ด))) |
14 | 13 | cbvrexvw 3227 |
. . . . . 6
โข
(โ๐ฅ โ
๐ ๐ = (๐ฅ ยท ๐ด) โ โ๐ฆ โ ๐ ๐ = (๐ฆ ยท ๐ด)) |
15 | | reeanv 3218 |
. . . . . . . 8
โข
(โ๐ฅ โ
๐ โ๐ฆ โ ๐ (๐ = (๐ฅ ยท ๐ด) โง ๐ = (๐ฆ ยท ๐ด)) โ (โ๐ฅ โ ๐ ๐ = (๐ฅ ยท ๐ด) โง โ๐ฆ โ ๐ ๐ = (๐ฆ ยท ๐ด))) |
16 | | cyccom.z |
. . . . . . . . . . . . . . . . 17
โข (๐ โ ๐ โ โ) |
17 | 16 | sseld 3944 |
. . . . . . . . . . . . . . . 16
โข (๐ โ (๐ฅ โ ๐ โ ๐ฅ โ โ)) |
18 | 17 | com12 32 |
. . . . . . . . . . . . . . 15
โข (๐ฅ โ ๐ โ (๐ โ ๐ฅ โ โ)) |
19 | 18 | adantr 482 |
. . . . . . . . . . . . . 14
โข ((๐ฅ โ ๐ โง ๐ฆ โ ๐) โ (๐ โ ๐ฅ โ โ)) |
20 | 19 | impcom 409 |
. . . . . . . . . . . . 13
โข ((๐ โง (๐ฅ โ ๐ โง ๐ฆ โ ๐)) โ ๐ฅ โ โ) |
21 | 16 | sseld 3944 |
. . . . . . . . . . . . . . 15
โข (๐ โ (๐ฆ โ ๐ โ ๐ฆ โ โ)) |
22 | 21 | a1d 25 |
. . . . . . . . . . . . . 14
โข (๐ โ (๐ฅ โ ๐ โ (๐ฆ โ ๐ โ ๐ฆ โ โ))) |
23 | 22 | imp32 420 |
. . . . . . . . . . . . 13
โข ((๐ โง (๐ฅ โ ๐ โง ๐ฆ โ ๐)) โ ๐ฆ โ โ) |
24 | 20, 23 | addcomd 11358 |
. . . . . . . . . . . 12
โข ((๐ โง (๐ฅ โ ๐ โง ๐ฆ โ ๐)) โ (๐ฅ + ๐ฆ) = (๐ฆ + ๐ฅ)) |
25 | 24 | oveq1d 7373 |
. . . . . . . . . . 11
โข ((๐ โง (๐ฅ โ ๐ โง ๐ฆ โ ๐)) โ ((๐ฅ + ๐ฆ) ยท ๐ด) = ((๐ฆ + ๐ฅ) ยท ๐ด)) |
26 | | simpr 486 |
. . . . . . . . . . . 12
โข ((๐ โง (๐ฅ โ ๐ โง ๐ฆ โ ๐)) โ (๐ฅ โ ๐ โง ๐ฆ โ ๐)) |
27 | | cyccom.d |
. . . . . . . . . . . . 13
โข (๐ โ โ๐ โ ๐ โ๐ โ ๐ ((๐ + ๐) ยท ๐ด) = ((๐ ยท ๐ด) + (๐ ยท ๐ด))) |
28 | 27 | adantr 482 |
. . . . . . . . . . . 12
โข ((๐ โง (๐ฅ โ ๐ โง ๐ฆ โ ๐)) โ โ๐ โ ๐ โ๐ โ ๐ ((๐ + ๐) ยท ๐ด) = ((๐ ยท ๐ด) + (๐ ยท ๐ด))) |
29 | | oveq1 7365 |
. . . . . . . . . . . . . . 15
โข (๐ = ๐ฅ โ (๐ + ๐) = (๐ฅ + ๐)) |
30 | 29 | oveq1d 7373 |
. . . . . . . . . . . . . 14
โข (๐ = ๐ฅ โ ((๐ + ๐) ยท ๐ด) = ((๐ฅ + ๐) ยท ๐ด)) |
31 | | oveq1 7365 |
. . . . . . . . . . . . . . 15
โข (๐ = ๐ฅ โ (๐ ยท ๐ด) = (๐ฅ ยท ๐ด)) |
32 | 31 | oveq1d 7373 |
. . . . . . . . . . . . . 14
โข (๐ = ๐ฅ โ ((๐ ยท ๐ด) + (๐ ยท ๐ด)) = ((๐ฅ ยท ๐ด) + (๐ ยท ๐ด))) |
33 | 30, 32 | eqeq12d 2753 |
. . . . . . . . . . . . 13
โข (๐ = ๐ฅ โ (((๐ + ๐) ยท ๐ด) = ((๐ ยท ๐ด) + (๐ ยท ๐ด)) โ ((๐ฅ + ๐) ยท ๐ด) = ((๐ฅ ยท ๐ด) + (๐ ยท ๐ด)))) |
34 | | oveq2 7366 |
. . . . . . . . . . . . . . 15
โข (๐ = ๐ฆ โ (๐ฅ + ๐) = (๐ฅ + ๐ฆ)) |
35 | 34 | oveq1d 7373 |
. . . . . . . . . . . . . 14
โข (๐ = ๐ฆ โ ((๐ฅ + ๐) ยท ๐ด) = ((๐ฅ + ๐ฆ) ยท ๐ด)) |
36 | | oveq1 7365 |
. . . . . . . . . . . . . . 15
โข (๐ = ๐ฆ โ (๐ ยท ๐ด) = (๐ฆ ยท ๐ด)) |
37 | 36 | oveq2d 7374 |
. . . . . . . . . . . . . 14
โข (๐ = ๐ฆ โ ((๐ฅ ยท ๐ด) + (๐ ยท ๐ด)) = ((๐ฅ ยท ๐ด) + (๐ฆ ยท ๐ด))) |
38 | 35, 37 | eqeq12d 2753 |
. . . . . . . . . . . . 13
โข (๐ = ๐ฆ โ (((๐ฅ + ๐) ยท ๐ด) = ((๐ฅ ยท ๐ด) + (๐ ยท ๐ด)) โ ((๐ฅ + ๐ฆ) ยท ๐ด) = ((๐ฅ ยท ๐ด) + (๐ฆ ยท ๐ด)))) |
39 | 33, 38 | rspc2va 3592 |
. . . . . . . . . . . 12
โข (((๐ฅ โ ๐ โง ๐ฆ โ ๐) โง โ๐ โ ๐ โ๐ โ ๐ ((๐ + ๐) ยท ๐ด) = ((๐ ยท ๐ด) + (๐ ยท ๐ด))) โ ((๐ฅ + ๐ฆ) ยท ๐ด) = ((๐ฅ ยท ๐ด) + (๐ฆ ยท ๐ด))) |
40 | 26, 28, 39 | syl2anc 585 |
. . . . . . . . . . 11
โข ((๐ โง (๐ฅ โ ๐ โง ๐ฆ โ ๐)) โ ((๐ฅ + ๐ฆ) ยท ๐ด) = ((๐ฅ ยท ๐ด) + (๐ฆ ยท ๐ด))) |
41 | 26 | ancomd 463 |
. . . . . . . . . . . 12
โข ((๐ โง (๐ฅ โ ๐ โง ๐ฆ โ ๐)) โ (๐ฆ โ ๐ โง ๐ฅ โ ๐)) |
42 | | oveq1 7365 |
. . . . . . . . . . . . . . 15
โข (๐ = ๐ฆ โ (๐ + ๐) = (๐ฆ + ๐)) |
43 | 42 | oveq1d 7373 |
. . . . . . . . . . . . . 14
โข (๐ = ๐ฆ โ ((๐ + ๐) ยท ๐ด) = ((๐ฆ + ๐) ยท ๐ด)) |
44 | | oveq1 7365 |
. . . . . . . . . . . . . . 15
โข (๐ = ๐ฆ โ (๐ ยท ๐ด) = (๐ฆ ยท ๐ด)) |
45 | 44 | oveq1d 7373 |
. . . . . . . . . . . . . 14
โข (๐ = ๐ฆ โ ((๐ ยท ๐ด) + (๐ ยท ๐ด)) = ((๐ฆ ยท ๐ด) + (๐ ยท ๐ด))) |
46 | 43, 45 | eqeq12d 2753 |
. . . . . . . . . . . . 13
โข (๐ = ๐ฆ โ (((๐ + ๐) ยท ๐ด) = ((๐ ยท ๐ด) + (๐ ยท ๐ด)) โ ((๐ฆ + ๐) ยท ๐ด) = ((๐ฆ ยท ๐ด) + (๐ ยท ๐ด)))) |
47 | | oveq2 7366 |
. . . . . . . . . . . . . . 15
โข (๐ = ๐ฅ โ (๐ฆ + ๐) = (๐ฆ + ๐ฅ)) |
48 | 47 | oveq1d 7373 |
. . . . . . . . . . . . . 14
โข (๐ = ๐ฅ โ ((๐ฆ + ๐) ยท ๐ด) = ((๐ฆ + ๐ฅ) ยท ๐ด)) |
49 | | oveq1 7365 |
. . . . . . . . . . . . . . 15
โข (๐ = ๐ฅ โ (๐ ยท ๐ด) = (๐ฅ ยท ๐ด)) |
50 | 49 | oveq2d 7374 |
. . . . . . . . . . . . . 14
โข (๐ = ๐ฅ โ ((๐ฆ ยท ๐ด) + (๐ ยท ๐ด)) = ((๐ฆ ยท ๐ด) + (๐ฅ ยท ๐ด))) |
51 | 48, 50 | eqeq12d 2753 |
. . . . . . . . . . . . 13
โข (๐ = ๐ฅ โ (((๐ฆ + ๐) ยท ๐ด) = ((๐ฆ ยท ๐ด) + (๐ ยท ๐ด)) โ ((๐ฆ + ๐ฅ) ยท ๐ด) = ((๐ฆ ยท ๐ด) + (๐ฅ ยท ๐ด)))) |
52 | 46, 51 | rspc2va 3592 |
. . . . . . . . . . . 12
โข (((๐ฆ โ ๐ โง ๐ฅ โ ๐) โง โ๐ โ ๐ โ๐ โ ๐ ((๐ + ๐) ยท ๐ด) = ((๐ ยท ๐ด) + (๐ ยท ๐ด))) โ ((๐ฆ + ๐ฅ) ยท ๐ด) = ((๐ฆ ยท ๐ด) + (๐ฅ ยท ๐ด))) |
53 | 41, 28, 52 | syl2anc 585 |
. . . . . . . . . . 11
โข ((๐ โง (๐ฅ โ ๐ โง ๐ฆ โ ๐)) โ ((๐ฆ + ๐ฅ) ยท ๐ด) = ((๐ฆ ยท ๐ด) + (๐ฅ ยท ๐ด))) |
54 | 25, 40, 53 | 3eqtr3d 2785 |
. . . . . . . . . 10
โข ((๐ โง (๐ฅ โ ๐ โง ๐ฆ โ ๐)) โ ((๐ฅ ยท ๐ด) + (๐ฆ ยท ๐ด)) = ((๐ฆ ยท ๐ด) + (๐ฅ ยท ๐ด))) |
55 | | oveq12 7367 |
. . . . . . . . . . 11
โข ((๐ = (๐ฅ ยท ๐ด) โง ๐ = (๐ฆ ยท ๐ด)) โ (๐ + ๐) = ((๐ฅ ยท ๐ด) + (๐ฆ ยท ๐ด))) |
56 | | oveq12 7367 |
. . . . . . . . . . . 12
โข ((๐ = (๐ฆ ยท ๐ด) โง ๐ = (๐ฅ ยท ๐ด)) โ (๐ + ๐) = ((๐ฆ ยท ๐ด) + (๐ฅ ยท ๐ด))) |
57 | 56 | ancoms 460 |
. . . . . . . . . . 11
โข ((๐ = (๐ฅ ยท ๐ด) โง ๐ = (๐ฆ ยท ๐ด)) โ (๐ + ๐) = ((๐ฆ ยท ๐ด) + (๐ฅ ยท ๐ด))) |
58 | 55, 57 | eqeq12d 2753 |
. . . . . . . . . 10
โข ((๐ = (๐ฅ ยท ๐ด) โง ๐ = (๐ฆ ยท ๐ด)) โ ((๐ + ๐) = (๐ + ๐) โ ((๐ฅ ยท ๐ด) + (๐ฆ ยท ๐ด)) = ((๐ฆ ยท ๐ด) + (๐ฅ ยท ๐ด)))) |
59 | 54, 58 | syl5ibrcom 247 |
. . . . . . . . 9
โข ((๐ โง (๐ฅ โ ๐ โง ๐ฆ โ ๐)) โ ((๐ = (๐ฅ ยท ๐ด) โง ๐ = (๐ฆ ยท ๐ด)) โ (๐ + ๐) = (๐ + ๐))) |
60 | 59 | rexlimdvva 3206 |
. . . . . . . 8
โข (๐ โ (โ๐ฅ โ ๐ โ๐ฆ โ ๐ (๐ = (๐ฅ ยท ๐ด) โง ๐ = (๐ฆ ยท ๐ด)) โ (๐ + ๐) = (๐ + ๐))) |
61 | 15, 60 | biimtrrid 242 |
. . . . . . 7
โข (๐ โ ((โ๐ฅ โ ๐ ๐ = (๐ฅ ยท ๐ด) โง โ๐ฆ โ ๐ ๐ = (๐ฆ ยท ๐ด)) โ (๐ + ๐) = (๐ + ๐))) |
62 | 61 | expd 417 |
. . . . . 6
โข (๐ โ (โ๐ฅ โ ๐ ๐ = (๐ฅ ยท ๐ด) โ (โ๐ฆ โ ๐ ๐ = (๐ฆ ยท ๐ด) โ (๐ + ๐) = (๐ + ๐)))) |
63 | 14, 62 | syl7bi 255 |
. . . . 5
โข (๐ โ (โ๐ฅ โ ๐ ๐ = (๐ฅ ยท ๐ด) โ (โ๐ฅ โ ๐ ๐ = (๐ฅ ยท ๐ด) โ (๐ + ๐) = (๐ + ๐)))) |
64 | 11, 63 | syld 47 |
. . . 4
โข (๐ โ (๐ โ ๐ถ โ (โ๐ฅ โ ๐ ๐ = (๐ฅ ยท ๐ด) โ (๐ + ๐) = (๐ + ๐)))) |
65 | 64 | com23 86 |
. . 3
โข (๐ โ (โ๐ฅ โ ๐ ๐ = (๐ฅ ยท ๐ด) โ (๐ โ ๐ถ โ (๐ + ๐) = (๐ + ๐)))) |
66 | 7, 65 | syld 47 |
. 2
โข (๐ โ (๐ โ ๐ถ โ (๐ โ ๐ถ โ (๐ + ๐) = (๐ + ๐)))) |
67 | 1, 2, 66 | mp2d 49 |
1
โข (๐ โ (๐ + ๐) = (๐ + ๐)) |