Step | Hyp | Ref
| Expression |
1 | | nmlno0.7 |
. . . . . 6
โข ๐ฟ = (๐ LnOp ๐) |
2 | | oveq1 7416 |
. . . . . 6
โข (๐ = if(๐ โ NrmCVec, ๐, โจโจ + , ยท โฉ,
absโฉ) โ (๐ LnOp
๐) = (if(๐ โ NrmCVec, ๐, โจโจ + , ยท โฉ,
absโฉ) LnOp ๐)) |
3 | 1, 2 | eqtrid 2785 |
. . . . 5
โข (๐ = if(๐ โ NrmCVec, ๐, โจโจ + , ยท โฉ,
absโฉ) โ ๐ฟ =
(if(๐ โ NrmCVec, ๐, โจโจ + , ยท
โฉ, absโฉ) LnOp ๐)) |
4 | 3 | eleq2d 2820 |
. . . 4
โข (๐ = if(๐ โ NrmCVec, ๐, โจโจ + , ยท โฉ,
absโฉ) โ (๐ โ
๐ฟ โ ๐ โ (if(๐ โ NrmCVec, ๐, โจโจ + , ยท โฉ,
absโฉ) LnOp ๐))) |
5 | | nmlno0.3 |
. . . . . . . 8
โข ๐ = (๐ normOpOLD ๐) |
6 | | oveq1 7416 |
. . . . . . . 8
โข (๐ = if(๐ โ NrmCVec, ๐, โจโจ + , ยท โฉ,
absโฉ) โ (๐
normOpOLD ๐) =
(if(๐ โ NrmCVec, ๐, โจโจ + , ยท
โฉ, absโฉ) normOpOLD ๐)) |
7 | 5, 6 | eqtrid 2785 |
. . . . . . 7
โข (๐ = if(๐ โ NrmCVec, ๐, โจโจ + , ยท โฉ,
absโฉ) โ ๐ =
(if(๐ โ NrmCVec, ๐, โจโจ + , ยท
โฉ, absโฉ) normOpOLD ๐)) |
8 | 7 | fveq1d 6894 |
. . . . . 6
โข (๐ = if(๐ โ NrmCVec, ๐, โจโจ + , ยท โฉ,
absโฉ) โ (๐โ๐) = ((if(๐ โ NrmCVec, ๐, โจโจ + , ยท โฉ,
absโฉ) normOpOLD ๐)โ๐)) |
9 | 8 | eqeq1d 2735 |
. . . . 5
โข (๐ = if(๐ โ NrmCVec, ๐, โจโจ + , ยท โฉ,
absโฉ) โ ((๐โ๐) = 0 โ ((if(๐ โ NrmCVec, ๐, โจโจ + , ยท โฉ,
absโฉ) normOpOLD ๐)โ๐) = 0)) |
10 | | nmlno0.0 |
. . . . . . 7
โข ๐ = (๐ 0op ๐) |
11 | | oveq1 7416 |
. . . . . . 7
โข (๐ = if(๐ โ NrmCVec, ๐, โจโจ + , ยท โฉ,
absโฉ) โ (๐
0op ๐) =
(if(๐ โ NrmCVec, ๐, โจโจ + , ยท
โฉ, absโฉ) 0op ๐)) |
12 | 10, 11 | eqtrid 2785 |
. . . . . 6
โข (๐ = if(๐ โ NrmCVec, ๐, โจโจ + , ยท โฉ,
absโฉ) โ ๐ =
(if(๐ โ NrmCVec, ๐, โจโจ + , ยท
โฉ, absโฉ) 0op ๐)) |
13 | 12 | eqeq2d 2744 |
. . . . 5
โข (๐ = if(๐ โ NrmCVec, ๐, โจโจ + , ยท โฉ,
absโฉ) โ (๐ =
๐ โ ๐ = (if(๐ โ NrmCVec, ๐, โจโจ + , ยท โฉ,
absโฉ) 0op ๐))) |
14 | 9, 13 | bibi12d 346 |
. . . 4
โข (๐ = if(๐ โ NrmCVec, ๐, โจโจ + , ยท โฉ,
absโฉ) โ (((๐โ๐) = 0 โ ๐ = ๐) โ (((if(๐ โ NrmCVec, ๐, โจโจ + , ยท โฉ,
absโฉ) normOpOLD ๐)โ๐) = 0 โ ๐ = (if(๐ โ NrmCVec, ๐, โจโจ + , ยท โฉ,
absโฉ) 0op ๐)))) |
15 | 4, 14 | imbi12d 345 |
. . 3
โข (๐ = if(๐ โ NrmCVec, ๐, โจโจ + , ยท โฉ,
absโฉ) โ ((๐
โ ๐ฟ โ ((๐โ๐) = 0 โ ๐ = ๐)) โ (๐ โ (if(๐ โ NrmCVec, ๐, โจโจ + , ยท โฉ,
absโฉ) LnOp ๐) โ
(((if(๐ โ NrmCVec,
๐, โจโจ + ,
ยท โฉ, absโฉ) normOpOLD ๐)โ๐) = 0 โ ๐ = (if(๐ โ NrmCVec, ๐, โจโจ + , ยท โฉ,
absโฉ) 0op ๐))))) |
16 | | oveq2 7417 |
. . . . 5
โข (๐ = if(๐ โ NrmCVec, ๐, โจโจ + , ยท โฉ,
absโฉ) โ (if(๐
โ NrmCVec, ๐,
โจโจ + , ยท โฉ, absโฉ) LnOp ๐) = (if(๐ โ NrmCVec, ๐, โจโจ + , ยท โฉ,
absโฉ) LnOp if(๐ โ
NrmCVec, ๐, โจโจ +
, ยท โฉ, absโฉ))) |
17 | 16 | eleq2d 2820 |
. . . 4
โข (๐ = if(๐ โ NrmCVec, ๐, โจโจ + , ยท โฉ,
absโฉ) โ (๐ โ
(if(๐ โ NrmCVec, ๐, โจโจ + , ยท
โฉ, absโฉ) LnOp ๐)
โ ๐ โ (if(๐ โ NrmCVec, ๐, โจโจ + , ยท
โฉ, absโฉ) LnOp if(๐ โ NrmCVec, ๐, โจโจ + , ยท โฉ,
absโฉ)))) |
18 | | oveq2 7417 |
. . . . . . 7
โข (๐ = if(๐ โ NrmCVec, ๐, โจโจ + , ยท โฉ,
absโฉ) โ (if(๐
โ NrmCVec, ๐,
โจโจ + , ยท โฉ, absโฉ) normOpOLD ๐) = (if(๐ โ NrmCVec, ๐, โจโจ + , ยท โฉ,
absโฉ) normOpOLD if(๐ โ NrmCVec, ๐, โจโจ + , ยท โฉ,
absโฉ))) |
19 | 18 | fveq1d 6894 |
. . . . . 6
โข (๐ = if(๐ โ NrmCVec, ๐, โจโจ + , ยท โฉ,
absโฉ) โ ((if(๐
โ NrmCVec, ๐,
โจโจ + , ยท โฉ, absโฉ) normOpOLD ๐)โ๐) = ((if(๐ โ NrmCVec, ๐, โจโจ + , ยท โฉ,
absโฉ) normOpOLD if(๐ โ NrmCVec, ๐, โจโจ + , ยท โฉ,
absโฉ))โ๐)) |
20 | 19 | eqeq1d 2735 |
. . . . 5
โข (๐ = if(๐ โ NrmCVec, ๐, โจโจ + , ยท โฉ,
absโฉ) โ (((if(๐
โ NrmCVec, ๐,
โจโจ + , ยท โฉ, absโฉ) normOpOLD ๐)โ๐) = 0 โ ((if(๐ โ NrmCVec, ๐, โจโจ + , ยท โฉ,
absโฉ) normOpOLD if(๐ โ NrmCVec, ๐, โจโจ + , ยท โฉ,
absโฉ))โ๐) =
0)) |
21 | | oveq2 7417 |
. . . . . 6
โข (๐ = if(๐ โ NrmCVec, ๐, โจโจ + , ยท โฉ,
absโฉ) โ (if(๐
โ NrmCVec, ๐,
โจโจ + , ยท โฉ, absโฉ) 0op ๐) = (if(๐ โ NrmCVec, ๐, โจโจ + , ยท โฉ,
absโฉ) 0op if(๐ โ NrmCVec, ๐, โจโจ + , ยท โฉ,
absโฉ))) |
22 | 21 | eqeq2d 2744 |
. . . . 5
โข (๐ = if(๐ โ NrmCVec, ๐, โจโจ + , ยท โฉ,
absโฉ) โ (๐ =
(if(๐ โ NrmCVec, ๐, โจโจ + , ยท
โฉ, absโฉ) 0op ๐) โ ๐ = (if(๐ โ NrmCVec, ๐, โจโจ + , ยท โฉ,
absโฉ) 0op if(๐ โ NrmCVec, ๐, โจโจ + , ยท โฉ,
absโฉ)))) |
23 | 20, 22 | bibi12d 346 |
. . . 4
โข (๐ = if(๐ โ NrmCVec, ๐, โจโจ + , ยท โฉ,
absโฉ) โ ((((if(๐
โ NrmCVec, ๐,
โจโจ + , ยท โฉ, absโฉ) normOpOLD ๐)โ๐) = 0 โ ๐ = (if(๐ โ NrmCVec, ๐, โจโจ + , ยท โฉ,
absโฉ) 0op ๐)) โ (((if(๐ โ NrmCVec, ๐, โจโจ + , ยท โฉ,
absโฉ) normOpOLD if(๐ โ NrmCVec, ๐, โจโจ + , ยท โฉ,
absโฉ))โ๐) = 0
โ ๐ = (if(๐ โ NrmCVec, ๐, โจโจ + , ยท
โฉ, absโฉ) 0op if(๐ โ NrmCVec, ๐, โจโจ + , ยท โฉ,
absโฉ))))) |
24 | 17, 23 | imbi12d 345 |
. . 3
โข (๐ = if(๐ โ NrmCVec, ๐, โจโจ + , ยท โฉ,
absโฉ) โ ((๐
โ (if(๐ โ
NrmCVec, ๐, โจโจ +
, ยท โฉ, absโฉ) LnOp ๐) โ (((if(๐ โ NrmCVec, ๐, โจโจ + , ยท โฉ,
absโฉ) normOpOLD ๐)โ๐) = 0 โ ๐ = (if(๐ โ NrmCVec, ๐, โจโจ + , ยท โฉ,
absโฉ) 0op ๐))) โ (๐ โ (if(๐ โ NrmCVec, ๐, โจโจ + , ยท โฉ,
absโฉ) LnOp if(๐ โ
NrmCVec, ๐, โจโจ +
, ยท โฉ, absโฉ)) โ (((if(๐ โ NrmCVec, ๐, โจโจ + , ยท โฉ,
absโฉ) normOpOLD if(๐ โ NrmCVec, ๐, โจโจ + , ยท โฉ,
absโฉ))โ๐) = 0
โ ๐ = (if(๐ โ NrmCVec, ๐, โจโจ + , ยท
โฉ, absโฉ) 0op if(๐ โ NrmCVec, ๐, โจโจ + , ยท โฉ,
absโฉ)))))) |
25 | | eqid 2733 |
. . . 4
โข (if(๐ โ NrmCVec, ๐, โจโจ + , ยท
โฉ, absโฉ) normOpOLD if(๐ โ NrmCVec, ๐, โจโจ + , ยท โฉ,
absโฉ)) = (if(๐ โ
NrmCVec, ๐, โจโจ +
, ยท โฉ, absโฉ) normOpOLD if(๐ โ NrmCVec, ๐, โจโจ + , ยท โฉ,
absโฉ)) |
26 | | eqid 2733 |
. . . 4
โข (if(๐ โ NrmCVec, ๐, โจโจ + , ยท
โฉ, absโฉ) 0op if(๐ โ NrmCVec, ๐, โจโจ + , ยท โฉ,
absโฉ)) = (if(๐ โ
NrmCVec, ๐, โจโจ +
, ยท โฉ, absโฉ) 0op if(๐ โ NrmCVec, ๐, โจโจ + , ยท โฉ,
absโฉ)) |
27 | | eqid 2733 |
. . . 4
โข (if(๐ โ NrmCVec, ๐, โจโจ + , ยท
โฉ, absโฉ) LnOp if(๐ โ NrmCVec, ๐, โจโจ + , ยท โฉ,
absโฉ)) = (if(๐ โ
NrmCVec, ๐, โจโจ +
, ยท โฉ, absโฉ) LnOp if(๐ โ NrmCVec, ๐, โจโจ + , ยท โฉ,
absโฉ)) |
28 | | elimnvu 29937 |
. . . 4
โข if(๐ โ NrmCVec, ๐, โจโจ + , ยท
โฉ, absโฉ) โ NrmCVec |
29 | | elimnvu 29937 |
. . . 4
โข if(๐ โ NrmCVec, ๐, โจโจ + , ยท
โฉ, absโฉ) โ NrmCVec |
30 | 25, 26, 27, 28, 29 | nmlno0i 30047 |
. . 3
โข (๐ โ (if(๐ โ NrmCVec, ๐, โจโจ + , ยท โฉ,
absโฉ) LnOp if(๐ โ
NrmCVec, ๐, โจโจ +
, ยท โฉ, absโฉ)) โ (((if(๐ โ NrmCVec, ๐, โจโจ + , ยท โฉ,
absโฉ) normOpOLD if(๐ โ NrmCVec, ๐, โจโจ + , ยท โฉ,
absโฉ))โ๐) = 0
โ ๐ = (if(๐ โ NrmCVec, ๐, โจโจ + , ยท
โฉ, absโฉ) 0op if(๐ โ NrmCVec, ๐, โจโจ + , ยท โฉ,
absโฉ)))) |
31 | 15, 24, 30 | dedth2h 4588 |
. 2
โข ((๐ โ NrmCVec โง ๐ โ NrmCVec) โ (๐ โ ๐ฟ โ ((๐โ๐) = 0 โ ๐ = ๐))) |
32 | 31 | 3impia 1118 |
1
โข ((๐ โ NrmCVec โง ๐ โ NrmCVec โง ๐ โ ๐ฟ) โ ((๐โ๐) = 0 โ ๐ = ๐)) |