Metamath Proof Explorer

Theorem pjsslem

Description: Lemma for subset relationships of projections. (Contributed by NM, 31-Oct-1999) (New usage is discouraged.)

Ref Expression
Hypotheses pjidm.1 ⊢ 𝐻 ∈ Cℋ
pjidm.2 ⊢ 𝐴 ∈ ℋ
pjsslem.1 ⊢ 𝐺 ∈ Cℋ
Assertion pjsslem ( ( ( projℎ ‘ ( ⊥ ‘ 𝐻 ) ) ‘ 𝐴 ) −ℎ ( ( projℎ ‘ ( ⊥ ‘ 𝐺 ) ) ‘ 𝐴 ) ) = ( ( ( projℎ ‘ 𝐺 ) ‘ 𝐴 ) −ℎ ( ( projℎ ‘ 𝐻 ) ‘ 𝐴 ) )

Proof

Step Hyp Ref Expression
1 pjidm.1 ⊢ 𝐻 ∈ Cℋ
2 pjidm.2 ⊢ 𝐴 ∈ ℋ
3 pjsslem.1 ⊢ 𝐺 ∈ Cℋ
4 pjo ⊢ ( ( 𝐻 ∈ Cℋ ∧ 𝐴 ∈ ℋ ) → ( ( projℎ ‘ ( ⊥ ‘ 𝐻 ) ) ‘ 𝐴 ) = ( ( ( projℎ ‘ ℋ ) ‘ 𝐴 ) −ℎ ( ( projℎ ‘ 𝐻 ) ‘ 𝐴 ) ) )
5 1 2 4 mp2an ⊢ ( ( projℎ ‘ ( ⊥ ‘ 𝐻 ) ) ‘ 𝐴 ) = ( ( ( projℎ ‘ ℋ ) ‘ 𝐴 ) −ℎ ( ( projℎ ‘ 𝐻 ) ‘ 𝐴 ) )
6 pjo ⊢ ( ( 𝐺 ∈ Cℋ ∧ 𝐴 ∈ ℋ ) → ( ( projℎ ‘ ( ⊥ ‘ 𝐺 ) ) ‘ 𝐴 ) = ( ( ( projℎ ‘ ℋ ) ‘ 𝐴 ) −ℎ ( ( projℎ ‘ 𝐺 ) ‘ 𝐴 ) ) )
7 3 2 6 mp2an ⊢ ( ( projℎ ‘ ( ⊥ ‘ 𝐺 ) ) ‘ 𝐴 ) = ( ( ( projℎ ‘ ℋ ) ‘ 𝐴 ) −ℎ ( ( projℎ ‘ 𝐺 ) ‘ 𝐴 ) )
8 5 7 oveq12i ⊢ ( ( ( projℎ ‘ ( ⊥ ‘ 𝐻 ) ) ‘ 𝐴 ) −ℎ ( ( projℎ ‘ ( ⊥ ‘ 𝐺 ) ) ‘ 𝐴 ) ) = ( ( ( ( projℎ ‘ ℋ ) ‘ 𝐴 ) −ℎ ( ( projℎ ‘ 𝐻 ) ‘ 𝐴 ) ) −ℎ ( ( ( projℎ ‘ ℋ ) ‘ 𝐴 ) −ℎ ( ( projℎ ‘ 𝐺 ) ‘ 𝐴 ) ) )
9 helch ⊢ ℋ ∈ Cℋ
10 9 2 pjclii ⊢ ( ( projℎ ‘ ℋ ) ‘ 𝐴 ) ∈ ℋ
11 1 2 pjhclii ⊢ ( ( projℎ ‘ 𝐻 ) ‘ 𝐴 ) ∈ ℋ
12 3 2 pjhclii ⊢ ( ( projℎ ‘ 𝐺 ) ‘ 𝐴 ) ∈ ℋ
13 10 11 10 12 hvsubsub4i ⊢ ( ( ( ( projℎ ‘ ℋ ) ‘ 𝐴 ) −ℎ ( ( projℎ ‘ 𝐻 ) ‘ 𝐴 ) ) −ℎ ( ( ( projℎ ‘ ℋ ) ‘ 𝐴 ) −ℎ ( ( projℎ ‘ 𝐺 ) ‘ 𝐴 ) ) ) = ( ( ( ( projℎ ‘ ℋ ) ‘ 𝐴 ) −ℎ ( ( projℎ ‘ ℋ ) ‘ 𝐴 ) ) −ℎ ( ( ( projℎ ‘ 𝐻 ) ‘ 𝐴 ) −ℎ ( ( projℎ ‘ 𝐺 ) ‘ 𝐴 ) ) )
14 hvsubid ⊢ ( ( ( projℎ ‘ ℋ ) ‘ 𝐴 ) ∈ ℋ → ( ( ( projℎ ‘ ℋ ) ‘ 𝐴 ) −ℎ ( ( projℎ ‘ ℋ ) ‘ 𝐴 ) ) = 0ℎ )
15 10 14 ax-mp ⊢ ( ( ( projℎ ‘ ℋ ) ‘ 𝐴 ) −ℎ ( ( projℎ ‘ ℋ ) ‘ 𝐴 ) ) = 0ℎ
16 15 oveq1i ⊢ ( ( ( ( projℎ ‘ ℋ ) ‘ 𝐴 ) −ℎ ( ( projℎ ‘ ℋ ) ‘ 𝐴 ) ) −ℎ ( ( ( projℎ ‘ 𝐻 ) ‘ 𝐴 ) −ℎ ( ( projℎ ‘ 𝐺 ) ‘ 𝐴 ) ) ) = ( 0ℎ −ℎ ( ( ( projℎ ‘ 𝐻 ) ‘ 𝐴 ) −ℎ ( ( projℎ ‘ 𝐺 ) ‘ 𝐴 ) ) )
17 8 13 16 3eqtri ⊢ ( ( ( projℎ ‘ ( ⊥ ‘ 𝐻 ) ) ‘ 𝐴 ) −ℎ ( ( projℎ ‘ ( ⊥ ‘ 𝐺 ) ) ‘ 𝐴 ) ) = ( 0ℎ −ℎ ( ( ( projℎ ‘ 𝐻 ) ‘ 𝐴 ) −ℎ ( ( projℎ ‘ 𝐺 ) ‘ 𝐴 ) ) )
18 11 12 hvsubcli ⊢ ( ( ( projℎ ‘ 𝐻 ) ‘ 𝐴 ) −ℎ ( ( projℎ ‘ 𝐺 ) ‘ 𝐴 ) ) ∈ ℋ
19 18 hv2negi ⊢ ( 0ℎ −ℎ ( ( ( projℎ ‘ 𝐻 ) ‘ 𝐴 ) −ℎ ( ( projℎ ‘ 𝐺 ) ‘ 𝐴 ) ) ) = ( - 1 ·ℎ ( ( ( projℎ ‘ 𝐻 ) ‘ 𝐴 ) −ℎ ( ( projℎ ‘ 𝐺 ) ‘ 𝐴 ) ) )
20 11 12 hvnegdii ⊢ ( - 1 ·ℎ ( ( ( projℎ ‘ 𝐻 ) ‘ 𝐴 ) −ℎ ( ( projℎ ‘ 𝐺 ) ‘ 𝐴 ) ) ) = ( ( ( projℎ ‘ 𝐺 ) ‘ 𝐴 ) −ℎ ( ( projℎ ‘ 𝐻 ) ‘ 𝐴 ) )
21 17 19 20 3eqtri ⊢ ( ( ( projℎ ‘ ( ⊥ ‘ 𝐻 ) ) ‘ 𝐴 ) −ℎ ( ( projℎ ‘ ( ⊥ ‘ 𝐺 ) ) ‘ 𝐴 ) ) = ( ( ( projℎ ‘ 𝐺 ) ‘ 𝐴 ) −ℎ ( ( projℎ ‘ 𝐻 ) ‘ 𝐴 ) )