Metamath Proof Explorer

Theorem pjspansn

Description: A projection on the span of a singleton. (The proof ws shortened by Mario Carneiro, 15-Dec-2013.) (Contributed by NM, 28-May-2006) (Revised by Mario Carneiro, 15-Dec-2013) (New usage is discouraged.)

Ref Expression
Assertion pjspansn ⊢ A ∈ ℋ ∧ B ∈ ℋ ∧ A ≠ 0 ℎ → proj ℎ ⁡ span ⁡ A ⁡ B = B ⋅ ih A norm ℎ ⁡ A 2 ⋅ ℎ A

Proof

Step Hyp Ref Expression
1 spansnch ⊢ A ∈ ℋ → span ⁡ A ∈ C ℋ
2 1 3ad2ant1 ⊢ A ∈ ℋ ∧ B ∈ ℋ ∧ A ≠ 0 ℎ → span ⁡ A ∈ C ℋ
3 simp2 ⊢ A ∈ ℋ ∧ B ∈ ℋ ∧ A ≠ 0 ℎ → B ∈ ℋ
4 eqid ⊢ proj ℎ ⁡ span ⁡ A ⁡ B = proj ℎ ⁡ span ⁡ A ⁡ B
5 pjeq ⊢ span ⁡ A ∈ C ℋ ∧ B ∈ ℋ → proj ℎ ⁡ span ⁡ A ⁡ B = proj ℎ ⁡ span ⁡ A ⁡ B ↔ proj ℎ ⁡ span ⁡ A ⁡ B ∈ span ⁡ A ∧ ∃ y ∈ ⊥ ⁡ span ⁡ A B = proj ℎ ⁡ span ⁡ A ⁡ B + ℎ y
6 4 5 mpbii ⊢ span ⁡ A ∈ C ℋ ∧ B ∈ ℋ → proj ℎ ⁡ span ⁡ A ⁡ B ∈ span ⁡ A ∧ ∃ y ∈ ⊥ ⁡ span ⁡ A B = proj ℎ ⁡ span ⁡ A ⁡ B + ℎ y
7 6 simprd ⊢ span ⁡ A ∈ C ℋ ∧ B ∈ ℋ → ∃ y ∈ ⊥ ⁡ span ⁡ A B = proj ℎ ⁡ span ⁡ A ⁡ B + ℎ y
8 2 3 7 syl2anc ⊢ A ∈ ℋ ∧ B ∈ ℋ ∧ A ≠ 0 ℎ → ∃ y ∈ ⊥ ⁡ span ⁡ A B = proj ℎ ⁡ span ⁡ A ⁡ B + ℎ y
9 oveq1 ⊢ B = proj ℎ ⁡ span ⁡ A ⁡ B + ℎ y → B ⋅ ih A = proj ℎ ⁡ span ⁡ A ⁡ B + ℎ y ⋅ ih A
10 9 ad2antll ⊢ A ∈ ℋ ∧ B ∈ ℋ ∧ A ≠ 0 ℎ ∧ y ∈ ⊥ ⁡ span ⁡ A ∧ B = proj ℎ ⁡ span ⁡ A ⁡ B + ℎ y → B ⋅ ih A = proj ℎ ⁡ span ⁡ A ⁡ B + ℎ y ⋅ ih A
11 pjhcl ⊢ span ⁡ A ∈ C ℋ ∧ B ∈ ℋ → proj ℎ ⁡ span ⁡ A ⁡ B ∈ ℋ
12 2 3 11 syl2anc ⊢ A ∈ ℋ ∧ B ∈ ℋ ∧ A ≠ 0 ℎ → proj ℎ ⁡ span ⁡ A ⁡ B ∈ ℋ
13 12 adantr ⊢ A ∈ ℋ ∧ B ∈ ℋ ∧ A ≠ 0 ℎ ∧ y ∈ ⊥ ⁡ span ⁡ A → proj ℎ ⁡ span ⁡ A ⁡ B ∈ ℋ
14 choccl ⊢ span ⁡ A ∈ C ℋ → ⊥ ⁡ span ⁡ A ∈ C ℋ
15 1 14 syl ⊢ A ∈ ℋ → ⊥ ⁡ span ⁡ A ∈ C ℋ
16 15 3ad2ant1 ⊢ A ∈ ℋ ∧ B ∈ ℋ ∧ A ≠ 0 ℎ → ⊥ ⁡ span ⁡ A ∈ C ℋ
17 chel ⊢ ⊥ ⁡ span ⁡ A ∈ C ℋ ∧ y ∈ ⊥ ⁡ span ⁡ A → y ∈ ℋ
18 16 17 sylan ⊢ A ∈ ℋ ∧ B ∈ ℋ ∧ A ≠ 0 ℎ ∧ y ∈ ⊥ ⁡ span ⁡ A → y ∈ ℋ
19 simpl1 ⊢ A ∈ ℋ ∧ B ∈ ℋ ∧ A ≠ 0 ℎ ∧ y ∈ ⊥ ⁡ span ⁡ A → A ∈ ℋ
20 ax-his2 ⊢ proj ℎ ⁡ span ⁡ A ⁡ B ∈ ℋ ∧ y ∈ ℋ ∧ A ∈ ℋ → proj ℎ ⁡ span ⁡ A ⁡ B + ℎ y ⋅ ih A = proj ℎ ⁡ span ⁡ A ⁡ B ⋅ ih A + y ⋅ ih A
21 13 18 19 20 syl3anc ⊢ A ∈ ℋ ∧ B ∈ ℋ ∧ A ≠ 0 ℎ ∧ y ∈ ⊥ ⁡ span ⁡ A → proj ℎ ⁡ span ⁡ A ⁡ B + ℎ y ⋅ ih A = proj ℎ ⁡ span ⁡ A ⁡ B ⋅ ih A + y ⋅ ih A
22 spansnsh ⊢ A ∈ ℋ → span ⁡ A ∈ S ℋ
23 22 adantr ⊢ A ∈ ℋ ∧ y ∈ ⊥ ⁡ span ⁡ A → span ⁡ A ∈ S ℋ
24 spansnid ⊢ A ∈ ℋ → A ∈ span ⁡ A
25 24 adantr ⊢ A ∈ ℋ ∧ y ∈ ⊥ ⁡ span ⁡ A → A ∈ span ⁡ A
26 simpr ⊢ A ∈ ℋ ∧ y ∈ ⊥ ⁡ span ⁡ A → y ∈ ⊥ ⁡ span ⁡ A
27 shocorth ⊢ span ⁡ A ∈ S ℋ → A ∈ span ⁡ A ∧ y ∈ ⊥ ⁡ span ⁡ A → A ⋅ ih y = 0
28 27 3impib ⊢ span ⁡ A ∈ S ℋ ∧ A ∈ span ⁡ A ∧ y ∈ ⊥ ⁡ span ⁡ A → A ⋅ ih y = 0
29 23 25 26 28 syl3anc ⊢ A ∈ ℋ ∧ y ∈ ⊥ ⁡ span ⁡ A → A ⋅ ih y = 0
30 15 17 sylan ⊢ A ∈ ℋ ∧ y ∈ ⊥ ⁡ span ⁡ A → y ∈ ℋ
31 orthcom ⊢ A ∈ ℋ ∧ y ∈ ℋ → A ⋅ ih y = 0 ↔ y ⋅ ih A = 0
32 30 31 syldan ⊢ A ∈ ℋ ∧ y ∈ ⊥ ⁡ span ⁡ A → A ⋅ ih y = 0 ↔ y ⋅ ih A = 0
33 29 32 mpbid ⊢ A ∈ ℋ ∧ y ∈ ⊥ ⁡ span ⁡ A → y ⋅ ih A = 0
34 33 3ad2antl1 ⊢ A ∈ ℋ ∧ B ∈ ℋ ∧ A ≠ 0 ℎ ∧ y ∈ ⊥ ⁡ span ⁡ A → y ⋅ ih A = 0
35 34 oveq2d ⊢ A ∈ ℋ ∧ B ∈ ℋ ∧ A ≠ 0 ℎ ∧ y ∈ ⊥ ⁡ span ⁡ A → proj ℎ ⁡ span ⁡ A ⁡ B ⋅ ih A + y ⋅ ih A = proj ℎ ⁡ span ⁡ A ⁡ B ⋅ ih A + 0
36 hicl ⊢ proj ℎ ⁡ span ⁡ A ⁡ B ∈ ℋ ∧ A ∈ ℋ → proj ℎ ⁡ span ⁡ A ⁡ B ⋅ ih A ∈ ℂ
37 13 19 36 syl2anc ⊢ A ∈ ℋ ∧ B ∈ ℋ ∧ A ≠ 0 ℎ ∧ y ∈ ⊥ ⁡ span ⁡ A → proj ℎ ⁡ span ⁡ A ⁡ B ⋅ ih A ∈ ℂ
38 37 addid1d ⊢ A ∈ ℋ ∧ B ∈ ℋ ∧ A ≠ 0 ℎ ∧ y ∈ ⊥ ⁡ span ⁡ A → proj ℎ ⁡ span ⁡ A ⁡ B ⋅ ih A + 0 = proj ℎ ⁡ span ⁡ A ⁡ B ⋅ ih A
39 21 35 38 3eqtrd ⊢ A ∈ ℋ ∧ B ∈ ℋ ∧ A ≠ 0 ℎ ∧ y ∈ ⊥ ⁡ span ⁡ A → proj ℎ ⁡ span ⁡ A ⁡ B + ℎ y ⋅ ih A = proj ℎ ⁡ span ⁡ A ⁡ B ⋅ ih A
40 39 adantrr ⊢ A ∈ ℋ ∧ B ∈ ℋ ∧ A ≠ 0 ℎ ∧ y ∈ ⊥ ⁡ span ⁡ A ∧ B = proj ℎ ⁡ span ⁡ A ⁡ B + ℎ y → proj ℎ ⁡ span ⁡ A ⁡ B + ℎ y ⋅ ih A = proj ℎ ⁡ span ⁡ A ⁡ B ⋅ ih A
41 10 40 eqtrd ⊢ A ∈ ℋ ∧ B ∈ ℋ ∧ A ≠ 0 ℎ ∧ y ∈ ⊥ ⁡ span ⁡ A ∧ B = proj ℎ ⁡ span ⁡ A ⁡ B + ℎ y → B ⋅ ih A = proj ℎ ⁡ span ⁡ A ⁡ B ⋅ ih A
42 41 oveq1d ⊢ A ∈ ℋ ∧ B ∈ ℋ ∧ A ≠ 0 ℎ ∧ y ∈ ⊥ ⁡ span ⁡ A ∧ B = proj ℎ ⁡ span ⁡ A ⁡ B + ℎ y → B ⋅ ih A norm ℎ ⁡ A 2 = proj ℎ ⁡ span ⁡ A ⁡ B ⋅ ih A norm ℎ ⁡ A 2
43 42 oveq1d ⊢ A ∈ ℋ ∧ B ∈ ℋ ∧ A ≠ 0 ℎ ∧ y ∈ ⊥ ⁡ span ⁡ A ∧ B = proj ℎ ⁡ span ⁡ A ⁡ B + ℎ y → B ⋅ ih A norm ℎ ⁡ A 2 ⋅ ℎ A = proj ℎ ⁡ span ⁡ A ⁡ B ⋅ ih A norm ℎ ⁡ A 2 ⋅ ℎ A
44 simpl1 ⊢ A ∈ ℋ ∧ B ∈ ℋ ∧ A ≠ 0 ℎ ∧ y ∈ ⊥ ⁡ span ⁡ A ∧ B = proj ℎ ⁡ span ⁡ A ⁡ B + ℎ y → A ∈ ℋ
45 simpl3 ⊢ A ∈ ℋ ∧ B ∈ ℋ ∧ A ≠ 0 ℎ ∧ y ∈ ⊥ ⁡ span ⁡ A ∧ B = proj ℎ ⁡ span ⁡ A ⁡ B + ℎ y → A ≠ 0 ℎ
46 axpjcl ⊢ span ⁡ A ∈ C ℋ ∧ B ∈ ℋ → proj ℎ ⁡ span ⁡ A ⁡ B ∈ span ⁡ A
47 2 3 46 syl2anc ⊢ A ∈ ℋ ∧ B ∈ ℋ ∧ A ≠ 0 ℎ → proj ℎ ⁡ span ⁡ A ⁡ B ∈ span ⁡ A
48 47 adantr ⊢ A ∈ ℋ ∧ B ∈ ℋ ∧ A ≠ 0 ℎ ∧ y ∈ ⊥ ⁡ span ⁡ A ∧ B = proj ℎ ⁡ span ⁡ A ⁡ B + ℎ y → proj ℎ ⁡ span ⁡ A ⁡ B ∈ span ⁡ A
49 normcan ⊢ A ∈ ℋ ∧ A ≠ 0 ℎ ∧ proj ℎ ⁡ span ⁡ A ⁡ B ∈ span ⁡ A → proj ℎ ⁡ span ⁡ A ⁡ B ⋅ ih A norm ℎ ⁡ A 2 ⋅ ℎ A = proj ℎ ⁡ span ⁡ A ⁡ B
50 44 45 48 49 syl3anc ⊢ A ∈ ℋ ∧ B ∈ ℋ ∧ A ≠ 0 ℎ ∧ y ∈ ⊥ ⁡ span ⁡ A ∧ B = proj ℎ ⁡ span ⁡ A ⁡ B + ℎ y → proj ℎ ⁡ span ⁡ A ⁡ B ⋅ ih A norm ℎ ⁡ A 2 ⋅ ℎ A = proj ℎ ⁡ span ⁡ A ⁡ B
51 43 50 eqtr2d ⊢ A ∈ ℋ ∧ B ∈ ℋ ∧ A ≠ 0 ℎ ∧ y ∈ ⊥ ⁡ span ⁡ A ∧ B = proj ℎ ⁡ span ⁡ A ⁡ B + ℎ y → proj ℎ ⁡ span ⁡ A ⁡ B = B ⋅ ih A norm ℎ ⁡ A 2 ⋅ ℎ A
52 8 51 rexlimddv ⊢ A ∈ ℋ ∧ B ∈ ℋ ∧ A ≠ 0 ℎ → proj ℎ ⁡ span ⁡ A ⁡ B = B ⋅ ih A norm ℎ ⁡ A 2 ⋅ ℎ A