Step | Hyp | Ref
| Expression |
1 | | cnre 11159 |
. 2
โข (๐ด โ โ โ
โ๐ฅ โ โ
โ๐ฆ โ โ
๐ด = (๐ฅ + (i ยท ๐ฆ))) |
2 | | recn 11148 |
. . . . . 6
โข (๐ฅ โ โ โ ๐ฅ โ
โ) |
3 | | ax-icn 11117 |
. . . . . . 7
โข i โ
โ |
4 | | recn 11148 |
. . . . . . 7
โข (๐ฆ โ โ โ ๐ฆ โ
โ) |
5 | | mulcl 11142 |
. . . . . . 7
โข ((i
โ โ โง ๐ฆ
โ โ) โ (i ยท ๐ฆ) โ โ) |
6 | 3, 4, 5 | sylancr 588 |
. . . . . 6
โข (๐ฆ โ โ โ (i
ยท ๐ฆ) โ
โ) |
7 | | ax-1cn 11116 |
. . . . . . 7
โข 1 โ
โ |
8 | | adddir 11153 |
. . . . . . 7
โข ((๐ฅ โ โ โง (i
ยท ๐ฆ) โ โ
โง 1 โ โ) โ ((๐ฅ + (i ยท ๐ฆ)) ยท 1) = ((๐ฅ ยท 1) + ((i ยท ๐ฆ) ยท 1))) |
9 | 7, 8 | mp3an3 1451 |
. . . . . 6
โข ((๐ฅ โ โ โง (i
ยท ๐ฆ) โ โ)
โ ((๐ฅ + (i ยท
๐ฆ)) ยท 1) = ((๐ฅ ยท 1) + ((i ยท
๐ฆ) ยท
1))) |
10 | 2, 6, 9 | syl2an 597 |
. . . . 5
โข ((๐ฅ โ โ โง ๐ฆ โ โ) โ ((๐ฅ + (i ยท ๐ฆ)) ยท 1) = ((๐ฅ ยท 1) + ((i ยท
๐ฆ) ยท
1))) |
11 | | ax-1rid 11128 |
. . . . . 6
โข (๐ฅ โ โ โ (๐ฅ ยท 1) = ๐ฅ) |
12 | | mulass 11146 |
. . . . . . . . 9
โข ((i
โ โ โง ๐ฆ
โ โ โง 1 โ โ) โ ((i ยท ๐ฆ) ยท 1) = (i ยท (๐ฆ ยท 1))) |
13 | 3, 7, 12 | mp3an13 1453 |
. . . . . . . 8
โข (๐ฆ โ โ โ ((i
ยท ๐ฆ) ยท 1) =
(i ยท (๐ฆ ยท
1))) |
14 | 4, 13 | syl 17 |
. . . . . . 7
โข (๐ฆ โ โ โ ((i
ยท ๐ฆ) ยท 1) =
(i ยท (๐ฆ ยท
1))) |
15 | | ax-1rid 11128 |
. . . . . . . 8
โข (๐ฆ โ โ โ (๐ฆ ยท 1) = ๐ฆ) |
16 | 15 | oveq2d 7378 |
. . . . . . 7
โข (๐ฆ โ โ โ (i
ยท (๐ฆ ยท 1)) =
(i ยท ๐ฆ)) |
17 | 14, 16 | eqtrd 2777 |
. . . . . 6
โข (๐ฆ โ โ โ ((i
ยท ๐ฆ) ยท 1) =
(i ยท ๐ฆ)) |
18 | 11, 17 | oveqan12d 7381 |
. . . . 5
โข ((๐ฅ โ โ โง ๐ฆ โ โ) โ ((๐ฅ ยท 1) + ((i ยท
๐ฆ) ยท 1)) = (๐ฅ + (i ยท ๐ฆ))) |
19 | 10, 18 | eqtrd 2777 |
. . . 4
โข ((๐ฅ โ โ โง ๐ฆ โ โ) โ ((๐ฅ + (i ยท ๐ฆ)) ยท 1) = (๐ฅ + (i ยท ๐ฆ))) |
20 | | oveq1 7369 |
. . . . 5
โข (๐ด = (๐ฅ + (i ยท ๐ฆ)) โ (๐ด ยท 1) = ((๐ฅ + (i ยท ๐ฆ)) ยท 1)) |
21 | | id 22 |
. . . . 5
โข (๐ด = (๐ฅ + (i ยท ๐ฆ)) โ ๐ด = (๐ฅ + (i ยท ๐ฆ))) |
22 | 20, 21 | eqeq12d 2753 |
. . . 4
โข (๐ด = (๐ฅ + (i ยท ๐ฆ)) โ ((๐ด ยท 1) = ๐ด โ ((๐ฅ + (i ยท ๐ฆ)) ยท 1) = (๐ฅ + (i ยท ๐ฆ)))) |
23 | 19, 22 | syl5ibrcom 247 |
. . 3
โข ((๐ฅ โ โ โง ๐ฆ โ โ) โ (๐ด = (๐ฅ + (i ยท ๐ฆ)) โ (๐ด ยท 1) = ๐ด)) |
24 | 23 | rexlimivv 3197 |
. 2
โข
(โ๐ฅ โ
โ โ๐ฆ โ
โ ๐ด = (๐ฅ + (i ยท ๐ฆ)) โ (๐ด ยท 1) = ๐ด) |
25 | 1, 24 | syl 17 |
1
โข (๐ด โ โ โ (๐ด ยท 1) = ๐ด) |