Metamath Proof Explorer


Theorem ch0le

Description: The zero subspace is the smallest member of CH . (Contributed by NM, 14-Aug-2002) (New usage is discouraged.)

Ref Expression
Assertion ch0le A C 0 A

Proof

Step Hyp Ref Expression
1 chsh A C A S
2 sh0le A S 0 A
3 1 2 syl A C 0 A