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𝐻 ) ‘ 𝐴 ) )