Metamath Proof Explorer

Theorem pjnormssi

Description: Theorem 4.5(i)<->(vi) of Beran p. 112. (Contributed by NM, 26-Sep-2001) (New usage is discouraged.)

Ref Expression
Hypotheses pjco.1 ⊢ 𝐺 ∈ Cℋ
pjco.2 ⊢ 𝐻 ∈ Cℋ
Assertion pjnormssi ( 𝐺 ⊆ 𝐻 ↔ ∀ 𝑥 ∈ ℋ ( normℎ ‘ ( ( projℎ ‘ 𝐺 ) ‘ 𝑥 ) ) ≤ ( normℎ ‘ ( ( projℎ ‘ 𝐻 ) ‘ 𝑥 ) ) )

Proof

Step Hyp Ref Expression
1 pjco.1 ⊢ 𝐺 ∈ Cℋ
2 pjco.2 ⊢ 𝐻 ∈ Cℋ
3 2 1 pjssmi ⊢ ( 𝑥 ∈ ℋ → ( 𝐺 ⊆ 𝐻 → ( ( ( projℎ ‘ 𝐻 ) ‘ 𝑥 ) −ℎ ( ( projℎ ‘ 𝐺 ) ‘ 𝑥 ) ) = ( ( projℎ ‘ ( 𝐻 ∩ ( ⊥ ‘ 𝐺 ) ) ) ‘ 𝑥 ) ) )
4 2 1 pjssge0i ⊢ ( 𝑥 ∈ ℋ → ( ( ( ( projℎ ‘ 𝐻 ) ‘ 𝑥 ) −ℎ ( ( projℎ ‘ 𝐺 ) ‘ 𝑥 ) ) = ( ( projℎ ‘ ( 𝐻 ∩ ( ⊥ ‘ 𝐺 ) ) ) ‘ 𝑥 ) → 0 ≤ ( ( ( ( projℎ ‘ 𝐻 ) ‘ 𝑥 ) −ℎ ( ( projℎ ‘ 𝐺 ) ‘ 𝑥 ) ) ·ih 𝑥 ) ) )
5 3 4 syld ⊢ ( 𝑥 ∈ ℋ → ( 𝐺 ⊆ 𝐻 → 0 ≤ ( ( ( ( projℎ ‘ 𝐻 ) ‘ 𝑥 ) −ℎ ( ( projℎ ‘ 𝐺 ) ‘ 𝑥 ) ) ·ih 𝑥 ) ) )
6 2 1 pjdifnormi ⊢ ( 𝑥 ∈ ℋ → ( 0 ≤ ( ( ( ( projℎ ‘ 𝐻 ) ‘ 𝑥 ) −ℎ ( ( projℎ ‘ 𝐺 ) ‘ 𝑥 ) ) ·ih 𝑥 ) ↔ ( normℎ ‘ ( ( projℎ ‘ 𝐺 ) ‘ 𝑥 ) ) ≤ ( normℎ ‘ ( ( projℎ ‘ 𝐻 ) ‘ 𝑥 ) ) ) )
7 5 6 sylibd ⊢ ( 𝑥 ∈ ℋ → ( 𝐺 ⊆ 𝐻 → ( normℎ ‘ ( ( projℎ ‘ 𝐺 ) ‘ 𝑥 ) ) ≤ ( normℎ ‘ ( ( projℎ ‘ 𝐻 ) ‘ 𝑥 ) ) ) )
8 7 com12 ⊢ ( 𝐺 ⊆ 𝐻 → ( 𝑥 ∈ ℋ → ( normℎ ‘ ( ( projℎ ‘ 𝐺 ) ‘ 𝑥 ) ) ≤ ( normℎ ‘ ( ( projℎ ‘ 𝐻 ) ‘ 𝑥 ) ) ) )
9 8 ralrimiv ⊢ ( 𝐺 ⊆ 𝐻 → ∀ 𝑥 ∈ ℋ ( normℎ ‘ ( ( projℎ ‘ 𝐺 ) ‘ 𝑥 ) ) ≤ ( normℎ ‘ ( ( projℎ ‘ 𝐻 ) ‘ 𝑥 ) ) )
10 2 choccli ⊢ ( ⊥ ‘ 𝐻 ) ∈ Cℋ
11 10 cheli ⊢ ( 𝑥 ∈ ( ⊥ ‘ 𝐻 ) → 𝑥 ∈ ℋ )
12 breq2 ⊢ ( ( normℎ ‘ ( ( projℎ ‘ 𝐻 ) ‘ 𝑥 ) ) = 0 → ( ( normℎ ‘ ( ( projℎ ‘ 𝐺 ) ‘ 𝑥 ) ) ≤ ( normℎ ‘ ( ( projℎ ‘ 𝐻 ) ‘ 𝑥 ) ) ↔ ( normℎ ‘ ( ( projℎ ‘ 𝐺 ) ‘ 𝑥 ) ) ≤ 0 ) )
13 12 biimpac ⊢ ( ( ( normℎ ‘ ( ( projℎ ‘ 𝐺 ) ‘ 𝑥 ) ) ≤ ( normℎ ‘ ( ( projℎ ‘ 𝐻 ) ‘ 𝑥 ) ) ∧ ( normℎ ‘ ( ( projℎ ‘ 𝐻 ) ‘ 𝑥 ) ) = 0 ) → ( normℎ ‘ ( ( projℎ ‘ 𝐺 ) ‘ 𝑥 ) ) ≤ 0 )
14 1 pjhcli ⊢ ( 𝑥 ∈ ℋ → ( ( projℎ ‘ 𝐺 ) ‘ 𝑥 ) ∈ ℋ )
15 normge0 ⊢ ( ( ( projℎ ‘ 𝐺 ) ‘ 𝑥 ) ∈ ℋ → 0 ≤ ( normℎ ‘ ( ( projℎ ‘ 𝐺 ) ‘ 𝑥 ) ) )
16 14 15 syl ⊢ ( 𝑥 ∈ ℋ → 0 ≤ ( normℎ ‘ ( ( projℎ ‘ 𝐺 ) ‘ 𝑥 ) ) )
17 normcl ⊢ ( ( ( projℎ ‘ 𝐺 ) ‘ 𝑥 ) ∈ ℋ → ( normℎ ‘ ( ( projℎ ‘ 𝐺 ) ‘ 𝑥 ) ) ∈ ℝ )
18 14 17 syl ⊢ ( 𝑥 ∈ ℋ → ( normℎ ‘ ( ( projℎ ‘ 𝐺 ) ‘ 𝑥 ) ) ∈ ℝ )
19 0re ⊢ 0 ∈ ℝ
20 letri3 ⊢ ( ( ( normℎ ‘ ( ( projℎ ‘ 𝐺 ) ‘ 𝑥 ) ) ∈ ℝ ∧ 0 ∈ ℝ ) → ( ( normℎ ‘ ( ( projℎ ‘ 𝐺 ) ‘ 𝑥 ) ) = 0 ↔ ( ( normℎ ‘ ( ( projℎ ‘ 𝐺 ) ‘ 𝑥 ) ) ≤ 0 ∧ 0 ≤ ( normℎ ‘ ( ( projℎ ‘ 𝐺 ) ‘ 𝑥 ) ) ) ) )
21 20 biimprd ⊢ ( ( ( normℎ ‘ ( ( projℎ ‘ 𝐺 ) ‘ 𝑥 ) ) ∈ ℝ ∧ 0 ∈ ℝ ) → ( ( ( normℎ ‘ ( ( projℎ ‘ 𝐺 ) ‘ 𝑥 ) ) ≤ 0 ∧ 0 ≤ ( normℎ ‘ ( ( projℎ ‘ 𝐺 ) ‘ 𝑥 ) ) ) → ( normℎ ‘ ( ( projℎ ‘ 𝐺 ) ‘ 𝑥 ) ) = 0 ) )
22 18 19 21 sylancl ⊢ ( 𝑥 ∈ ℋ → ( ( ( normℎ ‘ ( ( projℎ ‘ 𝐺 ) ‘ 𝑥 ) ) ≤ 0 ∧ 0 ≤ ( normℎ ‘ ( ( projℎ ‘ 𝐺 ) ‘ 𝑥 ) ) ) → ( normℎ ‘ ( ( projℎ ‘ 𝐺 ) ‘ 𝑥 ) ) = 0 ) )
23 16 22 sylan2i ⊢ ( 𝑥 ∈ ℋ → ( ( ( normℎ ‘ ( ( projℎ ‘ 𝐺 ) ‘ 𝑥 ) ) ≤ 0 ∧ 𝑥 ∈ ℋ ) → ( normℎ ‘ ( ( projℎ ‘ 𝐺 ) ‘ 𝑥 ) ) = 0 ) )
24 23 anabsi6 ⊢ ( ( 𝑥 ∈ ℋ ∧ ( normℎ ‘ ( ( projℎ ‘ 𝐺 ) ‘ 𝑥 ) ) ≤ 0 ) → ( normℎ ‘ ( ( projℎ ‘ 𝐺 ) ‘ 𝑥 ) ) = 0 )
25 13 24 sylan2 ⊢ ( ( 𝑥 ∈ ℋ ∧ ( ( normℎ ‘ ( ( projℎ ‘ 𝐺 ) ‘ 𝑥 ) ) ≤ ( normℎ ‘ ( ( projℎ ‘ 𝐻 ) ‘ 𝑥 ) ) ∧ ( normℎ ‘ ( ( projℎ ‘ 𝐻 ) ‘ 𝑥 ) ) = 0 ) ) → ( normℎ ‘ ( ( projℎ ‘ 𝐺 ) ‘ 𝑥 ) ) = 0 )
26 25 expr ⊢ ( ( 𝑥 ∈ ℋ ∧ ( normℎ ‘ ( ( projℎ ‘ 𝐺 ) ‘ 𝑥 ) ) ≤ ( normℎ ‘ ( ( projℎ ‘ 𝐻 ) ‘ 𝑥 ) ) ) → ( ( normℎ ‘ ( ( projℎ ‘ 𝐻 ) ‘ 𝑥 ) ) = 0 → ( normℎ ‘ ( ( projℎ ‘ 𝐺 ) ‘ 𝑥 ) ) = 0 ) )
27 2 pjhcli ⊢ ( 𝑥 ∈ ℋ → ( ( projℎ ‘ 𝐻 ) ‘ 𝑥 ) ∈ ℋ )
28 norm-i ⊢ ( ( ( projℎ ‘ 𝐻 ) ‘ 𝑥 ) ∈ ℋ → ( ( normℎ ‘ ( ( projℎ ‘ 𝐻 ) ‘ 𝑥 ) ) = 0 ↔ ( ( projℎ ‘ 𝐻 ) ‘ 𝑥 ) = 0ℎ ) )
29 27 28 syl ⊢ ( 𝑥 ∈ ℋ → ( ( normℎ ‘ ( ( projℎ ‘ 𝐻 ) ‘ 𝑥 ) ) = 0 ↔ ( ( projℎ ‘ 𝐻 ) ‘ 𝑥 ) = 0ℎ ) )
30 pjoc2 ⊢ ( ( 𝐻 ∈ Cℋ ∧ 𝑥 ∈ ℋ ) → ( 𝑥 ∈ ( ⊥ ‘ 𝐻 ) ↔ ( ( projℎ ‘ 𝐻 ) ‘ 𝑥 ) = 0ℎ ) )
31 2 30 mpan ⊢ ( 𝑥 ∈ ℋ → ( 𝑥 ∈ ( ⊥ ‘ 𝐻 ) ↔ ( ( projℎ ‘ 𝐻 ) ‘ 𝑥 ) = 0ℎ ) )
32 29 31 bitr4d ⊢ ( 𝑥 ∈ ℋ → ( ( normℎ ‘ ( ( projℎ ‘ 𝐻 ) ‘ 𝑥 ) ) = 0 ↔ 𝑥 ∈ ( ⊥ ‘ 𝐻 ) ) )
33 32 adantr ⊢ ( ( 𝑥 ∈ ℋ ∧ ( normℎ ‘ ( ( projℎ ‘ 𝐺 ) ‘ 𝑥 ) ) ≤ ( normℎ ‘ ( ( projℎ ‘ 𝐻 ) ‘ 𝑥 ) ) ) → ( ( normℎ ‘ ( ( projℎ ‘ 𝐻 ) ‘ 𝑥 ) ) = 0 ↔ 𝑥 ∈ ( ⊥ ‘ 𝐻 ) ) )
34 norm-i ⊢ ( ( ( projℎ ‘ 𝐺 ) ‘ 𝑥 ) ∈ ℋ → ( ( normℎ ‘ ( ( projℎ ‘ 𝐺 ) ‘ 𝑥 ) ) = 0 ↔ ( ( projℎ ‘ 𝐺 ) ‘ 𝑥 ) = 0ℎ ) )
35 14 34 syl ⊢ ( 𝑥 ∈ ℋ → ( ( normℎ ‘ ( ( projℎ ‘ 𝐺 ) ‘ 𝑥 ) ) = 0 ↔ ( ( projℎ ‘ 𝐺 ) ‘ 𝑥 ) = 0ℎ ) )
36 pjoc2 ⊢ ( ( 𝐺 ∈ Cℋ ∧ 𝑥 ∈ ℋ ) → ( 𝑥 ∈ ( ⊥ ‘ 𝐺 ) ↔ ( ( projℎ ‘ 𝐺 ) ‘ 𝑥 ) = 0ℎ ) )
37 1 36 mpan ⊢ ( 𝑥 ∈ ℋ → ( 𝑥 ∈ ( ⊥ ‘ 𝐺 ) ↔ ( ( projℎ ‘ 𝐺 ) ‘ 𝑥 ) = 0ℎ ) )
38 35 37 bitr4d ⊢ ( 𝑥 ∈ ℋ → ( ( normℎ ‘ ( ( projℎ ‘ 𝐺 ) ‘ 𝑥 ) ) = 0 ↔ 𝑥 ∈ ( ⊥ ‘ 𝐺 ) ) )
39 38 adantr ⊢ ( ( 𝑥 ∈ ℋ ∧ ( normℎ ‘ ( ( projℎ ‘ 𝐺 ) ‘ 𝑥 ) ) ≤ ( normℎ ‘ ( ( projℎ ‘ 𝐻 ) ‘ 𝑥 ) ) ) → ( ( normℎ ‘ ( ( projℎ ‘ 𝐺 ) ‘ 𝑥 ) ) = 0 ↔ 𝑥 ∈ ( ⊥ ‘ 𝐺 ) ) )
40 26 33 39 3imtr3d ⊢ ( ( 𝑥 ∈ ℋ ∧ ( normℎ ‘ ( ( projℎ ‘ 𝐺 ) ‘ 𝑥 ) ) ≤ ( normℎ ‘ ( ( projℎ ‘ 𝐻 ) ‘ 𝑥 ) ) ) → ( 𝑥 ∈ ( ⊥ ‘ 𝐻 ) → 𝑥 ∈ ( ⊥ ‘ 𝐺 ) ) )
41 40 ex ⊢ ( 𝑥 ∈ ℋ → ( ( normℎ ‘ ( ( projℎ ‘ 𝐺 ) ‘ 𝑥 ) ) ≤ ( normℎ ‘ ( ( projℎ ‘ 𝐻 ) ‘ 𝑥 ) ) → ( 𝑥 ∈ ( ⊥ ‘ 𝐻 ) → 𝑥 ∈ ( ⊥ ‘ 𝐺 ) ) ) )
42 41 a2i ⊢ ( ( 𝑥 ∈ ℋ → ( normℎ ‘ ( ( projℎ ‘ 𝐺 ) ‘ 𝑥 ) ) ≤ ( normℎ ‘ ( ( projℎ ‘ 𝐻 ) ‘ 𝑥 ) ) ) → ( 𝑥 ∈ ℋ → ( 𝑥 ∈ ( ⊥ ‘ 𝐻 ) → 𝑥 ∈ ( ⊥ ‘ 𝐺 ) ) ) )
43 11 42 syl5 ⊢ ( ( 𝑥 ∈ ℋ → ( normℎ ‘ ( ( projℎ ‘ 𝐺 ) ‘ 𝑥 ) ) ≤ ( normℎ ‘ ( ( projℎ ‘ 𝐻 ) ‘ 𝑥 ) ) ) → ( 𝑥 ∈ ( ⊥ ‘ 𝐻 ) → ( 𝑥 ∈ ( ⊥ ‘ 𝐻 ) → 𝑥 ∈ ( ⊥ ‘ 𝐺 ) ) ) )
44 43 pm2.43d ⊢ ( ( 𝑥 ∈ ℋ → ( normℎ ‘ ( ( projℎ ‘ 𝐺 ) ‘ 𝑥 ) ) ≤ ( normℎ ‘ ( ( projℎ ‘ 𝐻 ) ‘ 𝑥 ) ) ) → ( 𝑥 ∈ ( ⊥ ‘ 𝐻 ) → 𝑥 ∈ ( ⊥ ‘ 𝐺 ) ) )
45 44 alimi ⊢ ( ∀ 𝑥 ( 𝑥 ∈ ℋ → ( normℎ ‘ ( ( projℎ ‘ 𝐺 ) ‘ 𝑥 ) ) ≤ ( normℎ ‘ ( ( projℎ ‘ 𝐻 ) ‘ 𝑥 ) ) ) → ∀ 𝑥 ( 𝑥 ∈ ( ⊥ ‘ 𝐻 ) → 𝑥 ∈ ( ⊥ ‘ 𝐺 ) ) )
46 df-ral ⊢ ( ∀ 𝑥 ∈ ℋ ( normℎ ‘ ( ( projℎ ‘ 𝐺 ) ‘ 𝑥 ) ) ≤ ( normℎ ‘ ( ( projℎ ‘ 𝐻 ) ‘ 𝑥 ) ) ↔ ∀ 𝑥 ( 𝑥 ∈ ℋ → ( normℎ ‘ ( ( projℎ ‘ 𝐺 ) ‘ 𝑥 ) ) ≤ ( normℎ ‘ ( ( projℎ ‘ 𝐻 ) ‘ 𝑥 ) ) ) )
47 dfss2 ⊢ ( ( ⊥ ‘ 𝐻 ) ⊆ ( ⊥ ‘ 𝐺 ) ↔ ∀ 𝑥 ( 𝑥 ∈ ( ⊥ ‘ 𝐻 ) → 𝑥 ∈ ( ⊥ ‘ 𝐺 ) ) )
48 45 46 47 3imtr4i ⊢ ( ∀ 𝑥 ∈ ℋ ( normℎ ‘ ( ( projℎ ‘ 𝐺 ) ‘ 𝑥 ) ) ≤ ( normℎ ‘ ( ( projℎ ‘ 𝐻 ) ‘ 𝑥 ) ) → ( ⊥ ‘ 𝐻 ) ⊆ ( ⊥ ‘ 𝐺 ) )
49 1 2 chsscon3i ⊢ ( 𝐺 ⊆ 𝐻 ↔ ( ⊥ ‘ 𝐻 ) ⊆ ( ⊥ ‘ 𝐺 ) )
50 48 49 sylibr ⊢ ( ∀ 𝑥 ∈ ℋ ( normℎ ‘ ( ( projℎ ‘ 𝐺 ) ‘ 𝑥 ) ) ≤ ( normℎ ‘ ( ( projℎ ‘ 𝐻 ) ‘ 𝑥 ) ) → 𝐺 ⊆ 𝐻 )
51 9 50 impbii ⊢ ( 𝐺 ⊆ 𝐻 ↔ ∀ 𝑥 ∈ ℋ ( normℎ ‘ ( ( projℎ ‘ 𝐺 ) ‘ 𝑥 ) ) ≤ ( normℎ ‘ ( ( projℎ ‘ 𝐻 ) ‘ 𝑥 ) ) )