Metamath Proof Explorer

Theorem pjcji

Description: The projection on a subspace join is the sum of the projections. (Contributed by NM, 1-Nov-1999) (New usage is discouraged.)

Ref Expression
Hypotheses pjidm.1 ⊢ 𝐻 ∈ Cℋ
pjidm.2 ⊢ 𝐴 ∈ ℋ
pjsslem.1 ⊢ 𝐺 ∈ Cℋ
Assertion pjcji ( 𝐻 ⊆ ( ⊥ ‘ 𝐺 ) → ( ( projℎ ‘ ( 𝐻 ∨ℋ 𝐺 ) ) ‘ 𝐴 ) = ( ( ( projℎ ‘ 𝐻 ) ‘ 𝐴 ) +ℎ ( ( projℎ ‘ 𝐺 ) ‘ 𝐴 ) ) )

Proof

Step Hyp Ref Expression
1 pjidm.1 ⊢ 𝐻 ∈ Cℋ
2 pjidm.2 ⊢ 𝐴 ∈ ℋ
3 pjsslem.1 ⊢ 𝐺 ∈ Cℋ
4 3 choccli ⊢ ( ⊥ ‘ 𝐺 ) ∈ Cℋ
5 1 2 4 pjssmii ⊢ ( 𝐻 ⊆ ( ⊥ ‘ 𝐺 ) → ( ( ( projℎ ‘ ( ⊥ ‘ 𝐺 ) ) ‘ 𝐴 ) −ℎ ( ( projℎ ‘ 𝐻 ) ‘ 𝐴 ) ) = ( ( projℎ ‘ ( ( ⊥ ‘ 𝐺 ) ∩ ( ⊥ ‘ 𝐻 ) ) ) ‘ 𝐴 ) )
6 5 oveq2d ⊢ ( 𝐻 ⊆ ( ⊥ ‘ 𝐺 ) → ( 𝐴 −ℎ ( ( ( projℎ ‘ ( ⊥ ‘ 𝐺 ) ) ‘ 𝐴 ) −ℎ ( ( projℎ ‘ 𝐻 ) ‘ 𝐴 ) ) ) = ( 𝐴 −ℎ ( ( projℎ ‘ ( ( ⊥ ‘ 𝐺 ) ∩ ( ⊥ ‘ 𝐻 ) ) ) ‘ 𝐴 ) ) )
7 3 2 pjpoi ⊢ ( ( projℎ ‘ 𝐺 ) ‘ 𝐴 ) = ( 𝐴 −ℎ ( ( projℎ ‘ ( ⊥ ‘ 𝐺 ) ) ‘ 𝐴 ) )
8 7 oveq2i ⊢ ( ( ( projℎ ‘ 𝐻 ) ‘ 𝐴 ) +ℎ ( ( projℎ ‘ 𝐺 ) ‘ 𝐴 ) ) = ( ( ( projℎ ‘ 𝐻 ) ‘ 𝐴 ) +ℎ ( 𝐴 −ℎ ( ( projℎ ‘ ( ⊥ ‘ 𝐺 ) ) ‘ 𝐴 ) ) )
9 4 2 pjhclii ⊢ ( ( projℎ ‘ ( ⊥ ‘ 𝐺 ) ) ‘ 𝐴 ) ∈ ℋ
10 1 2 pjhclii ⊢ ( ( projℎ ‘ 𝐻 ) ‘ 𝐴 ) ∈ ℋ
11 9 10 hvnegdii ⊢ ( - 1 ·ℎ ( ( ( projℎ ‘ ( ⊥ ‘ 𝐺 ) ) ‘ 𝐴 ) −ℎ ( ( projℎ ‘ 𝐻 ) ‘ 𝐴 ) ) ) = ( ( ( projℎ ‘ 𝐻 ) ‘ 𝐴 ) −ℎ ( ( projℎ ‘ ( ⊥ ‘ 𝐺 ) ) ‘ 𝐴 ) )
12 11 oveq2i ⊢ ( 𝐴 +ℎ ( - 1 ·ℎ ( ( ( projℎ ‘ ( ⊥ ‘ 𝐺 ) ) ‘ 𝐴 ) −ℎ ( ( projℎ ‘ 𝐻 ) ‘ 𝐴 ) ) ) ) = ( 𝐴 +ℎ ( ( ( projℎ ‘ 𝐻 ) ‘ 𝐴 ) −ℎ ( ( projℎ ‘ ( ⊥ ‘ 𝐺 ) ) ‘ 𝐴 ) ) )
13 hvaddsub12 ⊢ ( ( ( ( projℎ ‘ 𝐻 ) ‘ 𝐴 ) ∈ ℋ ∧ 𝐴 ∈ ℋ ∧ ( ( projℎ ‘ ( ⊥ ‘ 𝐺 ) ) ‘ 𝐴 ) ∈ ℋ ) → ( ( ( projℎ ‘ 𝐻 ) ‘ 𝐴 ) +ℎ ( 𝐴 −ℎ ( ( projℎ ‘ ( ⊥ ‘ 𝐺 ) ) ‘ 𝐴 ) ) ) = ( 𝐴 +ℎ ( ( ( projℎ ‘ 𝐻 ) ‘ 𝐴 ) −ℎ ( ( projℎ ‘ ( ⊥ ‘ 𝐺 ) ) ‘ 𝐴 ) ) ) )
14 10 2 9 13 mp3an ⊢ ( ( ( projℎ ‘ 𝐻 ) ‘ 𝐴 ) +ℎ ( 𝐴 −ℎ ( ( projℎ ‘ ( ⊥ ‘ 𝐺 ) ) ‘ 𝐴 ) ) ) = ( 𝐴 +ℎ ( ( ( projℎ ‘ 𝐻 ) ‘ 𝐴 ) −ℎ ( ( projℎ ‘ ( ⊥ ‘ 𝐺 ) ) ‘ 𝐴 ) ) )
15 12 14 eqtr4i ⊢ ( 𝐴 +ℎ ( - 1 ·ℎ ( ( ( projℎ ‘ ( ⊥ ‘ 𝐺 ) ) ‘ 𝐴 ) −ℎ ( ( projℎ ‘ 𝐻 ) ‘ 𝐴 ) ) ) ) = ( ( ( projℎ ‘ 𝐻 ) ‘ 𝐴 ) +ℎ ( 𝐴 −ℎ ( ( projℎ ‘ ( ⊥ ‘ 𝐺 ) ) ‘ 𝐴 ) ) )
16 8 15 eqtr4i ⊢ ( ( ( projℎ ‘ 𝐻 ) ‘ 𝐴 ) +ℎ ( ( projℎ ‘ 𝐺 ) ‘ 𝐴 ) ) = ( 𝐴 +ℎ ( - 1 ·ℎ ( ( ( projℎ ‘ ( ⊥ ‘ 𝐺 ) ) ‘ 𝐴 ) −ℎ ( ( projℎ ‘ 𝐻 ) ‘ 𝐴 ) ) ) )
17 9 10 hvsubcli ⊢ ( ( ( projℎ ‘ ( ⊥ ‘ 𝐺 ) ) ‘ 𝐴 ) −ℎ ( ( projℎ ‘ 𝐻 ) ‘ 𝐴 ) ) ∈ ℋ
18 2 17 hvsubvali ⊢ ( 𝐴 −ℎ ( ( ( projℎ ‘ ( ⊥ ‘ 𝐺 ) ) ‘ 𝐴 ) −ℎ ( ( projℎ ‘ 𝐻 ) ‘ 𝐴 ) ) ) = ( 𝐴 +ℎ ( - 1 ·ℎ ( ( ( projℎ ‘ ( ⊥ ‘ 𝐺 ) ) ‘ 𝐴 ) −ℎ ( ( projℎ ‘ 𝐻 ) ‘ 𝐴 ) ) ) )
19 16 18 eqtr4i ⊢ ( ( ( projℎ ‘ 𝐻 ) ‘ 𝐴 ) +ℎ ( ( projℎ ‘ 𝐺 ) ‘ 𝐴 ) ) = ( 𝐴 −ℎ ( ( ( projℎ ‘ ( ⊥ ‘ 𝐺 ) ) ‘ 𝐴 ) −ℎ ( ( projℎ ‘ 𝐻 ) ‘ 𝐴 ) ) )
20 1 3 chjcomi ⊢ ( 𝐻 ∨ℋ 𝐺 ) = ( 𝐺 ∨ℋ 𝐻 )
21 3 1 chdmm4i ⊢ ( ⊥ ‘ ( ( ⊥ ‘ 𝐺 ) ∩ ( ⊥ ‘ 𝐻 ) ) ) = ( 𝐺 ∨ℋ 𝐻 )
22 20 21 eqtr4i ⊢ ( 𝐻 ∨ℋ 𝐺 ) = ( ⊥ ‘ ( ( ⊥ ‘ 𝐺 ) ∩ ( ⊥ ‘ 𝐻 ) ) )
23 22 fveq2i ⊢ ( projℎ ‘ ( 𝐻 ∨ℋ 𝐺 ) ) = ( projℎ ‘ ( ⊥ ‘ ( ( ⊥ ‘ 𝐺 ) ∩ ( ⊥ ‘ 𝐻 ) ) ) )
24 23 fveq1i ⊢ ( ( projℎ ‘ ( 𝐻 ∨ℋ 𝐺 ) ) ‘ 𝐴 ) = ( ( projℎ ‘ ( ⊥ ‘ ( ( ⊥ ‘ 𝐺 ) ∩ ( ⊥ ‘ 𝐻 ) ) ) ) ‘ 𝐴 )
25 1 choccli ⊢ ( ⊥ ‘ 𝐻 ) ∈ Cℋ
26 4 25 chincli ⊢ ( ( ⊥ ‘ 𝐺 ) ∩ ( ⊥ ‘ 𝐻 ) ) ∈ Cℋ
27 26 2 pjopi ⊢ ( ( projℎ ‘ ( ⊥ ‘ ( ( ⊥ ‘ 𝐺 ) ∩ ( ⊥ ‘ 𝐻 ) ) ) ) ‘ 𝐴 ) = ( 𝐴 −ℎ ( ( projℎ ‘ ( ( ⊥ ‘ 𝐺 ) ∩ ( ⊥ ‘ 𝐻 ) ) ) ‘ 𝐴 ) )
28 24 27 eqtri ⊢ ( ( projℎ ‘ ( 𝐻 ∨ℋ 𝐺 ) ) ‘ 𝐴 ) = ( 𝐴 −ℎ ( ( projℎ ‘ ( ( ⊥ ‘ 𝐺 ) ∩ ( ⊥ ‘ 𝐻 ) ) ) ‘ 𝐴 ) )
29 6 19 28 3eqtr4g ⊢ ( 𝐻 ⊆ ( ⊥ ‘ 𝐺 ) → ( ( ( projℎ ‘ 𝐻 ) ‘ 𝐴 ) +ℎ ( ( projℎ ‘ 𝐺 ) ‘ 𝐴 ) ) = ( ( projℎ ‘ ( 𝐻 ∨ℋ 𝐺 ) ) ‘ 𝐴 ) )
30 29 eqcomd ⊢ ( 𝐻 ⊆ ( ⊥ ‘ 𝐺 ) → ( ( projℎ ‘ ( 𝐻 ∨ℋ 𝐺 ) ) ‘ 𝐴 ) = ( ( ( projℎ ‘ 𝐻 ) ‘ 𝐴 ) +ℎ ( ( projℎ ‘ 𝐺 ) ‘ 𝐴 ) ) )