h1de2bi

Description: Membership in 1-dimensional subspace. All members are collinear with the generating vector. (Contributed by NM, 19-Jul-2001) (Revised by Mario Carneiro, 15-May-2014) (New usage is discouraged.)

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

Proof

Step	Hyp	Ref	Expression
1		h1de2.1	⊢ 𝐴 ∈ ℋ
2		h1de2.2	⊢ 𝐵 ∈ ℋ
3		his6	⊢ ( 𝐵 ∈ ℋ → ( ( 𝐵 ·_ih 𝐵 ) = 0 ↔ 𝐵 = 0_ℎ ) )
4	2 3	ax-mp	⊢ ( ( 𝐵 ·_ih 𝐵 ) = 0 ↔ 𝐵 = 0_ℎ )
5	4	necon3bii	⊢ ( ( 𝐵 ·_ih 𝐵 ) ≠ 0 ↔ 𝐵 ≠ 0_ℎ )
6	1 2	h1de2i	⊢ ( 𝐴 ∈ ( ⊥ ‘ ( ⊥ ‘ { 𝐵 } ) ) → ( ( 𝐵 ·_ih 𝐵 ) ·_ℎ 𝐴 ) = ( ( 𝐴 ·_ih 𝐵 ) ·_ℎ 𝐵 ) )
7	6	adantl	⊢ ( ( ( 𝐵 ·_ih 𝐵 ) ≠ 0 ∧ 𝐴 ∈ ( ⊥ ‘ ( ⊥ ‘ { 𝐵 } ) ) ) → ( ( 𝐵 ·_ih 𝐵 ) ·_ℎ 𝐴 ) = ( ( 𝐴 ·_ih 𝐵 ) ·_ℎ 𝐵 ) )
8	7	oveq2d	⊢ ( ( ( 𝐵 ·_ih 𝐵 ) ≠ 0 ∧ 𝐴 ∈ ( ⊥ ‘ ( ⊥ ‘ { 𝐵 } ) ) ) → ( ( 1 / ( 𝐵 ·_ih 𝐵 ) ) ·_ℎ ( ( 𝐵 ·_ih 𝐵 ) ·_ℎ 𝐴 ) ) = ( ( 1 / ( 𝐵 ·_ih 𝐵 ) ) ·_ℎ ( ( 𝐴 ·_ih 𝐵 ) ·_ℎ 𝐵 ) ) )
9	2 2	hicli	⊢ ( 𝐵 ·_ih 𝐵 ) ∈ ℂ
10	9	recclzi	⊢ ( ( 𝐵 ·_ih 𝐵 ) ≠ 0 → ( 1 / ( 𝐵 ·_ih 𝐵 ) ) ∈ ℂ )
11		ax-hvmulass	⊢ ( ( ( 1 / ( 𝐵 ·_ih 𝐵 ) ) ∈ ℂ ∧ ( 𝐵 ·_ih 𝐵 ) ∈ ℂ ∧ 𝐴 ∈ ℋ ) → ( ( ( 1 / ( 𝐵 ·_ih 𝐵 ) ) · ( 𝐵 ·_ih 𝐵 ) ) ·_ℎ 𝐴 ) = ( ( 1 / ( 𝐵 ·_ih 𝐵 ) ) ·_ℎ ( ( 𝐵 ·_ih 𝐵 ) ·_ℎ 𝐴 ) ) )
12	9 1 11	mp3an23	⊢ ( ( 1 / ( 𝐵 ·_ih 𝐵 ) ) ∈ ℂ → ( ( ( 1 / ( 𝐵 ·_ih 𝐵 ) ) · ( 𝐵 ·_ih 𝐵 ) ) ·_ℎ 𝐴 ) = ( ( 1 / ( 𝐵 ·_ih 𝐵 ) ) ·_ℎ ( ( 𝐵 ·_ih 𝐵 ) ·_ℎ 𝐴 ) ) )
13	10 12	syl	⊢ ( ( 𝐵 ·_ih 𝐵 ) ≠ 0 → ( ( ( 1 / ( 𝐵 ·_ih 𝐵 ) ) · ( 𝐵 ·_ih 𝐵 ) ) ·_ℎ 𝐴 ) = ( ( 1 / ( 𝐵 ·_ih 𝐵 ) ) ·_ℎ ( ( 𝐵 ·_ih 𝐵 ) ·_ℎ 𝐴 ) ) )
14		ax-1cn	⊢ 1 ∈ ℂ
15	14 9	divcan1zi	⊢ ( ( 𝐵 ·_ih 𝐵 ) ≠ 0 → ( ( 1 / ( 𝐵 ·_ih 𝐵 ) ) · ( 𝐵 ·_ih 𝐵 ) ) = 1 )
16	15	oveq1d	⊢ ( ( 𝐵 ·_ih 𝐵 ) ≠ 0 → ( ( ( 1 / ( 𝐵 ·_ih 𝐵 ) ) · ( 𝐵 ·_ih 𝐵 ) ) ·_ℎ 𝐴 ) = ( 1 ·_ℎ 𝐴 ) )
17	13 16	eqtr3d	⊢ ( ( 𝐵 ·_ih 𝐵 ) ≠ 0 → ( ( 1 / ( 𝐵 ·_ih 𝐵 ) ) ·_ℎ ( ( 𝐵 ·_ih 𝐵 ) ·_ℎ 𝐴 ) ) = ( 1 ·_ℎ 𝐴 ) )
18		ax-hvmulid	⊢ ( 𝐴 ∈ ℋ → ( 1 ·_ℎ 𝐴 ) = 𝐴 )
19	1 18	ax-mp	⊢ ( 1 ·_ℎ 𝐴 ) = 𝐴
20	17 19	eqtrdi	⊢ ( ( 𝐵 ·_ih 𝐵 ) ≠ 0 → ( ( 1 / ( 𝐵 ·_ih 𝐵 ) ) ·_ℎ ( ( 𝐵 ·_ih 𝐵 ) ·_ℎ 𝐴 ) ) = 𝐴 )
21	20	adantr	⊢ ( ( ( 𝐵 ·_ih 𝐵 ) ≠ 0 ∧ 𝐴 ∈ ( ⊥ ‘ ( ⊥ ‘ { 𝐵 } ) ) ) → ( ( 1 / ( 𝐵 ·_ih 𝐵 ) ) ·_ℎ ( ( 𝐵 ·_ih 𝐵 ) ·_ℎ 𝐴 ) ) = 𝐴 )
22	8 21	eqtr3d	⊢ ( ( ( 𝐵 ·_ih 𝐵 ) ≠ 0 ∧ 𝐴 ∈ ( ⊥ ‘ ( ⊥ ‘ { 𝐵 } ) ) ) → ( ( 1 / ( 𝐵 ·_ih 𝐵 ) ) ·_ℎ ( ( 𝐴 ·_ih 𝐵 ) ·_ℎ 𝐵 ) ) = 𝐴 )
23	1 2	hicli	⊢ ( 𝐴 ·_ih 𝐵 ) ∈ ℂ
24		ax-hvmulass	⊢ ( ( ( 1 / ( 𝐵 ·_ih 𝐵 ) ) ∈ ℂ ∧ ( 𝐴 ·_ih 𝐵 ) ∈ ℂ ∧ 𝐵 ∈ ℋ ) → ( ( ( 1 / ( 𝐵 ·_ih 𝐵 ) ) · ( 𝐴 ·_ih 𝐵 ) ) ·_ℎ 𝐵 ) = ( ( 1 / ( 𝐵 ·_ih 𝐵 ) ) ·_ℎ ( ( 𝐴 ·_ih 𝐵 ) ·_ℎ 𝐵 ) ) )
25	23 2 24	mp3an23	⊢ ( ( 1 / ( 𝐵 ·_ih 𝐵 ) ) ∈ ℂ → ( ( ( 1 / ( 𝐵 ·_ih 𝐵 ) ) · ( 𝐴 ·_ih 𝐵 ) ) ·_ℎ 𝐵 ) = ( ( 1 / ( 𝐵 ·_ih 𝐵 ) ) ·_ℎ ( ( 𝐴 ·_ih 𝐵 ) ·_ℎ 𝐵 ) ) )
26	10 25	syl	⊢ ( ( 𝐵 ·_ih 𝐵 ) ≠ 0 → ( ( ( 1 / ( 𝐵 ·_ih 𝐵 ) ) · ( 𝐴 ·_ih 𝐵 ) ) ·_ℎ 𝐵 ) = ( ( 1 / ( 𝐵 ·_ih 𝐵 ) ) ·_ℎ ( ( 𝐴 ·_ih 𝐵 ) ·_ℎ 𝐵 ) ) )
27		mulcom	⊢ ( ( ( 1 / ( 𝐵 ·_ih 𝐵 ) ) ∈ ℂ ∧ ( 𝐴 ·_ih 𝐵 ) ∈ ℂ ) → ( ( 1 / ( 𝐵 ·_ih 𝐵 ) ) · ( 𝐴 ·_ih 𝐵 ) ) = ( ( 𝐴 ·_ih 𝐵 ) · ( 1 / ( 𝐵 ·_ih 𝐵 ) ) ) )
28	10 23 27	sylancl	⊢ ( ( 𝐵 ·_ih 𝐵 ) ≠ 0 → ( ( 1 / ( 𝐵 ·_ih 𝐵 ) ) · ( 𝐴 ·_ih 𝐵 ) ) = ( ( 𝐴 ·_ih 𝐵 ) · ( 1 / ( 𝐵 ·_ih 𝐵 ) ) ) )
29	23 9	divreczi	⊢ ( ( 𝐵 ·_ih 𝐵 ) ≠ 0 → ( ( 𝐴 ·_ih 𝐵 ) / ( 𝐵 ·_ih 𝐵 ) ) = ( ( 𝐴 ·_ih 𝐵 ) · ( 1 / ( 𝐵 ·_ih 𝐵 ) ) ) )
30	28 29	eqtr4d	⊢ ( ( 𝐵 ·_ih 𝐵 ) ≠ 0 → ( ( 1 / ( 𝐵 ·_ih 𝐵 ) ) · ( 𝐴 ·_ih 𝐵 ) ) = ( ( 𝐴 ·_ih 𝐵 ) / ( 𝐵 ·_ih 𝐵 ) ) )
31	30	oveq1d	⊢ ( ( 𝐵 ·_ih 𝐵 ) ≠ 0 → ( ( ( 1 / ( 𝐵 ·_ih 𝐵 ) ) · ( 𝐴 ·_ih 𝐵 ) ) ·_ℎ 𝐵 ) = ( ( ( 𝐴 ·_ih 𝐵 ) / ( 𝐵 ·_ih 𝐵 ) ) ·_ℎ 𝐵 ) )
32	26 31	eqtr3d	⊢ ( ( 𝐵 ·_ih 𝐵 ) ≠ 0 → ( ( 1 / ( 𝐵 ·_ih 𝐵 ) ) ·_ℎ ( ( 𝐴 ·_ih 𝐵 ) ·_ℎ 𝐵 ) ) = ( ( ( 𝐴 ·_ih 𝐵 ) / ( 𝐵 ·_ih 𝐵 ) ) ·_ℎ 𝐵 ) )
33	32	adantr	⊢ ( ( ( 𝐵 ·_ih 𝐵 ) ≠ 0 ∧ 𝐴 ∈ ( ⊥ ‘ ( ⊥ ‘ { 𝐵 } ) ) ) → ( ( 1 / ( 𝐵 ·_ih 𝐵 ) ) ·_ℎ ( ( 𝐴 ·_ih 𝐵 ) ·_ℎ 𝐵 ) ) = ( ( ( 𝐴 ·_ih 𝐵 ) / ( 𝐵 ·_ih 𝐵 ) ) ·_ℎ 𝐵 ) )
34	22 33	eqtr3d	⊢ ( ( ( 𝐵 ·_ih 𝐵 ) ≠ 0 ∧ 𝐴 ∈ ( ⊥ ‘ ( ⊥ ‘ { 𝐵 } ) ) ) → 𝐴 = ( ( ( 𝐴 ·_ih 𝐵 ) / ( 𝐵 ·_ih 𝐵 ) ) ·_ℎ 𝐵 ) )
35	34	ex	⊢ ( ( 𝐵 ·_ih 𝐵 ) ≠ 0 → ( 𝐴 ∈ ( ⊥ ‘ ( ⊥ ‘ { 𝐵 } ) ) → 𝐴 = ( ( ( 𝐴 ·_ih 𝐵 ) / ( 𝐵 ·_ih 𝐵 ) ) ·_ℎ 𝐵 ) ) )
36	23 9	divclzi	⊢ ( ( 𝐵 ·_ih 𝐵 ) ≠ 0 → ( ( 𝐴 ·_ih 𝐵 ) / ( 𝐵 ·_ih 𝐵 ) ) ∈ ℂ )
37	2	elexi	⊢ 𝐵 ∈ V
38	37	snss	⊢ ( 𝐵 ∈ ℋ ↔ { 𝐵 } ⊆ ℋ )
39	2 38	mpbi	⊢ { 𝐵 } ⊆ ℋ
40		occl	⊢ ( { 𝐵 } ⊆ ℋ → ( ⊥ ‘ { 𝐵 } ) ∈ C_ℋ )
41	39 40	ax-mp	⊢ ( ⊥ ‘ { 𝐵 } ) ∈ C_ℋ
42	41	choccli	⊢ ( ⊥ ‘ ( ⊥ ‘ { 𝐵 } ) ) ∈ C_ℋ
43	42	chshii	⊢ ( ⊥ ‘ ( ⊥ ‘ { 𝐵 } ) ) ∈ S_ℋ
44		h1did	⊢ ( 𝐵 ∈ ℋ → 𝐵 ∈ ( ⊥ ‘ ( ⊥ ‘ { 𝐵 } ) ) )
45	2 44	ax-mp	⊢ 𝐵 ∈ ( ⊥ ‘ ( ⊥ ‘ { 𝐵 } ) )
46		shmulcl	⊢ ( ( ( ⊥ ‘ ( ⊥ ‘ { 𝐵 } ) ) ∈ S_ℋ ∧ ( ( 𝐴 ·_ih 𝐵 ) / ( 𝐵 ·_ih 𝐵 ) ) ∈ ℂ ∧ 𝐵 ∈ ( ⊥ ‘ ( ⊥ ‘ { 𝐵 } ) ) ) → ( ( ( 𝐴 ·_ih 𝐵 ) / ( 𝐵 ·_ih 𝐵 ) ) ·_ℎ 𝐵 ) ∈ ( ⊥ ‘ ( ⊥ ‘ { 𝐵 } ) ) )
47	43 45 46	mp3an13	⊢ ( ( ( 𝐴 ·_ih 𝐵 ) / ( 𝐵 ·_ih 𝐵 ) ) ∈ ℂ → ( ( ( 𝐴 ·_ih 𝐵 ) / ( 𝐵 ·_ih 𝐵 ) ) ·_ℎ 𝐵 ) ∈ ( ⊥ ‘ ( ⊥ ‘ { 𝐵 } ) ) )
48	36 47	syl	⊢ ( ( 𝐵 ·_ih 𝐵 ) ≠ 0 → ( ( ( 𝐴 ·_ih 𝐵 ) / ( 𝐵 ·_ih 𝐵 ) ) ·_ℎ 𝐵 ) ∈ ( ⊥ ‘ ( ⊥ ‘ { 𝐵 } ) ) )
49		eleq1	⊢ ( 𝐴 = ( ( ( 𝐴 ·_ih 𝐵 ) / ( 𝐵 ·_ih 𝐵 ) ) ·_ℎ 𝐵 ) → ( 𝐴 ∈ ( ⊥ ‘ ( ⊥ ‘ { 𝐵 } ) ) ↔ ( ( ( 𝐴 ·_ih 𝐵 ) / ( 𝐵 ·_ih 𝐵 ) ) ·_ℎ 𝐵 ) ∈ ( ⊥ ‘ ( ⊥ ‘ { 𝐵 } ) ) ) )
50	48 49	syl5ibrcom	⊢ ( ( 𝐵 ·_ih 𝐵 ) ≠ 0 → ( 𝐴 = ( ( ( 𝐴 ·_ih 𝐵 ) / ( 𝐵 ·_ih 𝐵 ) ) ·_ℎ 𝐵 ) → 𝐴 ∈ ( ⊥ ‘ ( ⊥ ‘ { 𝐵 } ) ) ) )
51	35 50	impbid	⊢ ( ( 𝐵 ·_ih 𝐵 ) ≠ 0 → ( 𝐴 ∈ ( ⊥ ‘ ( ⊥ ‘ { 𝐵 } ) ) ↔ 𝐴 = ( ( ( 𝐴 ·_ih 𝐵 ) / ( 𝐵 ·_ih 𝐵 ) ) ·_ℎ 𝐵 ) ) )
52	5 51	sylbir	⊢ ( 𝐵 ≠ 0_ℎ → ( 𝐴 ∈ ( ⊥ ‘ ( ⊥ ‘ { 𝐵 } ) ) ↔ 𝐴 = ( ( ( 𝐴 ·_ih 𝐵 ) / ( 𝐵 ·_ih 𝐵 ) ) ·_ℎ 𝐵 ) ) )

Metamath Proof Explorer

Theorem h1de2bi

Proof