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 | 3 | fvexi 6861 |
. . . . 5
โข ๐ โ V |
18 | | nn0ex 12426 |
. . . . 5
โข
โ0 โ V |
19 | | nnex 12166 |
. . . . . . . . 9
โข โ
โ V |
20 | 19 | rabex 5294 |
. . . . . . . 8
โข {๐ฆ โ โ โฃ (๐ฆ ยท ๐ฅ) = 0 } โ
V |
21 | | eqeq1 2741 |
. . . . . . . . 9
โข (๐ = {๐ฆ โ โ โฃ (๐ฆ ยท ๐ฅ) = 0 } โ (๐ = โ
โ {๐ฆ โ โ โฃ (๐ฆ ยท ๐ฅ) = 0 } =
โ
)) |
22 | | infeq1 9419 |
. . . . . . . . 9
โข (๐ = {๐ฆ โ โ โฃ (๐ฆ ยท ๐ฅ) = 0 } โ inf(๐, โ, < ) = inf({๐ฆ โ โ โฃ (๐ฆ ยท ๐ฅ) = 0 }, โ, <
)) |
23 | 21, 22 | ifbieq2d 4517 |
. . . . . . . 8
โข (๐ = {๐ฆ โ โ โฃ (๐ฆ ยท ๐ฅ) = 0 } โ if(๐ = โ
, 0, inf(๐, โ, < )) = if({๐ฆ โ โ โฃ (๐ฆ ยท ๐ฅ) = 0 } = โ
, 0, inf({๐ฆ โ โ โฃ (๐ฆ ยท ๐ฅ) = 0 }, โ, <
))) |
24 | 20, 23 | csbie 3896 |
. . . . . . 7
โข
โฆ{๐ฆ
โ โ โฃ (๐ฆ
ยท
๐ฅ) = 0 } / ๐โฆif(๐ = โ
, 0, inf(๐, โ, < )) = if({๐ฆ โ โ โฃ (๐ฆ ยท ๐ฅ) = 0 } = โ
, 0, inf({๐ฆ โ โ โฃ (๐ฆ ยท ๐ฅ) = 0 }, โ, <
)) |
25 | | 0nn0 12435 |
. . . . . . . . . 10
โข 0 โ
โ0 |
26 | 25 | a1i 11 |
. . . . . . . . 9
โข
((โค โง {๐ฆ
โ โ โฃ (๐ฆ
ยท
๐ฅ) = 0 } = โ
) โ 0
โ โ0) |
27 | | df-ne 2945 |
. . . . . . . . . . . 12
โข ({๐ฆ โ โ โฃ (๐ฆ ยท ๐ฅ) = 0 } โ โ
โ
ยฌ {๐ฆ โ โ
โฃ (๐ฆ ยท ๐ฅ) = 0 } =
โ
) |
28 | | ssrab2 4042 |
. . . . . . . . . . . . 13
โข {๐ฆ โ โ โฃ (๐ฆ ยท ๐ฅ) = 0 } โ
โ |
29 | | nnuz 12813 |
. . . . . . . . . . . . . . 15
โข โ =
(โคโฅโ1) |
30 | 28, 29 | sseqtri 3985 |
. . . . . . . . . . . . . 14
โข {๐ฆ โ โ โฃ (๐ฆ ยท ๐ฅ) = 0 } โ
(โคโฅโ1) |
31 | | infssuzcl 12864 |
. . . . . . . . . . . . . 14
โข (({๐ฆ โ โ โฃ (๐ฆ ยท ๐ฅ) = 0 } โ
(โคโฅโ1) โง {๐ฆ โ โ โฃ (๐ฆ ยท ๐ฅ) = 0 } โ โ
) โ
inf({๐ฆ โ โ
โฃ (๐ฆ ยท ๐ฅ) = 0 }, โ, < ) โ
{๐ฆ โ โ โฃ
(๐ฆ ยท ๐ฅ) = 0 }) |
32 | 30, 31 | mpan 689 |
. . . . . . . . . . . . 13
โข ({๐ฆ โ โ โฃ (๐ฆ ยท ๐ฅ) = 0 } โ โ
โ
inf({๐ฆ โ โ
โฃ (๐ฆ ยท ๐ฅ) = 0 }, โ, < ) โ
{๐ฆ โ โ โฃ
(๐ฆ ยท ๐ฅ) = 0 }) |
33 | 28, 32 | sselid 3947 |
. . . . . . . . . . . 12
โข ({๐ฆ โ โ โฃ (๐ฆ ยท ๐ฅ) = 0 } โ โ
โ
inf({๐ฆ โ โ
โฃ (๐ฆ ยท ๐ฅ) = 0 }, โ, < ) โ
โ) |
34 | 27, 33 | sylbir 234 |
. . . . . . . . . . 11
โข (ยฌ
{๐ฆ โ โ โฃ
(๐ฆ ยท ๐ฅ) = 0 } = โ
โ
inf({๐ฆ โ โ
โฃ (๐ฆ ยท ๐ฅ) = 0 }, โ, < ) โ
โ) |
35 | 34 | nnnn0d 12480 |
. . . . . . . . . 10
โข (ยฌ
{๐ฆ โ โ โฃ
(๐ฆ ยท ๐ฅ) = 0 } = โ
โ
inf({๐ฆ โ โ
โฃ (๐ฆ ยท ๐ฅ) = 0 }, โ, < ) โ
โ0) |
36 | 35 | adantl 483 |
. . . . . . . . 9
โข
((โค โง ยฌ {๐ฆ โ โ โฃ (๐ฆ ยท ๐ฅ) = 0 } = โ
) โ
inf({๐ฆ โ โ
โฃ (๐ฆ ยท ๐ฅ) = 0 }, โ, < ) โ
โ0) |
37 | 26, 36 | ifclda 4526 |
. . . . . . . 8
โข (โค
โ if({๐ฆ โ โ
โฃ (๐ฆ ยท ๐ฅ) = 0 } = โ
, 0, inf({๐ฆ โ โ โฃ (๐ฆ ยท ๐ฅ) = 0 }, โ, < )) โ
โ0) |
38 | 37 | mptru 1549 |
. . . . . . 7
โข if({๐ฆ โ โ โฃ (๐ฆ ยท ๐ฅ) = 0 } = โ
, 0, inf({๐ฆ โ โ โฃ (๐ฆ ยท ๐ฅ) = 0 }, โ, < )) โ
โ0 |
39 | 24, 38 | eqeltri 2834 |
. . . . . 6
โข
โฆ{๐ฆ
โ โ โฃ (๐ฆ
ยท
๐ฅ) = 0 } / ๐โฆif(๐ = โ
, 0, inf(๐, โ, < )) โ
โ0 |
40 | 39 | rgenw 3069 |
. . . . 5
โข
โ๐ฅ โ
๐ โฆ{๐ฆ โ โ โฃ (๐ฆ ยท ๐ฅ) = 0 } / ๐โฆif(๐ = โ
, 0, inf(๐, โ, < )) โ
โ0 |
41 | 17, 18, 40 | mptexw 7890 |
. . . 4
โข (๐ฅ โ ๐ โฆ โฆ{๐ฆ โ โ โฃ (๐ฆ ยท ๐ฅ) = 0 } / ๐โฆif(๐ = โ
, 0, inf(๐, โ, < ))) โ V |
42 | 15, 16, 41 | fvmpt 6953 |
. . 3
โข (๐บ โ V โ (odโ๐บ) = (๐ฅ โ ๐ โฆ โฆ{๐ฆ โ โ โฃ (๐ฆ ยท ๐ฅ) = 0 } / ๐โฆif(๐ = โ
, 0, inf(๐, โ, < )))) |
43 | | fvprc 6839 |
. . . 4
โข (ยฌ
๐บ โ V โ
(odโ๐บ) =
โ
) |
44 | | fvprc 6839 |
. . . . . . 7
โข (ยฌ
๐บ โ V โ
(Baseโ๐บ) =
โ
) |
45 | 3, 44 | eqtrid 2789 |
. . . . . 6
โข (ยฌ
๐บ โ V โ ๐ = โ
) |
46 | 45 | mpteq1d 5205 |
. . . . 5
โข (ยฌ
๐บ โ V โ (๐ฅ โ ๐ โฆ โฆ{๐ฆ โ โ โฃ (๐ฆ ยท ๐ฅ) = 0 } / ๐โฆif(๐ = โ
, 0, inf(๐, โ, < ))) = (๐ฅ โ โ
โฆ โฆ{๐ฆ โ โ โฃ (๐ฆ ยท ๐ฅ) = 0 } / ๐โฆif(๐ = โ
, 0, inf(๐, โ, < )))) |
47 | | mpt0 6648 |
. . . . 5
โข (๐ฅ โ โ
โฆ
โฆ{๐ฆ โ
โ โฃ (๐ฆ ยท ๐ฅ) = 0 } / ๐โฆif(๐ = โ
, 0, inf(๐, โ, < ))) =
โ
|
48 | 46, 47 | eqtrdi 2793 |
. . . 4
โข (ยฌ
๐บ โ V โ (๐ฅ โ ๐ โฆ โฆ{๐ฆ โ โ โฃ (๐ฆ ยท ๐ฅ) = 0 } / ๐โฆif(๐ = โ
, 0, inf(๐, โ, < ))) =
โ
) |
49 | 43, 48 | eqtr4d 2780 |
. . 3
โข (ยฌ
๐บ โ V โ
(odโ๐บ) = (๐ฅ โ ๐ โฆ โฆ{๐ฆ โ โ โฃ (๐ฆ ยท ๐ฅ) = 0 } / ๐โฆif(๐ = โ
, 0, inf(๐, โ, < )))) |
50 | 42, 49 | pm2.61i 182 |
. 2
โข
(odโ๐บ) =
(๐ฅ โ ๐ โฆ โฆ{๐ฆ โ โ โฃ (๐ฆ ยท ๐ฅ) = 0 } / ๐โฆif(๐ = โ
, 0, inf(๐, โ, < ))) |
51 | 1, 50 | eqtri 2765 |
1
โข ๐ = (๐ฅ โ ๐ โฆ โฆ{๐ฆ โ โ โฃ (๐ฆ ยท ๐ฅ) = 0 } / ๐โฆif(๐ = โ
, 0, inf(๐, โ, < ))) |