Step | Hyp | Ref
| Expression |
1 | | cnre 7952 |
. 2
โข (๐ด โ โ โ
โ๐ง โ โ
โ๐ค โ โ
๐ด = (๐ง + (i ยท ๐ค))) |
2 | | simpr 110 |
. . . . 5
โข ((๐ง โ โ โง ๐ค โ โ) โ ๐ค โ
โ) |
3 | | eqcom 2179 |
. . . . . . . . . 10
โข ((๐ง + (i ยท ๐ค)) = (๐ฅ + (i ยท ๐ฆ)) โ (๐ฅ + (i ยท ๐ฆ)) = (๐ง + (i ยท ๐ค))) |
4 | | cru 8558 |
. . . . . . . . . . 11
โข (((๐ฅ โ โ โง ๐ฆ โ โ) โง (๐ง โ โ โง ๐ค โ โ)) โ ((๐ฅ + (i ยท ๐ฆ)) = (๐ง + (i ยท ๐ค)) โ (๐ฅ = ๐ง โง ๐ฆ = ๐ค))) |
5 | 4 | ancoms 268 |
. . . . . . . . . 10
โข (((๐ง โ โ โง ๐ค โ โ) โง (๐ฅ โ โ โง ๐ฆ โ โ)) โ ((๐ฅ + (i ยท ๐ฆ)) = (๐ง + (i ยท ๐ค)) โ (๐ฅ = ๐ง โง ๐ฆ = ๐ค))) |
6 | 3, 5 | bitrid 192 |
. . . . . . . . 9
โข (((๐ง โ โ โง ๐ค โ โ) โง (๐ฅ โ โ โง ๐ฆ โ โ)) โ ((๐ง + (i ยท ๐ค)) = (๐ฅ + (i ยท ๐ฆ)) โ (๐ฅ = ๐ง โง ๐ฆ = ๐ค))) |
7 | 6 | anass1rs 571 |
. . . . . . . 8
โข ((((๐ง โ โ โง ๐ค โ โ) โง ๐ฆ โ โ) โง ๐ฅ โ โ) โ ((๐ง + (i ยท ๐ค)) = (๐ฅ + (i ยท ๐ฆ)) โ (๐ฅ = ๐ง โง ๐ฆ = ๐ค))) |
8 | 7 | rexbidva 2474 |
. . . . . . 7
โข (((๐ง โ โ โง ๐ค โ โ) โง ๐ฆ โ โ) โ
(โ๐ฅ โ โ
(๐ง + (i ยท ๐ค)) = (๐ฅ + (i ยท ๐ฆ)) โ โ๐ฅ โ โ (๐ฅ = ๐ง โง ๐ฆ = ๐ค))) |
9 | | biidd 172 |
. . . . . . . . 9
โข (๐ฅ = ๐ง โ (๐ฆ = ๐ค โ ๐ฆ = ๐ค)) |
10 | 9 | ceqsrexv 2867 |
. . . . . . . 8
โข (๐ง โ โ โ
(โ๐ฅ โ โ
(๐ฅ = ๐ง โง ๐ฆ = ๐ค) โ ๐ฆ = ๐ค)) |
11 | 10 | ad2antrr 488 |
. . . . . . 7
โข (((๐ง โ โ โง ๐ค โ โ) โง ๐ฆ โ โ) โ
(โ๐ฅ โ โ
(๐ฅ = ๐ง โง ๐ฆ = ๐ค) โ ๐ฆ = ๐ค)) |
12 | 8, 11 | bitrd 188 |
. . . . . 6
โข (((๐ง โ โ โง ๐ค โ โ) โง ๐ฆ โ โ) โ
(โ๐ฅ โ โ
(๐ง + (i ยท ๐ค)) = (๐ฅ + (i ยท ๐ฆ)) โ ๐ฆ = ๐ค)) |
13 | 12 | ralrimiva 2550 |
. . . . 5
โข ((๐ง โ โ โง ๐ค โ โ) โ
โ๐ฆ โ โ
(โ๐ฅ โ โ
(๐ง + (i ยท ๐ค)) = (๐ฅ + (i ยท ๐ฆ)) โ ๐ฆ = ๐ค)) |
14 | | reu6i 2928 |
. . . . 5
โข ((๐ค โ โ โง
โ๐ฆ โ โ
(โ๐ฅ โ โ
(๐ง + (i ยท ๐ค)) = (๐ฅ + (i ยท ๐ฆ)) โ ๐ฆ = ๐ค)) โ โ!๐ฆ โ โ โ๐ฅ โ โ (๐ง + (i ยท ๐ค)) = (๐ฅ + (i ยท ๐ฆ))) |
15 | 2, 13, 14 | syl2anc 411 |
. . . 4
โข ((๐ง โ โ โง ๐ค โ โ) โ
โ!๐ฆ โ โ
โ๐ฅ โ โ
(๐ง + (i ยท ๐ค)) = (๐ฅ + (i ยท ๐ฆ))) |
16 | | eqeq1 2184 |
. . . . . 6
โข (๐ด = (๐ง + (i ยท ๐ค)) โ (๐ด = (๐ฅ + (i ยท ๐ฆ)) โ (๐ง + (i ยท ๐ค)) = (๐ฅ + (i ยท ๐ฆ)))) |
17 | 16 | rexbidv 2478 |
. . . . 5
โข (๐ด = (๐ง + (i ยท ๐ค)) โ (โ๐ฅ โ โ ๐ด = (๐ฅ + (i ยท ๐ฆ)) โ โ๐ฅ โ โ (๐ง + (i ยท ๐ค)) = (๐ฅ + (i ยท ๐ฆ)))) |
18 | 17 | reubidv 2660 |
. . . 4
โข (๐ด = (๐ง + (i ยท ๐ค)) โ (โ!๐ฆ โ โ โ๐ฅ โ โ ๐ด = (๐ฅ + (i ยท ๐ฆ)) โ โ!๐ฆ โ โ โ๐ฅ โ โ (๐ง + (i ยท ๐ค)) = (๐ฅ + (i ยท ๐ฆ)))) |
19 | 15, 18 | syl5ibrcom 157 |
. . 3
โข ((๐ง โ โ โง ๐ค โ โ) โ (๐ด = (๐ง + (i ยท ๐ค)) โ โ!๐ฆ โ โ โ๐ฅ โ โ ๐ด = (๐ฅ + (i ยท ๐ฆ)))) |
20 | 19 | rexlimivv 2600 |
. 2
โข
(โ๐ง โ
โ โ๐ค โ
โ ๐ด = (๐ง + (i ยท ๐ค)) โ โ!๐ฆ โ โ โ๐ฅ โ โ ๐ด = (๐ฅ + (i ยท ๐ฆ))) |
21 | 1, 20 | syl 14 |
1
โข (๐ด โ โ โ
โ!๐ฆ โ โ
โ๐ฅ โ โ
๐ด = (๐ฅ + (i ยท ๐ฆ))) |