Metamath Proof Explorer

Theorem siilem2

Description: Lemma for sii . (Contributed by NM, 24-Nov-2007) (New usage is discouraged.)

Ref Expression
Hypotheses siii.1 ⊢X=BaseSet⁡U
siii.6 ⊢N=normCV⁡U
siii.7 ⊢P=⋅𝑖OLD⁡U
siii.9 ⊢U∈CPreHilOLD
siii.a ⊢A∈X
siii.b ⊢B∈X
siii2.3 ⊢M=-v⁡U
siii2.4 ⊢S=⋅𝑠OLD⁡U
Assertion siilem2 ⊢C∈ℂ∧C⁢APB∈ℝ∧0≤C⁢APB→BPA=C⁢N⁡B2→APB⁢C⁢N⁡B2≤N⁡A⁢N⁡B

Proof

Step Hyp Ref Expression
1 siii.1 ⊢X=BaseSet⁡U
2 siii.6 ⊢N=normCV⁡U
3 siii.7 ⊢P=⋅𝑖OLD⁡U
4 siii.9 ⊢U∈CPreHilOLD
5 siii.a ⊢A∈X
6 siii.b ⊢B∈X
7 siii2.3 ⊢M=-v⁡U
8 siii2.4 ⊢S=⋅𝑠OLD⁡U
9 oveq1 ⊢C=ifC∈ℂ∧C⁢APB∈ℝ∧0≤C⁢APBC0→C⁢N⁡B2=ifC∈ℂ∧C⁢APB∈ℝ∧0≤C⁢APBC0⁢N⁡B2
10 9 eqeq2d ⊢C=ifC∈ℂ∧C⁢APB∈ℝ∧0≤C⁢APBC0→BPA=C⁢N⁡B2↔BPA=ifC∈ℂ∧C⁢APB∈ℝ∧0≤C⁢APBC0⁢N⁡B2
11 9 oveq2d ⊢C=ifC∈ℂ∧C⁢APB∈ℝ∧0≤C⁢APBC0→APB⁢C⁢N⁡B2=APB⁢ifC∈ℂ∧C⁢APB∈ℝ∧0≤C⁢APBC0⁢N⁡B2
12 11 fveq2d ⊢C=ifC∈ℂ∧C⁢APB∈ℝ∧0≤C⁢APBC0→APB⁢C⁢N⁡B2=APB⁢ifC∈ℂ∧C⁢APB∈ℝ∧0≤C⁢APBC0⁢N⁡B2
13 12 breq1d ⊢C=ifC∈ℂ∧C⁢APB∈ℝ∧0≤C⁢APBC0→APB⁢C⁢N⁡B2≤N⁡A⁢N⁡B↔APB⁢ifC∈ℂ∧C⁢APB∈ℝ∧0≤C⁢APBC0⁢N⁡B2≤N⁡A⁢N⁡B
14 10 13 imbi12d ⊢C=ifC∈ℂ∧C⁢APB∈ℝ∧0≤C⁢APBC0→BPA=C⁢N⁡B2→APB⁢C⁢N⁡B2≤N⁡A⁢N⁡B↔BPA=ifC∈ℂ∧C⁢APB∈ℝ∧0≤C⁢APBC0⁢N⁡B2→APB⁢ifC∈ℂ∧C⁢APB∈ℝ∧0≤C⁢APBC0⁢N⁡B2≤N⁡A⁢N⁡B
15 eleq1 ⊢C=ifC∈ℂ∧C⁢APB∈ℝ∧0≤C⁢APBC0→C∈ℂ↔ifC∈ℂ∧C⁢APB∈ℝ∧0≤C⁢APBC0∈ℂ
16 oveq1 ⊢C=ifC∈ℂ∧C⁢APB∈ℝ∧0≤C⁢APBC0→C⁢APB=ifC∈ℂ∧C⁢APB∈ℝ∧0≤C⁢APBC0⁢APB
17 16 eleq1d ⊢C=ifC∈ℂ∧C⁢APB∈ℝ∧0≤C⁢APBC0→C⁢APB∈ℝ↔ifC∈ℂ∧C⁢APB∈ℝ∧0≤C⁢APBC0⁢APB∈ℝ
18 16 breq2d ⊢C=ifC∈ℂ∧C⁢APB∈ℝ∧0≤C⁢APBC0→0≤C⁢APB↔0≤ifC∈ℂ∧C⁢APB∈ℝ∧0≤C⁢APBC0⁢APB
19 15 17 18 3anbi123d ⊢C=ifC∈ℂ∧C⁢APB∈ℝ∧0≤C⁢APBC0→C∈ℂ∧C⁢APB∈ℝ∧0≤C⁢APB↔ifC∈ℂ∧C⁢APB∈ℝ∧0≤C⁢APBC0∈ℂ∧ifC∈ℂ∧C⁢APB∈ℝ∧0≤C⁢APBC0⁢APB∈ℝ∧0≤ifC∈ℂ∧C⁢APB∈ℝ∧0≤C⁢APBC0⁢APB
20 eleq1 ⊢0=ifC∈ℂ∧C⁢APB∈ℝ∧0≤C⁢APBC0→0∈ℂ↔ifC∈ℂ∧C⁢APB∈ℝ∧0≤C⁢APBC0∈ℂ
21 oveq1 ⊢0=ifC∈ℂ∧C⁢APB∈ℝ∧0≤C⁢APBC0→0⋅APB=ifC∈ℂ∧C⁢APB∈ℝ∧0≤C⁢APBC0⁢APB
22 21 eleq1d ⊢0=ifC∈ℂ∧C⁢APB∈ℝ∧0≤C⁢APBC0→0⋅APB∈ℝ↔ifC∈ℂ∧C⁢APB∈ℝ∧0≤C⁢APBC0⁢APB∈ℝ
23 21 breq2d ⊢0=ifC∈ℂ∧C⁢APB∈ℝ∧0≤C⁢APBC0→0≤0⋅APB↔0≤ifC∈ℂ∧C⁢APB∈ℝ∧0≤C⁢APBC0⁢APB
24 20 22 23 3anbi123d ⊢0=ifC∈ℂ∧C⁢APB∈ℝ∧0≤C⁢APBC0→0∈ℂ∧0⋅APB∈ℝ∧0≤0⋅APB↔ifC∈ℂ∧C⁢APB∈ℝ∧0≤C⁢APBC0∈ℂ∧ifC∈ℂ∧C⁢APB∈ℝ∧0≤C⁢APBC0⁢APB∈ℝ∧0≤ifC∈ℂ∧C⁢APB∈ℝ∧0≤C⁢APBC0⁢APB
25 0cn ⊢0∈ℂ
26 4 phnvi ⊢U∈NrmCVec
27 1 3 dipcl ⊢U∈NrmCVec∧A∈X∧B∈X→APB∈ℂ
28 26 5 6 27 mp3an ⊢APB∈ℂ
29 28 mul02i ⊢0⋅APB=0
30 0re ⊢0∈ℝ
31 29 30 eqeltri ⊢0⋅APB∈ℝ
32 0le0 ⊢0≤0
33 32 29 breqtrri ⊢0≤0⋅APB
34 25 31 33 3pm3.2i ⊢0∈ℂ∧0⋅APB∈ℝ∧0≤0⋅APB
35 19 24 34 elimhyp ⊢ifC∈ℂ∧C⁢APB∈ℝ∧0≤C⁢APBC0∈ℂ∧ifC∈ℂ∧C⁢APB∈ℝ∧0≤C⁢APBC0⁢APB∈ℝ∧0≤ifC∈ℂ∧C⁢APB∈ℝ∧0≤C⁢APBC0⁢APB
36 35 simp1i ⊢ifC∈ℂ∧C⁢APB∈ℝ∧0≤C⁢APBC0∈ℂ
37 35 simp2i ⊢ifC∈ℂ∧C⁢APB∈ℝ∧0≤C⁢APBC0⁢APB∈ℝ
38 35 simp3i ⊢0≤ifC∈ℂ∧C⁢APB∈ℝ∧0≤C⁢APBC0⁢APB
39 1 2 3 4 5 6 7 8 36 37 38 siilem1 ⊢BPA=ifC∈ℂ∧C⁢APB∈ℝ∧0≤C⁢APBC0⁢N⁡B2→APB⁢ifC∈ℂ∧C⁢APB∈ℝ∧0≤C⁢APBC0⁢N⁡B2≤N⁡A⁢N⁡B
40 14 39 dedth ⊢C∈ℂ∧C⁢APB∈ℝ∧0≤C⁢APB→BPA=C⁢N⁡B2→APB⁢C⁢N⁡B2≤N⁡A⁢N⁡B