Step | Hyp | Ref
| Expression |
1 | | elin 3930 |
. . 3
โข (๐ โ (LinOp โฉ ContOp)
โ (๐ โ LinOp
โง ๐ โ
ContOp)) |
2 | | fveq1 6845 |
. . . . . . . 8
โข (๐ = if(๐ โ (LinOp โฉ ContOp), ๐, ( I โพ โ)) โ
(๐โ๐ด) = (if(๐ โ (LinOp โฉ ContOp), ๐, ( I โพ
โ))โ๐ด)) |
3 | 2 | fveq2d 6850 |
. . . . . . 7
โข (๐ = if(๐ โ (LinOp โฉ ContOp), ๐, ( I โพ โ)) โ
(normโโ(๐โ๐ด)) =
(normโโ(if(๐ โ (LinOp โฉ ContOp), ๐, ( I โพ
โ))โ๐ด))) |
4 | | fveq2 6846 |
. . . . . . . 8
โข (๐ = if(๐ โ (LinOp โฉ ContOp), ๐, ( I โพ โ)) โ
(normopโ๐)
= (normopโif(๐ โ (LinOp โฉ ContOp), ๐, ( I โพ
โ)))) |
5 | 4 | oveq1d 7376 |
. . . . . . 7
โข (๐ = if(๐ โ (LinOp โฉ ContOp), ๐, ( I โพ โ)) โ
((normopโ๐) ยท
(normโโ๐ด)) = ((normopโif(๐ โ (LinOp โฉ ContOp),
๐, ( I โพ โ)))
ยท (normโโ๐ด))) |
6 | 3, 5 | breq12d 5122 |
. . . . . 6
โข (๐ = if(๐ โ (LinOp โฉ ContOp), ๐, ( I โพ โ)) โ
((normโโ(๐โ๐ด)) โค ((normopโ๐) ยท
(normโโ๐ด)) โ
(normโโ(if(๐ โ (LinOp โฉ ContOp), ๐, ( I โพ
โ))โ๐ด)) โค
((normopโif(๐ โ (LinOp โฉ ContOp), ๐, ( I โพ โ)))
ยท (normโโ๐ด)))) |
7 | 6 | imbi2d 341 |
. . . . 5
โข (๐ = if(๐ โ (LinOp โฉ ContOp), ๐, ( I โพ โ)) โ
((๐ด โ โ โ
(normโโ(๐โ๐ด)) โค ((normopโ๐) ยท
(normโโ๐ด))) โ (๐ด โ โ โ
(normโโ(if(๐ โ (LinOp โฉ ContOp), ๐, ( I โพ
โ))โ๐ด)) โค
((normopโif(๐ โ (LinOp โฉ ContOp), ๐, ( I โพ โ)))
ยท (normโโ๐ด))))) |
8 | | idlnop 30983 |
. . . . . . . . . 10
โข ( I
โพ โ) โ LinOp |
9 | | idcnop 30972 |
. . . . . . . . . 10
โข ( I
โพ โ) โ ContOp |
10 | | elin 3930 |
. . . . . . . . . 10
โข (( I
โพ โ) โ (LinOp โฉ ContOp) โ (( I โพ โ)
โ LinOp โง ( I โพ โ) โ ContOp)) |
11 | 8, 9, 10 | mpbir2an 710 |
. . . . . . . . 9
โข ( I
โพ โ) โ (LinOp โฉ ContOp) |
12 | 11 | elimel 4559 |
. . . . . . . 8
โข if(๐ โ (LinOp โฉ ContOp),
๐, ( I โพ โ))
โ (LinOp โฉ ContOp) |
13 | | elin 3930 |
. . . . . . . 8
โข (if(๐ โ (LinOp โฉ ContOp),
๐, ( I โพ โ))
โ (LinOp โฉ ContOp) โ (if(๐ โ (LinOp โฉ ContOp), ๐, ( I โพ โ)) โ
LinOp โง if(๐ โ
(LinOp โฉ ContOp), ๐, (
I โพ โ)) โ ContOp)) |
14 | 12, 13 | mpbi 229 |
. . . . . . 7
โข (if(๐ โ (LinOp โฉ ContOp),
๐, ( I โพ โ))
โ LinOp โง if(๐
โ (LinOp โฉ ContOp), ๐, ( I โพ โ)) โ
ContOp) |
15 | 14 | simpli 485 |
. . . . . 6
โข if(๐ โ (LinOp โฉ ContOp),
๐, ( I โพ โ))
โ LinOp |
16 | 14 | simpri 487 |
. . . . . 6
โข if(๐ โ (LinOp โฉ ContOp),
๐, ( I โพ โ))
โ ContOp |
17 | 15, 16 | nmcoplbi 31019 |
. . . . 5
โข (๐ด โ โ โ
(normโโ(if(๐ โ (LinOp โฉ ContOp), ๐, ( I โพ
โ))โ๐ด)) โค
((normopโif(๐ โ (LinOp โฉ ContOp), ๐, ( I โพ โ)))
ยท (normโโ๐ด))) |
18 | 7, 17 | dedth 4548 |
. . . 4
โข (๐ โ (LinOp โฉ ContOp)
โ (๐ด โ โ
โ (normโโ(๐โ๐ด)) โค ((normopโ๐) ยท
(normโโ๐ด)))) |
19 | 18 | imp 408 |
. . 3
โข ((๐ โ (LinOp โฉ ContOp)
โง ๐ด โ โ)
โ (normโโ(๐โ๐ด)) โค ((normopโ๐) ยท
(normโโ๐ด))) |
20 | 1, 19 | sylanbr 583 |
. 2
โข (((๐ โ LinOp โง ๐ โ ContOp) โง ๐ด โ โ) โ
(normโโ(๐โ๐ด)) โค ((normopโ๐) ยท
(normโโ๐ด))) |
21 | 20 | 3impa 1111 |
1
โข ((๐ โ LinOp โง ๐ โ ContOp โง ๐ด โ โ) โ
(normโโ(๐โ๐ด)) โค ((normopโ๐) ยท
(normโโ๐ด))) |