Step | Hyp | Ref
| Expression |
1 | | gexval.4 |
. 2
โข ๐ธ = (gExโ๐บ) |
2 | | df-gex 19318 |
. . 3
โข gEx =
(๐ โ V โฆ
โฆ{๐ฆ โ
โ โฃ โ๐ฅ
โ (Baseโ๐)(๐ฆ(.gโ๐)๐ฅ) = (0gโ๐)} / ๐โฆif(๐ = โ
, 0, inf(๐, โ, < ))) |
3 | | nnex 12166 |
. . . . . 6
โข โ
โ V |
4 | 3 | rabex 5294 |
. . . . 5
โข {๐ฆ โ โ โฃ
โ๐ฅ โ
(Baseโ๐)(๐ฆ(.gโ๐)๐ฅ) = (0gโ๐)} โ V |
5 | 4 | a1i 11 |
. . . 4
โข ((๐บ โ ๐ โง ๐ = ๐บ) โ {๐ฆ โ โ โฃ โ๐ฅ โ (Baseโ๐)(๐ฆ(.gโ๐)๐ฅ) = (0gโ๐)} โ V) |
6 | | simpr 486 |
. . . . . . . . . . . . 13
โข ((๐บ โ ๐ โง ๐ = ๐บ) โ ๐ = ๐บ) |
7 | 6 | fveq2d 6851 |
. . . . . . . . . . . 12
โข ((๐บ โ ๐ โง ๐ = ๐บ) โ (Baseโ๐) = (Baseโ๐บ)) |
8 | | gexval.1 |
. . . . . . . . . . . 12
โข ๐ = (Baseโ๐บ) |
9 | 7, 8 | eqtr4di 2795 |
. . . . . . . . . . 11
โข ((๐บ โ ๐ โง ๐ = ๐บ) โ (Baseโ๐) = ๐) |
10 | 6 | fveq2d 6851 |
. . . . . . . . . . . . . 14
โข ((๐บ โ ๐ โง ๐ = ๐บ) โ (.gโ๐) = (.gโ๐บ)) |
11 | | gexval.2 |
. . . . . . . . . . . . . 14
โข ยท =
(.gโ๐บ) |
12 | 10, 11 | eqtr4di 2795 |
. . . . . . . . . . . . 13
โข ((๐บ โ ๐ โง ๐ = ๐บ) โ (.gโ๐) = ยท ) |
13 | 12 | oveqd 7379 |
. . . . . . . . . . . 12
โข ((๐บ โ ๐ โง ๐ = ๐บ) โ (๐ฆ(.gโ๐)๐ฅ) = (๐ฆ ยท ๐ฅ)) |
14 | 6 | fveq2d 6851 |
. . . . . . . . . . . . 13
โข ((๐บ โ ๐ โง ๐ = ๐บ) โ (0gโ๐) = (0gโ๐บ)) |
15 | | gexval.3 |
. . . . . . . . . . . . 13
โข 0 =
(0gโ๐บ) |
16 | 14, 15 | eqtr4di 2795 |
. . . . . . . . . . . 12
โข ((๐บ โ ๐ โง ๐ = ๐บ) โ (0gโ๐) = 0 ) |
17 | 13, 16 | eqeq12d 2753 |
. . . . . . . . . . 11
โข ((๐บ โ ๐ โง ๐ = ๐บ) โ ((๐ฆ(.gโ๐)๐ฅ) = (0gโ๐) โ (๐ฆ ยท ๐ฅ) = 0 )) |
18 | 9, 17 | raleqbidv 3322 |
. . . . . . . . . 10
โข ((๐บ โ ๐ โง ๐ = ๐บ) โ (โ๐ฅ โ (Baseโ๐)(๐ฆ(.gโ๐)๐ฅ) = (0gโ๐) โ โ๐ฅ โ ๐ (๐ฆ ยท ๐ฅ) = 0 )) |
19 | 18 | rabbidv 3418 |
. . . . . . . . 9
โข ((๐บ โ ๐ โง ๐ = ๐บ) โ {๐ฆ โ โ โฃ โ๐ฅ โ (Baseโ๐)(๐ฆ(.gโ๐)๐ฅ) = (0gโ๐)} = {๐ฆ โ โ โฃ โ๐ฅ โ ๐ (๐ฆ ยท ๐ฅ) = 0 }) |
20 | | gexval.i |
. . . . . . . . 9
โข ๐ผ = {๐ฆ โ โ โฃ โ๐ฅ โ ๐ (๐ฆ ยท ๐ฅ) = 0 } |
21 | 19, 20 | eqtr4di 2795 |
. . . . . . . 8
โข ((๐บ โ ๐ โง ๐ = ๐บ) โ {๐ฆ โ โ โฃ โ๐ฅ โ (Baseโ๐)(๐ฆ(.gโ๐)๐ฅ) = (0gโ๐)} = ๐ผ) |
22 | 21 | eqeq2d 2748 |
. . . . . . 7
โข ((๐บ โ ๐ โง ๐ = ๐บ) โ (๐ = {๐ฆ โ โ โฃ โ๐ฅ โ (Baseโ๐)(๐ฆ(.gโ๐)๐ฅ) = (0gโ๐)} โ ๐ = ๐ผ)) |
23 | 22 | biimpa 478 |
. . . . . 6
โข (((๐บ โ ๐ โง ๐ = ๐บ) โง ๐ = {๐ฆ โ โ โฃ โ๐ฅ โ (Baseโ๐)(๐ฆ(.gโ๐)๐ฅ) = (0gโ๐)}) โ ๐ = ๐ผ) |
24 | 23 | eqeq1d 2739 |
. . . . 5
โข (((๐บ โ ๐ โง ๐ = ๐บ) โง ๐ = {๐ฆ โ โ โฃ โ๐ฅ โ (Baseโ๐)(๐ฆ(.gโ๐)๐ฅ) = (0gโ๐)}) โ (๐ = โ
โ ๐ผ = โ
)) |
25 | 23 | infeq1d 9420 |
. . . . 5
โข (((๐บ โ ๐ โง ๐ = ๐บ) โง ๐ = {๐ฆ โ โ โฃ โ๐ฅ โ (Baseโ๐)(๐ฆ(.gโ๐)๐ฅ) = (0gโ๐)}) โ inf(๐, โ, < ) = inf(๐ผ, โ, < )) |
26 | 24, 25 | ifbieq2d 4517 |
. . . 4
โข (((๐บ โ ๐ โง ๐ = ๐บ) โง ๐ = {๐ฆ โ โ โฃ โ๐ฅ โ (Baseโ๐)(๐ฆ(.gโ๐)๐ฅ) = (0gโ๐)}) โ if(๐ = โ
, 0, inf(๐, โ, < )) = if(๐ผ = โ
, 0, inf(๐ผ, โ, < ))) |
27 | 5, 26 | csbied 3898 |
. . 3
โข ((๐บ โ ๐ โง ๐ = ๐บ) โ โฆ{๐ฆ โ โ โฃ โ๐ฅ โ (Baseโ๐)(๐ฆ(.gโ๐)๐ฅ) = (0gโ๐)} / ๐โฆif(๐ = โ
, 0, inf(๐, โ, < )) = if(๐ผ = โ
, 0, inf(๐ผ, โ, < ))) |
28 | | elex 3466 |
. . 3
โข (๐บ โ ๐ โ ๐บ โ V) |
29 | | c0ex 11156 |
. . . . 5
โข 0 โ
V |
30 | | ltso 11242 |
. . . . . 6
โข < Or
โ |
31 | 30 | infex 9436 |
. . . . 5
โข inf(๐ผ, โ, < ) โ
V |
32 | 29, 31 | ifex 4541 |
. . . 4
โข if(๐ผ = โ
, 0, inf(๐ผ, โ, < )) โ
V |
33 | 32 | a1i 11 |
. . 3
โข (๐บ โ ๐ โ if(๐ผ = โ
, 0, inf(๐ผ, โ, < )) โ
V) |
34 | 2, 27, 28, 33 | fvmptd2 6961 |
. 2
โข (๐บ โ ๐ โ (gExโ๐บ) = if(๐ผ = โ
, 0, inf(๐ผ, โ, < ))) |
35 | 1, 34 | eqtrid 2789 |
1
โข (๐บ โ ๐ โ ๐ธ = if(๐ผ = โ
, 0, inf(๐ผ, โ, < ))) |