pjopythi

Description: Pythagorean theorem for projections on orthogonal subspaces. (Contributed by NM, 1-Nov-1999) (New usage is discouraged.)

	Ref	Expression
Hypotheses	pjoi0.1	$⊢ G \in C_{ℋ}$
	pjoi0.2	$⊢ H \in C_{ℋ}$
	pjoi0.3	$⊢ A \in ℋ$
Assertion	pjopythi	$⊢ G \subseteq ⊥ (H) \to {{norm}_{ℎ} ({proj}_{ℎ} (G) (A) +_{ℎ} {proj}_{ℎ} (H) (A))}^{2} = {{norm}_{ℎ} ({proj}_{ℎ} (G) (A))}^{2} + {{norm}_{ℎ} ({proj}_{ℎ} (H) (A))}^{2}$

Step	Hyp	Ref	Expression
1		pjoi0.1	$⊢ G \in C_{ℋ}$
2		pjoi0.2	$⊢ H \in C_{ℋ}$
3		pjoi0.3	$⊢ A \in ℋ$
4	1 2 3	pjoi0i	$⊢ G \subseteq ⊥ (H) \to {proj}_{ℎ} (G) (A) \cdot_{ih} {proj}_{ℎ} (H) (A) = 0$
5	1 3	pjhclii	$⊢ {proj}_{ℎ} (G) (A) \in ℋ$
6	2 3	pjhclii	$⊢ {proj}_{ℎ} (H) (A) \in ℋ$
7	5 6	normpythi	$⊢ {proj}_{ℎ} (G) (A) \cdot_{ih} {proj}_{ℎ} (H) (A) = 0 \to {{norm}_{ℎ} ({proj}_{ℎ} (G) (A) +_{ℎ} {proj}_{ℎ} (H) (A))}^{2} = {{norm}_{ℎ} ({proj}_{ℎ} (G) (A))}^{2} + {{norm}_{ℎ} ({proj}_{ℎ} (H) (A))}^{2}$
8	4 7	syl	$⊢ G \subseteq ⊥ (H) \to {{norm}_{ℎ} ({proj}_{ℎ} (G) (A) +_{ℎ} {proj}_{ℎ} (H) (A))}^{2} = {{norm}_{ℎ} ({proj}_{ℎ} (G) (A))}^{2} + {{norm}_{ℎ} ({proj}_{ℎ} (H) (A))}^{2}$

Metamath Proof Explorer