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⋅ihBB⋅ihB⋅ℎ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=ifA∈ℋA0ℎ→A∈⊥⁡⊥⁡B↔ifA∈ℋA0ℎ∈⊥⁡⊥⁡B
5 id ⊢A=ifA∈ℋA0ℎ→A=ifA∈ℋA0ℎ
6 oveq1 ⊢A=ifA∈ℋA0ℎ→A⋅ihB=ifA∈ℋA0ℎ⋅ihB
7 6 oveq1d ⊢A=ifA∈ℋA0ℎ→A⋅ihBB⋅ihB=ifA∈ℋA0ℎ⋅ihBB⋅ihB
8 7 oveq1d ⊢A=ifA∈ℋA0ℎ→A⋅ihBB⋅ihB⋅ℎB=ifA∈ℋA0ℎ⋅ihBB⋅ihB⋅ℎB
9 5 8 eqeq12d ⊢A=ifA∈ℋA0ℎ→A=A⋅ihBB⋅ihB⋅ℎB↔ifA∈ℋA0ℎ=ifA∈ℋA0ℎ⋅ihBB⋅ihB⋅ℎB
10 4 9 bibi12d ⊢A=ifA∈ℋA0ℎ→A∈⊥⁡⊥⁡B↔A=A⋅ihBB⋅ihB⋅ℎB↔ifA∈ℋA0ℎ∈⊥⁡⊥⁡B↔ifA∈ℋA0ℎ=ifA∈ℋA0ℎ⋅ihBB⋅ihB⋅ℎB
11 10 imbi2d ⊢A=ifA∈ℋA0ℎ→B≠0ℎ→A∈⊥⁡⊥⁡B↔A=A⋅ihBB⋅ihB⋅ℎB↔B≠0ℎ→ifA∈ℋA0ℎ∈⊥⁡⊥⁡B↔ifA∈ℋA0ℎ=ifA∈ℋA0ℎ⋅ihBB⋅ihB⋅ℎB
12 neeq1 ⊢B=ifB∈ℋB0ℎ→B≠0ℎ↔ifB∈ℋB0ℎ≠0ℎ
13 sneq ⊢B=ifB∈ℋB0ℎ→B=ifB∈ℋB0ℎ
14 13 fveq2d ⊢B=ifB∈ℋB0ℎ→⊥⁡B=⊥⁡ifB∈ℋB0ℎ
15 14 fveq2d ⊢B=ifB∈ℋB0ℎ→⊥⁡⊥⁡B=⊥⁡⊥⁡ifB∈ℋB0ℎ
16 15 eleq2d ⊢B=ifB∈ℋB0ℎ→ifA∈ℋA0ℎ∈⊥⁡⊥⁡B↔ifA∈ℋA0ℎ∈⊥⁡⊥⁡ifB∈ℋB0ℎ
17 oveq2 ⊢B=ifB∈ℋB0ℎ→ifA∈ℋA0ℎ⋅ihB=ifA∈ℋA0ℎ⋅ihifB∈ℋB0ℎ
18 oveq1 ⊢B=ifB∈ℋB0ℎ→B⋅ihB=ifB∈ℋB0ℎ⋅ihB
19 oveq2 ⊢B=ifB∈ℋB0ℎ→ifB∈ℋB0ℎ⋅ihB=ifB∈ℋB0ℎ⋅ihifB∈ℋB0ℎ
20 18 19 eqtrd ⊢B=ifB∈ℋB0ℎ→B⋅ihB=ifB∈ℋB0ℎ⋅ihifB∈ℋB0ℎ
21 17 20 oveq12d ⊢B=ifB∈ℋB0ℎ→ifA∈ℋA0ℎ⋅ihBB⋅ihB=ifA∈ℋA0ℎ⋅ihifB∈ℋB0ℎifB∈ℋB0ℎ⋅ihifB∈ℋB0ℎ
22 id ⊢B=ifB∈ℋB0ℎ→B=ifB∈ℋB0ℎ
23 21 22 oveq12d ⊢B=ifB∈ℋB0ℎ→ifA∈ℋA0ℎ⋅ihBB⋅ihB⋅ℎB=ifA∈ℋA0ℎ⋅ihifB∈ℋB0ℎifB∈ℋB0ℎ⋅ihifB∈ℋB0ℎ⋅ℎifB∈ℋB0ℎ
24 23 eqeq2d ⊢B=ifB∈ℋB0ℎ→ifA∈ℋA0ℎ=ifA∈ℋA0ℎ⋅ihBB⋅ihB⋅ℎB↔ifA∈ℋA0ℎ=ifA∈ℋA0ℎ⋅ihifB∈ℋB0ℎifB∈ℋB0ℎ⋅ihifB∈ℋB0ℎ⋅ℎifB∈ℋB0ℎ
25 16 24 bibi12d ⊢B=ifB∈ℋB0ℎ→ifA∈ℋA0ℎ∈⊥⁡⊥⁡B↔ifA∈ℋA0ℎ=ifA∈ℋA0ℎ⋅ihBB⋅ihB⋅ℎB↔ifA∈ℋA0ℎ∈⊥⁡⊥⁡ifB∈ℋB0ℎ↔ifA∈ℋA0ℎ=ifA∈ℋA0ℎ⋅ihifB∈ℋB0ℎifB∈ℋB0ℎ⋅ihifB∈ℋB0ℎ⋅ℎifB∈ℋB0ℎ
26 12 25 imbi12d ⊢B=ifB∈ℋB0ℎ→B≠0ℎ→ifA∈ℋA0ℎ∈⊥⁡⊥⁡B↔ifA∈ℋA0ℎ=ifA∈ℋA0ℎ⋅ihBB⋅ihB⋅ℎB↔ifB∈ℋB0ℎ≠0ℎ→ifA∈ℋA0ℎ∈⊥⁡⊥⁡ifB∈ℋB0ℎ↔ifA∈ℋA0ℎ=ifA∈ℋA0ℎ⋅ihifB∈ℋB0ℎifB∈ℋB0ℎ⋅ihifB∈ℋB0ℎ⋅ℎifB∈ℋB0ℎ
27 ifhvhv0 ⊢ifA∈ℋA0ℎ∈ℋ
28 ifhvhv0 ⊢ifB∈ℋB0ℎ∈ℋ
29 27 28 h1de2bi ⊢ifB∈ℋB0ℎ≠0ℎ→ifA∈ℋA0ℎ∈⊥⁡⊥⁡ifB∈ℋB0ℎ↔ifA∈ℋA0ℎ=ifA∈ℋA0ℎ⋅ihifB∈ℋB0ℎifB∈ℋB0ℎ⋅ihifB∈ℋB0ℎ⋅ℎifB∈ℋB0ℎ
30 11 26 29 dedth2h ⊢A∈ℋ∧B∈ℋ→B≠0ℎ→A∈⊥⁡⊥⁡B↔A=A⋅ihBB⋅ihB⋅ℎB
31 30 3impia ⊢A∈ℋ∧B∈ℋ∧B≠0ℎ→A∈⊥⁡⊥⁡B↔A=A⋅ihBB⋅ihB⋅ℎB
32 3 31 bitrd ⊢A∈ℋ∧B∈ℋ∧B≠0ℎ→A∈span⁡B↔A=A⋅ihBB⋅ihB⋅ℎB