Metamath Proof Explorer

Theorem pjdifnormii

Description: Theorem 4.5(v)<->(vi) of Beran p. 112. (Contributed by NM, 13-Aug-2000) (New usage is discouraged.)

Ref Expression
Hypotheses pjidm.1 ⊢H∈Cℋ
pjidm.2 ⊢A∈ℋ
pjsslem.1 ⊢G∈Cℋ
Assertion pjdifnormii ⊢0≤projℎ⁡G⁡A-ℎprojℎ⁡H⁡A⋅ihA↔normℎ⁡projℎ⁡H⁡A≤normℎ⁡projℎ⁡G⁡A

Proof

Step Hyp Ref Expression
1 pjidm.1 ⊢H∈Cℋ
2 pjidm.2 ⊢A∈ℋ
3 pjsslem.1 ⊢G∈Cℋ
4 3 2 pjhclii ⊢projℎ⁡G⁡A∈ℋ
5 4 normcli ⊢normℎ⁡projℎ⁡G⁡A∈ℝ
6 5 resqcli ⊢normℎ⁡projℎ⁡G⁡A2∈ℝ
7 1 2 pjhclii ⊢projℎ⁡H⁡A∈ℋ
8 7 normcli ⊢normℎ⁡projℎ⁡H⁡A∈ℝ
9 8 resqcli ⊢normℎ⁡projℎ⁡H⁡A2∈ℝ
10 6 9 subge0i ⊢0≤normℎ⁡projℎ⁡G⁡A2−normℎ⁡projℎ⁡H⁡A2↔normℎ⁡projℎ⁡H⁡A2≤normℎ⁡projℎ⁡G⁡A2
11 his2sub ⊢projℎ⁡G⁡A∈ℋ∧projℎ⁡H⁡A∈ℋ∧A∈ℋ→projℎ⁡G⁡A-ℎprojℎ⁡H⁡A⋅ihA=projℎ⁡G⁡A⋅ihA−projℎ⁡H⁡A⋅ihA
12 4 7 2 11 mp3an ⊢projℎ⁡G⁡A-ℎprojℎ⁡H⁡A⋅ihA=projℎ⁡G⁡A⋅ihA−projℎ⁡H⁡A⋅ihA
13 3 2 pjinormii ⊢projℎ⁡G⁡A⋅ihA=normℎ⁡projℎ⁡G⁡A2
14 1 2 pjinormii ⊢projℎ⁡H⁡A⋅ihA=normℎ⁡projℎ⁡H⁡A2
15 13 14 oveq12i ⊢projℎ⁡G⁡A⋅ihA−projℎ⁡H⁡A⋅ihA=normℎ⁡projℎ⁡G⁡A2−normℎ⁡projℎ⁡H⁡A2
16 12 15 eqtri ⊢projℎ⁡G⁡A-ℎprojℎ⁡H⁡A⋅ihA=normℎ⁡projℎ⁡G⁡A2−normℎ⁡projℎ⁡H⁡A2
17 16 breq2i ⊢0≤projℎ⁡G⁡A-ℎprojℎ⁡H⁡A⋅ihA↔0≤normℎ⁡projℎ⁡G⁡A2−normℎ⁡projℎ⁡H⁡A2
18 normge0 ⊢projℎ⁡H⁡A∈ℋ→0≤normℎ⁡projℎ⁡H⁡A
19 7 18 ax-mp ⊢0≤normℎ⁡projℎ⁡H⁡A
20 normge0 ⊢projℎ⁡G⁡A∈ℋ→0≤normℎ⁡projℎ⁡G⁡A
21 4 20 ax-mp ⊢0≤normℎ⁡projℎ⁡G⁡A
22 8 5 le2sqi ⊢0≤normℎ⁡projℎ⁡H⁡A∧0≤normℎ⁡projℎ⁡G⁡A→normℎ⁡projℎ⁡H⁡A≤normℎ⁡projℎ⁡G⁡A↔normℎ⁡projℎ⁡H⁡A2≤normℎ⁡projℎ⁡G⁡A2
23 19 21 22 mp2an ⊢normℎ⁡projℎ⁡H⁡A≤normℎ⁡projℎ⁡G⁡A↔normℎ⁡projℎ⁡H⁡A2≤normℎ⁡projℎ⁡G⁡A2
24 10 17 23 3bitr4i ⊢0≤projℎ⁡G⁡A-ℎprojℎ⁡H⁡A⋅ihA↔normℎ⁡projℎ⁡H⁡A≤normℎ⁡projℎ⁡G⁡A