Metamath Proof Explorer

Theorem h1de2i

Description: Membership in 1-dimensional subspace. All members are collinear with the generating vector. (Contributed by NM, 17-Jul-2001) (New usage is discouraged.)

Ref Expression
Hypotheses h1de2.1 ⊢ A ∈ ℋ
h1de2.2 ⊢ B ∈ ℋ
Assertion h1de2i ⊢ A ∈ ⊥ ⁡ ⊥ ⁡ B → B ⋅ ih B ⋅ ℎ A = A ⋅ ih B ⋅ ℎ B

Proof

Step Hyp Ref Expression
1 h1de2.1 ⊢ A ∈ ℋ
2 h1de2.2 ⊢ B ∈ ℋ
3 2 2 hicli ⊢ B ⋅ ih B ∈ ℂ
4 3 1 hvmulcli ⊢ B ⋅ ih B ⋅ ℎ A ∈ ℋ
5 1 2 hicli ⊢ A ⋅ ih B ∈ ℂ
6 5 2 hvmulcli ⊢ A ⋅ ih B ⋅ ℎ B ∈ ℋ
7 his2sub ⊢ B ⋅ ih B ⋅ ℎ A ∈ ℋ ∧ A ⋅ ih B ⋅ ℎ B ∈ ℋ ∧ A ∈ ℋ → B ⋅ ih B ⋅ ℎ A - ℎ A ⋅ ih B ⋅ ℎ B ⋅ ih A = B ⋅ ih B ⋅ ℎ A ⋅ ih A − A ⋅ ih B ⋅ ℎ B ⋅ ih A
8 4 6 1 7 mp3an ⊢ B ⋅ ih B ⋅ ℎ A - ℎ A ⋅ ih B ⋅ ℎ B ⋅ ih A = B ⋅ ih B ⋅ ℎ A ⋅ ih A − A ⋅ ih B ⋅ ℎ B ⋅ ih A
9 ax-his3 ⊢ B ⋅ ih B ∈ ℂ ∧ A ∈ ℋ ∧ A ∈ ℋ → B ⋅ ih B ⋅ ℎ A ⋅ ih A = B ⋅ ih B ⁢ A ⋅ ih A
10 3 1 1 9 mp3an ⊢ B ⋅ ih B ⋅ ℎ A ⋅ ih A = B ⋅ ih B ⁢ A ⋅ ih A
11 1 1 hicli ⊢ A ⋅ ih A ∈ ℂ
12 3 11 mulcomi ⊢ B ⋅ ih B ⁢ A ⋅ ih A = A ⋅ ih A ⁢ B ⋅ ih B
13 10 12 eqtri ⊢ B ⋅ ih B ⋅ ℎ A ⋅ ih A = A ⋅ ih A ⁢ B ⋅ ih B
14 ax-his3 ⊢ A ⋅ ih B ∈ ℂ ∧ B ∈ ℋ ∧ A ∈ ℋ → A ⋅ ih B ⋅ ℎ B ⋅ ih A = A ⋅ ih B ⁢ B ⋅ ih A
15 5 2 1 14 mp3an ⊢ A ⋅ ih B ⋅ ℎ B ⋅ ih A = A ⋅ ih B ⁢ B ⋅ ih A
16 13 15 oveq12i ⊢ B ⋅ ih B ⋅ ℎ A ⋅ ih A − A ⋅ ih B ⋅ ℎ B ⋅ ih A = A ⋅ ih A ⁢ B ⋅ ih B − A ⋅ ih B ⁢ B ⋅ ih A
17 8 16 eqtr2i ⊢ A ⋅ ih A ⁢ B ⋅ ih B − A ⋅ ih B ⁢ B ⋅ ih A = B ⋅ ih B ⋅ ℎ A - ℎ A ⋅ ih B ⋅ ℎ B ⋅ ih A
18 his2sub ⊢ B ⋅ ih B ⋅ ℎ A ∈ ℋ ∧ A ⋅ ih B ⋅ ℎ B ∈ ℋ ∧ B ∈ ℋ → B ⋅ ih B ⋅ ℎ A - ℎ A ⋅ ih B ⋅ ℎ B ⋅ ih B = B ⋅ ih B ⋅ ℎ A ⋅ ih B − A ⋅ ih B ⋅ ℎ B ⋅ ih B
19 4 6 2 18 mp3an ⊢ B ⋅ ih B ⋅ ℎ A - ℎ A ⋅ ih B ⋅ ℎ B ⋅ ih B = B ⋅ ih B ⋅ ℎ A ⋅ ih B − A ⋅ ih B ⋅ ℎ B ⋅ ih B
20 3 5 mulcomi ⊢ B ⋅ ih B ⁢ A ⋅ ih B = A ⋅ ih B ⁢ B ⋅ ih B
21 ax-his3 ⊢ B ⋅ ih B ∈ ℂ ∧ A ∈ ℋ ∧ B ∈ ℋ → B ⋅ ih B ⋅ ℎ A ⋅ ih B = B ⋅ ih B ⁢ A ⋅ ih B
22 3 1 2 21 mp3an ⊢ B ⋅ ih B ⋅ ℎ A ⋅ ih B = B ⋅ ih B ⁢ A ⋅ ih B
23 ax-his3 ⊢ A ⋅ ih B ∈ ℂ ∧ B ∈ ℋ ∧ B ∈ ℋ → A ⋅ ih B ⋅ ℎ B ⋅ ih B = A ⋅ ih B ⁢ B ⋅ ih B
24 5 2 2 23 mp3an ⊢ A ⋅ ih B ⋅ ℎ B ⋅ ih B = A ⋅ ih B ⁢ B ⋅ ih B
25 20 22 24 3eqtr4i ⊢ B ⋅ ih B ⋅ ℎ A ⋅ ih B = A ⋅ ih B ⋅ ℎ B ⋅ ih B
26 4 2 hicli ⊢ B ⋅ ih B ⋅ ℎ A ⋅ ih B ∈ ℂ
27 6 2 hicli ⊢ A ⋅ ih B ⋅ ℎ B ⋅ ih B ∈ ℂ
28 26 27 subeq0i ⊢ B ⋅ ih B ⋅ ℎ A ⋅ ih B − A ⋅ ih B ⋅ ℎ B ⋅ ih B = 0 ↔ B ⋅ ih B ⋅ ℎ A ⋅ ih B = A ⋅ ih B ⋅ ℎ B ⋅ ih B
29 25 28 mpbir ⊢ B ⋅ ih B ⋅ ℎ A ⋅ ih B − A ⋅ ih B ⋅ ℎ B ⋅ ih B = 0
30 19 29 eqtri ⊢ B ⋅ ih B ⋅ ℎ A - ℎ A ⋅ ih B ⋅ ℎ B ⋅ ih B = 0
31 2 h1dei ⊢ A ∈ ⊥ ⁡ ⊥ ⁡ B ↔ A ∈ ℋ ∧ ∀ x ∈ ℋ B ⋅ ih x = 0 → A ⋅ ih x = 0
32 1 31 mpbiran ⊢ A ∈ ⊥ ⁡ ⊥ ⁡ B ↔ ∀ x ∈ ℋ B ⋅ ih x = 0 → A ⋅ ih x = 0
33 4 6 hvsubcli ⊢ B ⋅ ih B ⋅ ℎ A - ℎ A ⋅ ih B ⋅ ℎ B ∈ ℋ
34 oveq2 ⊢ x = B ⋅ ih B ⋅ ℎ A - ℎ A ⋅ ih B ⋅ ℎ B → B ⋅ ih x = B ⋅ ih B ⋅ ih B ⋅ ℎ A - ℎ A ⋅ ih B ⋅ ℎ B
35 34 eqeq1d ⊢ x = B ⋅ ih B ⋅ ℎ A - ℎ A ⋅ ih B ⋅ ℎ B → B ⋅ ih x = 0 ↔ B ⋅ ih B ⋅ ih B ⋅ ℎ A - ℎ A ⋅ ih B ⋅ ℎ B = 0
36 oveq2 ⊢ x = B ⋅ ih B ⋅ ℎ A - ℎ A ⋅ ih B ⋅ ℎ B → A ⋅ ih x = A ⋅ ih B ⋅ ih B ⋅ ℎ A - ℎ A ⋅ ih B ⋅ ℎ B
37 36 eqeq1d ⊢ x = B ⋅ ih B ⋅ ℎ A - ℎ A ⋅ ih B ⋅ ℎ B → A ⋅ ih x = 0 ↔ A ⋅ ih B ⋅ ih B ⋅ ℎ A - ℎ A ⋅ ih B ⋅ ℎ B = 0
38 35 37 imbi12d ⊢ x = B ⋅ ih B ⋅ ℎ A - ℎ A ⋅ ih B ⋅ ℎ B → B ⋅ ih x = 0 → A ⋅ ih x = 0 ↔ B ⋅ ih B ⋅ ih B ⋅ ℎ A - ℎ A ⋅ ih B ⋅ ℎ B = 0 → A ⋅ ih B ⋅ ih B ⋅ ℎ A - ℎ A ⋅ ih B ⋅ ℎ B = 0
39 38 rspcv ⊢ B ⋅ ih B ⋅ ℎ A - ℎ A ⋅ ih B ⋅ ℎ B ∈ ℋ → ∀ x ∈ ℋ B ⋅ ih x = 0 → A ⋅ ih x = 0 → B ⋅ ih B ⋅ ih B ⋅ ℎ A - ℎ A ⋅ ih B ⋅ ℎ B = 0 → A ⋅ ih B ⋅ ih B ⋅ ℎ A - ℎ A ⋅ ih B ⋅ ℎ B = 0
40 33 39 ax-mp ⊢ ∀ x ∈ ℋ B ⋅ ih x = 0 → A ⋅ ih x = 0 → B ⋅ ih B ⋅ ih B ⋅ ℎ A - ℎ A ⋅ ih B ⋅ ℎ B = 0 → A ⋅ ih B ⋅ ih B ⋅ ℎ A - ℎ A ⋅ ih B ⋅ ℎ B = 0
41 32 40 sylbi ⊢ A ∈ ⊥ ⁡ ⊥ ⁡ B → B ⋅ ih B ⋅ ih B ⋅ ℎ A - ℎ A ⋅ ih B ⋅ ℎ B = 0 → A ⋅ ih B ⋅ ih B ⋅ ℎ A - ℎ A ⋅ ih B ⋅ ℎ B = 0
42 orthcom ⊢ B ⋅ ih B ⋅ ℎ A - ℎ A ⋅ ih B ⋅ ℎ B ∈ ℋ ∧ B ∈ ℋ → B ⋅ ih B ⋅ ℎ A - ℎ A ⋅ ih B ⋅ ℎ B ⋅ ih B = 0 ↔ B ⋅ ih B ⋅ ih B ⋅ ℎ A - ℎ A ⋅ ih B ⋅ ℎ B = 0
43 33 2 42 mp2an ⊢ B ⋅ ih B ⋅ ℎ A - ℎ A ⋅ ih B ⋅ ℎ B ⋅ ih B = 0 ↔ B ⋅ ih B ⋅ ih B ⋅ ℎ A - ℎ A ⋅ ih B ⋅ ℎ B = 0
44 orthcom ⊢ B ⋅ ih B ⋅ ℎ A - ℎ A ⋅ ih B ⋅ ℎ B ∈ ℋ ∧ A ∈ ℋ → B ⋅ ih B ⋅ ℎ A - ℎ A ⋅ ih B ⋅ ℎ B ⋅ ih A = 0 ↔ A ⋅ ih B ⋅ ih B ⋅ ℎ A - ℎ A ⋅ ih B ⋅ ℎ B = 0
45 33 1 44 mp2an ⊢ B ⋅ ih B ⋅ ℎ A - ℎ A ⋅ ih B ⋅ ℎ B ⋅ ih A = 0 ↔ A ⋅ ih B ⋅ ih B ⋅ ℎ A - ℎ A ⋅ ih B ⋅ ℎ B = 0
46 41 43 45 3imtr4g ⊢ A ∈ ⊥ ⁡ ⊥ ⁡ B → B ⋅ ih B ⋅ ℎ A - ℎ A ⋅ ih B ⋅ ℎ B ⋅ ih B = 0 → B ⋅ ih B ⋅ ℎ A - ℎ A ⋅ ih B ⋅ ℎ B ⋅ ih A = 0
47 30 46 mpi ⊢ A ∈ ⊥ ⁡ ⊥ ⁡ B → B ⋅ ih B ⋅ ℎ A - ℎ A ⋅ ih B ⋅ ℎ B ⋅ ih A = 0
48 17 47 syl5eq ⊢ A ∈ ⊥ ⁡ ⊥ ⁡ B → A ⋅ ih A ⁢ B ⋅ ih B − A ⋅ ih B ⁢ B ⋅ ih A = 0
49 11 3 mulcli ⊢ A ⋅ ih A ⁢ B ⋅ ih B ∈ ℂ
50 2 1 hicli ⊢ B ⋅ ih A ∈ ℂ
51 5 50 mulcli ⊢ A ⋅ ih B ⁢ B ⋅ ih A ∈ ℂ
52 49 51 subeq0i ⊢ A ⋅ ih A ⁢ B ⋅ ih B − A ⋅ ih B ⁢ B ⋅ ih A = 0 ↔ A ⋅ ih A ⁢ B ⋅ ih B = A ⋅ ih B ⁢ B ⋅ ih A
53 48 52 sylib ⊢ A ∈ ⊥ ⁡ ⊥ ⁡ B → A ⋅ ih A ⁢ B ⋅ ih B = A ⋅ ih B ⁢ B ⋅ ih A
54 53 eqcomd ⊢ A ∈ ⊥ ⁡ ⊥ ⁡ B → A ⋅ ih B ⁢ B ⋅ ih A = A ⋅ ih A ⁢ B ⋅ ih B
55 1 2 bcseqi ⊢ A ⋅ ih B ⁢ B ⋅ ih A = A ⋅ ih A ⁢ B ⋅ ih B ↔ B ⋅ ih B ⋅ ℎ A = A ⋅ ih B ⋅ ℎ B
56 54 55 sylib ⊢ A ∈ ⊥ ⁡ ⊥ ⁡ B → B ⋅ ih B ⋅ ℎ A = A ⋅ ih B ⋅ ℎ B