This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem pjsumi

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

Ref Expression
Hypotheses pjsumt.1 ⊢ G ∈ C ℋ
pjsumt.2 ⊢ H ∈ C ℋ
Assertion pjsumi ⊢ A ∈ ℋ → G ⊆ ⊥ ⁡ H → proj ℎ ⁡ G + ℋ H ⁡ A = proj ℎ ⁡ G ⁡ A + ℎ proj ℎ ⁡ H ⁡ A

Proof

Step Hyp Ref Expression
1 pjsumt.1 ⊢ G ∈ C ℋ
2 pjsumt.2 ⊢ H ∈ C ℋ
3 1 2 osumi ⊢ G ⊆ ⊥ ⁡ H → G + ℋ H = G ∨ ℋ H
4 3 fveq2d ⊢ G ⊆ ⊥ ⁡ H → proj ℎ ⁡ G + ℋ H = proj ℎ ⁡ G ∨ ℋ H
5 4 fveq1d ⊢ G ⊆ ⊥ ⁡ H → proj ℎ ⁡ G + ℋ H ⁡ A = proj ℎ ⁡ G ∨ ℋ H ⁡ A
6 5 adantl ⊢ A ∈ ℋ ∧ G ⊆ ⊥ ⁡ H → proj ℎ ⁡ G + ℋ H ⁡ A = proj ℎ ⁡ G ∨ ℋ H ⁡ A
7 pjcjt2 ⊢ G ∈ C ℋ ∧ H ∈ C ℋ ∧ A ∈ ℋ → G ⊆ ⊥ ⁡ H → proj ℎ ⁡ G ∨ ℋ H ⁡ A = proj ℎ ⁡ G ⁡ A + ℎ proj ℎ ⁡ H ⁡ A
8 1 2 7 mp3an12 ⊢ A ∈ ℋ → G ⊆ ⊥ ⁡ H → proj ℎ ⁡ G ∨ ℋ H ⁡ A = proj ℎ ⁡ G ⁡ A + ℎ proj ℎ ⁡ H ⁡ A
9 8 imp ⊢ A ∈ ℋ ∧ G ⊆ ⊥ ⁡ H → proj ℎ ⁡ G ∨ ℋ H ⁡ A = proj ℎ ⁡ G ⁡ A + ℎ proj ℎ ⁡ H ⁡ A
10 6 9 eqtrd ⊢ A ∈ ℋ ∧ G ⊆ ⊥ ⁡ H → proj ℎ ⁡ G + ℋ H ⁡ A = proj ℎ ⁡ G ⁡ A + ℎ proj ℎ ⁡ H ⁡ A
11 10 ex ⊢ A ∈ ℋ → G ⊆ ⊥ ⁡ H → proj ℎ ⁡ G + ℋ H ⁡ A = proj ℎ ⁡ G ⁡ A + ℎ proj ℎ ⁡ H ⁡ A