This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem pjvi

Description: The value of a projection in terms of components. (Contributed by NM, 28-Nov-2000) (New usage is discouraged.)

		Ref	Expression
	Hypothesis	pjfn.1	$⊢ H \in C_{ℋ}$
	Assertion	pjvi	$⊢ (A \in H \land B \in ⊥ (H)) \to {proj}_{ℎ} (H) (A +_{ℎ} B) = A$

Step	Hyp	Ref	Expression
1		pjfn.1	$⊢ H \in C_{ℋ}$
2	1	pjcompi	$⊢ (A \in H \land B \in ⊥ (H)) \to {proj}_{ℎ} (H) (A +_{ℎ} B) = A$