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⋅ihAnormℎ⁡A2⋅ℎ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⁡AB=projℎ⁡span⁡A⁡B+ℎy
6 4 5 mpbii ⊢span⁡A∈Cℋ∧B∈ℋ→projℎ⁡span⁡A⁡B∈span⁡A∧∃y∈⊥⁡span⁡AB=projℎ⁡span⁡A⁡B+ℎy
7 6 simprd ⊢span⁡A∈Cℋ∧B∈ℋ→∃y∈⊥⁡span⁡AB=projℎ⁡span⁡A⁡B+ℎy
8 2 3 7 syl2anc ⊢A∈ℋ∧B∈ℋ∧A≠0ℎ→∃y∈⊥⁡span⁡AB=projℎ⁡span⁡A⁡B+ℎy
9 oveq1 ⊢B=projℎ⁡span⁡A⁡B+ℎy→B⋅ihA=projℎ⁡span⁡A⁡B+ℎy⋅ihA
10 9 ad2antll ⊢A∈ℋ∧B∈ℋ∧A≠0ℎ∧y∈⊥⁡span⁡A∧B=projℎ⁡span⁡A⁡B+ℎy→B⋅ihA=projℎ⁡span⁡A⁡B+ℎy⋅ihA
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⋅ihA=projℎ⁡span⁡A⁡B⋅ihA+y⋅ihA
21 13 18 19 20 syl3anc ⊢A∈ℋ∧B∈ℋ∧A≠0ℎ∧y∈⊥⁡span⁡A→projℎ⁡span⁡A⁡B+ℎy⋅ihA=projℎ⁡span⁡A⁡B⋅ihA+y⋅ihA
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⋅ihy=0
28 27 3impib ⊢span⁡A∈Sℋ∧A∈span⁡A∧y∈⊥⁡span⁡A→A⋅ihy=0
29 23 25 26 28 syl3anc ⊢A∈ℋ∧y∈⊥⁡span⁡A→A⋅ihy=0
30 15 17 sylan ⊢A∈ℋ∧y∈⊥⁡span⁡A→y∈ℋ
31 orthcom ⊢A∈ℋ∧y∈ℋ→A⋅ihy=0↔y⋅ihA=0
32 30 31 syldan ⊢A∈ℋ∧y∈⊥⁡span⁡A→A⋅ihy=0↔y⋅ihA=0
33 29 32 mpbid ⊢A∈ℋ∧y∈⊥⁡span⁡A→y⋅ihA=0
34 33 3ad2antl1 ⊢A∈ℋ∧B∈ℋ∧A≠0ℎ∧y∈⊥⁡span⁡A→y⋅ihA=0
35 34 oveq2d ⊢A∈ℋ∧B∈ℋ∧A≠0ℎ∧y∈⊥⁡span⁡A→projℎ⁡span⁡A⁡B⋅ihA+y⋅ihA=projℎ⁡span⁡A⁡B⋅ihA+0
36 hicl ⊢projℎ⁡span⁡A⁡B∈ℋ∧A∈ℋ→projℎ⁡span⁡A⁡B⋅ihA∈ℂ
37 13 19 36 syl2anc ⊢A∈ℋ∧B∈ℋ∧A≠0ℎ∧y∈⊥⁡span⁡A→projℎ⁡span⁡A⁡B⋅ihA∈ℂ
38 37 addridd ⊢A∈ℋ∧B∈ℋ∧A≠0ℎ∧y∈⊥⁡span⁡A→projℎ⁡span⁡A⁡B⋅ihA+0=projℎ⁡span⁡A⁡B⋅ihA
39 21 35 38 3eqtrd ⊢A∈ℋ∧B∈ℋ∧A≠0ℎ∧y∈⊥⁡span⁡A→projℎ⁡span⁡A⁡B+ℎy⋅ihA=projℎ⁡span⁡A⁡B⋅ihA
40 39 adantrr ⊢A∈ℋ∧B∈ℋ∧A≠0ℎ∧y∈⊥⁡span⁡A∧B=projℎ⁡span⁡A⁡B+ℎy→projℎ⁡span⁡A⁡B+ℎy⋅ihA=projℎ⁡span⁡A⁡B⋅ihA
41 10 40 eqtrd ⊢A∈ℋ∧B∈ℋ∧A≠0ℎ∧y∈⊥⁡span⁡A∧B=projℎ⁡span⁡A⁡B+ℎy→B⋅ihA=projℎ⁡span⁡A⁡B⋅ihA
42 41 oveq1d ⊢A∈ℋ∧B∈ℋ∧A≠0ℎ∧y∈⊥⁡span⁡A∧B=projℎ⁡span⁡A⁡B+ℎy→B⋅ihAnormℎ⁡A2=projℎ⁡span⁡A⁡B⋅ihAnormℎ⁡A2
43 42 oveq1d ⊢A∈ℋ∧B∈ℋ∧A≠0ℎ∧y∈⊥⁡span⁡A∧B=projℎ⁡span⁡A⁡B+ℎy→B⋅ihAnormℎ⁡A2⋅ℎA=projℎ⁡span⁡A⁡B⋅ihAnormℎ⁡A2⋅ℎ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⋅ihAnormℎ⁡A2⋅ℎ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⋅ihAnormℎ⁡A2⋅ℎ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⋅ihAnormℎ⁡A2⋅ℎA
52 8 51 rexlimddv ⊢A∈ℋ∧B∈ℋ∧A≠0ℎ→projℎ⁡span⁡A⁡B=B⋅ihAnormℎ⁡A2⋅ℎA