Metamath Proof Explorer


Theorem pjopyth

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

Ref Expression
Assertion pjopyth ( ( 𝐻C𝐺C𝐴 ∈ ℋ ) → ( 𝐻 ⊆ ( ⊥ ‘ 𝐺 ) → ( ( norm ‘ ( ( ( proj𝐻 ) ‘ 𝐴 ) + ( ( proj𝐺 ) ‘ 𝐴 ) ) ) ↑ 2 ) = ( ( ( norm ‘ ( ( proj𝐻 ) ‘ 𝐴 ) ) ↑ 2 ) + ( ( norm ‘ ( ( proj𝐺 ) ‘ 𝐴 ) ) ↑ 2 ) ) ) )

Proof

Step Hyp Ref Expression
1 sseq1 ( 𝐻 = if ( 𝐻C , 𝐻 , ℋ ) → ( 𝐻 ⊆ ( ⊥ ‘ 𝐺 ) ↔ if ( 𝐻C , 𝐻 , ℋ ) ⊆ ( ⊥ ‘ 𝐺 ) ) )
2 fveq2 ( 𝐻 = if ( 𝐻C , 𝐻 , ℋ ) → ( proj𝐻 ) = ( proj ‘ if ( 𝐻C , 𝐻 , ℋ ) ) )
3 2 fveq1d ( 𝐻 = if ( 𝐻C , 𝐻 , ℋ ) → ( ( proj𝐻 ) ‘ 𝐴 ) = ( ( proj ‘ if ( 𝐻C , 𝐻 , ℋ ) ) ‘ 𝐴 ) )
4 3 oveq1d ( 𝐻 = if ( 𝐻C , 𝐻 , ℋ ) → ( ( ( proj𝐻 ) ‘ 𝐴 ) + ( ( proj𝐺 ) ‘ 𝐴 ) ) = ( ( ( proj ‘ if ( 𝐻C , 𝐻 , ℋ ) ) ‘ 𝐴 ) + ( ( proj𝐺 ) ‘ 𝐴 ) ) )
5 4 fveq2d ( 𝐻 = if ( 𝐻C , 𝐻 , ℋ ) → ( norm ‘ ( ( ( proj𝐻 ) ‘ 𝐴 ) + ( ( proj𝐺 ) ‘ 𝐴 ) ) ) = ( norm ‘ ( ( ( proj ‘ if ( 𝐻C , 𝐻 , ℋ ) ) ‘ 𝐴 ) + ( ( proj𝐺 ) ‘ 𝐴 ) ) ) )
6 5 oveq1d ( 𝐻 = if ( 𝐻C , 𝐻 , ℋ ) → ( ( norm ‘ ( ( ( proj𝐻 ) ‘ 𝐴 ) + ( ( proj𝐺 ) ‘ 𝐴 ) ) ) ↑ 2 ) = ( ( norm ‘ ( ( ( proj ‘ if ( 𝐻C , 𝐻 , ℋ ) ) ‘ 𝐴 ) + ( ( proj𝐺 ) ‘ 𝐴 ) ) ) ↑ 2 ) )
7 3 fveq2d ( 𝐻 = if ( 𝐻C , 𝐻 , ℋ ) → ( norm ‘ ( ( proj𝐻 ) ‘ 𝐴 ) ) = ( norm ‘ ( ( proj ‘ if ( 𝐻C , 𝐻 , ℋ ) ) ‘ 𝐴 ) ) )
8 7 oveq1d ( 𝐻 = if ( 𝐻C , 𝐻 , ℋ ) → ( ( norm ‘ ( ( proj𝐻 ) ‘ 𝐴 ) ) ↑ 2 ) = ( ( norm ‘ ( ( proj ‘ if ( 𝐻C , 𝐻 , ℋ ) ) ‘ 𝐴 ) ) ↑ 2 ) )
9 8 oveq1d ( 𝐻 = if ( 𝐻C , 𝐻 , ℋ ) → ( ( ( norm ‘ ( ( proj𝐻 ) ‘ 𝐴 ) ) ↑ 2 ) + ( ( norm ‘ ( ( proj𝐺 ) ‘ 𝐴 ) ) ↑ 2 ) ) = ( ( ( norm ‘ ( ( proj ‘ if ( 𝐻C , 𝐻 , ℋ ) ) ‘ 𝐴 ) ) ↑ 2 ) + ( ( norm ‘ ( ( proj𝐺 ) ‘ 𝐴 ) ) ↑ 2 ) ) )
10 6 9 eqeq12d ( 𝐻 = if ( 𝐻C , 𝐻 , ℋ ) → ( ( ( norm ‘ ( ( ( proj𝐻 ) ‘ 𝐴 ) + ( ( proj𝐺 ) ‘ 𝐴 ) ) ) ↑ 2 ) = ( ( ( norm ‘ ( ( proj𝐻 ) ‘ 𝐴 ) ) ↑ 2 ) + ( ( norm ‘ ( ( proj𝐺 ) ‘ 𝐴 ) ) ↑ 2 ) ) ↔ ( ( norm ‘ ( ( ( proj ‘ if ( 𝐻C , 𝐻 , ℋ ) ) ‘ 𝐴 ) + ( ( proj𝐺 ) ‘ 𝐴 ) ) ) ↑ 2 ) = ( ( ( norm ‘ ( ( proj ‘ if ( 𝐻C , 𝐻 , ℋ ) ) ‘ 𝐴 ) ) ↑ 2 ) + ( ( norm ‘ ( ( proj𝐺 ) ‘ 𝐴 ) ) ↑ 2 ) ) ) )
11 1 10 imbi12d ( 𝐻 = if ( 𝐻C , 𝐻 , ℋ ) → ( ( 𝐻 ⊆ ( ⊥ ‘ 𝐺 ) → ( ( norm ‘ ( ( ( proj𝐻 ) ‘ 𝐴 ) + ( ( proj𝐺 ) ‘ 𝐴 ) ) ) ↑ 2 ) = ( ( ( norm ‘ ( ( proj𝐻 ) ‘ 𝐴 ) ) ↑ 2 ) + ( ( norm ‘ ( ( proj𝐺 ) ‘ 𝐴 ) ) ↑ 2 ) ) ) ↔ ( if ( 𝐻C , 𝐻 , ℋ ) ⊆ ( ⊥ ‘ 𝐺 ) → ( ( norm ‘ ( ( ( proj ‘ if ( 𝐻C , 𝐻 , ℋ ) ) ‘ 𝐴 ) + ( ( proj𝐺 ) ‘ 𝐴 ) ) ) ↑ 2 ) = ( ( ( norm ‘ ( ( proj ‘ if ( 𝐻C , 𝐻 , ℋ ) ) ‘ 𝐴 ) ) ↑ 2 ) + ( ( norm ‘ ( ( proj𝐺 ) ‘ 𝐴 ) ) ↑ 2 ) ) ) ) )
12 fveq2 ( 𝐺 = if ( 𝐺C , 𝐺 , ℋ ) → ( ⊥ ‘ 𝐺 ) = ( ⊥ ‘ if ( 𝐺C , 𝐺 , ℋ ) ) )
13 12 sseq2d ( 𝐺 = if ( 𝐺C , 𝐺 , ℋ ) → ( if ( 𝐻C , 𝐻 , ℋ ) ⊆ ( ⊥ ‘ 𝐺 ) ↔ if ( 𝐻C , 𝐻 , ℋ ) ⊆ ( ⊥ ‘ if ( 𝐺C , 𝐺 , ℋ ) ) ) )
14 fveq2 ( 𝐺 = if ( 𝐺C , 𝐺 , ℋ ) → ( proj𝐺 ) = ( proj ‘ if ( 𝐺C , 𝐺 , ℋ ) ) )
15 14 fveq1d ( 𝐺 = if ( 𝐺C , 𝐺 , ℋ ) → ( ( proj𝐺 ) ‘ 𝐴 ) = ( ( proj ‘ if ( 𝐺C , 𝐺 , ℋ ) ) ‘ 𝐴 ) )
16 15 oveq2d ( 𝐺 = if ( 𝐺C , 𝐺 , ℋ ) → ( ( ( proj ‘ if ( 𝐻C , 𝐻 , ℋ ) ) ‘ 𝐴 ) + ( ( proj𝐺 ) ‘ 𝐴 ) ) = ( ( ( proj ‘ if ( 𝐻C , 𝐻 , ℋ ) ) ‘ 𝐴 ) + ( ( proj ‘ if ( 𝐺C , 𝐺 , ℋ ) ) ‘ 𝐴 ) ) )
17 16 fveq2d ( 𝐺 = if ( 𝐺C , 𝐺 , ℋ ) → ( norm ‘ ( ( ( proj ‘ if ( 𝐻C , 𝐻 , ℋ ) ) ‘ 𝐴 ) + ( ( proj𝐺 ) ‘ 𝐴 ) ) ) = ( norm ‘ ( ( ( proj ‘ if ( 𝐻C , 𝐻 , ℋ ) ) ‘ 𝐴 ) + ( ( proj ‘ if ( 𝐺C , 𝐺 , ℋ ) ) ‘ 𝐴 ) ) ) )
18 17 oveq1d ( 𝐺 = if ( 𝐺C , 𝐺 , ℋ ) → ( ( norm ‘ ( ( ( proj ‘ if ( 𝐻C , 𝐻 , ℋ ) ) ‘ 𝐴 ) + ( ( proj𝐺 ) ‘ 𝐴 ) ) ) ↑ 2 ) = ( ( norm ‘ ( ( ( proj ‘ if ( 𝐻C , 𝐻 , ℋ ) ) ‘ 𝐴 ) + ( ( proj ‘ if ( 𝐺C , 𝐺 , ℋ ) ) ‘ 𝐴 ) ) ) ↑ 2 ) )
19 15 fveq2d ( 𝐺 = if ( 𝐺C , 𝐺 , ℋ ) → ( norm ‘ ( ( proj𝐺 ) ‘ 𝐴 ) ) = ( norm ‘ ( ( proj ‘ if ( 𝐺C , 𝐺 , ℋ ) ) ‘ 𝐴 ) ) )
20 19 oveq1d ( 𝐺 = if ( 𝐺C , 𝐺 , ℋ ) → ( ( norm ‘ ( ( proj𝐺 ) ‘ 𝐴 ) ) ↑ 2 ) = ( ( norm ‘ ( ( proj ‘ if ( 𝐺C , 𝐺 , ℋ ) ) ‘ 𝐴 ) ) ↑ 2 ) )
21 20 oveq2d ( 𝐺 = if ( 𝐺C , 𝐺 , ℋ ) → ( ( ( norm ‘ ( ( proj ‘ if ( 𝐻C , 𝐻 , ℋ ) ) ‘ 𝐴 ) ) ↑ 2 ) + ( ( norm ‘ ( ( proj𝐺 ) ‘ 𝐴 ) ) ↑ 2 ) ) = ( ( ( norm ‘ ( ( proj ‘ if ( 𝐻C , 𝐻 , ℋ ) ) ‘ 𝐴 ) ) ↑ 2 ) + ( ( norm ‘ ( ( proj ‘ if ( 𝐺C , 𝐺 , ℋ ) ) ‘ 𝐴 ) ) ↑ 2 ) ) )
22 18 21 eqeq12d ( 𝐺 = if ( 𝐺C , 𝐺 , ℋ ) → ( ( ( norm ‘ ( ( ( proj ‘ if ( 𝐻C , 𝐻 , ℋ ) ) ‘ 𝐴 ) + ( ( proj𝐺 ) ‘ 𝐴 ) ) ) ↑ 2 ) = ( ( ( norm ‘ ( ( proj ‘ if ( 𝐻C , 𝐻 , ℋ ) ) ‘ 𝐴 ) ) ↑ 2 ) + ( ( norm ‘ ( ( proj𝐺 ) ‘ 𝐴 ) ) ↑ 2 ) ) ↔ ( ( norm ‘ ( ( ( proj ‘ if ( 𝐻C , 𝐻 , ℋ ) ) ‘ 𝐴 ) + ( ( proj ‘ if ( 𝐺C , 𝐺 , ℋ ) ) ‘ 𝐴 ) ) ) ↑ 2 ) = ( ( ( norm ‘ ( ( proj ‘ if ( 𝐻C , 𝐻 , ℋ ) ) ‘ 𝐴 ) ) ↑ 2 ) + ( ( norm ‘ ( ( proj ‘ if ( 𝐺C , 𝐺 , ℋ ) ) ‘ 𝐴 ) ) ↑ 2 ) ) ) )
23 13 22 imbi12d ( 𝐺 = if ( 𝐺C , 𝐺 , ℋ ) → ( ( if ( 𝐻C , 𝐻 , ℋ ) ⊆ ( ⊥ ‘ 𝐺 ) → ( ( norm ‘ ( ( ( proj ‘ if ( 𝐻C , 𝐻 , ℋ ) ) ‘ 𝐴 ) + ( ( proj𝐺 ) ‘ 𝐴 ) ) ) ↑ 2 ) = ( ( ( norm ‘ ( ( proj ‘ if ( 𝐻C , 𝐻 , ℋ ) ) ‘ 𝐴 ) ) ↑ 2 ) + ( ( norm ‘ ( ( proj𝐺 ) ‘ 𝐴 ) ) ↑ 2 ) ) ) ↔ ( if ( 𝐻C , 𝐻 , ℋ ) ⊆ ( ⊥ ‘ if ( 𝐺C , 𝐺 , ℋ ) ) → ( ( norm ‘ ( ( ( proj ‘ if ( 𝐻C , 𝐻 , ℋ ) ) ‘ 𝐴 ) + ( ( proj ‘ if ( 𝐺C , 𝐺 , ℋ ) ) ‘ 𝐴 ) ) ) ↑ 2 ) = ( ( ( norm ‘ ( ( proj ‘ if ( 𝐻C , 𝐻 , ℋ ) ) ‘ 𝐴 ) ) ↑ 2 ) + ( ( norm ‘ ( ( proj ‘ if ( 𝐺C , 𝐺 , ℋ ) ) ‘ 𝐴 ) ) ↑ 2 ) ) ) ) )
24 fveq2 ( 𝐴 = if ( 𝐴 ∈ ℋ , 𝐴 , 0 ) → ( ( proj ‘ if ( 𝐻C , 𝐻 , ℋ ) ) ‘ 𝐴 ) = ( ( proj ‘ if ( 𝐻C , 𝐻 , ℋ ) ) ‘ if ( 𝐴 ∈ ℋ , 𝐴 , 0 ) ) )
25 fveq2 ( 𝐴 = if ( 𝐴 ∈ ℋ , 𝐴 , 0 ) → ( ( proj ‘ if ( 𝐺C , 𝐺 , ℋ ) ) ‘ 𝐴 ) = ( ( proj ‘ if ( 𝐺C , 𝐺 , ℋ ) ) ‘ if ( 𝐴 ∈ ℋ , 𝐴 , 0 ) ) )
26 24 25 oveq12d ( 𝐴 = if ( 𝐴 ∈ ℋ , 𝐴 , 0 ) → ( ( ( proj ‘ if ( 𝐻C , 𝐻 , ℋ ) ) ‘ 𝐴 ) + ( ( proj ‘ if ( 𝐺C , 𝐺 , ℋ ) ) ‘ 𝐴 ) ) = ( ( ( proj ‘ if ( 𝐻C , 𝐻 , ℋ ) ) ‘ if ( 𝐴 ∈ ℋ , 𝐴 , 0 ) ) + ( ( proj ‘ if ( 𝐺C , 𝐺 , ℋ ) ) ‘ if ( 𝐴 ∈ ℋ , 𝐴 , 0 ) ) ) )
27 26 fveq2d ( 𝐴 = if ( 𝐴 ∈ ℋ , 𝐴 , 0 ) → ( norm ‘ ( ( ( proj ‘ if ( 𝐻C , 𝐻 , ℋ ) ) ‘ 𝐴 ) + ( ( proj ‘ if ( 𝐺C , 𝐺 , ℋ ) ) ‘ 𝐴 ) ) ) = ( norm ‘ ( ( ( proj ‘ if ( 𝐻C , 𝐻 , ℋ ) ) ‘ if ( 𝐴 ∈ ℋ , 𝐴 , 0 ) ) + ( ( proj ‘ if ( 𝐺C , 𝐺 , ℋ ) ) ‘ if ( 𝐴 ∈ ℋ , 𝐴 , 0 ) ) ) ) )
28 27 oveq1d ( 𝐴 = if ( 𝐴 ∈ ℋ , 𝐴 , 0 ) → ( ( norm ‘ ( ( ( proj ‘ if ( 𝐻C , 𝐻 , ℋ ) ) ‘ 𝐴 ) + ( ( proj ‘ if ( 𝐺C , 𝐺 , ℋ ) ) ‘ 𝐴 ) ) ) ↑ 2 ) = ( ( norm ‘ ( ( ( proj ‘ if ( 𝐻C , 𝐻 , ℋ ) ) ‘ if ( 𝐴 ∈ ℋ , 𝐴 , 0 ) ) + ( ( proj ‘ if ( 𝐺C , 𝐺 , ℋ ) ) ‘ if ( 𝐴 ∈ ℋ , 𝐴 , 0 ) ) ) ) ↑ 2 ) )
29 24 fveq2d ( 𝐴 = if ( 𝐴 ∈ ℋ , 𝐴 , 0 ) → ( norm ‘ ( ( proj ‘ if ( 𝐻C , 𝐻 , ℋ ) ) ‘ 𝐴 ) ) = ( norm ‘ ( ( proj ‘ if ( 𝐻C , 𝐻 , ℋ ) ) ‘ if ( 𝐴 ∈ ℋ , 𝐴 , 0 ) ) ) )
30 29 oveq1d ( 𝐴 = if ( 𝐴 ∈ ℋ , 𝐴 , 0 ) → ( ( norm ‘ ( ( proj ‘ if ( 𝐻C , 𝐻 , ℋ ) ) ‘ 𝐴 ) ) ↑ 2 ) = ( ( norm ‘ ( ( proj ‘ if ( 𝐻C , 𝐻 , ℋ ) ) ‘ if ( 𝐴 ∈ ℋ , 𝐴 , 0 ) ) ) ↑ 2 ) )
31 25 fveq2d ( 𝐴 = if ( 𝐴 ∈ ℋ , 𝐴 , 0 ) → ( norm ‘ ( ( proj ‘ if ( 𝐺C , 𝐺 , ℋ ) ) ‘ 𝐴 ) ) = ( norm ‘ ( ( proj ‘ if ( 𝐺C , 𝐺 , ℋ ) ) ‘ if ( 𝐴 ∈ ℋ , 𝐴 , 0 ) ) ) )
32 31 oveq1d ( 𝐴 = if ( 𝐴 ∈ ℋ , 𝐴 , 0 ) → ( ( norm ‘ ( ( proj ‘ if ( 𝐺C , 𝐺 , ℋ ) ) ‘ 𝐴 ) ) ↑ 2 ) = ( ( norm ‘ ( ( proj ‘ if ( 𝐺C , 𝐺 , ℋ ) ) ‘ if ( 𝐴 ∈ ℋ , 𝐴 , 0 ) ) ) ↑ 2 ) )
33 30 32 oveq12d ( 𝐴 = if ( 𝐴 ∈ ℋ , 𝐴 , 0 ) → ( ( ( norm ‘ ( ( proj ‘ if ( 𝐻C , 𝐻 , ℋ ) ) ‘ 𝐴 ) ) ↑ 2 ) + ( ( norm ‘ ( ( proj ‘ if ( 𝐺C , 𝐺 , ℋ ) ) ‘ 𝐴 ) ) ↑ 2 ) ) = ( ( ( norm ‘ ( ( proj ‘ if ( 𝐻C , 𝐻 , ℋ ) ) ‘ if ( 𝐴 ∈ ℋ , 𝐴 , 0 ) ) ) ↑ 2 ) + ( ( norm ‘ ( ( proj ‘ if ( 𝐺C , 𝐺 , ℋ ) ) ‘ if ( 𝐴 ∈ ℋ , 𝐴 , 0 ) ) ) ↑ 2 ) ) )
34 28 33 eqeq12d ( 𝐴 = if ( 𝐴 ∈ ℋ , 𝐴 , 0 ) → ( ( ( norm ‘ ( ( ( proj ‘ if ( 𝐻C , 𝐻 , ℋ ) ) ‘ 𝐴 ) + ( ( proj ‘ if ( 𝐺C , 𝐺 , ℋ ) ) ‘ 𝐴 ) ) ) ↑ 2 ) = ( ( ( norm ‘ ( ( proj ‘ if ( 𝐻C , 𝐻 , ℋ ) ) ‘ 𝐴 ) ) ↑ 2 ) + ( ( norm ‘ ( ( proj ‘ if ( 𝐺C , 𝐺 , ℋ ) ) ‘ 𝐴 ) ) ↑ 2 ) ) ↔ ( ( norm ‘ ( ( ( proj ‘ if ( 𝐻C , 𝐻 , ℋ ) ) ‘ if ( 𝐴 ∈ ℋ , 𝐴 , 0 ) ) + ( ( proj ‘ if ( 𝐺C , 𝐺 , ℋ ) ) ‘ if ( 𝐴 ∈ ℋ , 𝐴 , 0 ) ) ) ) ↑ 2 ) = ( ( ( norm ‘ ( ( proj ‘ if ( 𝐻C , 𝐻 , ℋ ) ) ‘ if ( 𝐴 ∈ ℋ , 𝐴 , 0 ) ) ) ↑ 2 ) + ( ( norm ‘ ( ( proj ‘ if ( 𝐺C , 𝐺 , ℋ ) ) ‘ if ( 𝐴 ∈ ℋ , 𝐴 , 0 ) ) ) ↑ 2 ) ) ) )
35 34 imbi2d ( 𝐴 = if ( 𝐴 ∈ ℋ , 𝐴 , 0 ) → ( ( if ( 𝐻C , 𝐻 , ℋ ) ⊆ ( ⊥ ‘ if ( 𝐺C , 𝐺 , ℋ ) ) → ( ( norm ‘ ( ( ( proj ‘ if ( 𝐻C , 𝐻 , ℋ ) ) ‘ 𝐴 ) + ( ( proj ‘ if ( 𝐺C , 𝐺 , ℋ ) ) ‘ 𝐴 ) ) ) ↑ 2 ) = ( ( ( norm ‘ ( ( proj ‘ if ( 𝐻C , 𝐻 , ℋ ) ) ‘ 𝐴 ) ) ↑ 2 ) + ( ( norm ‘ ( ( proj ‘ if ( 𝐺C , 𝐺 , ℋ ) ) ‘ 𝐴 ) ) ↑ 2 ) ) ) ↔ ( if ( 𝐻C , 𝐻 , ℋ ) ⊆ ( ⊥ ‘ if ( 𝐺C , 𝐺 , ℋ ) ) → ( ( norm ‘ ( ( ( proj ‘ if ( 𝐻C , 𝐻 , ℋ ) ) ‘ if ( 𝐴 ∈ ℋ , 𝐴 , 0 ) ) + ( ( proj ‘ if ( 𝐺C , 𝐺 , ℋ ) ) ‘ if ( 𝐴 ∈ ℋ , 𝐴 , 0 ) ) ) ) ↑ 2 ) = ( ( ( norm ‘ ( ( proj ‘ if ( 𝐻C , 𝐻 , ℋ ) ) ‘ if ( 𝐴 ∈ ℋ , 𝐴 , 0 ) ) ) ↑ 2 ) + ( ( norm ‘ ( ( proj ‘ if ( 𝐺C , 𝐺 , ℋ ) ) ‘ if ( 𝐴 ∈ ℋ , 𝐴 , 0 ) ) ) ↑ 2 ) ) ) ) )
36 ifchhv if ( 𝐻C , 𝐻 , ℋ ) ∈ C
37 ifchhv if ( 𝐺C , 𝐺 , ℋ ) ∈ C
38 ifhvhv0 if ( 𝐴 ∈ ℋ , 𝐴 , 0 ) ∈ ℋ
39 36 37 38 pjopythi ( if ( 𝐻C , 𝐻 , ℋ ) ⊆ ( ⊥ ‘ if ( 𝐺C , 𝐺 , ℋ ) ) → ( ( norm ‘ ( ( ( proj ‘ if ( 𝐻C , 𝐻 , ℋ ) ) ‘ if ( 𝐴 ∈ ℋ , 𝐴 , 0 ) ) + ( ( proj ‘ if ( 𝐺C , 𝐺 , ℋ ) ) ‘ if ( 𝐴 ∈ ℋ , 𝐴 , 0 ) ) ) ) ↑ 2 ) = ( ( ( norm ‘ ( ( proj ‘ if ( 𝐻C , 𝐻 , ℋ ) ) ‘ if ( 𝐴 ∈ ℋ , 𝐴 , 0 ) ) ) ↑ 2 ) + ( ( norm ‘ ( ( proj ‘ if ( 𝐺C , 𝐺 , ℋ ) ) ‘ if ( 𝐴 ∈ ℋ , 𝐴 , 0 ) ) ) ↑ 2 ) ) )
40 11 23 35 39 dedth3h ( ( 𝐻C𝐺C𝐴 ∈ ℋ ) → ( 𝐻 ⊆ ( ⊥ ‘ 𝐺 ) → ( ( norm ‘ ( ( ( proj𝐻 ) ‘ 𝐴 ) + ( ( proj𝐺 ) ‘ 𝐴 ) ) ) ↑ 2 ) = ( ( ( norm ‘ ( ( proj𝐻 ) ‘ 𝐴 ) ) ↑ 2 ) + ( ( norm ‘ ( ( proj𝐺 ) ‘ 𝐴 ) ) ↑ 2 ) ) ) )