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 ) ) ) )