Metamath Proof Explorer

Theorem 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 ⊢ A ∈ ℋ
h1de2.2 ⊢ B ∈ ℋ
Assertion h1de2bi ⊢ B ≠ 0 ℎ → A ∈ ⊥ ⁡ ⊥ ⁡ B ↔ A = A ⋅ ih B B ⋅ ih B ⋅ ℎ B

Proof

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