Metamath Proof Explorer


Syntax definition cdjh

Description: Extend class notation with subspace join for DVecH vector space.

Ref Expression
Assertion cdjh class joinH