h1de2i

Description: Membership in 1-dimensional subspace. All members are collinear with the generating vector. (Contributed by NM, 17-Jul-2001) (New usage is discouraged.)

	Ref	Expression
Hypotheses	h1de2.1	⊢ 𝐴 ∈ ℋ
	h1de2.2	⊢ 𝐵 ∈ ℋ
Assertion	h1de2i	⊢ ( 𝐴 ∈ ( ⊥ ‘ ( ⊥ ‘ { 𝐵 } ) ) → ( ( 𝐵 ·_ih 𝐵 ) ·_ℎ 𝐴 ) = ( ( 𝐴 ·_ih 𝐵 ) ·_ℎ 𝐵 ) )

Proof

Step	Hyp	Ref	Expression
1		h1de2.1	⊢ 𝐴 ∈ ℋ
2		h1de2.2	⊢ 𝐵 ∈ ℋ
3	2 2	hicli	⊢ ( 𝐵 ·_ih 𝐵 ) ∈ ℂ
4	3 1	hvmulcli	⊢ ( ( 𝐵 ·_ih 𝐵 ) ·_ℎ 𝐴 ) ∈ ℋ
5	1 2	hicli	⊢ ( 𝐴 ·_ih 𝐵 ) ∈ ℂ
6	5 2	hvmulcli	⊢ ( ( 𝐴 ·_ih 𝐵 ) ·_ℎ 𝐵 ) ∈ ℋ
7		his2sub	⊢ ( ( ( ( 𝐵 ·_ih 𝐵 ) ·_ℎ 𝐴 ) ∈ ℋ ∧ ( ( 𝐴 ·_ih 𝐵 ) ·_ℎ 𝐵 ) ∈ ℋ ∧ 𝐴 ∈ ℋ ) → ( ( ( ( 𝐵 ·_ih 𝐵 ) ·_ℎ 𝐴 ) −_ℎ ( ( 𝐴 ·_ih 𝐵 ) ·_ℎ 𝐵 ) ) ·_ih 𝐴 ) = ( ( ( ( 𝐵 ·_ih 𝐵 ) ·_ℎ 𝐴 ) ·_ih 𝐴 ) − ( ( ( 𝐴 ·_ih 𝐵 ) ·_ℎ 𝐵 ) ·_ih 𝐴 ) ) )
8	4 6 1 7	mp3an	⊢ ( ( ( ( 𝐵 ·_ih 𝐵 ) ·_ℎ 𝐴 ) −_ℎ ( ( 𝐴 ·_ih 𝐵 ) ·_ℎ 𝐵 ) ) ·_ih 𝐴 ) = ( ( ( ( 𝐵 ·_ih 𝐵 ) ·_ℎ 𝐴 ) ·_ih 𝐴 ) − ( ( ( 𝐴 ·_ih 𝐵 ) ·_ℎ 𝐵 ) ·_ih 𝐴 ) )
9		ax-his3	⊢ ( ( ( 𝐵 ·_ih 𝐵 ) ∈ ℂ ∧ 𝐴 ∈ ℋ ∧ 𝐴 ∈ ℋ ) → ( ( ( 𝐵 ·_ih 𝐵 ) ·_ℎ 𝐴 ) ·_ih 𝐴 ) = ( ( 𝐵 ·_ih 𝐵 ) · ( 𝐴 ·_ih 𝐴 ) ) )
10	3 1 1 9	mp3an	⊢ ( ( ( 𝐵 ·_ih 𝐵 ) ·_ℎ 𝐴 ) ·_ih 𝐴 ) = ( ( 𝐵 ·_ih 𝐵 ) · ( 𝐴 ·_ih 𝐴 ) )
11	1 1	hicli	⊢ ( 𝐴 ·_ih 𝐴 ) ∈ ℂ
12	3 11	mulcomi	⊢ ( ( 𝐵 ·_ih 𝐵 ) · ( 𝐴 ·_ih 𝐴 ) ) = ( ( 𝐴 ·_ih 𝐴 ) · ( 𝐵 ·_ih 𝐵 ) )
13	10 12	eqtri	⊢ ( ( ( 𝐵 ·_ih 𝐵 ) ·_ℎ 𝐴 ) ·_ih 𝐴 ) = ( ( 𝐴 ·_ih 𝐴 ) · ( 𝐵 ·_ih 𝐵 ) )
14		ax-his3	⊢ ( ( ( 𝐴 ·_ih 𝐵 ) ∈ ℂ ∧ 𝐵 ∈ ℋ ∧ 𝐴 ∈ ℋ ) → ( ( ( 𝐴 ·_ih 𝐵 ) ·_ℎ 𝐵 ) ·_ih 𝐴 ) = ( ( 𝐴 ·_ih 𝐵 ) · ( 𝐵 ·_ih 𝐴 ) ) )
15	5 2 1 14	mp3an	⊢ ( ( ( 𝐴 ·_ih 𝐵 ) ·_ℎ 𝐵 ) ·_ih 𝐴 ) = ( ( 𝐴 ·_ih 𝐵 ) · ( 𝐵 ·_ih 𝐴 ) )
16	13 15	oveq12i	⊢ ( ( ( ( 𝐵 ·_ih 𝐵 ) ·_ℎ 𝐴 ) ·_ih 𝐴 ) − ( ( ( 𝐴 ·_ih 𝐵 ) ·_ℎ 𝐵 ) ·_ih 𝐴 ) ) = ( ( ( 𝐴 ·_ih 𝐴 ) · ( 𝐵 ·_ih 𝐵 ) ) − ( ( 𝐴 ·_ih 𝐵 ) · ( 𝐵 ·_ih 𝐴 ) ) )
17	8 16	eqtr2i	⊢ ( ( ( 𝐴 ·_ih 𝐴 ) · ( 𝐵 ·_ih 𝐵 ) ) − ( ( 𝐴 ·_ih 𝐵 ) · ( 𝐵 ·_ih 𝐴 ) ) ) = ( ( ( ( 𝐵 ·_ih 𝐵 ) ·_ℎ 𝐴 ) −_ℎ ( ( 𝐴 ·_ih 𝐵 ) ·_ℎ 𝐵 ) ) ·_ih 𝐴 )
18		his2sub	⊢ ( ( ( ( 𝐵 ·_ih 𝐵 ) ·_ℎ 𝐴 ) ∈ ℋ ∧ ( ( 𝐴 ·_ih 𝐵 ) ·_ℎ 𝐵 ) ∈ ℋ ∧ 𝐵 ∈ ℋ ) → ( ( ( ( 𝐵 ·_ih 𝐵 ) ·_ℎ 𝐴 ) −_ℎ ( ( 𝐴 ·_ih 𝐵 ) ·_ℎ 𝐵 ) ) ·_ih 𝐵 ) = ( ( ( ( 𝐵 ·_ih 𝐵 ) ·_ℎ 𝐴 ) ·_ih 𝐵 ) − ( ( ( 𝐴 ·_ih 𝐵 ) ·_ℎ 𝐵 ) ·_ih 𝐵 ) ) )
19	4 6 2 18	mp3an	⊢ ( ( ( ( 𝐵 ·_ih 𝐵 ) ·_ℎ 𝐴 ) −_ℎ ( ( 𝐴 ·_ih 𝐵 ) ·_ℎ 𝐵 ) ) ·_ih 𝐵 ) = ( ( ( ( 𝐵 ·_ih 𝐵 ) ·_ℎ 𝐴 ) ·_ih 𝐵 ) − ( ( ( 𝐴 ·_ih 𝐵 ) ·_ℎ 𝐵 ) ·_ih 𝐵 ) )
20	3 5	mulcomi	⊢ ( ( 𝐵 ·_ih 𝐵 ) · ( 𝐴 ·_ih 𝐵 ) ) = ( ( 𝐴 ·_ih 𝐵 ) · ( 𝐵 ·_ih 𝐵 ) )
21		ax-his3	⊢ ( ( ( 𝐵 ·_ih 𝐵 ) ∈ ℂ ∧ 𝐴 ∈ ℋ ∧ 𝐵 ∈ ℋ ) → ( ( ( 𝐵 ·_ih 𝐵 ) ·_ℎ 𝐴 ) ·_ih 𝐵 ) = ( ( 𝐵 ·_ih 𝐵 ) · ( 𝐴 ·_ih 𝐵 ) ) )
22	3 1 2 21	mp3an	⊢ ( ( ( 𝐵 ·_ih 𝐵 ) ·_ℎ 𝐴 ) ·_ih 𝐵 ) = ( ( 𝐵 ·_ih 𝐵 ) · ( 𝐴 ·_ih 𝐵 ) )
23		ax-his3	⊢ ( ( ( 𝐴 ·_ih 𝐵 ) ∈ ℂ ∧ 𝐵 ∈ ℋ ∧ 𝐵 ∈ ℋ ) → ( ( ( 𝐴 ·_ih 𝐵 ) ·_ℎ 𝐵 ) ·_ih 𝐵 ) = ( ( 𝐴 ·_ih 𝐵 ) · ( 𝐵 ·_ih 𝐵 ) ) )
24	5 2 2 23	mp3an	⊢ ( ( ( 𝐴 ·_ih 𝐵 ) ·_ℎ 𝐵 ) ·_ih 𝐵 ) = ( ( 𝐴 ·_ih 𝐵 ) · ( 𝐵 ·_ih 𝐵 ) )
25	20 22 24	3eqtr4i	⊢ ( ( ( 𝐵 ·_ih 𝐵 ) ·_ℎ 𝐴 ) ·_ih 𝐵 ) = ( ( ( 𝐴 ·_ih 𝐵 ) ·_ℎ 𝐵 ) ·_ih 𝐵 )
26	4 2	hicli	⊢ ( ( ( 𝐵 ·_ih 𝐵 ) ·_ℎ 𝐴 ) ·_ih 𝐵 ) ∈ ℂ
27	6 2	hicli	⊢ ( ( ( 𝐴 ·_ih 𝐵 ) ·_ℎ 𝐵 ) ·_ih 𝐵 ) ∈ ℂ
28	26 27	subeq0i	⊢ ( ( ( ( ( 𝐵 ·_ih 𝐵 ) ·_ℎ 𝐴 ) ·_ih 𝐵 ) − ( ( ( 𝐴 ·_ih 𝐵 ) ·_ℎ 𝐵 ) ·_ih 𝐵 ) ) = 0 ↔ ( ( ( 𝐵 ·_ih 𝐵 ) ·_ℎ 𝐴 ) ·_ih 𝐵 ) = ( ( ( 𝐴 ·_ih 𝐵 ) ·_ℎ 𝐵 ) ·_ih 𝐵 ) )
29	25 28	mpbir	⊢ ( ( ( ( 𝐵 ·_ih 𝐵 ) ·_ℎ 𝐴 ) ·_ih 𝐵 ) − ( ( ( 𝐴 ·_ih 𝐵 ) ·_ℎ 𝐵 ) ·_ih 𝐵 ) ) = 0
30	19 29	eqtri	⊢ ( ( ( ( 𝐵 ·_ih 𝐵 ) ·_ℎ 𝐴 ) −_ℎ ( ( 𝐴 ·_ih 𝐵 ) ·_ℎ 𝐵 ) ) ·_ih 𝐵 ) = 0
31	2	h1dei	⊢ ( 𝐴 ∈ ( ⊥ ‘ ( ⊥ ‘ { 𝐵 } ) ) ↔ ( 𝐴 ∈ ℋ ∧ ∀ 𝑥 ∈ ℋ ( ( 𝐵 ·_ih 𝑥 ) = 0 → ( 𝐴 ·_ih 𝑥 ) = 0 ) ) )
32	1 31	mpbiran	⊢ ( 𝐴 ∈ ( ⊥ ‘ ( ⊥ ‘ { 𝐵 } ) ) ↔ ∀ 𝑥 ∈ ℋ ( ( 𝐵 ·_ih 𝑥 ) = 0 → ( 𝐴 ·_ih 𝑥 ) = 0 ) )
33	4 6	hvsubcli	⊢ ( ( ( 𝐵 ·_ih 𝐵 ) ·_ℎ 𝐴 ) −_ℎ ( ( 𝐴 ·_ih 𝐵 ) ·_ℎ 𝐵 ) ) ∈ ℋ
34		oveq2	⊢ ( 𝑥 = ( ( ( 𝐵 ·_ih 𝐵 ) ·_ℎ 𝐴 ) −_ℎ ( ( 𝐴 ·_ih 𝐵 ) ·_ℎ 𝐵 ) ) → ( 𝐵 ·_ih 𝑥 ) = ( 𝐵 ·_ih ( ( ( 𝐵 ·_ih 𝐵 ) ·_ℎ 𝐴 ) −_ℎ ( ( 𝐴 ·_ih 𝐵 ) ·_ℎ 𝐵 ) ) ) )
35	34	eqeq1d	⊢ ( 𝑥 = ( ( ( 𝐵 ·_ih 𝐵 ) ·_ℎ 𝐴 ) −_ℎ ( ( 𝐴 ·_ih 𝐵 ) ·_ℎ 𝐵 ) ) → ( ( 𝐵 ·_ih 𝑥 ) = 0 ↔ ( 𝐵 ·_ih ( ( ( 𝐵 ·_ih 𝐵 ) ·_ℎ 𝐴 ) −_ℎ ( ( 𝐴 ·_ih 𝐵 ) ·_ℎ 𝐵 ) ) ) = 0 ) )
36		oveq2	⊢ ( 𝑥 = ( ( ( 𝐵 ·_ih 𝐵 ) ·_ℎ 𝐴 ) −_ℎ ( ( 𝐴 ·_ih 𝐵 ) ·_ℎ 𝐵 ) ) → ( 𝐴 ·_ih 𝑥 ) = ( 𝐴 ·_ih ( ( ( 𝐵 ·_ih 𝐵 ) ·_ℎ 𝐴 ) −_ℎ ( ( 𝐴 ·_ih 𝐵 ) ·_ℎ 𝐵 ) ) ) )
37	36	eqeq1d	⊢ ( 𝑥 = ( ( ( 𝐵 ·_ih 𝐵 ) ·_ℎ 𝐴 ) −_ℎ ( ( 𝐴 ·_ih 𝐵 ) ·_ℎ 𝐵 ) ) → ( ( 𝐴 ·_ih 𝑥 ) = 0 ↔ ( 𝐴 ·_ih ( ( ( 𝐵 ·_ih 𝐵 ) ·_ℎ 𝐴 ) −_ℎ ( ( 𝐴 ·_ih 𝐵 ) ·_ℎ 𝐵 ) ) ) = 0 ) )
38	35 37	imbi12d	⊢ ( 𝑥 = ( ( ( 𝐵 ·_ih 𝐵 ) ·_ℎ 𝐴 ) −_ℎ ( ( 𝐴 ·_ih 𝐵 ) ·_ℎ 𝐵 ) ) → ( ( ( 𝐵 ·_ih 𝑥 ) = 0 → ( 𝐴 ·_ih 𝑥 ) = 0 ) ↔ ( ( 𝐵 ·_ih ( ( ( 𝐵 ·_ih 𝐵 ) ·_ℎ 𝐴 ) −_ℎ ( ( 𝐴 ·_ih 𝐵 ) ·_ℎ 𝐵 ) ) ) = 0 → ( 𝐴 ·_ih ( ( ( 𝐵 ·_ih 𝐵 ) ·_ℎ 𝐴 ) −_ℎ ( ( 𝐴 ·_ih 𝐵 ) ·_ℎ 𝐵 ) ) ) = 0 ) ) )
39	38	rspcv	⊢ ( ( ( ( 𝐵 ·_ih 𝐵 ) ·_ℎ 𝐴 ) −_ℎ ( ( 𝐴 ·_ih 𝐵 ) ·_ℎ 𝐵 ) ) ∈ ℋ → ( ∀ 𝑥 ∈ ℋ ( ( 𝐵 ·_ih 𝑥 ) = 0 → ( 𝐴 ·_ih 𝑥 ) = 0 ) → ( ( 𝐵 ·_ih ( ( ( 𝐵 ·_ih 𝐵 ) ·_ℎ 𝐴 ) −_ℎ ( ( 𝐴 ·_ih 𝐵 ) ·_ℎ 𝐵 ) ) ) = 0 → ( 𝐴 ·_ih ( ( ( 𝐵 ·_ih 𝐵 ) ·_ℎ 𝐴 ) −_ℎ ( ( 𝐴 ·_ih 𝐵 ) ·_ℎ 𝐵 ) ) ) = 0 ) ) )
40	33 39	ax-mp	⊢ ( ∀ 𝑥 ∈ ℋ ( ( 𝐵 ·_ih 𝑥 ) = 0 → ( 𝐴 ·_ih 𝑥 ) = 0 ) → ( ( 𝐵 ·_ih ( ( ( 𝐵 ·_ih 𝐵 ) ·_ℎ 𝐴 ) −_ℎ ( ( 𝐴 ·_ih 𝐵 ) ·_ℎ 𝐵 ) ) ) = 0 → ( 𝐴 ·_ih ( ( ( 𝐵 ·_ih 𝐵 ) ·_ℎ 𝐴 ) −_ℎ ( ( 𝐴 ·_ih 𝐵 ) ·_ℎ 𝐵 ) ) ) = 0 ) )
41	32 40	sylbi	⊢ ( 𝐴 ∈ ( ⊥ ‘ ( ⊥ ‘ { 𝐵 } ) ) → ( ( 𝐵 ·_ih ( ( ( 𝐵 ·_ih 𝐵 ) ·_ℎ 𝐴 ) −_ℎ ( ( 𝐴 ·_ih 𝐵 ) ·_ℎ 𝐵 ) ) ) = 0 → ( 𝐴 ·_ih ( ( ( 𝐵 ·_ih 𝐵 ) ·_ℎ 𝐴 ) −_ℎ ( ( 𝐴 ·_ih 𝐵 ) ·_ℎ 𝐵 ) ) ) = 0 ) )
42		orthcom	⊢ ( ( ( ( ( 𝐵 ·_ih 𝐵 ) ·_ℎ 𝐴 ) −_ℎ ( ( 𝐴 ·_ih 𝐵 ) ·_ℎ 𝐵 ) ) ∈ ℋ ∧ 𝐵 ∈ ℋ ) → ( ( ( ( ( 𝐵 ·_ih 𝐵 ) ·_ℎ 𝐴 ) −_ℎ ( ( 𝐴 ·_ih 𝐵 ) ·_ℎ 𝐵 ) ) ·_ih 𝐵 ) = 0 ↔ ( 𝐵 ·_ih ( ( ( 𝐵 ·_ih 𝐵 ) ·_ℎ 𝐴 ) −_ℎ ( ( 𝐴 ·_ih 𝐵 ) ·_ℎ 𝐵 ) ) ) = 0 ) )
43	33 2 42	mp2an	⊢ ( ( ( ( ( 𝐵 ·_ih 𝐵 ) ·_ℎ 𝐴 ) −_ℎ ( ( 𝐴 ·_ih 𝐵 ) ·_ℎ 𝐵 ) ) ·_ih 𝐵 ) = 0 ↔ ( 𝐵 ·_ih ( ( ( 𝐵 ·_ih 𝐵 ) ·_ℎ 𝐴 ) −_ℎ ( ( 𝐴 ·_ih 𝐵 ) ·_ℎ 𝐵 ) ) ) = 0 )
44		orthcom	⊢ ( ( ( ( ( 𝐵 ·_ih 𝐵 ) ·_ℎ 𝐴 ) −_ℎ ( ( 𝐴 ·_ih 𝐵 ) ·_ℎ 𝐵 ) ) ∈ ℋ ∧ 𝐴 ∈ ℋ ) → ( ( ( ( ( 𝐵 ·_ih 𝐵 ) ·_ℎ 𝐴 ) −_ℎ ( ( 𝐴 ·_ih 𝐵 ) ·_ℎ 𝐵 ) ) ·_ih 𝐴 ) = 0 ↔ ( 𝐴 ·_ih ( ( ( 𝐵 ·_ih 𝐵 ) ·_ℎ 𝐴 ) −_ℎ ( ( 𝐴 ·_ih 𝐵 ) ·_ℎ 𝐵 ) ) ) = 0 ) )
45	33 1 44	mp2an	⊢ ( ( ( ( ( 𝐵 ·_ih 𝐵 ) ·_ℎ 𝐴 ) −_ℎ ( ( 𝐴 ·_ih 𝐵 ) ·_ℎ 𝐵 ) ) ·_ih 𝐴 ) = 0 ↔ ( 𝐴 ·_ih ( ( ( 𝐵 ·_ih 𝐵 ) ·_ℎ 𝐴 ) −_ℎ ( ( 𝐴 ·_ih 𝐵 ) ·_ℎ 𝐵 ) ) ) = 0 )
46	41 43 45	3imtr4g	⊢ ( 𝐴 ∈ ( ⊥ ‘ ( ⊥ ‘ { 𝐵 } ) ) → ( ( ( ( ( 𝐵 ·_ih 𝐵 ) ·_ℎ 𝐴 ) −_ℎ ( ( 𝐴 ·_ih 𝐵 ) ·_ℎ 𝐵 ) ) ·_ih 𝐵 ) = 0 → ( ( ( ( 𝐵 ·_ih 𝐵 ) ·_ℎ 𝐴 ) −_ℎ ( ( 𝐴 ·_ih 𝐵 ) ·_ℎ 𝐵 ) ) ·_ih 𝐴 ) = 0 ) )
47	30 46	mpi	⊢ ( 𝐴 ∈ ( ⊥ ‘ ( ⊥ ‘ { 𝐵 } ) ) → ( ( ( ( 𝐵 ·_ih 𝐵 ) ·_ℎ 𝐴 ) −_ℎ ( ( 𝐴 ·_ih 𝐵 ) ·_ℎ 𝐵 ) ) ·_ih 𝐴 ) = 0 )
48	17 47	syl5eq	⊢ ( 𝐴 ∈ ( ⊥ ‘ ( ⊥ ‘ { 𝐵 } ) ) → ( ( ( 𝐴 ·_ih 𝐴 ) · ( 𝐵 ·_ih 𝐵 ) ) − ( ( 𝐴 ·_ih 𝐵 ) · ( 𝐵 ·_ih 𝐴 ) ) ) = 0 )
49	11 3	mulcli	⊢ ( ( 𝐴 ·_ih 𝐴 ) · ( 𝐵 ·_ih 𝐵 ) ) ∈ ℂ
50	2 1	hicli	⊢ ( 𝐵 ·_ih 𝐴 ) ∈ ℂ
51	5 50	mulcli	⊢ ( ( 𝐴 ·_ih 𝐵 ) · ( 𝐵 ·_ih 𝐴 ) ) ∈ ℂ
52	49 51	subeq0i	⊢ ( ( ( ( 𝐴 ·_ih 𝐴 ) · ( 𝐵 ·_ih 𝐵 ) ) − ( ( 𝐴 ·_ih 𝐵 ) · ( 𝐵 ·_ih 𝐴 ) ) ) = 0 ↔ ( ( 𝐴 ·_ih 𝐴 ) · ( 𝐵 ·_ih 𝐵 ) ) = ( ( 𝐴 ·_ih 𝐵 ) · ( 𝐵 ·_ih 𝐴 ) ) )
53	48 52	sylib	⊢ ( 𝐴 ∈ ( ⊥ ‘ ( ⊥ ‘ { 𝐵 } ) ) → ( ( 𝐴 ·_ih 𝐴 ) · ( 𝐵 ·_ih 𝐵 ) ) = ( ( 𝐴 ·_ih 𝐵 ) · ( 𝐵 ·_ih 𝐴 ) ) )
54	53	eqcomd	⊢ ( 𝐴 ∈ ( ⊥ ‘ ( ⊥ ‘ { 𝐵 } ) ) → ( ( 𝐴 ·_ih 𝐵 ) · ( 𝐵 ·_ih 𝐴 ) ) = ( ( 𝐴 ·_ih 𝐴 ) · ( 𝐵 ·_ih 𝐵 ) ) )
55	1 2	bcseqi	⊢ ( ( ( 𝐴 ·_ih 𝐵 ) · ( 𝐵 ·_ih 𝐴 ) ) = ( ( 𝐴 ·_ih 𝐴 ) · ( 𝐵 ·_ih 𝐵 ) ) ↔ ( ( 𝐵 ·_ih 𝐵 ) ·_ℎ 𝐴 ) = ( ( 𝐴 ·_ih 𝐵 ) ·_ℎ 𝐵 ) )
56	54 55	sylib	⊢ ( 𝐴 ∈ ( ⊥ ‘ ( ⊥ ‘ { 𝐵 } ) ) → ( ( 𝐵 ·_ih 𝐵 ) ·_ℎ 𝐴 ) = ( ( 𝐴 ·_ih 𝐵 ) ·_ℎ 𝐵 ) )

Metamath Proof Explorer

Theorem h1de2i

Proof