Step | Hyp | Ref
| Expression |
1 | | cnre 11160 |
. 2
โข (๐ด โ โ โ
โ๐ง โ โ
โ๐ค โ โ
๐ด = (๐ง + (i ยท ๐ค))) |
2 | | simpr 486 |
. . . . 5
โข ((๐ง โ โ โง ๐ค โ โ) โ ๐ค โ
โ) |
3 | | eqcom 2740 |
. . . . . . . . . 10
โข ((๐ง + (i ยท ๐ค)) = (๐ฅ + (i ยท ๐ฆ)) โ (๐ฅ + (i ยท ๐ฆ)) = (๐ง + (i ยท ๐ค))) |
4 | | cru 12153 |
. . . . . . . . . . 11
โข (((๐ฅ โ โ โง ๐ฆ โ โ) โง (๐ง โ โ โง ๐ค โ โ)) โ ((๐ฅ + (i ยท ๐ฆ)) = (๐ง + (i ยท ๐ค)) โ (๐ฅ = ๐ง โง ๐ฆ = ๐ค))) |
5 | 4 | ancoms 460 |
. . . . . . . . . 10
โข (((๐ง โ โ โง ๐ค โ โ) โง (๐ฅ โ โ โง ๐ฆ โ โ)) โ ((๐ฅ + (i ยท ๐ฆ)) = (๐ง + (i ยท ๐ค)) โ (๐ฅ = ๐ง โง ๐ฆ = ๐ค))) |
6 | 3, 5 | bitrid 283 |
. . . . . . . . 9
โข (((๐ง โ โ โง ๐ค โ โ) โง (๐ฅ โ โ โง ๐ฆ โ โ)) โ ((๐ง + (i ยท ๐ค)) = (๐ฅ + (i ยท ๐ฆ)) โ (๐ฅ = ๐ง โง ๐ฆ = ๐ค))) |
7 | 6 | anass1rs 654 |
. . . . . . . 8
โข ((((๐ง โ โ โง ๐ค โ โ) โง ๐ฆ โ โ) โง ๐ฅ โ โ) โ ((๐ง + (i ยท ๐ค)) = (๐ฅ + (i ยท ๐ฆ)) โ (๐ฅ = ๐ง โง ๐ฆ = ๐ค))) |
8 | 7 | rexbidva 3170 |
. . . . . . 7
โข (((๐ง โ โ โง ๐ค โ โ) โง ๐ฆ โ โ) โ
(โ๐ฅ โ โ
(๐ง + (i ยท ๐ค)) = (๐ฅ + (i ยท ๐ฆ)) โ โ๐ฅ โ โ (๐ฅ = ๐ง โง ๐ฆ = ๐ค))) |
9 | | biidd 262 |
. . . . . . . . 9
โข (๐ฅ = ๐ง โ (๐ฆ = ๐ค โ ๐ฆ = ๐ค)) |
10 | 9 | ceqsrexv 3609 |
. . . . . . . 8
โข (๐ง โ โ โ
(โ๐ฅ โ โ
(๐ฅ = ๐ง โง ๐ฆ = ๐ค) โ ๐ฆ = ๐ค)) |
11 | 10 | ad2antrr 725 |
. . . . . . 7
โข (((๐ง โ โ โง ๐ค โ โ) โง ๐ฆ โ โ) โ
(โ๐ฅ โ โ
(๐ฅ = ๐ง โง ๐ฆ = ๐ค) โ ๐ฆ = ๐ค)) |
12 | 8, 11 | bitrd 279 |
. . . . . 6
โข (((๐ง โ โ โง ๐ค โ โ) โง ๐ฆ โ โ) โ
(โ๐ฅ โ โ
(๐ง + (i ยท ๐ค)) = (๐ฅ + (i ยท ๐ฆ)) โ ๐ฆ = ๐ค)) |
13 | 12 | ralrimiva 3140 |
. . . . 5
โข ((๐ง โ โ โง ๐ค โ โ) โ
โ๐ฆ โ โ
(โ๐ฅ โ โ
(๐ง + (i ยท ๐ค)) = (๐ฅ + (i ยท ๐ฆ)) โ ๐ฆ = ๐ค)) |
14 | | reu6i 3690 |
. . . . 5
โข ((๐ค โ โ โง
โ๐ฆ โ โ
(โ๐ฅ โ โ
(๐ง + (i ยท ๐ค)) = (๐ฅ + (i ยท ๐ฆ)) โ ๐ฆ = ๐ค)) โ โ!๐ฆ โ โ โ๐ฅ โ โ (๐ง + (i ยท ๐ค)) = (๐ฅ + (i ยท ๐ฆ))) |
15 | 2, 13, 14 | syl2anc 585 |
. . . 4
โข ((๐ง โ โ โง ๐ค โ โ) โ
โ!๐ฆ โ โ
โ๐ฅ โ โ
(๐ง + (i ยท ๐ค)) = (๐ฅ + (i ยท ๐ฆ))) |
16 | | eqeq1 2737 |
. . . . . 6
โข (๐ด = (๐ง + (i ยท ๐ค)) โ (๐ด = (๐ฅ + (i ยท ๐ฆ)) โ (๐ง + (i ยท ๐ค)) = (๐ฅ + (i ยท ๐ฆ)))) |
17 | 16 | rexbidv 3172 |
. . . . 5
โข (๐ด = (๐ง + (i ยท ๐ค)) โ (โ๐ฅ โ โ ๐ด = (๐ฅ + (i ยท ๐ฆ)) โ โ๐ฅ โ โ (๐ง + (i ยท ๐ค)) = (๐ฅ + (i ยท ๐ฆ)))) |
18 | 17 | reubidv 3370 |
. . . 4
โข (๐ด = (๐ง + (i ยท ๐ค)) โ (โ!๐ฆ โ โ โ๐ฅ โ โ ๐ด = (๐ฅ + (i ยท ๐ฆ)) โ โ!๐ฆ โ โ โ๐ฅ โ โ (๐ง + (i ยท ๐ค)) = (๐ฅ + (i ยท ๐ฆ)))) |
19 | 15, 18 | syl5ibrcom 247 |
. . 3
โข ((๐ง โ โ โง ๐ค โ โ) โ (๐ด = (๐ง + (i ยท ๐ค)) โ โ!๐ฆ โ โ โ๐ฅ โ โ ๐ด = (๐ฅ + (i ยท ๐ฆ)))) |
20 | 19 | rexlimivv 3193 |
. 2
โข
(โ๐ง โ
โ โ๐ค โ
โ ๐ด = (๐ง + (i ยท ๐ค)) โ โ!๐ฆ โ โ โ๐ฅ โ โ ๐ด = (๐ฅ + (i ยท ๐ฆ))) |
21 | 1, 20 | syl 17 |
1
โข (๐ด โ โ โ
โ!๐ฆ โ โ
โ๐ฅ โ โ
๐ด = (๐ฅ + (i ยท ๐ฆ))) |