Step | Hyp | Ref
| Expression |
1 | | mdetuni.a |
. . . . 5
โข ๐ด = (๐ Mat ๐
) |
2 | | mdetuni.b |
. . . . 5
โข ๐ต = (Baseโ๐ด) |
3 | | mdetuni.k |
. . . . 5
โข ๐พ = (Baseโ๐
) |
4 | | mdetuni.0g |
. . . . 5
โข 0 =
(0gโ๐
) |
5 | | mdetuni.1r |
. . . . 5
โข 1 =
(1rโ๐
) |
6 | | mdetuni.pg |
. . . . 5
โข + =
(+gโ๐
) |
7 | | mdetuni.tg |
. . . . 5
โข ยท =
(.rโ๐
) |
8 | | mdetuni.n |
. . . . 5
โข (๐ โ ๐ โ Fin) |
9 | | mdetuni.r |
. . . . 5
โข (๐ โ ๐
โ Ring) |
10 | | mdetuni.ff |
. . . . 5
โข (๐ โ ๐ท:๐ตโถ๐พ) |
11 | | mdetuni.al |
. . . . 5
โข (๐ โ โ๐ฅ โ ๐ต โ๐ฆ โ ๐ โ๐ง โ ๐ ((๐ฆ โ ๐ง โง โ๐ค โ ๐ (๐ฆ๐ฅ๐ค) = (๐ง๐ฅ๐ค)) โ (๐ทโ๐ฅ) = 0 )) |
12 | | mdetuni.li |
. . . . 5
โข (๐ โ โ๐ฅ โ ๐ต โ๐ฆ โ ๐ต โ๐ง โ ๐ต โ๐ค โ ๐ (((๐ฅ โพ ({๐ค} ร ๐)) = ((๐ฆ โพ ({๐ค} ร ๐)) โf + (๐ง โพ ({๐ค} ร ๐))) โง (๐ฅ โพ ((๐ โ {๐ค}) ร ๐)) = (๐ฆ โพ ((๐ โ {๐ค}) ร ๐)) โง (๐ฅ โพ ((๐ โ {๐ค}) ร ๐)) = (๐ง โพ ((๐ โ {๐ค}) ร ๐))) โ (๐ทโ๐ฅ) = ((๐ทโ๐ฆ) + (๐ทโ๐ง)))) |
13 | | mdetuni.sc |
. . . . 5
โข (๐ โ โ๐ฅ โ ๐ต โ๐ฆ โ ๐พ โ๐ง โ ๐ต โ๐ค โ ๐ (((๐ฅ โพ ({๐ค} ร ๐)) = ((({๐ค} ร ๐) ร {๐ฆ}) โf ยท (๐ง โพ ({๐ค} ร ๐))) โง (๐ฅ โพ ((๐ โ {๐ค}) ร ๐)) = (๐ง โพ ((๐ โ {๐ค}) ร ๐))) โ (๐ทโ๐ฅ) = (๐ฆ ยท (๐ทโ๐ง)))) |
14 | | mdetunilem6.ph |
. . . . 5
โข (๐ โ ๐) |
15 | | mdetunilem6.ef |
. . . . . 6
โข (๐ โ (๐ธ โ ๐ โง ๐น โ ๐ โง ๐ธ โ ๐น)) |
16 | 15 | simp1d 1143 |
. . . . 5
โข (๐ โ ๐ธ โ ๐) |
17 | | mdetunilem6.gh |
. . . . . . . 8
โข ((๐ โง ๐ โ ๐) โ (๐บ โ ๐พ โง ๐ป โ ๐พ)) |
18 | 17 | simprd 497 |
. . . . . . 7
โข ((๐ โง ๐ โ ๐) โ ๐ป โ ๐พ) |
19 | 18 | 3adant2 1132 |
. . . . . 6
โข ((๐ โง ๐ โ ๐ โง ๐ โ ๐) โ ๐ป โ ๐พ) |
20 | 17 | simpld 496 |
. . . . . . 7
โข ((๐ โง ๐ โ ๐) โ ๐บ โ ๐พ) |
21 | 20 | 3adant2 1132 |
. . . . . 6
โข ((๐ โง ๐ โ ๐ โง ๐ โ ๐) โ ๐บ โ ๐พ) |
22 | | ringgrp 19977 |
. . . . . . . . . . 11
โข (๐
โ Ring โ ๐
โ Grp) |
23 | 14, 9, 22 | 3syl 18 |
. . . . . . . . . 10
โข (๐ โ ๐
โ Grp) |
24 | 23 | adantr 482 |
. . . . . . . . 9
โข ((๐ โง ๐ โ ๐) โ ๐
โ Grp) |
25 | 3, 6 | grpcl 18764 |
. . . . . . . . 9
โข ((๐
โ Grp โง ๐ป โ ๐พ โง ๐บ โ ๐พ) โ (๐ป + ๐บ) โ ๐พ) |
26 | 24, 18, 20, 25 | syl3anc 1372 |
. . . . . . . 8
โข ((๐ โง ๐ โ ๐) โ (๐ป + ๐บ) โ ๐พ) |
27 | 26 | 3adant2 1132 |
. . . . . . 7
โข ((๐ โง ๐ โ ๐ โง ๐ โ ๐) โ (๐ป + ๐บ) โ ๐พ) |
28 | | mdetunilem6.i |
. . . . . . 7
โข ((๐ โง ๐ โ ๐ โง ๐ โ ๐) โ ๐ผ โ ๐พ) |
29 | 27, 28 | ifcld 4536 |
. . . . . 6
โข ((๐ โง ๐ โ ๐ โง ๐ โ ๐) โ if(๐ = ๐น, (๐ป + ๐บ), ๐ผ) โ ๐พ) |
30 | 19, 21, 29 | 3jca 1129 |
. . . . 5
โข ((๐ โง ๐ โ ๐ โง ๐ โ ๐) โ (๐ป โ ๐พ โง ๐บ โ ๐พ โง if(๐ = ๐น, (๐ป + ๐บ), ๐ผ) โ ๐พ)) |
31 | 1, 2, 3, 4, 5, 6, 7, 8, 9, 10,
11, 12, 13, 14, 16, 30 | mdetunilem5 21988 |
. . . 4
โข (๐ โ (๐ทโ(๐ โ ๐, ๐ โ ๐ โฆ if(๐ = ๐ธ, (๐ป + ๐บ), if(๐ = ๐น, (๐ป + ๐บ), ๐ผ)))) = ((๐ทโ(๐ โ ๐, ๐ โ ๐ โฆ if(๐ = ๐ธ, ๐ป, if(๐ = ๐น, (๐ป + ๐บ), ๐ผ)))) + (๐ทโ(๐ โ ๐, ๐ โ ๐ โฆ if(๐ = ๐ธ, ๐บ, if(๐ = ๐น, (๐ป + ๐บ), ๐ผ)))))) |
32 | 1, 2, 3, 4, 5, 6, 7, 8, 9, 10,
11, 12, 13, 14, 15, 26, 28 | mdetunilem2 21985 |
. . . 4
โข (๐ โ (๐ทโ(๐ โ ๐, ๐ โ ๐ โฆ if(๐ = ๐ธ, (๐ป + ๐บ), if(๐ = ๐น, (๐ป + ๐บ), ๐ผ)))) = 0 ) |
33 | 15 | simp2d 1144 |
. . . . . . . 8
โข (๐ โ ๐น โ ๐) |
34 | 19, 28 | ifcld 4536 |
. . . . . . . . 9
โข ((๐ โง ๐ โ ๐ โง ๐ โ ๐) โ if(๐ = ๐ธ, ๐ป, ๐ผ) โ ๐พ) |
35 | 19, 21, 34 | 3jca 1129 |
. . . . . . . 8
โข ((๐ โง ๐ โ ๐ โง ๐ โ ๐) โ (๐ป โ ๐พ โง ๐บ โ ๐พ โง if(๐ = ๐ธ, ๐ป, ๐ผ) โ ๐พ)) |
36 | 1, 2, 3, 4, 5, 6, 7, 8, 9, 10,
11, 12, 13, 14, 33, 35 | mdetunilem5 21988 |
. . . . . . 7
โข (๐ โ (๐ทโ(๐ โ ๐, ๐ โ ๐ โฆ if(๐ = ๐น, (๐ป + ๐บ), if(๐ = ๐ธ, ๐ป, ๐ผ)))) = ((๐ทโ(๐ โ ๐, ๐ โ ๐ โฆ if(๐ = ๐น, ๐ป, if(๐ = ๐ธ, ๐ป, ๐ผ)))) + (๐ทโ(๐ โ ๐, ๐ โ ๐ โฆ if(๐ = ๐น, ๐บ, if(๐ = ๐ธ, ๐ป, ๐ผ)))))) |
37 | 15 | simp3d 1145 |
. . . . . . . . . . 11
โข (๐ โ ๐ธ โ ๐น) |
38 | 37 | necomd 2996 |
. . . . . . . . . 10
โข (๐ โ ๐น โ ๐ธ) |
39 | 33, 16, 38 | 3jca 1129 |
. . . . . . . . 9
โข (๐ โ (๐น โ ๐ โง ๐ธ โ ๐ โง ๐น โ ๐ธ)) |
40 | 1, 2, 3, 4, 5, 6, 7, 8, 9, 10,
11, 12, 13, 14, 39, 18, 28 | mdetunilem2 21985 |
. . . . . . . 8
โข (๐ โ (๐ทโ(๐ โ ๐, ๐ โ ๐ โฆ if(๐ = ๐น, ๐ป, if(๐ = ๐ธ, ๐ป, ๐ผ)))) = 0 ) |
41 | 40 | oveq1d 7376 |
. . . . . . 7
โข (๐ โ ((๐ทโ(๐ โ ๐, ๐ โ ๐ โฆ if(๐ = ๐น, ๐ป, if(๐ = ๐ธ, ๐ป, ๐ผ)))) + (๐ทโ(๐ โ ๐, ๐ โ ๐ โฆ if(๐ = ๐น, ๐บ, if(๐ = ๐ธ, ๐ป, ๐ผ))))) = ( 0 + (๐ทโ(๐ โ ๐, ๐ โ ๐ โฆ if(๐ = ๐น, ๐บ, if(๐ = ๐ธ, ๐ป, ๐ผ)))))) |
42 | 37 | neneqd 2945 |
. . . . . . . . . . . . . 14
โข (๐ โ ยฌ ๐ธ = ๐น) |
43 | | eqtr2 2757 |
. . . . . . . . . . . . . 14
โข ((๐ = ๐ธ โง ๐ = ๐น) โ ๐ธ = ๐น) |
44 | 42, 43 | nsyl 140 |
. . . . . . . . . . . . 13
โข (๐ โ ยฌ (๐ = ๐ธ โง ๐ = ๐น)) |
45 | 44 | 3ad2ant1 1134 |
. . . . . . . . . . . 12
โข ((๐ โง ๐ โ ๐ โง ๐ โ ๐) โ ยฌ (๐ = ๐ธ โง ๐ = ๐น)) |
46 | | ifcomnan 4546 |
. . . . . . . . . . . 12
โข (ยฌ
(๐ = ๐ธ โง ๐ = ๐น) โ if(๐ = ๐ธ, ๐ป, if(๐ = ๐น, ๐บ, ๐ผ)) = if(๐ = ๐น, ๐บ, if(๐ = ๐ธ, ๐ป, ๐ผ))) |
47 | 45, 46 | syl 17 |
. . . . . . . . . . 11
โข ((๐ โง ๐ โ ๐ โง ๐ โ ๐) โ if(๐ = ๐ธ, ๐ป, if(๐ = ๐น, ๐บ, ๐ผ)) = if(๐ = ๐น, ๐บ, if(๐ = ๐ธ, ๐ป, ๐ผ))) |
48 | 47 | mpoeq3dva 7438 |
. . . . . . . . . 10
โข (๐ โ (๐ โ ๐, ๐ โ ๐ โฆ if(๐ = ๐ธ, ๐ป, if(๐ = ๐น, ๐บ, ๐ผ))) = (๐ โ ๐, ๐ โ ๐ โฆ if(๐ = ๐น, ๐บ, if(๐ = ๐ธ, ๐ป, ๐ผ)))) |
49 | 48 | fveq2d 6850 |
. . . . . . . . 9
โข (๐ โ (๐ทโ(๐ โ ๐, ๐ โ ๐ โฆ if(๐ = ๐ธ, ๐ป, if(๐ = ๐น, ๐บ, ๐ผ)))) = (๐ทโ(๐ โ ๐, ๐ โ ๐ โฆ if(๐ = ๐น, ๐บ, if(๐ = ๐ธ, ๐ป, ๐ผ))))) |
50 | 14, 10 | syl 17 |
. . . . . . . . . 10
โข (๐ โ ๐ท:๐ตโถ๐พ) |
51 | 14, 8 | syl 17 |
. . . . . . . . . . 11
โข (๐ โ ๐ โ Fin) |
52 | 21, 28 | ifcld 4536 |
. . . . . . . . . . . 12
โข ((๐ โง ๐ โ ๐ โง ๐ โ ๐) โ if(๐ = ๐น, ๐บ, ๐ผ) โ ๐พ) |
53 | 19, 52 | ifcld 4536 |
. . . . . . . . . . 11
โข ((๐ โง ๐ โ ๐ โง ๐ โ ๐) โ if(๐ = ๐ธ, ๐ป, if(๐ = ๐น, ๐บ, ๐ผ)) โ ๐พ) |
54 | 1, 3, 2, 51, 23, 53 | matbas2d 21795 |
. . . . . . . . . 10
โข (๐ โ (๐ โ ๐, ๐ โ ๐ โฆ if(๐ = ๐ธ, ๐ป, if(๐ = ๐น, ๐บ, ๐ผ))) โ ๐ต) |
55 | 50, 54 | ffvelcdmd 7040 |
. . . . . . . . 9
โข (๐ โ (๐ทโ(๐ โ ๐, ๐ โ ๐ โฆ if(๐ = ๐ธ, ๐ป, if(๐ = ๐น, ๐บ, ๐ผ)))) โ ๐พ) |
56 | 49, 55 | eqeltrrd 2835 |
. . . . . . . 8
โข (๐ โ (๐ทโ(๐ โ ๐, ๐ โ ๐ โฆ if(๐ = ๐น, ๐บ, if(๐ = ๐ธ, ๐ป, ๐ผ)))) โ ๐พ) |
57 | 3, 6, 4 | grplid 18788 |
. . . . . . . 8
โข ((๐
โ Grp โง (๐ทโ(๐ โ ๐, ๐ โ ๐ โฆ if(๐ = ๐น, ๐บ, if(๐ = ๐ธ, ๐ป, ๐ผ)))) โ ๐พ) โ ( 0 + (๐ทโ(๐ โ ๐, ๐ โ ๐ โฆ if(๐ = ๐น, ๐บ, if(๐ = ๐ธ, ๐ป, ๐ผ))))) = (๐ทโ(๐ โ ๐, ๐ โ ๐ โฆ if(๐ = ๐น, ๐บ, if(๐ = ๐ธ, ๐ป, ๐ผ))))) |
58 | 23, 56, 57 | syl2anc 585 |
. . . . . . 7
โข (๐ โ ( 0 + (๐ทโ(๐ โ ๐, ๐ โ ๐ โฆ if(๐ = ๐น, ๐บ, if(๐ = ๐ธ, ๐ป, ๐ผ))))) = (๐ทโ(๐ โ ๐, ๐ โ ๐ โฆ if(๐ = ๐น, ๐บ, if(๐ = ๐ธ, ๐ป, ๐ผ))))) |
59 | 36, 41, 58 | 3eqtrd 2777 |
. . . . . 6
โข (๐ โ (๐ทโ(๐ โ ๐, ๐ โ ๐ โฆ if(๐ = ๐น, (๐ป + ๐บ), if(๐ = ๐ธ, ๐ป, ๐ผ)))) = (๐ทโ(๐ โ ๐, ๐ โ ๐ โฆ if(๐ = ๐น, ๐บ, if(๐ = ๐ธ, ๐ป, ๐ผ))))) |
60 | | ifcomnan 4546 |
. . . . . . . . 9
โข (ยฌ
(๐ = ๐ธ โง ๐ = ๐น) โ if(๐ = ๐ธ, ๐ป, if(๐ = ๐น, (๐ป + ๐บ), ๐ผ)) = if(๐ = ๐น, (๐ป + ๐บ), if(๐ = ๐ธ, ๐ป, ๐ผ))) |
61 | 45, 60 | syl 17 |
. . . . . . . 8
โข ((๐ โง ๐ โ ๐ โง ๐ โ ๐) โ if(๐ = ๐ธ, ๐ป, if(๐ = ๐น, (๐ป + ๐บ), ๐ผ)) = if(๐ = ๐น, (๐ป + ๐บ), if(๐ = ๐ธ, ๐ป, ๐ผ))) |
62 | 61 | mpoeq3dva 7438 |
. . . . . . 7
โข (๐ โ (๐ โ ๐, ๐ โ ๐ โฆ if(๐ = ๐ธ, ๐ป, if(๐ = ๐น, (๐ป + ๐บ), ๐ผ))) = (๐ โ ๐, ๐ โ ๐ โฆ if(๐ = ๐น, (๐ป + ๐บ), if(๐ = ๐ธ, ๐ป, ๐ผ)))) |
63 | 62 | fveq2d 6850 |
. . . . . 6
โข (๐ โ (๐ทโ(๐ โ ๐, ๐ โ ๐ โฆ if(๐ = ๐ธ, ๐ป, if(๐ = ๐น, (๐ป + ๐บ), ๐ผ)))) = (๐ทโ(๐ โ ๐, ๐ โ ๐ โฆ if(๐ = ๐น, (๐ป + ๐บ), if(๐ = ๐ธ, ๐ป, ๐ผ))))) |
64 | 59, 63, 49 | 3eqtr4d 2783 |
. . . . 5
โข (๐ โ (๐ทโ(๐ โ ๐, ๐ โ ๐ โฆ if(๐ = ๐ธ, ๐ป, if(๐ = ๐น, (๐ป + ๐บ), ๐ผ)))) = (๐ทโ(๐ โ ๐, ๐ โ ๐ โฆ if(๐ = ๐ธ, ๐ป, if(๐ = ๐น, ๐บ, ๐ผ))))) |
65 | 21, 28 | ifcld 4536 |
. . . . . . . . 9
โข ((๐ โง ๐ โ ๐ โง ๐ โ ๐) โ if(๐ = ๐ธ, ๐บ, ๐ผ) โ ๐พ) |
66 | 19, 21, 65 | 3jca 1129 |
. . . . . . . 8
โข ((๐ โง ๐ โ ๐ โง ๐ โ ๐) โ (๐ป โ ๐พ โง ๐บ โ ๐พ โง if(๐ = ๐ธ, ๐บ, ๐ผ) โ ๐พ)) |
67 | 1, 2, 3, 4, 5, 6, 7, 8, 9, 10,
11, 12, 13, 14, 33, 66 | mdetunilem5 21988 |
. . . . . . 7
โข (๐ โ (๐ทโ(๐ โ ๐, ๐ โ ๐ โฆ if(๐ = ๐น, (๐ป + ๐บ), if(๐ = ๐ธ, ๐บ, ๐ผ)))) = ((๐ทโ(๐ โ ๐, ๐ โ ๐ โฆ if(๐ = ๐น, ๐ป, if(๐ = ๐ธ, ๐บ, ๐ผ)))) + (๐ทโ(๐ โ ๐, ๐ โ ๐ โฆ if(๐ = ๐น, ๐บ, if(๐ = ๐ธ, ๐บ, ๐ผ)))))) |
68 | 1, 2, 3, 4, 5, 6, 7, 8, 9, 10,
11, 12, 13, 14, 39, 20, 28 | mdetunilem2 21985 |
. . . . . . . 8
โข (๐ โ (๐ทโ(๐ โ ๐, ๐ โ ๐ โฆ if(๐ = ๐น, ๐บ, if(๐ = ๐ธ, ๐บ, ๐ผ)))) = 0 ) |
69 | 68 | oveq2d 7377 |
. . . . . . 7
โข (๐ โ ((๐ทโ(๐ โ ๐, ๐ โ ๐ โฆ if(๐ = ๐น, ๐ป, if(๐ = ๐ธ, ๐บ, ๐ผ)))) + (๐ทโ(๐ โ ๐, ๐ โ ๐ โฆ if(๐ = ๐น, ๐บ, if(๐ = ๐ธ, ๐บ, ๐ผ))))) = ((๐ทโ(๐ โ ๐, ๐ โ ๐ โฆ if(๐ = ๐น, ๐ป, if(๐ = ๐ธ, ๐บ, ๐ผ)))) + 0 )) |
70 | | ifcomnan 4546 |
. . . . . . . . . . . 12
โข (ยฌ
(๐ = ๐ธ โง ๐ = ๐น) โ if(๐ = ๐ธ, ๐บ, if(๐ = ๐น, ๐ป, ๐ผ)) = if(๐ = ๐น, ๐ป, if(๐ = ๐ธ, ๐บ, ๐ผ))) |
71 | 45, 70 | syl 17 |
. . . . . . . . . . 11
โข ((๐ โง ๐ โ ๐ โง ๐ โ ๐) โ if(๐ = ๐ธ, ๐บ, if(๐ = ๐น, ๐ป, ๐ผ)) = if(๐ = ๐น, ๐ป, if(๐ = ๐ธ, ๐บ, ๐ผ))) |
72 | 71 | mpoeq3dva 7438 |
. . . . . . . . . 10
โข (๐ โ (๐ โ ๐, ๐ โ ๐ โฆ if(๐ = ๐ธ, ๐บ, if(๐ = ๐น, ๐ป, ๐ผ))) = (๐ โ ๐, ๐ โ ๐ โฆ if(๐ = ๐น, ๐ป, if(๐ = ๐ธ, ๐บ, ๐ผ)))) |
73 | 72 | fveq2d 6850 |
. . . . . . . . 9
โข (๐ โ (๐ทโ(๐ โ ๐, ๐ โ ๐ โฆ if(๐ = ๐ธ, ๐บ, if(๐ = ๐น, ๐ป, ๐ผ)))) = (๐ทโ(๐ โ ๐, ๐ โ ๐ โฆ if(๐ = ๐น, ๐ป, if(๐ = ๐ธ, ๐บ, ๐ผ))))) |
74 | 19, 28 | ifcld 4536 |
. . . . . . . . . . . 12
โข ((๐ โง ๐ โ ๐ โง ๐ โ ๐) โ if(๐ = ๐น, ๐ป, ๐ผ) โ ๐พ) |
75 | 21, 74 | ifcld 4536 |
. . . . . . . . . . 11
โข ((๐ โง ๐ โ ๐ โง ๐ โ ๐) โ if(๐ = ๐ธ, ๐บ, if(๐ = ๐น, ๐ป, ๐ผ)) โ ๐พ) |
76 | 1, 3, 2, 51, 23, 75 | matbas2d 21795 |
. . . . . . . . . 10
โข (๐ โ (๐ โ ๐, ๐ โ ๐ โฆ if(๐ = ๐ธ, ๐บ, if(๐ = ๐น, ๐ป, ๐ผ))) โ ๐ต) |
77 | 50, 76 | ffvelcdmd 7040 |
. . . . . . . . 9
โข (๐ โ (๐ทโ(๐ โ ๐, ๐ โ ๐ โฆ if(๐ = ๐ธ, ๐บ, if(๐ = ๐น, ๐ป, ๐ผ)))) โ ๐พ) |
78 | 73, 77 | eqeltrrd 2835 |
. . . . . . . 8
โข (๐ โ (๐ทโ(๐ โ ๐, ๐ โ ๐ โฆ if(๐ = ๐น, ๐ป, if(๐ = ๐ธ, ๐บ, ๐ผ)))) โ ๐พ) |
79 | 3, 6, 4 | grprid 18789 |
. . . . . . . 8
โข ((๐
โ Grp โง (๐ทโ(๐ โ ๐, ๐ โ ๐ โฆ if(๐ = ๐น, ๐ป, if(๐ = ๐ธ, ๐บ, ๐ผ)))) โ ๐พ) โ ((๐ทโ(๐ โ ๐, ๐ โ ๐ โฆ if(๐ = ๐น, ๐ป, if(๐ = ๐ธ, ๐บ, ๐ผ)))) + 0 ) = (๐ทโ(๐ โ ๐, ๐ โ ๐ โฆ if(๐ = ๐น, ๐ป, if(๐ = ๐ธ, ๐บ, ๐ผ))))) |
80 | 23, 78, 79 | syl2anc 585 |
. . . . . . 7
โข (๐ โ ((๐ทโ(๐ โ ๐, ๐ โ ๐ โฆ if(๐ = ๐น, ๐ป, if(๐ = ๐ธ, ๐บ, ๐ผ)))) + 0 ) = (๐ทโ(๐ โ ๐, ๐ โ ๐ โฆ if(๐ = ๐น, ๐ป, if(๐ = ๐ธ, ๐บ, ๐ผ))))) |
81 | 67, 69, 80 | 3eqtrd 2777 |
. . . . . 6
โข (๐ โ (๐ทโ(๐ โ ๐, ๐ โ ๐ โฆ if(๐ = ๐น, (๐ป + ๐บ), if(๐ = ๐ธ, ๐บ, ๐ผ)))) = (๐ทโ(๐ โ ๐, ๐ โ ๐ โฆ if(๐ = ๐น, ๐ป, if(๐ = ๐ธ, ๐บ, ๐ผ))))) |
82 | | ifcomnan 4546 |
. . . . . . . . 9
โข (ยฌ
(๐ = ๐ธ โง ๐ = ๐น) โ if(๐ = ๐ธ, ๐บ, if(๐ = ๐น, (๐ป + ๐บ), ๐ผ)) = if(๐ = ๐น, (๐ป + ๐บ), if(๐ = ๐ธ, ๐บ, ๐ผ))) |
83 | 45, 82 | syl 17 |
. . . . . . . 8
โข ((๐ โง ๐ โ ๐ โง ๐ โ ๐) โ if(๐ = ๐ธ, ๐บ, if(๐ = ๐น, (๐ป + ๐บ), ๐ผ)) = if(๐ = ๐น, (๐ป + ๐บ), if(๐ = ๐ธ, ๐บ, ๐ผ))) |
84 | 83 | mpoeq3dva 7438 |
. . . . . . 7
โข (๐ โ (๐ โ ๐, ๐ โ ๐ โฆ if(๐ = ๐ธ, ๐บ, if(๐ = ๐น, (๐ป + ๐บ), ๐ผ))) = (๐ โ ๐, ๐ โ ๐ โฆ if(๐ = ๐น, (๐ป + ๐บ), if(๐ = ๐ธ, ๐บ, ๐ผ)))) |
85 | 84 | fveq2d 6850 |
. . . . . 6
โข (๐ โ (๐ทโ(๐ โ ๐, ๐ โ ๐ โฆ if(๐ = ๐ธ, ๐บ, if(๐ = ๐น, (๐ป + ๐บ), ๐ผ)))) = (๐ทโ(๐ โ ๐, ๐ โ ๐ โฆ if(๐ = ๐น, (๐ป + ๐บ), if(๐ = ๐ธ, ๐บ, ๐ผ))))) |
86 | 81, 85, 73 | 3eqtr4d 2783 |
. . . . 5
โข (๐ โ (๐ทโ(๐ โ ๐, ๐ โ ๐ โฆ if(๐ = ๐ธ, ๐บ, if(๐ = ๐น, (๐ป + ๐บ), ๐ผ)))) = (๐ทโ(๐ โ ๐, ๐ โ ๐ โฆ if(๐ = ๐ธ, ๐บ, if(๐ = ๐น, ๐ป, ๐ผ))))) |
87 | 64, 86 | oveq12d 7379 |
. . . 4
โข (๐ โ ((๐ทโ(๐ โ ๐, ๐ โ ๐ โฆ if(๐ = ๐ธ, ๐ป, if(๐ = ๐น, (๐ป + ๐บ), ๐ผ)))) + (๐ทโ(๐ โ ๐, ๐ โ ๐ โฆ if(๐ = ๐ธ, ๐บ, if(๐ = ๐น, (๐ป + ๐บ), ๐ผ))))) = ((๐ทโ(๐ โ ๐, ๐ โ ๐ โฆ if(๐ = ๐ธ, ๐ป, if(๐ = ๐น, ๐บ, ๐ผ)))) + (๐ทโ(๐ โ ๐, ๐ โ ๐ โฆ if(๐ = ๐ธ, ๐บ, if(๐ = ๐น, ๐ป, ๐ผ)))))) |
88 | 31, 32, 87 | 3eqtr3rd 2782 |
. . 3
โข (๐ โ ((๐ทโ(๐ โ ๐, ๐ โ ๐ โฆ if(๐ = ๐ธ, ๐ป, if(๐ = ๐น, ๐บ, ๐ผ)))) + (๐ทโ(๐ โ ๐, ๐ โ ๐ โฆ if(๐ = ๐ธ, ๐บ, if(๐ = ๐น, ๐ป, ๐ผ))))) = 0 ) |
89 | | eqid 2733 |
. . . . 5
โข
(invgโ๐
) = (invgโ๐
) |
90 | 3, 6, 4, 89 | grpinvid1 18810 |
. . . 4
โข ((๐
โ Grp โง (๐ทโ(๐ โ ๐, ๐ โ ๐ โฆ if(๐ = ๐ธ, ๐ป, if(๐ = ๐น, ๐บ, ๐ผ)))) โ ๐พ โง (๐ทโ(๐ โ ๐, ๐ โ ๐ โฆ if(๐ = ๐ธ, ๐บ, if(๐ = ๐น, ๐ป, ๐ผ)))) โ ๐พ) โ (((invgโ๐
)โ(๐ทโ(๐ โ ๐, ๐ โ ๐ โฆ if(๐ = ๐ธ, ๐ป, if(๐ = ๐น, ๐บ, ๐ผ))))) = (๐ทโ(๐ โ ๐, ๐ โ ๐ โฆ if(๐ = ๐ธ, ๐บ, if(๐ = ๐น, ๐ป, ๐ผ)))) โ ((๐ทโ(๐ โ ๐, ๐ โ ๐ โฆ if(๐ = ๐ธ, ๐ป, if(๐ = ๐น, ๐บ, ๐ผ)))) + (๐ทโ(๐ โ ๐, ๐ โ ๐ โฆ if(๐ = ๐ธ, ๐บ, if(๐ = ๐น, ๐ป, ๐ผ))))) = 0 )) |
91 | 23, 55, 77, 90 | syl3anc 1372 |
. . 3
โข (๐ โ
(((invgโ๐
)โ(๐ทโ(๐ โ ๐, ๐ โ ๐ โฆ if(๐ = ๐ธ, ๐ป, if(๐ = ๐น, ๐บ, ๐ผ))))) = (๐ทโ(๐ โ ๐, ๐ โ ๐ โฆ if(๐ = ๐ธ, ๐บ, if(๐ = ๐น, ๐ป, ๐ผ)))) โ ((๐ทโ(๐ โ ๐, ๐ โ ๐ โฆ if(๐ = ๐ธ, ๐ป, if(๐ = ๐น, ๐บ, ๐ผ)))) + (๐ทโ(๐ โ ๐, ๐ โ ๐ โฆ if(๐ = ๐ธ, ๐บ, if(๐ = ๐น, ๐ป, ๐ผ))))) = 0 )) |
92 | 88, 91 | mpbird 257 |
. 2
โข (๐ โ
((invgโ๐
)โ(๐ทโ(๐ โ ๐, ๐ โ ๐ โฆ if(๐ = ๐ธ, ๐ป, if(๐ = ๐น, ๐บ, ๐ผ))))) = (๐ทโ(๐ โ ๐, ๐ โ ๐ โฆ if(๐ = ๐ธ, ๐บ, if(๐ = ๐น, ๐ป, ๐ผ))))) |
93 | 92 | eqcomd 2739 |
1
โข (๐ โ (๐ทโ(๐ โ ๐, ๐ โ ๐ โฆ if(๐ = ๐ธ, ๐บ, if(๐ = ๐น, ๐ป, ๐ผ)))) = ((invgโ๐
)โ(๐ทโ(๐ โ ๐, ๐ โ ๐ โฆ if(๐ = ๐ธ, ๐ป, if(๐ = ๐น, ๐บ, ๐ผ)))))) |