Step | Hyp | Ref
| Expression |
1 | | odval.4 |
. 2
โข ๐ = (odโ๐บ) |
2 | | fveq2 6847 |
. . . . . 6
โข (๐ = ๐บ โ (Baseโ๐) = (Baseโ๐บ)) |
3 | | odval.1 |
. . . . . 6
โข ๐ = (Baseโ๐บ) |
4 | 2, 3 | eqtr4di 2795 |
. . . . 5
โข (๐ = ๐บ โ (Baseโ๐) = ๐) |
5 | | fveq2 6847 |
. . . . . . . . . 10
โข (๐ = ๐บ โ (.gโ๐) = (.gโ๐บ)) |
6 | | odval.2 |
. . . . . . . . . 10
โข ยท =
(.gโ๐บ) |
7 | 5, 6 | eqtr4di 2795 |
. . . . . . . . 9
โข (๐ = ๐บ โ (.gโ๐) = ยท ) |
8 | 7 | oveqd 7379 |
. . . . . . . 8
โข (๐ = ๐บ โ (๐ฆ(.gโ๐)๐ฅ) = (๐ฆ ยท ๐ฅ)) |
9 | | fveq2 6847 |
. . . . . . . . 9
โข (๐ = ๐บ โ (0gโ๐) = (0gโ๐บ)) |
10 | | odval.3 |
. . . . . . . . 9
โข 0 =
(0gโ๐บ) |
11 | 9, 10 | eqtr4di 2795 |
. . . . . . . 8
โข (๐ = ๐บ โ (0gโ๐) = 0 ) |
12 | 8, 11 | eqeq12d 2753 |
. . . . . . 7
โข (๐ = ๐บ โ ((๐ฆ(.gโ๐)๐ฅ) = (0gโ๐) โ (๐ฆ ยท ๐ฅ) = 0 )) |
13 | 12 | rabbidv 3418 |
. . . . . 6
โข (๐ = ๐บ โ {๐ฆ โ โ โฃ (๐ฆ(.gโ๐)๐ฅ) = (0gโ๐)} = {๐ฆ โ โ โฃ (๐ฆ ยท ๐ฅ) = 0 }) |
14 | 13 | csbeq1d 3864 |
. . . . 5
โข (๐ = ๐บ โ โฆ{๐ฆ โ โ โฃ (๐ฆ(.gโ๐)๐ฅ) = (0gโ๐)} / ๐โฆif(๐ = โ
, 0, inf(๐, โ, < )) = โฆ{๐ฆ โ โ โฃ (๐ฆ ยท ๐ฅ) = 0 } / ๐โฆif(๐ = โ
, 0, inf(๐, โ, < ))) |
15 | 4, 14 | mpteq12dv 5201 |
. . . 4
โข (๐ = ๐บ โ (๐ฅ โ (Baseโ๐) โฆ โฆ{๐ฆ โ โ โฃ (๐ฆ(.gโ๐)๐ฅ) = (0gโ๐)} / ๐โฆif(๐ = โ
, 0, inf(๐, โ, < ))) = (๐ฅ โ ๐ โฆ โฆ{๐ฆ โ โ โฃ (๐ฆ ยท ๐ฅ) = 0 } / ๐โฆif(๐ = โ
, 0, inf(๐, โ, < )))) |
16 | | df-od 19317 |
. . . 4
โข od =
(๐ โ V โฆ (๐ฅ โ (Baseโ๐) โฆ โฆ{๐ฆ โ โ โฃ (๐ฆ(.gโ๐)๐ฅ) = (0gโ๐)} / ๐โฆif(๐ = โ
, 0, inf(๐, โ, < )))) |
17 | 15, 16, 3 | mptfvmpt 7183 |
. . 3
โข (๐บ โ V โ (odโ๐บ) = (๐ฅ โ ๐ โฆ โฆ{๐ฆ โ โ โฃ (๐ฆ ยท ๐ฅ) = 0 } / ๐โฆif(๐ = โ
, 0, inf(๐, โ, < )))) |
18 | | fvprc 6839 |
. . . 4
โข (ยฌ
๐บ โ V โ
(odโ๐บ) =
โ
) |
19 | | fvprc 6839 |
. . . . . . 7
โข (ยฌ
๐บ โ V โ
(Baseโ๐บ) =
โ
) |
20 | 3, 19 | eqtrid 2789 |
. . . . . 6
โข (ยฌ
๐บ โ V โ ๐ = โ
) |
21 | 20 | mpteq1d 5205 |
. . . . 5
โข (ยฌ
๐บ โ V โ (๐ฅ โ ๐ โฆ โฆ{๐ฆ โ โ โฃ (๐ฆ ยท ๐ฅ) = 0 } / ๐โฆif(๐ = โ
, 0, inf(๐, โ, < ))) = (๐ฅ โ โ
โฆ โฆ{๐ฆ โ โ โฃ (๐ฆ ยท ๐ฅ) = 0 } / ๐โฆif(๐ = โ
, 0, inf(๐, โ, < )))) |
22 | | mpt0 6648 |
. . . . 5
โข (๐ฅ โ โ
โฆ
โฆ{๐ฆ โ
โ โฃ (๐ฆ ยท ๐ฅ) = 0 } / ๐โฆif(๐ = โ
, 0, inf(๐, โ, < ))) =
โ
|
23 | 21, 22 | eqtrdi 2793 |
. . . 4
โข (ยฌ
๐บ โ V โ (๐ฅ โ ๐ โฆ โฆ{๐ฆ โ โ โฃ (๐ฆ ยท ๐ฅ) = 0 } / ๐โฆif(๐ = โ
, 0, inf(๐, โ, < ))) =
โ
) |
24 | 18, 23 | eqtr4d 2780 |
. . 3
โข (ยฌ
๐บ โ V โ
(odโ๐บ) = (๐ฅ โ ๐ โฆ โฆ{๐ฆ โ โ โฃ (๐ฆ ยท ๐ฅ) = 0 } / ๐โฆif(๐ = โ
, 0, inf(๐, โ, < )))) |
25 | 17, 24 | pm2.61i 182 |
. 2
โข
(odโ๐บ) =
(๐ฅ โ ๐ โฆ โฆ{๐ฆ โ โ โฃ (๐ฆ ยท ๐ฅ) = 0 } / ๐โฆif(๐ = โ
, 0, inf(๐, โ, < ))) |
26 | 1, 25 | eqtri 2765 |
1
โข ๐ = (๐ฅ โ ๐ โฆ โฆ{๐ฆ โ โ โฃ (๐ฆ ยท ๐ฅ) = 0 } / ๐โฆif(๐ = โ
, 0, inf(๐, โ, < ))) |