Step | Hyp | Ref
| Expression |
1 | | oveq1 7411 |
. . . . . 6
โข (๐ฆ = ๐ โ (๐ฆ ยท ๐ฅ) = (๐ ยท ๐ฅ)) |
2 | 1 | eqeq1d 2728 |
. . . . 5
โข (๐ฆ = ๐ โ ((๐ฆ ยท ๐ฅ) = 0 โ (๐ ยท ๐ฅ) = 0 )) |
3 | 2 | ralbidv 3171 |
. . . 4
โข (๐ฆ = ๐ โ (โ๐ฅ โ ๐ (๐ฆ ยท ๐ฅ) = 0 โ โ๐ฅ โ ๐ (๐ ยท ๐ฅ) = 0 )) |
4 | 3 | elrab 3678 |
. . 3
โข (๐ โ {๐ฆ โ โ โฃ โ๐ฅ โ ๐ (๐ฆ ยท ๐ฅ) = 0 } โ (๐ โ โ โง
โ๐ฅ โ ๐ (๐ ยท ๐ฅ) = 0 )) |
5 | | gexcl.1 |
. . . . . 6
โข ๐ = (Baseโ๐บ) |
6 | | gexid.3 |
. . . . . 6
โข ยท =
(.gโ๐บ) |
7 | | gexid.4 |
. . . . . 6
โข 0 =
(0gโ๐บ) |
8 | | gexcl.2 |
. . . . . 6
โข ๐ธ = (gExโ๐บ) |
9 | | eqid 2726 |
. . . . . 6
โข {๐ฆ โ โ โฃ
โ๐ฅ โ ๐ (๐ฆ ยท ๐ฅ) = 0 } = {๐ฆ โ โ โฃ โ๐ฅ โ ๐ (๐ฆ ยท ๐ฅ) = 0 } |
10 | 5, 6, 7, 8, 9 | gexval 19495 |
. . . . 5
โข (๐บ โ ๐ โ ๐ธ = if({๐ฆ โ โ โฃ โ๐ฅ โ ๐ (๐ฆ ยท ๐ฅ) = 0 } = โ
, 0, inf({๐ฆ โ โ โฃ
โ๐ฅ โ ๐ (๐ฆ ยท ๐ฅ) = 0 }, โ, <
))) |
11 | | ne0i 4329 |
. . . . . 6
โข (๐ โ {๐ฆ โ โ โฃ โ๐ฅ โ ๐ (๐ฆ ยท ๐ฅ) = 0 } โ {๐ฆ โ โ โฃ
โ๐ฅ โ ๐ (๐ฆ ยท ๐ฅ) = 0 } โ
โ
) |
12 | | ifnefalse 4535 |
. . . . . 6
โข ({๐ฆ โ โ โฃ
โ๐ฅ โ ๐ (๐ฆ ยท ๐ฅ) = 0 } โ โ
โ
if({๐ฆ โ โ
โฃ โ๐ฅ โ
๐ (๐ฆ ยท ๐ฅ) = 0 } = โ
, 0, inf({๐ฆ โ โ โฃ
โ๐ฅ โ ๐ (๐ฆ ยท ๐ฅ) = 0 }, โ, < )) =
inf({๐ฆ โ โ
โฃ โ๐ฅ โ
๐ (๐ฆ ยท ๐ฅ) = 0 }, โ, <
)) |
13 | 11, 12 | syl 17 |
. . . . 5
โข (๐ โ {๐ฆ โ โ โฃ โ๐ฅ โ ๐ (๐ฆ ยท ๐ฅ) = 0 } โ if({๐ฆ โ โ โฃ
โ๐ฅ โ ๐ (๐ฆ ยท ๐ฅ) = 0 } = โ
, 0, inf({๐ฆ โ โ โฃ
โ๐ฅ โ ๐ (๐ฆ ยท ๐ฅ) = 0 }, โ, < )) =
inf({๐ฆ โ โ
โฃ โ๐ฅ โ
๐ (๐ฆ ยท ๐ฅ) = 0 }, โ, <
)) |
14 | 10, 13 | sylan9eq 2786 |
. . . 4
โข ((๐บ โ ๐ โง ๐ โ {๐ฆ โ โ โฃ โ๐ฅ โ ๐ (๐ฆ ยท ๐ฅ) = 0 }) โ ๐ธ = inf({๐ฆ โ โ โฃ โ๐ฅ โ ๐ (๐ฆ ยท ๐ฅ) = 0 }, โ, <
)) |
15 | | ssrab2 4072 |
. . . . . 6
โข {๐ฆ โ โ โฃ
โ๐ฅ โ ๐ (๐ฆ ยท ๐ฅ) = 0 } โ
โ |
16 | | nnuz 12866 |
. . . . . . . 8
โข โ =
(โคโฅโ1) |
17 | 15, 16 | sseqtri 4013 |
. . . . . . 7
โข {๐ฆ โ โ โฃ
โ๐ฅ โ ๐ (๐ฆ ยท ๐ฅ) = 0 } โ
(โคโฅโ1) |
18 | 11 | adantl 481 |
. . . . . . 7
โข ((๐บ โ ๐ โง ๐ โ {๐ฆ โ โ โฃ โ๐ฅ โ ๐ (๐ฆ ยท ๐ฅ) = 0 }) โ {๐ฆ โ โ โฃ
โ๐ฅ โ ๐ (๐ฆ ยท ๐ฅ) = 0 } โ
โ
) |
19 | | infssuzcl 12917 |
. . . . . . 7
โข (({๐ฆ โ โ โฃ
โ๐ฅ โ ๐ (๐ฆ ยท ๐ฅ) = 0 } โ
(โคโฅโ1) โง {๐ฆ โ โ โฃ โ๐ฅ โ ๐ (๐ฆ ยท ๐ฅ) = 0 } โ โ
) โ
inf({๐ฆ โ โ
โฃ โ๐ฅ โ
๐ (๐ฆ ยท ๐ฅ) = 0 }, โ, < ) โ
{๐ฆ โ โ โฃ
โ๐ฅ โ ๐ (๐ฆ ยท ๐ฅ) = 0 }) |
20 | 17, 18, 19 | sylancr 586 |
. . . . . 6
โข ((๐บ โ ๐ โง ๐ โ {๐ฆ โ โ โฃ โ๐ฅ โ ๐ (๐ฆ ยท ๐ฅ) = 0 }) โ inf({๐ฆ โ โ โฃ
โ๐ฅ โ ๐ (๐ฆ ยท ๐ฅ) = 0 }, โ, < ) โ
{๐ฆ โ โ โฃ
โ๐ฅ โ ๐ (๐ฆ ยท ๐ฅ) = 0 }) |
21 | 15, 20 | sselid 3975 |
. . . . 5
โข ((๐บ โ ๐ โง ๐ โ {๐ฆ โ โ โฃ โ๐ฅ โ ๐ (๐ฆ ยท ๐ฅ) = 0 }) โ inf({๐ฆ โ โ โฃ
โ๐ฅ โ ๐ (๐ฆ ยท ๐ฅ) = 0 }, โ, < ) โ
โ) |
22 | | infssuzle 12916 |
. . . . . . 7
โข (({๐ฆ โ โ โฃ
โ๐ฅ โ ๐ (๐ฆ ยท ๐ฅ) = 0 } โ
(โคโฅโ1) โง ๐ โ {๐ฆ โ โ โฃ โ๐ฅ โ ๐ (๐ฆ ยท ๐ฅ) = 0 }) โ inf({๐ฆ โ โ โฃ
โ๐ฅ โ ๐ (๐ฆ ยท ๐ฅ) = 0 }, โ, < ) โค
๐) |
23 | 17, 22 | mpan 687 |
. . . . . 6
โข (๐ โ {๐ฆ โ โ โฃ โ๐ฅ โ ๐ (๐ฆ ยท ๐ฅ) = 0 } โ inf({๐ฆ โ โ โฃ
โ๐ฅ โ ๐ (๐ฆ ยท ๐ฅ) = 0 }, โ, < ) โค
๐) |
24 | 23 | adantl 481 |
. . . . 5
โข ((๐บ โ ๐ โง ๐ โ {๐ฆ โ โ โฃ โ๐ฅ โ ๐ (๐ฆ ยท ๐ฅ) = 0 }) โ inf({๐ฆ โ โ โฃ
โ๐ฅ โ ๐ (๐ฆ ยท ๐ฅ) = 0 }, โ, < ) โค
๐) |
25 | | elrabi 3672 |
. . . . . . . 8
โข (๐ โ {๐ฆ โ โ โฃ โ๐ฅ โ ๐ (๐ฆ ยท ๐ฅ) = 0 } โ ๐ โ โ) |
26 | 25 | nnzd 12586 |
. . . . . . 7
โข (๐ โ {๐ฆ โ โ โฃ โ๐ฅ โ ๐ (๐ฆ ยท ๐ฅ) = 0 } โ ๐ โ โค) |
27 | | fznn 13572 |
. . . . . . 7
โข (๐ โ โค โ
(inf({๐ฆ โ โ
โฃ โ๐ฅ โ
๐ (๐ฆ ยท ๐ฅ) = 0 }, โ, < ) โ
(1...๐) โ (inf({๐ฆ โ โ โฃ
โ๐ฅ โ ๐ (๐ฆ ยท ๐ฅ) = 0 }, โ, < ) โ
โ โง inf({๐ฆ โ
โ โฃ โ๐ฅ
โ ๐ (๐ฆ ยท ๐ฅ) = 0 }, โ, < ) โค
๐))) |
28 | 26, 27 | syl 17 |
. . . . . 6
โข (๐ โ {๐ฆ โ โ โฃ โ๐ฅ โ ๐ (๐ฆ ยท ๐ฅ) = 0 } โ (inf({๐ฆ โ โ โฃ
โ๐ฅ โ ๐ (๐ฆ ยท ๐ฅ) = 0 }, โ, < ) โ
(1...๐) โ (inf({๐ฆ โ โ โฃ
โ๐ฅ โ ๐ (๐ฆ ยท ๐ฅ) = 0 }, โ, < ) โ
โ โง inf({๐ฆ โ
โ โฃ โ๐ฅ
โ ๐ (๐ฆ ยท ๐ฅ) = 0 }, โ, < ) โค
๐))) |
29 | 28 | adantl 481 |
. . . . 5
โข ((๐บ โ ๐ โง ๐ โ {๐ฆ โ โ โฃ โ๐ฅ โ ๐ (๐ฆ ยท ๐ฅ) = 0 }) โ (inf({๐ฆ โ โ โฃ
โ๐ฅ โ ๐ (๐ฆ ยท ๐ฅ) = 0 }, โ, < ) โ
(1...๐) โ (inf({๐ฆ โ โ โฃ
โ๐ฅ โ ๐ (๐ฆ ยท ๐ฅ) = 0 }, โ, < ) โ
โ โง inf({๐ฆ โ
โ โฃ โ๐ฅ
โ ๐ (๐ฆ ยท ๐ฅ) = 0 }, โ, < ) โค
๐))) |
30 | 21, 24, 29 | mpbir2and 710 |
. . . 4
โข ((๐บ โ ๐ โง ๐ โ {๐ฆ โ โ โฃ โ๐ฅ โ ๐ (๐ฆ ยท ๐ฅ) = 0 }) โ inf({๐ฆ โ โ โฃ
โ๐ฅ โ ๐ (๐ฆ ยท ๐ฅ) = 0 }, โ, < ) โ
(1...๐)) |
31 | 14, 30 | eqeltrd 2827 |
. . 3
โข ((๐บ โ ๐ โง ๐ โ {๐ฆ โ โ โฃ โ๐ฅ โ ๐ (๐ฆ ยท ๐ฅ) = 0 }) โ ๐ธ โ (1...๐)) |
32 | 4, 31 | sylan2br 594 |
. 2
โข ((๐บ โ ๐ โง (๐ โ โ โง โ๐ฅ โ ๐ (๐ ยท ๐ฅ) = 0 )) โ ๐ธ โ (1...๐)) |
33 | 32 | 3impb 1112 |
1
โข ((๐บ โ ๐ โง ๐ โ โ โง โ๐ฅ โ ๐ (๐ ยท ๐ฅ) = 0 ) โ ๐ธ โ (1...๐)) |