elspansn2

Description: Membership in the span of a singleton. All members are collinear with the generating vector. (Contributed by NM, 5-Jun-2004) (New usage is discouraged.)

		Ref	Expression
	Assertion	elspansn2	⊢ ( ( 𝐴 ∈ ℋ ∧ 𝐵 ∈ ℋ ∧ 𝐵 ≠ 0_ℎ ) → ( 𝐴 ∈ ( span ‘ { 𝐵 } ) ↔ 𝐴 = ( ( ( 𝐴 ·_ih 𝐵 ) / ( 𝐵 ·_ih 𝐵 ) ) ·_ℎ 𝐵 ) ) )

Proof

Step	Hyp	Ref	Expression
1		spansn	⊢ ( 𝐵 ∈ ℋ → ( span ‘ { 𝐵 } ) = ( ⊥ ‘ ( ⊥ ‘ { 𝐵 } ) ) )
2	1	eleq2d	⊢ ( 𝐵 ∈ ℋ → ( 𝐴 ∈ ( span ‘ { 𝐵 } ) ↔ 𝐴 ∈ ( ⊥ ‘ ( ⊥ ‘ { 𝐵 } ) ) ) )
3	2	3ad2ant2	⊢ ( ( 𝐴 ∈ ℋ ∧ 𝐵 ∈ ℋ ∧ 𝐵 ≠ 0_ℎ ) → ( 𝐴 ∈ ( span ‘ { 𝐵 } ) ↔ 𝐴 ∈ ( ⊥ ‘ ( ⊥ ‘ { 𝐵 } ) ) ) )
4		eleq1	⊢ ( 𝐴 = if ( 𝐴 ∈ ℋ , 𝐴 , 0_ℎ ) → ( 𝐴 ∈ ( ⊥ ‘ ( ⊥ ‘ { 𝐵 } ) ) ↔ if ( 𝐴 ∈ ℋ , 𝐴 , 0_ℎ ) ∈ ( ⊥ ‘ ( ⊥ ‘ { 𝐵 } ) ) ) )
5		id	⊢ ( 𝐴 = if ( 𝐴 ∈ ℋ , 𝐴 , 0_ℎ ) → 𝐴 = if ( 𝐴 ∈ ℋ , 𝐴 , 0_ℎ ) )
6		oveq1	⊢ ( 𝐴 = if ( 𝐴 ∈ ℋ , 𝐴 , 0_ℎ ) → ( 𝐴 ·_ih 𝐵 ) = ( if ( 𝐴 ∈ ℋ , 𝐴 , 0_ℎ ) ·_ih 𝐵 ) )
7	6	oveq1d	⊢ ( 𝐴 = if ( 𝐴 ∈ ℋ , 𝐴 , 0_ℎ ) → ( ( 𝐴 ·_ih 𝐵 ) / ( 𝐵 ·_ih 𝐵 ) ) = ( ( if ( 𝐴 ∈ ℋ , 𝐴 , 0_ℎ ) ·_ih 𝐵 ) / ( 𝐵 ·_ih 𝐵 ) ) )
8	7	oveq1d	⊢ ( 𝐴 = if ( 𝐴 ∈ ℋ , 𝐴 , 0_ℎ ) → ( ( ( 𝐴 ·_ih 𝐵 ) / ( 𝐵 ·_ih 𝐵 ) ) ·_ℎ 𝐵 ) = ( ( ( if ( 𝐴 ∈ ℋ , 𝐴 , 0_ℎ ) ·_ih 𝐵 ) / ( 𝐵 ·_ih 𝐵 ) ) ·_ℎ 𝐵 ) )
9	5 8	eqeq12d	⊢ ( 𝐴 = if ( 𝐴 ∈ ℋ , 𝐴 , 0_ℎ ) → ( 𝐴 = ( ( ( 𝐴 ·_ih 𝐵 ) / ( 𝐵 ·_ih 𝐵 ) ) ·_ℎ 𝐵 ) ↔ if ( 𝐴 ∈ ℋ , 𝐴 , 0_ℎ ) = ( ( ( if ( 𝐴 ∈ ℋ , 𝐴 , 0_ℎ ) ·_ih 𝐵 ) / ( 𝐵 ·_ih 𝐵 ) ) ·_ℎ 𝐵 ) ) )
10	4 9	bibi12d	⊢ ( 𝐴 = if ( 𝐴 ∈ ℋ , 𝐴 , 0_ℎ ) → ( ( 𝐴 ∈ ( ⊥ ‘ ( ⊥ ‘ { 𝐵 } ) ) ↔ 𝐴 = ( ( ( 𝐴 ·_ih 𝐵 ) / ( 𝐵 ·_ih 𝐵 ) ) ·_ℎ 𝐵 ) ) ↔ ( if ( 𝐴 ∈ ℋ , 𝐴 , 0_ℎ ) ∈ ( ⊥ ‘ ( ⊥ ‘ { 𝐵 } ) ) ↔ if ( 𝐴 ∈ ℋ , 𝐴 , 0_ℎ ) = ( ( ( if ( 𝐴 ∈ ℋ , 𝐴 , 0_ℎ ) ·_ih 𝐵 ) / ( 𝐵 ·_ih 𝐵 ) ) ·_ℎ 𝐵 ) ) ) )
11	10	imbi2d	⊢ ( 𝐴 = if ( 𝐴 ∈ ℋ , 𝐴 , 0_ℎ ) → ( ( 𝐵 ≠ 0_ℎ → ( 𝐴 ∈ ( ⊥ ‘ ( ⊥ ‘ { 𝐵 } ) ) ↔ 𝐴 = ( ( ( 𝐴 ·_ih 𝐵 ) / ( 𝐵 ·_ih 𝐵 ) ) ·_ℎ 𝐵 ) ) ) ↔ ( 𝐵 ≠ 0_ℎ → ( if ( 𝐴 ∈ ℋ , 𝐴 , 0_ℎ ) ∈ ( ⊥ ‘ ( ⊥ ‘ { 𝐵 } ) ) ↔ if ( 𝐴 ∈ ℋ , 𝐴 , 0_ℎ ) = ( ( ( if ( 𝐴 ∈ ℋ , 𝐴 , 0_ℎ ) ·_ih 𝐵 ) / ( 𝐵 ·_ih 𝐵 ) ) ·_ℎ 𝐵 ) ) ) ) )
12		neeq1	⊢ ( 𝐵 = if ( 𝐵 ∈ ℋ , 𝐵 , 0_ℎ ) → ( 𝐵 ≠ 0_ℎ ↔ if ( 𝐵 ∈ ℋ , 𝐵 , 0_ℎ ) ≠ 0_ℎ ) )
13		sneq	⊢ ( 𝐵 = if ( 𝐵 ∈ ℋ , 𝐵 , 0_ℎ ) → { 𝐵 } = { if ( 𝐵 ∈ ℋ , 𝐵 , 0_ℎ ) } )
14	13	fveq2d	⊢ ( 𝐵 = if ( 𝐵 ∈ ℋ , 𝐵 , 0_ℎ ) → ( ⊥ ‘ { 𝐵 } ) = ( ⊥ ‘ { if ( 𝐵 ∈ ℋ , 𝐵 , 0_ℎ ) } ) )
15	14	fveq2d	⊢ ( 𝐵 = if ( 𝐵 ∈ ℋ , 𝐵 , 0_ℎ ) → ( ⊥ ‘ ( ⊥ ‘ { 𝐵 } ) ) = ( ⊥ ‘ ( ⊥ ‘ { if ( 𝐵 ∈ ℋ , 𝐵 , 0_ℎ ) } ) ) )
16	15	eleq2d	⊢ ( 𝐵 = if ( 𝐵 ∈ ℋ , 𝐵 , 0_ℎ ) → ( if ( 𝐴 ∈ ℋ , 𝐴 , 0_ℎ ) ∈ ( ⊥ ‘ ( ⊥ ‘ { 𝐵 } ) ) ↔ if ( 𝐴 ∈ ℋ , 𝐴 , 0_ℎ ) ∈ ( ⊥ ‘ ( ⊥ ‘ { if ( 𝐵 ∈ ℋ , 𝐵 , 0_ℎ ) } ) ) ) )
17		oveq2	⊢ ( 𝐵 = if ( 𝐵 ∈ ℋ , 𝐵 , 0_ℎ ) → ( if ( 𝐴 ∈ ℋ , 𝐴 , 0_ℎ ) ·_ih 𝐵 ) = ( if ( 𝐴 ∈ ℋ , 𝐴 , 0_ℎ ) ·_ih if ( 𝐵 ∈ ℋ , 𝐵 , 0_ℎ ) ) )
18		oveq1	⊢ ( 𝐵 = if ( 𝐵 ∈ ℋ , 𝐵 , 0_ℎ ) → ( 𝐵 ·_ih 𝐵 ) = ( if ( 𝐵 ∈ ℋ , 𝐵 , 0_ℎ ) ·_ih 𝐵 ) )
19		oveq2	⊢ ( 𝐵 = if ( 𝐵 ∈ ℋ , 𝐵 , 0_ℎ ) → ( if ( 𝐵 ∈ ℋ , 𝐵 , 0_ℎ ) ·_ih 𝐵 ) = ( if ( 𝐵 ∈ ℋ , 𝐵 , 0_ℎ ) ·_ih if ( 𝐵 ∈ ℋ , 𝐵 , 0_ℎ ) ) )
20	18 19	eqtrd	⊢ ( 𝐵 = if ( 𝐵 ∈ ℋ , 𝐵 , 0_ℎ ) → ( 𝐵 ·_ih 𝐵 ) = ( if ( 𝐵 ∈ ℋ , 𝐵 , 0_ℎ ) ·_ih if ( 𝐵 ∈ ℋ , 𝐵 , 0_ℎ ) ) )
21	17 20	oveq12d	⊢ ( 𝐵 = if ( 𝐵 ∈ ℋ , 𝐵 , 0_ℎ ) → ( ( if ( 𝐴 ∈ ℋ , 𝐴 , 0_ℎ ) ·_ih 𝐵 ) / ( 𝐵 ·_ih 𝐵 ) ) = ( ( if ( 𝐴 ∈ ℋ , 𝐴 , 0_ℎ ) ·_ih if ( 𝐵 ∈ ℋ , 𝐵 , 0_ℎ ) ) / ( if ( 𝐵 ∈ ℋ , 𝐵 , 0_ℎ ) ·_ih if ( 𝐵 ∈ ℋ , 𝐵 , 0_ℎ ) ) ) )
22		id	⊢ ( 𝐵 = if ( 𝐵 ∈ ℋ , 𝐵 , 0_ℎ ) → 𝐵 = if ( 𝐵 ∈ ℋ , 𝐵 , 0_ℎ ) )
23	21 22	oveq12d	⊢ ( 𝐵 = if ( 𝐵 ∈ ℋ , 𝐵 , 0_ℎ ) → ( ( ( if ( 𝐴 ∈ ℋ , 𝐴 , 0_ℎ ) ·_ih 𝐵 ) / ( 𝐵 ·_ih 𝐵 ) ) ·_ℎ 𝐵 ) = ( ( ( if ( 𝐴 ∈ ℋ , 𝐴 , 0_ℎ ) ·_ih if ( 𝐵 ∈ ℋ , 𝐵 , 0_ℎ ) ) / ( if ( 𝐵 ∈ ℋ , 𝐵 , 0_ℎ ) ·_ih if ( 𝐵 ∈ ℋ , 𝐵 , 0_ℎ ) ) ) ·_ℎ if ( 𝐵 ∈ ℋ , 𝐵 , 0_ℎ ) ) )
24	23	eqeq2d	⊢ ( 𝐵 = if ( 𝐵 ∈ ℋ , 𝐵 , 0_ℎ ) → ( if ( 𝐴 ∈ ℋ , 𝐴 , 0_ℎ ) = ( ( ( if ( 𝐴 ∈ ℋ , 𝐴 , 0_ℎ ) ·_ih 𝐵 ) / ( 𝐵 ·_ih 𝐵 ) ) ·_ℎ 𝐵 ) ↔ if ( 𝐴 ∈ ℋ , 𝐴 , 0_ℎ ) = ( ( ( if ( 𝐴 ∈ ℋ , 𝐴 , 0_ℎ ) ·_ih if ( 𝐵 ∈ ℋ , 𝐵 , 0_ℎ ) ) / ( if ( 𝐵 ∈ ℋ , 𝐵 , 0_ℎ ) ·_ih if ( 𝐵 ∈ ℋ , 𝐵 , 0_ℎ ) ) ) ·_ℎ if ( 𝐵 ∈ ℋ , 𝐵 , 0_ℎ ) ) ) )
25	16 24	bibi12d	⊢ ( 𝐵 = if ( 𝐵 ∈ ℋ , 𝐵 , 0_ℎ ) → ( ( if ( 𝐴 ∈ ℋ , 𝐴 , 0_ℎ ) ∈ ( ⊥ ‘ ( ⊥ ‘ { 𝐵 } ) ) ↔ if ( 𝐴 ∈ ℋ , 𝐴 , 0_ℎ ) = ( ( ( if ( 𝐴 ∈ ℋ , 𝐴 , 0_ℎ ) ·_ih 𝐵 ) / ( 𝐵 ·_ih 𝐵 ) ) ·_ℎ 𝐵 ) ) ↔ ( if ( 𝐴 ∈ ℋ , 𝐴 , 0_ℎ ) ∈ ( ⊥ ‘ ( ⊥ ‘ { if ( 𝐵 ∈ ℋ , 𝐵 , 0_ℎ ) } ) ) ↔ if ( 𝐴 ∈ ℋ , 𝐴 , 0_ℎ ) = ( ( ( if ( 𝐴 ∈ ℋ , 𝐴 , 0_ℎ ) ·_ih if ( 𝐵 ∈ ℋ , 𝐵 , 0_ℎ ) ) / ( if ( 𝐵 ∈ ℋ , 𝐵 , 0_ℎ ) ·_ih if ( 𝐵 ∈ ℋ , 𝐵 , 0_ℎ ) ) ) ·_ℎ if ( 𝐵 ∈ ℋ , 𝐵 , 0_ℎ ) ) ) ) )
26	12 25	imbi12d	⊢ ( 𝐵 = if ( 𝐵 ∈ ℋ , 𝐵 , 0_ℎ ) → ( ( 𝐵 ≠ 0_ℎ → ( if ( 𝐴 ∈ ℋ , 𝐴 , 0_ℎ ) ∈ ( ⊥ ‘ ( ⊥ ‘ { 𝐵 } ) ) ↔ if ( 𝐴 ∈ ℋ , 𝐴 , 0_ℎ ) = ( ( ( if ( 𝐴 ∈ ℋ , 𝐴 , 0_ℎ ) ·_ih 𝐵 ) / ( 𝐵 ·_ih 𝐵 ) ) ·_ℎ 𝐵 ) ) ) ↔ ( if ( 𝐵 ∈ ℋ , 𝐵 , 0_ℎ ) ≠ 0_ℎ → ( if ( 𝐴 ∈ ℋ , 𝐴 , 0_ℎ ) ∈ ( ⊥ ‘ ( ⊥ ‘ { if ( 𝐵 ∈ ℋ , 𝐵 , 0_ℎ ) } ) ) ↔ if ( 𝐴 ∈ ℋ , 𝐴 , 0_ℎ ) = ( ( ( if ( 𝐴 ∈ ℋ , 𝐴 , 0_ℎ ) ·_ih if ( 𝐵 ∈ ℋ , 𝐵 , 0_ℎ ) ) / ( if ( 𝐵 ∈ ℋ , 𝐵 , 0_ℎ ) ·_ih if ( 𝐵 ∈ ℋ , 𝐵 , 0_ℎ ) ) ) ·_ℎ if ( 𝐵 ∈ ℋ , 𝐵 , 0_ℎ ) ) ) ) ) )
27		ifhvhv0	⊢ if ( 𝐴 ∈ ℋ , 𝐴 , 0_ℎ ) ∈ ℋ
28		ifhvhv0	⊢ if ( 𝐵 ∈ ℋ , 𝐵 , 0_ℎ ) ∈ ℋ
29	27 28	h1de2bi	⊢ ( if ( 𝐵 ∈ ℋ , 𝐵 , 0_ℎ ) ≠ 0_ℎ → ( if ( 𝐴 ∈ ℋ , 𝐴 , 0_ℎ ) ∈ ( ⊥ ‘ ( ⊥ ‘ { if ( 𝐵 ∈ ℋ , 𝐵 , 0_ℎ ) } ) ) ↔ if ( 𝐴 ∈ ℋ , 𝐴 , 0_ℎ ) = ( ( ( if ( 𝐴 ∈ ℋ , 𝐴 , 0_ℎ ) ·_ih if ( 𝐵 ∈ ℋ , 𝐵 , 0_ℎ ) ) / ( if ( 𝐵 ∈ ℋ , 𝐵 , 0_ℎ ) ·_ih if ( 𝐵 ∈ ℋ , 𝐵 , 0_ℎ ) ) ) ·_ℎ if ( 𝐵 ∈ ℋ , 𝐵 , 0_ℎ ) ) ) )
30	11 26 29	dedth2h	⊢ ( ( 𝐴 ∈ ℋ ∧ 𝐵 ∈ ℋ ) → ( 𝐵 ≠ 0_ℎ → ( 𝐴 ∈ ( ⊥ ‘ ( ⊥ ‘ { 𝐵 } ) ) ↔ 𝐴 = ( ( ( 𝐴 ·_ih 𝐵 ) / ( 𝐵 ·_ih 𝐵 ) ) ·_ℎ 𝐵 ) ) ) )
31	30	3impia	⊢ ( ( 𝐴 ∈ ℋ ∧ 𝐵 ∈ ℋ ∧ 𝐵 ≠ 0_ℎ ) → ( 𝐴 ∈ ( ⊥ ‘ ( ⊥ ‘ { 𝐵 } ) ) ↔ 𝐴 = ( ( ( 𝐴 ·_ih 𝐵 ) / ( 𝐵 ·_ih 𝐵 ) ) ·_ℎ 𝐵 ) ) )
32	3 31	bitrd	⊢ ( ( 𝐴 ∈ ℋ ∧ 𝐵 ∈ ℋ ∧ 𝐵 ≠ 0_ℎ ) → ( 𝐴 ∈ ( span ‘ { 𝐵 } ) ↔ 𝐴 = ( ( ( 𝐴 ·_ih 𝐵 ) / ( 𝐵 ·_ih 𝐵 ) ) ·_ℎ 𝐵 ) ) )

Metamath Proof Explorer

Theorem elspansn2

Proof