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⋅ihB⋅ℎA=A⋅ihB⋅ℎB

Proof

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