Metamath Proof Explorer

Theorem pjss2i

Description: Subset relationship for projections. Theorem 4.5(i)->(ii) of Beran p. 112. (Contributed by NM, 31-Oct-1999) (New usage is discouraged.)

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

Proof

Step Hyp Ref Expression
1 pjidm.1 ⊢ 𝐻 ∈ Cℋ
2 pjidm.2 ⊢ 𝐴 ∈ ℋ
3 pjsslem.1 ⊢ 𝐺 ∈ Cℋ
4 1 choccli ⊢ ( ⊥ ‘ 𝐻 ) ∈ Cℋ
5 4 2 pjclii ⊢ ( ( projℎ ‘ ( ⊥ ‘ 𝐻 ) ) ‘ 𝐴 ) ∈ ( ⊥ ‘ 𝐻 )
6 1 3 chsscon3i ⊢ ( 𝐻 ⊆ 𝐺 ↔ ( ⊥ ‘ 𝐺 ) ⊆ ( ⊥ ‘ 𝐻 ) )
7 3 choccli ⊢ ( ⊥ ‘ 𝐺 ) ∈ Cℋ
8 7 2 pjclii ⊢ ( ( projℎ ‘ ( ⊥ ‘ 𝐺 ) ) ‘ 𝐴 ) ∈ ( ⊥ ‘ 𝐺 )
9 ssel ⊢ ( ( ⊥ ‘ 𝐺 ) ⊆ ( ⊥ ‘ 𝐻 ) → ( ( ( projℎ ‘ ( ⊥ ‘ 𝐺 ) ) ‘ 𝐴 ) ∈ ( ⊥ ‘ 𝐺 ) → ( ( projℎ ‘ ( ⊥ ‘ 𝐺 ) ) ‘ 𝐴 ) ∈ ( ⊥ ‘ 𝐻 ) ) )
10 8 9 mpi ⊢ ( ( ⊥ ‘ 𝐺 ) ⊆ ( ⊥ ‘ 𝐻 ) → ( ( projℎ ‘ ( ⊥ ‘ 𝐺 ) ) ‘ 𝐴 ) ∈ ( ⊥ ‘ 𝐻 ) )
11 6 10 sylbi ⊢ ( 𝐻 ⊆ 𝐺 → ( ( projℎ ‘ ( ⊥ ‘ 𝐺 ) ) ‘ 𝐴 ) ∈ ( ⊥ ‘ 𝐻 ) )
12 4 chshii ⊢ ( ⊥ ‘ 𝐻 ) ∈ Sℋ
13 shsubcl ⊢ ( ( ( ⊥ ‘ 𝐻 ) ∈ Sℋ ∧ ( ( projℎ ‘ ( ⊥ ‘ 𝐻 ) ) ‘ 𝐴 ) ∈ ( ⊥ ‘ 𝐻 ) ∧ ( ( projℎ ‘ ( ⊥ ‘ 𝐺 ) ) ‘ 𝐴 ) ∈ ( ⊥ ‘ 𝐻 ) ) → ( ( ( projℎ ‘ ( ⊥ ‘ 𝐻 ) ) ‘ 𝐴 ) −ℎ ( ( projℎ ‘ ( ⊥ ‘ 𝐺 ) ) ‘ 𝐴 ) ) ∈ ( ⊥ ‘ 𝐻 ) )
14 12 13 mp3an1 ⊢ ( ( ( ( projℎ ‘ ( ⊥ ‘ 𝐻 ) ) ‘ 𝐴 ) ∈ ( ⊥ ‘ 𝐻 ) ∧ ( ( projℎ ‘ ( ⊥ ‘ 𝐺 ) ) ‘ 𝐴 ) ∈ ( ⊥ ‘ 𝐻 ) ) → ( ( ( projℎ ‘ ( ⊥ ‘ 𝐻 ) ) ‘ 𝐴 ) −ℎ ( ( projℎ ‘ ( ⊥ ‘ 𝐺 ) ) ‘ 𝐴 ) ) ∈ ( ⊥ ‘ 𝐻 ) )
15 5 11 14 sylancr ⊢ ( 𝐻 ⊆ 𝐺 → ( ( ( projℎ ‘ ( ⊥ ‘ 𝐻 ) ) ‘ 𝐴 ) −ℎ ( ( projℎ ‘ ( ⊥ ‘ 𝐺 ) ) ‘ 𝐴 ) ) ∈ ( ⊥ ‘ 𝐻 ) )
16 1 2 3 pjsslem ⊢ ( ( ( projℎ ‘ ( ⊥ ‘ 𝐻 ) ) ‘ 𝐴 ) −ℎ ( ( projℎ ‘ ( ⊥ ‘ 𝐺 ) ) ‘ 𝐴 ) ) = ( ( ( projℎ ‘ 𝐺 ) ‘ 𝐴 ) −ℎ ( ( projℎ ‘ 𝐻 ) ‘ 𝐴 ) )
17 16 eleq1i ⊢ ( ( ( ( projℎ ‘ ( ⊥ ‘ 𝐻 ) ) ‘ 𝐴 ) −ℎ ( ( projℎ ‘ ( ⊥ ‘ 𝐺 ) ) ‘ 𝐴 ) ) ∈ ( ⊥ ‘ 𝐻 ) ↔ ( ( ( projℎ ‘ 𝐺 ) ‘ 𝐴 ) −ℎ ( ( projℎ ‘ 𝐻 ) ‘ 𝐴 ) ) ∈ ( ⊥ ‘ 𝐻 ) )
18 3 2 pjhclii ⊢ ( ( projℎ ‘ 𝐺 ) ‘ 𝐴 ) ∈ ℋ
19 1 2 pjhclii ⊢ ( ( projℎ ‘ 𝐻 ) ‘ 𝐴 ) ∈ ℋ
20 18 19 hvsubcli ⊢ ( ( ( projℎ ‘ 𝐺 ) ‘ 𝐴 ) −ℎ ( ( projℎ ‘ 𝐻 ) ‘ 𝐴 ) ) ∈ ℋ
21 1 20 pjoc2i ⊢ ( ( ( ( projℎ ‘ 𝐺 ) ‘ 𝐴 ) −ℎ ( ( projℎ ‘ 𝐻 ) ‘ 𝐴 ) ) ∈ ( ⊥ ‘ 𝐻 ) ↔ ( ( projℎ ‘ 𝐻 ) ‘ ( ( ( projℎ ‘ 𝐺 ) ‘ 𝐴 ) −ℎ ( ( projℎ ‘ 𝐻 ) ‘ 𝐴 ) ) ) = 0ℎ )
22 17 21 bitri ⊢ ( ( ( ( projℎ ‘ ( ⊥ ‘ 𝐻 ) ) ‘ 𝐴 ) −ℎ ( ( projℎ ‘ ( ⊥ ‘ 𝐺 ) ) ‘ 𝐴 ) ) ∈ ( ⊥ ‘ 𝐻 ) ↔ ( ( projℎ ‘ 𝐻 ) ‘ ( ( ( projℎ ‘ 𝐺 ) ‘ 𝐴 ) −ℎ ( ( projℎ ‘ 𝐻 ) ‘ 𝐴 ) ) ) = 0ℎ )
23 1 18 19 pjsubii ⊢ ( ( projℎ ‘ 𝐻 ) ‘ ( ( ( projℎ ‘ 𝐺 ) ‘ 𝐴 ) −ℎ ( ( projℎ ‘ 𝐻 ) ‘ 𝐴 ) ) ) = ( ( ( projℎ ‘ 𝐻 ) ‘ ( ( projℎ ‘ 𝐺 ) ‘ 𝐴 ) ) −ℎ ( ( projℎ ‘ 𝐻 ) ‘ ( ( projℎ ‘ 𝐻 ) ‘ 𝐴 ) ) )
24 23 eqeq1i ⊢ ( ( ( projℎ ‘ 𝐻 ) ‘ ( ( ( projℎ ‘ 𝐺 ) ‘ 𝐴 ) −ℎ ( ( projℎ ‘ 𝐻 ) ‘ 𝐴 ) ) ) = 0ℎ ↔ ( ( ( projℎ ‘ 𝐻 ) ‘ ( ( projℎ ‘ 𝐺 ) ‘ 𝐴 ) ) −ℎ ( ( projℎ ‘ 𝐻 ) ‘ ( ( projℎ ‘ 𝐻 ) ‘ 𝐴 ) ) ) = 0ℎ )
25 1 18 pjhclii ⊢ ( ( projℎ ‘ 𝐻 ) ‘ ( ( projℎ ‘ 𝐺 ) ‘ 𝐴 ) ) ∈ ℋ
26 1 19 pjhclii ⊢ ( ( projℎ ‘ 𝐻 ) ‘ ( ( projℎ ‘ 𝐻 ) ‘ 𝐴 ) ) ∈ ℋ
27 25 26 hvsubeq0i ⊢ ( ( ( ( projℎ ‘ 𝐻 ) ‘ ( ( projℎ ‘ 𝐺 ) ‘ 𝐴 ) ) −ℎ ( ( projℎ ‘ 𝐻 ) ‘ ( ( projℎ ‘ 𝐻 ) ‘ 𝐴 ) ) ) = 0ℎ ↔ ( ( projℎ ‘ 𝐻 ) ‘ ( ( projℎ ‘ 𝐺 ) ‘ 𝐴 ) ) = ( ( projℎ ‘ 𝐻 ) ‘ ( ( projℎ ‘ 𝐻 ) ‘ 𝐴 ) ) )
28 24 27 bitri ⊢ ( ( ( projℎ ‘ 𝐻 ) ‘ ( ( ( projℎ ‘ 𝐺 ) ‘ 𝐴 ) −ℎ ( ( projℎ ‘ 𝐻 ) ‘ 𝐴 ) ) ) = 0ℎ ↔ ( ( projℎ ‘ 𝐻 ) ‘ ( ( projℎ ‘ 𝐺 ) ‘ 𝐴 ) ) = ( ( projℎ ‘ 𝐻 ) ‘ ( ( projℎ ‘ 𝐻 ) ‘ 𝐴 ) ) )
29 1 2 pjidmi ⊢ ( ( projℎ ‘ 𝐻 ) ‘ ( ( projℎ ‘ 𝐻 ) ‘ 𝐴 ) ) = ( ( projℎ ‘ 𝐻 ) ‘ 𝐴 )
30 29 eqeq2i ⊢ ( ( ( projℎ ‘ 𝐻 ) ‘ ( ( projℎ ‘ 𝐺 ) ‘ 𝐴 ) ) = ( ( projℎ ‘ 𝐻 ) ‘ ( ( projℎ ‘ 𝐻 ) ‘ 𝐴 ) ) ↔ ( ( projℎ ‘ 𝐻 ) ‘ ( ( projℎ ‘ 𝐺 ) ‘ 𝐴 ) ) = ( ( projℎ ‘ 𝐻 ) ‘ 𝐴 ) )
31 22 28 30 3bitrri ⊢ ( ( ( projℎ ‘ 𝐻 ) ‘ ( ( projℎ ‘ 𝐺 ) ‘ 𝐴 ) ) = ( ( projℎ ‘ 𝐻 ) ‘ 𝐴 ) ↔ ( ( ( projℎ ‘ ( ⊥ ‘ 𝐻 ) ) ‘ 𝐴 ) −ℎ ( ( projℎ ‘ ( ⊥ ‘ 𝐺 ) ) ‘ 𝐴 ) ) ∈ ( ⊥ ‘ 𝐻 ) )
32 15 31 sylibr ⊢ ( 𝐻 ⊆ 𝐺 → ( ( projℎ ‘ 𝐻 ) ‘ ( ( projℎ ‘ 𝐺 ) ‘ 𝐴 ) ) = ( ( projℎ ‘ 𝐻 ) ‘ 𝐴 ) )