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 syl6eq 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