Metamath Proof Explorer

Theorem 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 ⊢ A ∈ ℋ ∧ B ∈ ℋ ∧ B ≠ 0 ℎ → A ∈ span ⁡ B ↔ A = A ⋅ ih B B ⋅ ih B ⋅ ℎ B

Proof

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