Step | Hyp | Ref
| Expression |
1 | | oveq1 7416 |
. . . 4
โข (๐ฅ = 0 โ (๐ฅ(.gโโfld)๐ต) =
(0(.gโโfld)๐ต)) |
2 | | oveq1 7416 |
. . . 4
โข (๐ฅ = 0 โ (๐ฅ ยท ๐ต) = (0 ยท ๐ต)) |
3 | 1, 2 | eqeq12d 2749 |
. . 3
โข (๐ฅ = 0 โ ((๐ฅ(.gโโfld)๐ต) = (๐ฅ ยท ๐ต) โ
(0(.gโโfld)๐ต) = (0 ยท ๐ต))) |
4 | | oveq1 7416 |
. . . 4
โข (๐ฅ = ๐ฆ โ (๐ฅ(.gโโfld)๐ต) = (๐ฆ(.gโโfld)๐ต)) |
5 | | oveq1 7416 |
. . . 4
โข (๐ฅ = ๐ฆ โ (๐ฅ ยท ๐ต) = (๐ฆ ยท ๐ต)) |
6 | 4, 5 | eqeq12d 2749 |
. . 3
โข (๐ฅ = ๐ฆ โ ((๐ฅ(.gโโfld)๐ต) = (๐ฅ ยท ๐ต) โ (๐ฆ(.gโโfld)๐ต) = (๐ฆ ยท ๐ต))) |
7 | | oveq1 7416 |
. . . 4
โข (๐ฅ = (๐ฆ + 1) โ (๐ฅ(.gโโfld)๐ต) = ((๐ฆ +
1)(.gโโfld)๐ต)) |
8 | | oveq1 7416 |
. . . 4
โข (๐ฅ = (๐ฆ + 1) โ (๐ฅ ยท ๐ต) = ((๐ฆ + 1) ยท ๐ต)) |
9 | 7, 8 | eqeq12d 2749 |
. . 3
โข (๐ฅ = (๐ฆ + 1) โ ((๐ฅ(.gโโfld)๐ต) = (๐ฅ ยท ๐ต) โ ((๐ฆ +
1)(.gโโfld)๐ต) = ((๐ฆ + 1) ยท ๐ต))) |
10 | | oveq1 7416 |
. . . 4
โข (๐ฅ = -๐ฆ โ (๐ฅ(.gโโfld)๐ต) = (-๐ฆ(.gโโfld)๐ต)) |
11 | | oveq1 7416 |
. . . 4
โข (๐ฅ = -๐ฆ โ (๐ฅ ยท ๐ต) = (-๐ฆ ยท ๐ต)) |
12 | 10, 11 | eqeq12d 2749 |
. . 3
โข (๐ฅ = -๐ฆ โ ((๐ฅ(.gโโfld)๐ต) = (๐ฅ ยท ๐ต) โ (-๐ฆ(.gโโfld)๐ต) = (-๐ฆ ยท ๐ต))) |
13 | | oveq1 7416 |
. . . 4
โข (๐ฅ = ๐ด โ (๐ฅ(.gโโfld)๐ต) = (๐ด(.gโโfld)๐ต)) |
14 | | oveq1 7416 |
. . . 4
โข (๐ฅ = ๐ด โ (๐ฅ ยท ๐ต) = (๐ด ยท ๐ต)) |
15 | 13, 14 | eqeq12d 2749 |
. . 3
โข (๐ฅ = ๐ด โ ((๐ฅ(.gโโfld)๐ต) = (๐ฅ ยท ๐ต) โ (๐ด(.gโโfld)๐ต) = (๐ด ยท ๐ต))) |
16 | | cnfldbas 20948 |
. . . . 5
โข โ =
(Baseโโfld) |
17 | | cnfld0 20969 |
. . . . 5
โข 0 =
(0gโโfld) |
18 | | eqid 2733 |
. . . . 5
โข
(.gโโfld) =
(.gโโfld) |
19 | 16, 17, 18 | mulg0 18957 |
. . . 4
โข (๐ต โ โ โ
(0(.gโโfld)๐ต) = 0) |
20 | | mul02 11392 |
. . . 4
โข (๐ต โ โ โ (0
ยท ๐ต) =
0) |
21 | 19, 20 | eqtr4d 2776 |
. . 3
โข (๐ต โ โ โ
(0(.gโโfld)๐ต) = (0 ยท ๐ต)) |
22 | | oveq1 7416 |
. . . . 5
โข ((๐ฆ(.gโโfld)๐ต) = (๐ฆ ยท ๐ต) โ ((๐ฆ(.gโโfld)๐ต) + ๐ต) = ((๐ฆ ยท ๐ต) + ๐ต)) |
23 | | cnring 20967 |
. . . . . . . 8
โข
โfld โ Ring |
24 | | ringmnd 20066 |
. . . . . . . 8
โข
(โfld โ Ring โ โfld โ
Mnd) |
25 | 23, 24 | ax-mp 5 |
. . . . . . 7
โข
โfld โ Mnd |
26 | | cnfldadd 20949 |
. . . . . . . 8
โข + =
(+gโโfld) |
27 | 16, 18, 26 | mulgnn0p1 18965 |
. . . . . . 7
โข
((โfld โ Mnd โง ๐ฆ โ โ0 โง ๐ต โ โ) โ ((๐ฆ +
1)(.gโโfld)๐ต) = ((๐ฆ(.gโโfld)๐ต) + ๐ต)) |
28 | 25, 27 | mp3an1 1449 |
. . . . . 6
โข ((๐ฆ โ โ0
โง ๐ต โ โ)
โ ((๐ฆ +
1)(.gโโfld)๐ต) = ((๐ฆ(.gโโfld)๐ต) + ๐ต)) |
29 | | nn0cn 12482 |
. . . . . . . 8
โข (๐ฆ โ โ0
โ ๐ฆ โ
โ) |
30 | 29 | adantr 482 |
. . . . . . 7
โข ((๐ฆ โ โ0
โง ๐ต โ โ)
โ ๐ฆ โ
โ) |
31 | | simpr 486 |
. . . . . . 7
โข ((๐ฆ โ โ0
โง ๐ต โ โ)
โ ๐ต โ
โ) |
32 | 30, 31 | adddirp1d 11240 |
. . . . . 6
โข ((๐ฆ โ โ0
โง ๐ต โ โ)
โ ((๐ฆ + 1) ยท
๐ต) = ((๐ฆ ยท ๐ต) + ๐ต)) |
33 | 28, 32 | eqeq12d 2749 |
. . . . 5
โข ((๐ฆ โ โ0
โง ๐ต โ โ)
โ (((๐ฆ +
1)(.gโโfld)๐ต) = ((๐ฆ + 1) ยท ๐ต) โ ((๐ฆ(.gโโfld)๐ต) + ๐ต) = ((๐ฆ ยท ๐ต) + ๐ต))) |
34 | 22, 33 | imbitrrid 245 |
. . . 4
โข ((๐ฆ โ โ0
โง ๐ต โ โ)
โ ((๐ฆ(.gโโfld)๐ต) = (๐ฆ ยท ๐ต) โ ((๐ฆ +
1)(.gโโfld)๐ต) = ((๐ฆ + 1) ยท ๐ต))) |
35 | 34 | expcom 415 |
. . 3
โข (๐ต โ โ โ (๐ฆ โ โ0
โ ((๐ฆ(.gโโfld)๐ต) = (๐ฆ ยท ๐ต) โ ((๐ฆ +
1)(.gโโfld)๐ต) = ((๐ฆ + 1) ยท ๐ต)))) |
36 | | fveq2 6892 |
. . . . 5
โข ((๐ฆ(.gโโfld)๐ต) = (๐ฆ ยท ๐ต) โ
((invgโโfld)โ(๐ฆ(.gโโfld)๐ต)) =
((invgโโfld)โ(๐ฆ ยท ๐ต))) |
37 | | eqid 2733 |
. . . . . . 7
โข
(invgโโfld) =
(invgโโfld) |
38 | 16, 18, 37 | mulgnegnn 18964 |
. . . . . 6
โข ((๐ฆ โ โ โง ๐ต โ โ) โ (-๐ฆ(.gโโfld)๐ต) =
((invgโโfld)โ(๐ฆ(.gโโfld)๐ต))) |
39 | | nncn 12220 |
. . . . . . . 8
โข (๐ฆ โ โ โ ๐ฆ โ
โ) |
40 | | mulneg1 11650 |
. . . . . . . 8
โข ((๐ฆ โ โ โง ๐ต โ โ) โ (-๐ฆ ยท ๐ต) = -(๐ฆ ยท ๐ต)) |
41 | 39, 40 | sylan 581 |
. . . . . . 7
โข ((๐ฆ โ โ โง ๐ต โ โ) โ (-๐ฆ ยท ๐ต) = -(๐ฆ ยท ๐ต)) |
42 | | mulcl 11194 |
. . . . . . . . 9
โข ((๐ฆ โ โ โง ๐ต โ โ) โ (๐ฆ ยท ๐ต) โ โ) |
43 | 39, 42 | sylan 581 |
. . . . . . . 8
โข ((๐ฆ โ โ โง ๐ต โ โ) โ (๐ฆ ยท ๐ต) โ โ) |
44 | | cnfldneg 20971 |
. . . . . . . 8
โข ((๐ฆ ยท ๐ต) โ โ โ
((invgโโfld)โ(๐ฆ ยท ๐ต)) = -(๐ฆ ยท ๐ต)) |
45 | 43, 44 | syl 17 |
. . . . . . 7
โข ((๐ฆ โ โ โง ๐ต โ โ) โ
((invgโโfld)โ(๐ฆ ยท ๐ต)) = -(๐ฆ ยท ๐ต)) |
46 | 41, 45 | eqtr4d 2776 |
. . . . . 6
โข ((๐ฆ โ โ โง ๐ต โ โ) โ (-๐ฆ ยท ๐ต) =
((invgโโfld)โ(๐ฆ ยท ๐ต))) |
47 | 38, 46 | eqeq12d 2749 |
. . . . 5
โข ((๐ฆ โ โ โง ๐ต โ โ) โ ((-๐ฆ(.gโโfld)๐ต) = (-๐ฆ ยท ๐ต) โ
((invgโโfld)โ(๐ฆ(.gโโfld)๐ต)) =
((invgโโfld)โ(๐ฆ ยท ๐ต)))) |
48 | 36, 47 | imbitrrid 245 |
. . . 4
โข ((๐ฆ โ โ โง ๐ต โ โ) โ ((๐ฆ(.gโโfld)๐ต) = (๐ฆ ยท ๐ต) โ (-๐ฆ(.gโโfld)๐ต) = (-๐ฆ ยท ๐ต))) |
49 | 48 | expcom 415 |
. . 3
โข (๐ต โ โ โ (๐ฆ โ โ โ ((๐ฆ(.gโโfld)๐ต) = (๐ฆ ยท ๐ต) โ (-๐ฆ(.gโโfld)๐ต) = (-๐ฆ ยท ๐ต)))) |
50 | 3, 6, 9, 12, 15, 21, 35, 49 | zindd 12663 |
. 2
โข (๐ต โ โ โ (๐ด โ โค โ (๐ด(.gโโfld)๐ต) = (๐ด ยท ๐ต))) |
51 | 50 | impcom 409 |
1
โข ((๐ด โ โค โง ๐ต โ โ) โ (๐ด(.gโโfld)๐ต) = (๐ด ยท ๐ต)) |