Metamath Proof Explorer


Theorem h1datomi

Description: A 1-dimensional subspace is an atom. (Contributed by NM, 20-Jul-2001) (New usage is discouraged.)

Ref Expression
Hypotheses h1datom.1 A C
h1datom.2 B
Assertion h1datomi A B A = B A = 0

Proof

Step Hyp Ref Expression
1 h1datom.1 A C
2 h1datom.2 B
3 1 chne0i A 0 x A x 0
4 ssel A B x A x B
5 2 h1de2ci x B y x = y B
6 oveq1 y = 0 y B = 0 B
7 ax-hvmul0 B 0 B = 0
8 2 7 ax-mp 0 B = 0
9 6 8 eqtrdi y = 0 y B = 0
10 eqeq1 x = y B x = 0 y B = 0
11 9 10 syl5ibr x = y B y = 0 x = 0
12 11 necon3d x = y B x 0 y 0
13 12 adantl y x = y B x 0 y 0
14 reccl y y 0 1 y
15 1 chshii A S
16 shmulcl A S 1 y x A 1 y x A
17 15 16 mp3an1 1 y x A 1 y x A
18 17 ex 1 y x A 1 y x A
19 14 18 syl y y 0 x A 1 y x A
20 19 adantr y y 0 x = y B x A 1 y x A
21 oveq2 x = y B 1 y x = 1 y y B
22 simpl y y 0 y
23 ax-hvmulass 1 y y B 1 y y B = 1 y y B
24 2 23 mp3an3 1 y y 1 y y B = 1 y y B
25 14 22 24 syl2anc y y 0 1 y y B = 1 y y B
26 recid2 y y 0 1 y y = 1
27 26 oveq1d y y 0 1 y y B = 1 B
28 25 27 eqtr3d y y 0 1 y y B = 1 B
29 ax-hvmulid B 1 B = B
30 2 29 ax-mp 1 B = B
31 28 30 eqtrdi y y 0 1 y y B = B
32 21 31 sylan9eqr y y 0 x = y B 1 y x = B
33 32 eleq1d y y 0 x = y B 1 y x A B A
34 20 33 sylibd y y 0 x = y B x A B A
35 34 exp31 y y 0 x = y B x A B A
36 35 com23 y x = y B y 0 x A B A
37 36 imp y x = y B y 0 x A B A
38 13 37 syld y x = y B x 0 x A B A
39 38 com3r x A y x = y B x 0 B A
40 39 expd x A y x = y B x 0 B A
41 40 rexlimdv x A y x = y B x 0 B A
42 5 41 syl5bi x A x B x 0 B A
43 4 42 sylcom A B x A x 0 B A
44 43 rexlimdv A B x A x 0 B A
45 3 44 syl5bi A B A 0 B A
46 snssi B A B A
47 snssi B B
48 2 47 ax-mp B
49 1 chssii A
50 48 49 occon2i B A B A
51 46 50 syl B A B A
52 1 ococi A = A
53 51 52 sseqtrdi B A B A
54 45 53 syl6 A B A 0 B A
55 54 anc2li A B A 0 A B B A
56 eqss A = B A B B A
57 55 56 syl6ibr A B A 0 A = B
58 57 necon1d A B A B A = 0
59 neor A = B A = 0 A B A = 0
60 58 59 sylibr A B A = B A = 0