Metamath Proof Explorer

Theorem pjpythi

Description: Pythagorean theorem for projections. (Contributed by NM, 27-Oct-1999) (New usage is discouraged.)

Ref Expression
Hypotheses pjnorm.1 ⊢H∈Cℋ
pjnorm.2 ⊢A∈ℋ
Assertion pjpythi ⊢normℎ⁡A2=normℎ⁡projℎ⁡H⁡A2+normℎ⁡projℎ⁡⊥⁡H⁡A2

Proof

Step Hyp Ref Expression
1 pjnorm.1 ⊢H∈Cℋ
2 pjnorm.2 ⊢A∈ℋ
3 1 2 pjpji ⊢A=projℎ⁡H⁡A+ℎprojℎ⁡⊥⁡H⁡A
4 3 fveq2i ⊢normℎ⁡A=normℎ⁡projℎ⁡H⁡A+ℎprojℎ⁡⊥⁡H⁡A
5 4 oveq1i ⊢normℎ⁡A2=normℎ⁡projℎ⁡H⁡A+ℎprojℎ⁡⊥⁡H⁡A2
6 1 chshii ⊢H∈Sℋ
7 shococss ⊢H∈Sℋ→H⊆⊥⁡⊥⁡H
8 1 choccli ⊢⊥⁡H∈Cℋ
9 1 8 2 pjopythi ⊢H⊆⊥⁡⊥⁡H→normℎ⁡projℎ⁡H⁡A+ℎprojℎ⁡⊥⁡H⁡A2=normℎ⁡projℎ⁡H⁡A2+normℎ⁡projℎ⁡⊥⁡H⁡A2
10 6 7 9 mp2b ⊢normℎ⁡projℎ⁡H⁡A+ℎprojℎ⁡⊥⁡H⁡A2=normℎ⁡projℎ⁡H⁡A2+normℎ⁡projℎ⁡⊥⁡H⁡A2
11 5 10 eqtri ⊢normℎ⁡A2=normℎ⁡projℎ⁡H⁡A2+normℎ⁡projℎ⁡⊥⁡H⁡A2