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	⊢ ( ( 𝐴 ∈ ℋ ∧ 𝐵 ∈ ℋ ∧ 𝐴 ≠ 0_ℎ ) → ( ( proj_ℎ ‘ ( span ‘ { 𝐴 } ) ) ‘ 𝐵 ) = ( ( ( 𝐵 ·_ih 𝐴 ) / ( ( norm_ℎ ‘ 𝐴 ) ↑ 2 ) ) ·_ℎ 𝐴 ) )

Proof

Step	Hyp	Ref	Expression
1		spansnch	⊢ ( 𝐴 ∈ ℋ → ( span ‘ { 𝐴 } ) ∈ C_ℋ )
2	1	3ad2ant1	⊢ ( ( 𝐴 ∈ ℋ ∧ 𝐵 ∈ ℋ ∧ 𝐴 ≠ 0_ℎ ) → ( span ‘ { 𝐴 } ) ∈ C_ℋ )
3		simp2	⊢ ( ( 𝐴 ∈ ℋ ∧ 𝐵 ∈ ℋ ∧ 𝐴 ≠ 0_ℎ ) → 𝐵 ∈ ℋ )
4		eqid	⊢ ( ( proj_ℎ ‘ ( span ‘ { 𝐴 } ) ) ‘ 𝐵 ) = ( ( proj_ℎ ‘ ( span ‘ { 𝐴 } ) ) ‘ 𝐵 )
5		pjeq	⊢ ( ( ( span ‘ { 𝐴 } ) ∈ C_ℋ ∧ 𝐵 ∈ ℋ ) → ( ( ( proj_ℎ ‘ ( span ‘ { 𝐴 } ) ) ‘ 𝐵 ) = ( ( proj_ℎ ‘ ( span ‘ { 𝐴 } ) ) ‘ 𝐵 ) ↔ ( ( ( proj_ℎ ‘ ( span ‘ { 𝐴 } ) ) ‘ 𝐵 ) ∈ ( span ‘ { 𝐴 } ) ∧ ∃ 𝑦 ∈ ( ⊥ ‘ ( span ‘ { 𝐴 } ) ) 𝐵 = ( ( ( proj_ℎ ‘ ( span ‘ { 𝐴 } ) ) ‘ 𝐵 ) +_ℎ 𝑦 ) ) ) )
6	4 5	mpbii	⊢ ( ( ( span ‘ { 𝐴 } ) ∈ C_ℋ ∧ 𝐵 ∈ ℋ ) → ( ( ( proj_ℎ ‘ ( span ‘ { 𝐴 } ) ) ‘ 𝐵 ) ∈ ( span ‘ { 𝐴 } ) ∧ ∃ 𝑦 ∈ ( ⊥ ‘ ( span ‘ { 𝐴 } ) ) 𝐵 = ( ( ( proj_ℎ ‘ ( span ‘ { 𝐴 } ) ) ‘ 𝐵 ) +_ℎ 𝑦 ) ) )
7	6	simprd	⊢ ( ( ( span ‘ { 𝐴 } ) ∈ C_ℋ ∧ 𝐵 ∈ ℋ ) → ∃ 𝑦 ∈ ( ⊥ ‘ ( span ‘ { 𝐴 } ) ) 𝐵 = ( ( ( proj_ℎ ‘ ( span ‘ { 𝐴 } ) ) ‘ 𝐵 ) +_ℎ 𝑦 ) )
8	2 3 7	syl2anc	⊢ ( ( 𝐴 ∈ ℋ ∧ 𝐵 ∈ ℋ ∧ 𝐴 ≠ 0_ℎ ) → ∃ 𝑦 ∈ ( ⊥ ‘ ( span ‘ { 𝐴 } ) ) 𝐵 = ( ( ( proj_ℎ ‘ ( span ‘ { 𝐴 } ) ) ‘ 𝐵 ) +_ℎ 𝑦 ) )
9		oveq1	⊢ ( 𝐵 = ( ( ( proj_ℎ ‘ ( span ‘ { 𝐴 } ) ) ‘ 𝐵 ) +_ℎ 𝑦 ) → ( 𝐵 ·_ih 𝐴 ) = ( ( ( ( proj_ℎ ‘ ( span ‘ { 𝐴 } ) ) ‘ 𝐵 ) +_ℎ 𝑦 ) ·_ih 𝐴 ) )
10	9	ad2antll	⊢ ( ( ( 𝐴 ∈ ℋ ∧ 𝐵 ∈ ℋ ∧ 𝐴 ≠ 0_ℎ ) ∧ ( 𝑦 ∈ ( ⊥ ‘ ( span ‘ { 𝐴 } ) ) ∧ 𝐵 = ( ( ( proj_ℎ ‘ ( span ‘ { 𝐴 } ) ) ‘ 𝐵 ) +_ℎ 𝑦 ) ) ) → ( 𝐵 ·_ih 𝐴 ) = ( ( ( ( proj_ℎ ‘ ( span ‘ { 𝐴 } ) ) ‘ 𝐵 ) +_ℎ 𝑦 ) ·_ih 𝐴 ) )
11		pjhcl	⊢ ( ( ( span ‘ { 𝐴 } ) ∈ C_ℋ ∧ 𝐵 ∈ ℋ ) → ( ( proj_ℎ ‘ ( span ‘ { 𝐴 } ) ) ‘ 𝐵 ) ∈ ℋ )
12	2 3 11	syl2anc	⊢ ( ( 𝐴 ∈ ℋ ∧ 𝐵 ∈ ℋ ∧ 𝐴 ≠ 0_ℎ ) → ( ( proj_ℎ ‘ ( span ‘ { 𝐴 } ) ) ‘ 𝐵 ) ∈ ℋ )
13	12	adantr	⊢ ( ( ( 𝐴 ∈ ℋ ∧ 𝐵 ∈ ℋ ∧ 𝐴 ≠ 0_ℎ ) ∧ 𝑦 ∈ ( ⊥ ‘ ( span ‘ { 𝐴 } ) ) ) → ( ( proj_ℎ ‘ ( span ‘ { 𝐴 } ) ) ‘ 𝐵 ) ∈ ℋ )
14		choccl	⊢ ( ( span ‘ { 𝐴 } ) ∈ C_ℋ → ( ⊥ ‘ ( span ‘ { 𝐴 } ) ) ∈ C_ℋ )
15	1 14	syl	⊢ ( 𝐴 ∈ ℋ → ( ⊥ ‘ ( span ‘ { 𝐴 } ) ) ∈ C_ℋ )
16	15	3ad2ant1	⊢ ( ( 𝐴 ∈ ℋ ∧ 𝐵 ∈ ℋ ∧ 𝐴 ≠ 0_ℎ ) → ( ⊥ ‘ ( span ‘ { 𝐴 } ) ) ∈ C_ℋ )
17		chel	⊢ ( ( ( ⊥ ‘ ( span ‘ { 𝐴 } ) ) ∈ C_ℋ ∧ 𝑦 ∈ ( ⊥ ‘ ( span ‘ { 𝐴 } ) ) ) → 𝑦 ∈ ℋ )
18	16 17	sylan	⊢ ( ( ( 𝐴 ∈ ℋ ∧ 𝐵 ∈ ℋ ∧ 𝐴 ≠ 0_ℎ ) ∧ 𝑦 ∈ ( ⊥ ‘ ( span ‘ { 𝐴 } ) ) ) → 𝑦 ∈ ℋ )
19		simpl1	⊢ ( ( ( 𝐴 ∈ ℋ ∧ 𝐵 ∈ ℋ ∧ 𝐴 ≠ 0_ℎ ) ∧ 𝑦 ∈ ( ⊥ ‘ ( span ‘ { 𝐴 } ) ) ) → 𝐴 ∈ ℋ )
20		ax-his2	⊢ ( ( ( ( proj_ℎ ‘ ( span ‘ { 𝐴 } ) ) ‘ 𝐵 ) ∈ ℋ ∧ 𝑦 ∈ ℋ ∧ 𝐴 ∈ ℋ ) → ( ( ( ( proj_ℎ ‘ ( span ‘ { 𝐴 } ) ) ‘ 𝐵 ) +_ℎ 𝑦 ) ·_ih 𝐴 ) = ( ( ( ( proj_ℎ ‘ ( span ‘ { 𝐴 } ) ) ‘ 𝐵 ) ·_ih 𝐴 ) + ( 𝑦 ·_ih 𝐴 ) ) )
21	13 18 19 20	syl3anc	⊢ ( ( ( 𝐴 ∈ ℋ ∧ 𝐵 ∈ ℋ ∧ 𝐴 ≠ 0_ℎ ) ∧ 𝑦 ∈ ( ⊥ ‘ ( span ‘ { 𝐴 } ) ) ) → ( ( ( ( proj_ℎ ‘ ( span ‘ { 𝐴 } ) ) ‘ 𝐵 ) +_ℎ 𝑦 ) ·_ih 𝐴 ) = ( ( ( ( proj_ℎ ‘ ( span ‘ { 𝐴 } ) ) ‘ 𝐵 ) ·_ih 𝐴 ) + ( 𝑦 ·_ih 𝐴 ) ) )
22		spansnsh	⊢ ( 𝐴 ∈ ℋ → ( span ‘ { 𝐴 } ) ∈ S_ℋ )
23	22	adantr	⊢ ( ( 𝐴 ∈ ℋ ∧ 𝑦 ∈ ( ⊥ ‘ ( span ‘ { 𝐴 } ) ) ) → ( span ‘ { 𝐴 } ) ∈ S_ℋ )
24		spansnid	⊢ ( 𝐴 ∈ ℋ → 𝐴 ∈ ( span ‘ { 𝐴 } ) )
25	24	adantr	⊢ ( ( 𝐴 ∈ ℋ ∧ 𝑦 ∈ ( ⊥ ‘ ( span ‘ { 𝐴 } ) ) ) → 𝐴 ∈ ( span ‘ { 𝐴 } ) )
26		simpr	⊢ ( ( 𝐴 ∈ ℋ ∧ 𝑦 ∈ ( ⊥ ‘ ( span ‘ { 𝐴 } ) ) ) → 𝑦 ∈ ( ⊥ ‘ ( span ‘ { 𝐴 } ) ) )
27		shocorth	⊢ ( ( span ‘ { 𝐴 } ) ∈ S_ℋ → ( ( 𝐴 ∈ ( span ‘ { 𝐴 } ) ∧ 𝑦 ∈ ( ⊥ ‘ ( span ‘ { 𝐴 } ) ) ) → ( 𝐴 ·_ih 𝑦 ) = 0 ) )
28	27	3impib	⊢ ( ( ( span ‘ { 𝐴 } ) ∈ S_ℋ ∧ 𝐴 ∈ ( span ‘ { 𝐴 } ) ∧ 𝑦 ∈ ( ⊥ ‘ ( span ‘ { 𝐴 } ) ) ) → ( 𝐴 ·_ih 𝑦 ) = 0 )
29	23 25 26 28	syl3anc	⊢ ( ( 𝐴 ∈ ℋ ∧ 𝑦 ∈ ( ⊥ ‘ ( span ‘ { 𝐴 } ) ) ) → ( 𝐴 ·_ih 𝑦 ) = 0 )
30	15 17	sylan	⊢ ( ( 𝐴 ∈ ℋ ∧ 𝑦 ∈ ( ⊥ ‘ ( span ‘ { 𝐴 } ) ) ) → 𝑦 ∈ ℋ )
31		orthcom	⊢ ( ( 𝐴 ∈ ℋ ∧ 𝑦 ∈ ℋ ) → ( ( 𝐴 ·_ih 𝑦 ) = 0 ↔ ( 𝑦 ·_ih 𝐴 ) = 0 ) )
32	30 31	syldan	⊢ ( ( 𝐴 ∈ ℋ ∧ 𝑦 ∈ ( ⊥ ‘ ( span ‘ { 𝐴 } ) ) ) → ( ( 𝐴 ·_ih 𝑦 ) = 0 ↔ ( 𝑦 ·_ih 𝐴 ) = 0 ) )
33	29 32	mpbid	⊢ ( ( 𝐴 ∈ ℋ ∧ 𝑦 ∈ ( ⊥ ‘ ( span ‘ { 𝐴 } ) ) ) → ( 𝑦 ·_ih 𝐴 ) = 0 )
34	33	3ad2antl1	⊢ ( ( ( 𝐴 ∈ ℋ ∧ 𝐵 ∈ ℋ ∧ 𝐴 ≠ 0_ℎ ) ∧ 𝑦 ∈ ( ⊥ ‘ ( span ‘ { 𝐴 } ) ) ) → ( 𝑦 ·_ih 𝐴 ) = 0 )
35	34	oveq2d	⊢ ( ( ( 𝐴 ∈ ℋ ∧ 𝐵 ∈ ℋ ∧ 𝐴 ≠ 0_ℎ ) ∧ 𝑦 ∈ ( ⊥ ‘ ( span ‘ { 𝐴 } ) ) ) → ( ( ( ( proj_ℎ ‘ ( span ‘ { 𝐴 } ) ) ‘ 𝐵 ) ·_ih 𝐴 ) + ( 𝑦 ·_ih 𝐴 ) ) = ( ( ( ( proj_ℎ ‘ ( span ‘ { 𝐴 } ) ) ‘ 𝐵 ) ·_ih 𝐴 ) + 0 ) )
36		hicl	⊢ ( ( ( ( proj_ℎ ‘ ( span ‘ { 𝐴 } ) ) ‘ 𝐵 ) ∈ ℋ ∧ 𝐴 ∈ ℋ ) → ( ( ( proj_ℎ ‘ ( span ‘ { 𝐴 } ) ) ‘ 𝐵 ) ·_ih 𝐴 ) ∈ ℂ )
37	13 19 36	syl2anc	⊢ ( ( ( 𝐴 ∈ ℋ ∧ 𝐵 ∈ ℋ ∧ 𝐴 ≠ 0_ℎ ) ∧ 𝑦 ∈ ( ⊥ ‘ ( span ‘ { 𝐴 } ) ) ) → ( ( ( proj_ℎ ‘ ( span ‘ { 𝐴 } ) ) ‘ 𝐵 ) ·_ih 𝐴 ) ∈ ℂ )
38	37	addridd	⊢ ( ( ( 𝐴 ∈ ℋ ∧ 𝐵 ∈ ℋ ∧ 𝐴 ≠ 0_ℎ ) ∧ 𝑦 ∈ ( ⊥ ‘ ( span ‘ { 𝐴 } ) ) ) → ( ( ( ( proj_ℎ ‘ ( span ‘ { 𝐴 } ) ) ‘ 𝐵 ) ·_ih 𝐴 ) + 0 ) = ( ( ( proj_ℎ ‘ ( span ‘ { 𝐴 } ) ) ‘ 𝐵 ) ·_ih 𝐴 ) )
39	21 35 38	3eqtrd	⊢ ( ( ( 𝐴 ∈ ℋ ∧ 𝐵 ∈ ℋ ∧ 𝐴 ≠ 0_ℎ ) ∧ 𝑦 ∈ ( ⊥ ‘ ( span ‘ { 𝐴 } ) ) ) → ( ( ( ( proj_ℎ ‘ ( span ‘ { 𝐴 } ) ) ‘ 𝐵 ) +_ℎ 𝑦 ) ·_ih 𝐴 ) = ( ( ( proj_ℎ ‘ ( span ‘ { 𝐴 } ) ) ‘ 𝐵 ) ·_ih 𝐴 ) )
40	39	adantrr	⊢ ( ( ( 𝐴 ∈ ℋ ∧ 𝐵 ∈ ℋ ∧ 𝐴 ≠ 0_ℎ ) ∧ ( 𝑦 ∈ ( ⊥ ‘ ( span ‘ { 𝐴 } ) ) ∧ 𝐵 = ( ( ( proj_ℎ ‘ ( span ‘ { 𝐴 } ) ) ‘ 𝐵 ) +_ℎ 𝑦 ) ) ) → ( ( ( ( proj_ℎ ‘ ( span ‘ { 𝐴 } ) ) ‘ 𝐵 ) +_ℎ 𝑦 ) ·_ih 𝐴 ) = ( ( ( proj_ℎ ‘ ( span ‘ { 𝐴 } ) ) ‘ 𝐵 ) ·_ih 𝐴 ) )
41	10 40	eqtrd	⊢ ( ( ( 𝐴 ∈ ℋ ∧ 𝐵 ∈ ℋ ∧ 𝐴 ≠ 0_ℎ ) ∧ ( 𝑦 ∈ ( ⊥ ‘ ( span ‘ { 𝐴 } ) ) ∧ 𝐵 = ( ( ( proj_ℎ ‘ ( span ‘ { 𝐴 } ) ) ‘ 𝐵 ) +_ℎ 𝑦 ) ) ) → ( 𝐵 ·_ih 𝐴 ) = ( ( ( proj_ℎ ‘ ( span ‘ { 𝐴 } ) ) ‘ 𝐵 ) ·_ih 𝐴 ) )
42	41	oveq1d	⊢ ( ( ( 𝐴 ∈ ℋ ∧ 𝐵 ∈ ℋ ∧ 𝐴 ≠ 0_ℎ ) ∧ ( 𝑦 ∈ ( ⊥ ‘ ( span ‘ { 𝐴 } ) ) ∧ 𝐵 = ( ( ( proj_ℎ ‘ ( span ‘ { 𝐴 } ) ) ‘ 𝐵 ) +_ℎ 𝑦 ) ) ) → ( ( 𝐵 ·_ih 𝐴 ) / ( ( norm_ℎ ‘ 𝐴 ) ↑ 2 ) ) = ( ( ( ( proj_ℎ ‘ ( span ‘ { 𝐴 } ) ) ‘ 𝐵 ) ·_ih 𝐴 ) / ( ( norm_ℎ ‘ 𝐴 ) ↑ 2 ) ) )
43	42	oveq1d	⊢ ( ( ( 𝐴 ∈ ℋ ∧ 𝐵 ∈ ℋ ∧ 𝐴 ≠ 0_ℎ ) ∧ ( 𝑦 ∈ ( ⊥ ‘ ( span ‘ { 𝐴 } ) ) ∧ 𝐵 = ( ( ( proj_ℎ ‘ ( span ‘ { 𝐴 } ) ) ‘ 𝐵 ) +_ℎ 𝑦 ) ) ) → ( ( ( 𝐵 ·_ih 𝐴 ) / ( ( norm_ℎ ‘ 𝐴 ) ↑ 2 ) ) ·_ℎ 𝐴 ) = ( ( ( ( ( proj_ℎ ‘ ( span ‘ { 𝐴 } ) ) ‘ 𝐵 ) ·_ih 𝐴 ) / ( ( norm_ℎ ‘ 𝐴 ) ↑ 2 ) ) ·_ℎ 𝐴 ) )
44		simpl1	⊢ ( ( ( 𝐴 ∈ ℋ ∧ 𝐵 ∈ ℋ ∧ 𝐴 ≠ 0_ℎ ) ∧ ( 𝑦 ∈ ( ⊥ ‘ ( span ‘ { 𝐴 } ) ) ∧ 𝐵 = ( ( ( proj_ℎ ‘ ( span ‘ { 𝐴 } ) ) ‘ 𝐵 ) +_ℎ 𝑦 ) ) ) → 𝐴 ∈ ℋ )
45		simpl3	⊢ ( ( ( 𝐴 ∈ ℋ ∧ 𝐵 ∈ ℋ ∧ 𝐴 ≠ 0_ℎ ) ∧ ( 𝑦 ∈ ( ⊥ ‘ ( span ‘ { 𝐴 } ) ) ∧ 𝐵 = ( ( ( proj_ℎ ‘ ( span ‘ { 𝐴 } ) ) ‘ 𝐵 ) +_ℎ 𝑦 ) ) ) → 𝐴 ≠ 0_ℎ )
46		axpjcl	⊢ ( ( ( span ‘ { 𝐴 } ) ∈ C_ℋ ∧ 𝐵 ∈ ℋ ) → ( ( proj_ℎ ‘ ( span ‘ { 𝐴 } ) ) ‘ 𝐵 ) ∈ ( span ‘ { 𝐴 } ) )
47	2 3 46	syl2anc	⊢ ( ( 𝐴 ∈ ℋ ∧ 𝐵 ∈ ℋ ∧ 𝐴 ≠ 0_ℎ ) → ( ( proj_ℎ ‘ ( span ‘ { 𝐴 } ) ) ‘ 𝐵 ) ∈ ( span ‘ { 𝐴 } ) )
48	47	adantr	⊢ ( ( ( 𝐴 ∈ ℋ ∧ 𝐵 ∈ ℋ ∧ 𝐴 ≠ 0_ℎ ) ∧ ( 𝑦 ∈ ( ⊥ ‘ ( span ‘ { 𝐴 } ) ) ∧ 𝐵 = ( ( ( proj_ℎ ‘ ( span ‘ { 𝐴 } ) ) ‘ 𝐵 ) +_ℎ 𝑦 ) ) ) → ( ( proj_ℎ ‘ ( span ‘ { 𝐴 } ) ) ‘ 𝐵 ) ∈ ( span ‘ { 𝐴 } ) )
49		normcan	⊢ ( ( 𝐴 ∈ ℋ ∧ 𝐴 ≠ 0_ℎ ∧ ( ( proj_ℎ ‘ ( span ‘ { 𝐴 } ) ) ‘ 𝐵 ) ∈ ( span ‘ { 𝐴 } ) ) → ( ( ( ( ( proj_ℎ ‘ ( span ‘ { 𝐴 } ) ) ‘ 𝐵 ) ·_ih 𝐴 ) / ( ( norm_ℎ ‘ 𝐴 ) ↑ 2 ) ) ·_ℎ 𝐴 ) = ( ( proj_ℎ ‘ ( span ‘ { 𝐴 } ) ) ‘ 𝐵 ) )
50	44 45 48 49	syl3anc	⊢ ( ( ( 𝐴 ∈ ℋ ∧ 𝐵 ∈ ℋ ∧ 𝐴 ≠ 0_ℎ ) ∧ ( 𝑦 ∈ ( ⊥ ‘ ( span ‘ { 𝐴 } ) ) ∧ 𝐵 = ( ( ( proj_ℎ ‘ ( span ‘ { 𝐴 } ) ) ‘ 𝐵 ) +_ℎ 𝑦 ) ) ) → ( ( ( ( ( proj_ℎ ‘ ( span ‘ { 𝐴 } ) ) ‘ 𝐵 ) ·_ih 𝐴 ) / ( ( norm_ℎ ‘ 𝐴 ) ↑ 2 ) ) ·_ℎ 𝐴 ) = ( ( proj_ℎ ‘ ( span ‘ { 𝐴 } ) ) ‘ 𝐵 ) )
51	43 50	eqtr2d	⊢ ( ( ( 𝐴 ∈ ℋ ∧ 𝐵 ∈ ℋ ∧ 𝐴 ≠ 0_ℎ ) ∧ ( 𝑦 ∈ ( ⊥ ‘ ( span ‘ { 𝐴 } ) ) ∧ 𝐵 = ( ( ( proj_ℎ ‘ ( span ‘ { 𝐴 } ) ) ‘ 𝐵 ) +_ℎ 𝑦 ) ) ) → ( ( proj_ℎ ‘ ( span ‘ { 𝐴 } ) ) ‘ 𝐵 ) = ( ( ( 𝐵 ·_ih 𝐴 ) / ( ( norm_ℎ ‘ 𝐴 ) ↑ 2 ) ) ·_ℎ 𝐴 ) )
52	8 51	rexlimddv	⊢ ( ( 𝐴 ∈ ℋ ∧ 𝐵 ∈ ℋ ∧ 𝐴 ≠ 0_ℎ ) → ( ( proj_ℎ ‘ ( span ‘ { 𝐴 } ) ) ‘ 𝐵 ) = ( ( ( 𝐵 ·_ih 𝐴 ) / ( ( norm_ℎ ‘ 𝐴 ) ↑ 2 ) ) ·_ℎ 𝐴 ) )

Metamath Proof Explorer

Theorem pjspansn

Proof