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

Proof

Step Hyp Ref Expression
1 h1de2.1 ⊢A∈ℋ
2 h1de2.2 ⊢B∈ℋ
3 his6 ⊢B∈ℋ→B⋅ihB=0↔B=0ℎ
4 2 3 ax-mp ⊢B⋅ihB=0↔B=0ℎ
5 4 necon3bii ⊢B⋅ihB≠0↔B≠0ℎ
6 1 2 h1de2i ⊢A∈⊥⁡⊥⁡B→B⋅ihB⋅ℎA=A⋅ihB⋅ℎB
7 6 adantl ⊢B⋅ihB≠0∧A∈⊥⁡⊥⁡B→B⋅ihB⋅ℎA=A⋅ihB⋅ℎB
8 7 oveq2d ⊢B⋅ihB≠0∧A∈⊥⁡⊥⁡B→1B⋅ihB⋅ℎB⋅ihB⋅ℎA=1B⋅ihB⋅ℎA⋅ihB⋅ℎB
9 2 2 hicli ⊢B⋅ihB∈ℂ
10 9 recclzi ⊢B⋅ihB≠0→1B⋅ihB∈ℂ
11 ax-hvmulass ⊢1B⋅ihB∈ℂ∧B⋅ihB∈ℂ∧A∈ℋ→1B⋅ihB⁢B⋅ihB⋅ℎA=1B⋅ihB⋅ℎB⋅ihB⋅ℎA
12 9 1 11 mp3an23 ⊢1B⋅ihB∈ℂ→1B⋅ihB⁢B⋅ihB⋅ℎA=1B⋅ihB⋅ℎB⋅ihB⋅ℎA
13 10 12 syl ⊢B⋅ihB≠0→1B⋅ihB⁢B⋅ihB⋅ℎA=1B⋅ihB⋅ℎB⋅ihB⋅ℎA
14 ax-1cn ⊢1∈ℂ
15 14 9 divcan1zi ⊢B⋅ihB≠0→1B⋅ihB⁢B⋅ihB=1
16 15 oveq1d ⊢B⋅ihB≠0→1B⋅ihB⁢B⋅ihB⋅ℎA=1⋅ℎA
17 13 16 eqtr3d ⊢B⋅ihB≠0→1B⋅ihB⋅ℎB⋅ihB⋅ℎA=1⋅ℎA
18 ax-hvmulid ⊢A∈ℋ→1⋅ℎA=A
19 1 18 ax-mp ⊢1⋅ℎA=A
20 17 19 eqtrdi ⊢B⋅ihB≠0→1B⋅ihB⋅ℎB⋅ihB⋅ℎA=A
21 20 adantr ⊢B⋅ihB≠0∧A∈⊥⁡⊥⁡B→1B⋅ihB⋅ℎB⋅ihB⋅ℎA=A
22 8 21 eqtr3d ⊢B⋅ihB≠0∧A∈⊥⁡⊥⁡B→1B⋅ihB⋅ℎA⋅ihB⋅ℎB=A
23 1 2 hicli ⊢A⋅ihB∈ℂ
24 ax-hvmulass ⊢1B⋅ihB∈ℂ∧A⋅ihB∈ℂ∧B∈ℋ→1B⋅ihB⁢A⋅ihB⋅ℎB=1B⋅ihB⋅ℎA⋅ihB⋅ℎB
25 23 2 24 mp3an23 ⊢1B⋅ihB∈ℂ→1B⋅ihB⁢A⋅ihB⋅ℎB=1B⋅ihB⋅ℎA⋅ihB⋅ℎB
26 10 25 syl ⊢B⋅ihB≠0→1B⋅ihB⁢A⋅ihB⋅ℎB=1B⋅ihB⋅ℎA⋅ihB⋅ℎB
27 mulcom ⊢1B⋅ihB∈ℂ∧A⋅ihB∈ℂ→1B⋅ihB⁢A⋅ihB=A⋅ihB⁢1B⋅ihB
28 10 23 27 sylancl ⊢B⋅ihB≠0→1B⋅ihB⁢A⋅ihB=A⋅ihB⁢1B⋅ihB
29 23 9 divreczi ⊢B⋅ihB≠0→A⋅ihBB⋅ihB=A⋅ihB⁢1B⋅ihB
30 28 29 eqtr4d ⊢B⋅ihB≠0→1B⋅ihB⁢A⋅ihB=A⋅ihBB⋅ihB
31 30 oveq1d ⊢B⋅ihB≠0→1B⋅ihB⁢A⋅ihB⋅ℎB=A⋅ihBB⋅ihB⋅ℎB
32 26 31 eqtr3d ⊢B⋅ihB≠0→1B⋅ihB⋅ℎA⋅ihB⋅ℎB=A⋅ihBB⋅ihB⋅ℎB
33 32 adantr ⊢B⋅ihB≠0∧A∈⊥⁡⊥⁡B→1B⋅ihB⋅ℎA⋅ihB⋅ℎB=A⋅ihBB⋅ihB⋅ℎB
34 22 33 eqtr3d ⊢B⋅ihB≠0∧A∈⊥⁡⊥⁡B→A=A⋅ihBB⋅ihB⋅ℎB
35 34 ex ⊢B⋅ihB≠0→A∈⊥⁡⊥⁡B→A=A⋅ihBB⋅ihB⋅ℎB
36 23 9 divclzi ⊢B⋅ihB≠0→A⋅ihBB⋅ihB∈ℂ
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⋅ihBB⋅ihB∈ℂ∧B∈⊥⁡⊥⁡B→A⋅ihBB⋅ihB⋅ℎB∈⊥⁡⊥⁡B
47 43 45 46 mp3an13 ⊢A⋅ihBB⋅ihB∈ℂ→A⋅ihBB⋅ihB⋅ℎB∈⊥⁡⊥⁡B
48 36 47 syl ⊢B⋅ihB≠0→A⋅ihBB⋅ihB⋅ℎB∈⊥⁡⊥⁡B
49 eleq1 ⊢A=A⋅ihBB⋅ihB⋅ℎB→A∈⊥⁡⊥⁡B↔A⋅ihBB⋅ihB⋅ℎB∈⊥⁡⊥⁡B
50 48 49 syl5ibrcom ⊢B⋅ihB≠0→A=A⋅ihBB⋅ihB⋅ℎB→A∈⊥⁡⊥⁡B
51 35 50 impbid ⊢B⋅ihB≠0→A∈⊥⁡⊥⁡B↔A=A⋅ihBB⋅ihB⋅ℎB
52 5 51 sylbir ⊢B≠0ℎ→A∈⊥⁡⊥⁡B↔A=A⋅ihBB⋅ihB⋅ℎB