Metamath Proof Explorer


Theorem ch1dle

Description: A 1-dimensional subspace is less than or equal to any member of CH containing its generating vector. (Contributed by NM, 30-May-2004) (New usage is discouraged.)

Ref Expression
Assertion ch1dle A C B A B A

Proof

Step Hyp Ref Expression
1 chsh A C A S
2 sh1dle A S B A B A
3 1 2 sylan A C B A B A