Metamath Proof Explorer


Theorem h1datom

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

Ref Expression
Assertion h1datom A C B A B A = B A = 0

Proof

Step Hyp Ref Expression
1 sseq1 A = if A C A 0 A B if A C A 0 B
2 eqeq1 A = if A C A 0 A = B if A C A 0 = B
3 eqeq1 A = if A C A 0 A = 0 if A C A 0 = 0
4 2 3 orbi12d A = if A C A 0 A = B A = 0 if A C A 0 = B if A C A 0 = 0
5 1 4 imbi12d A = if A C A 0 A B A = B A = 0 if A C A 0 B if A C A 0 = B if A C A 0 = 0
6 sneq B = if B B 0 B = if B B 0
7 6 fveq2d B = if B B 0 B = if B B 0
8 7 fveq2d B = if B B 0 B = if B B 0
9 8 sseq2d B = if B B 0 if A C A 0 B if A C A 0 if B B 0
10 8 eqeq2d B = if B B 0 if A C A 0 = B if A C A 0 = if B B 0
11 10 orbi1d B = if B B 0 if A C A 0 = B if A C A 0 = 0 if A C A 0 = if B B 0 if A C A 0 = 0
12 9 11 imbi12d B = if B B 0 if A C A 0 B if A C A 0 = B if A C A 0 = 0 if A C A 0 if B B 0 if A C A 0 = if B B 0 if A C A 0 = 0
13 h0elch 0 C
14 13 elimel if A C A 0 C
15 ifhvhv0 if B B 0
16 14 15 h1datomi if A C A 0 if B B 0 if A C A 0 = if B B 0 if A C A 0 = 0
17 5 12 16 dedth2h A C B A B A = B A = 0