# Metamath Proof Explorer

## Theorem pjssmii

Description: Projection meet property. Remark in Kalmbach p. 66. Also Theorem 4.5(i)->(iv) 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 pjssmii ( 𝐻𝐺 → ( ( ( proj𝐺 ) ‘ 𝐴 ) − ( ( proj𝐻 ) ‘ 𝐴 ) ) = ( ( proj ‘ ( 𝐺 ∩ ( ⊥ ‘ 𝐻 ) ) ) ‘ 𝐴 ) )

### Proof

Step Hyp Ref Expression
1 pjidm.1 𝐻C
2 pjidm.2 𝐴 ∈ ℋ
3 pjsslem.1 𝐺C
4 1 choccli ( ⊥ ‘ 𝐻 ) ∈ C
5 3 4 chincli ( 𝐺 ∩ ( ⊥ ‘ 𝐻 ) ) ∈ C
6 3 2 pjhclii ( ( proj𝐺 ) ‘ 𝐴 ) ∈ ℋ
7 1 2 pjhclii ( ( proj𝐻 ) ‘ 𝐴 ) ∈ ℋ
8 5 6 7 pjsubii ( ( proj ‘ ( 𝐺 ∩ ( ⊥ ‘ 𝐻 ) ) ) ‘ ( ( ( proj𝐺 ) ‘ 𝐴 ) − ( ( proj𝐻 ) ‘ 𝐴 ) ) ) = ( ( ( proj ‘ ( 𝐺 ∩ ( ⊥ ‘ 𝐻 ) ) ) ‘ ( ( proj𝐺 ) ‘ 𝐴 ) ) − ( ( proj ‘ ( 𝐺 ∩ ( ⊥ ‘ 𝐻 ) ) ) ‘ ( ( proj𝐻 ) ‘ 𝐴 ) ) )
9 5 6 pjhclii ( ( proj ‘ ( 𝐺 ∩ ( ⊥ ‘ 𝐻 ) ) ) ‘ ( ( proj𝐺 ) ‘ 𝐴 ) ) ∈ ℋ
10 5 7 pjhclii ( ( proj ‘ ( 𝐺 ∩ ( ⊥ ‘ 𝐻 ) ) ) ‘ ( ( proj𝐻 ) ‘ 𝐴 ) ) ∈ ℋ
11 9 10 hvsubvali ( ( ( proj ‘ ( 𝐺 ∩ ( ⊥ ‘ 𝐻 ) ) ) ‘ ( ( proj𝐺 ) ‘ 𝐴 ) ) − ( ( proj ‘ ( 𝐺 ∩ ( ⊥ ‘ 𝐻 ) ) ) ‘ ( ( proj𝐻 ) ‘ 𝐴 ) ) ) = ( ( ( proj ‘ ( 𝐺 ∩ ( ⊥ ‘ 𝐻 ) ) ) ‘ ( ( proj𝐺 ) ‘ 𝐴 ) ) + ( - 1 · ( ( proj ‘ ( 𝐺 ∩ ( ⊥ ‘ 𝐻 ) ) ) ‘ ( ( proj𝐻 ) ‘ 𝐴 ) ) ) )
12 inss1 ( 𝐺 ∩ ( ⊥ ‘ 𝐻 ) ) ⊆ 𝐺
13 5 2 3 pjss2i ( ( 𝐺 ∩ ( ⊥ ‘ 𝐻 ) ) ⊆ 𝐺 → ( ( proj ‘ ( 𝐺 ∩ ( ⊥ ‘ 𝐻 ) ) ) ‘ ( ( proj𝐺 ) ‘ 𝐴 ) ) = ( ( proj ‘ ( 𝐺 ∩ ( ⊥ ‘ 𝐻 ) ) ) ‘ 𝐴 ) )
14 12 13 ax-mp ( ( proj ‘ ( 𝐺 ∩ ( ⊥ ‘ 𝐻 ) ) ) ‘ ( ( proj𝐺 ) ‘ 𝐴 ) ) = ( ( proj ‘ ( 𝐺 ∩ ( ⊥ ‘ 𝐻 ) ) ) ‘ 𝐴 )
15 1 chshii 𝐻S
16 shococss ( 𝐻S𝐻 ⊆ ( ⊥ ‘ ( ⊥ ‘ 𝐻 ) ) )
17 15 16 ax-mp 𝐻 ⊆ ( ⊥ ‘ ( ⊥ ‘ 𝐻 ) )
18 inss2 ( 𝐺 ∩ ( ⊥ ‘ 𝐻 ) ) ⊆ ( ⊥ ‘ 𝐻 )
19 5 4 chsscon3i ( ( 𝐺 ∩ ( ⊥ ‘ 𝐻 ) ) ⊆ ( ⊥ ‘ 𝐻 ) ↔ ( ⊥ ‘ ( ⊥ ‘ 𝐻 ) ) ⊆ ( ⊥ ‘ ( 𝐺 ∩ ( ⊥ ‘ 𝐻 ) ) ) )
20 18 19 mpbi ( ⊥ ‘ ( ⊥ ‘ 𝐻 ) ) ⊆ ( ⊥ ‘ ( 𝐺 ∩ ( ⊥ ‘ 𝐻 ) ) )
21 17 20 sstri 𝐻 ⊆ ( ⊥ ‘ ( 𝐺 ∩ ( ⊥ ‘ 𝐻 ) ) )
22 1 2 pjclii ( ( proj𝐻 ) ‘ 𝐴 ) ∈ 𝐻
23 21 22 sselii ( ( proj𝐻 ) ‘ 𝐴 ) ∈ ( ⊥ ‘ ( 𝐺 ∩ ( ⊥ ‘ 𝐻 ) ) )
24 5 7 pjoc2i ( ( ( proj𝐻 ) ‘ 𝐴 ) ∈ ( ⊥ ‘ ( 𝐺 ∩ ( ⊥ ‘ 𝐻 ) ) ) ↔ ( ( proj ‘ ( 𝐺 ∩ ( ⊥ ‘ 𝐻 ) ) ) ‘ ( ( proj𝐻 ) ‘ 𝐴 ) ) = 0 )
25 23 24 mpbi ( ( proj ‘ ( 𝐺 ∩ ( ⊥ ‘ 𝐻 ) ) ) ‘ ( ( proj𝐻 ) ‘ 𝐴 ) ) = 0
26 25 oveq2i ( - 1 · ( ( proj ‘ ( 𝐺 ∩ ( ⊥ ‘ 𝐻 ) ) ) ‘ ( ( proj𝐻 ) ‘ 𝐴 ) ) ) = ( - 1 · 0 )
27 neg1cn - 1 ∈ ℂ
28 hvmul0 ( - 1 ∈ ℂ → ( - 1 · 0 ) = 0 )
29 27 28 ax-mp ( - 1 · 0 ) = 0
30 26 29 eqtri ( - 1 · ( ( proj ‘ ( 𝐺 ∩ ( ⊥ ‘ 𝐻 ) ) ) ‘ ( ( proj𝐻 ) ‘ 𝐴 ) ) ) = 0
31 14 30 oveq12i ( ( ( proj ‘ ( 𝐺 ∩ ( ⊥ ‘ 𝐻 ) ) ) ‘ ( ( proj𝐺 ) ‘ 𝐴 ) ) + ( - 1 · ( ( proj ‘ ( 𝐺 ∩ ( ⊥ ‘ 𝐻 ) ) ) ‘ ( ( proj𝐻 ) ‘ 𝐴 ) ) ) ) = ( ( ( proj ‘ ( 𝐺 ∩ ( ⊥ ‘ 𝐻 ) ) ) ‘ 𝐴 ) + 0 )
32 5 2 pjhclii ( ( proj ‘ ( 𝐺 ∩ ( ⊥ ‘ 𝐻 ) ) ) ‘ 𝐴 ) ∈ ℋ
33 ax-hvaddid ( ( ( proj ‘ ( 𝐺 ∩ ( ⊥ ‘ 𝐻 ) ) ) ‘ 𝐴 ) ∈ ℋ → ( ( ( proj ‘ ( 𝐺 ∩ ( ⊥ ‘ 𝐻 ) ) ) ‘ 𝐴 ) + 0 ) = ( ( proj ‘ ( 𝐺 ∩ ( ⊥ ‘ 𝐻 ) ) ) ‘ 𝐴 ) )
34 32 33 ax-mp ( ( ( proj ‘ ( 𝐺 ∩ ( ⊥ ‘ 𝐻 ) ) ) ‘ 𝐴 ) + 0 ) = ( ( proj ‘ ( 𝐺 ∩ ( ⊥ ‘ 𝐻 ) ) ) ‘ 𝐴 )
35 31 34 eqtri ( ( ( proj ‘ ( 𝐺 ∩ ( ⊥ ‘ 𝐻 ) ) ) ‘ ( ( proj𝐺 ) ‘ 𝐴 ) ) + ( - 1 · ( ( proj ‘ ( 𝐺 ∩ ( ⊥ ‘ 𝐻 ) ) ) ‘ ( ( proj𝐻 ) ‘ 𝐴 ) ) ) ) = ( ( proj ‘ ( 𝐺 ∩ ( ⊥ ‘ 𝐻 ) ) ) ‘ 𝐴 )
36 11 35 eqtri ( ( ( proj ‘ ( 𝐺 ∩ ( ⊥ ‘ 𝐻 ) ) ) ‘ ( ( proj𝐺 ) ‘ 𝐴 ) ) − ( ( proj ‘ ( 𝐺 ∩ ( ⊥ ‘ 𝐻 ) ) ) ‘ ( ( proj𝐻 ) ‘ 𝐴 ) ) ) = ( ( proj ‘ ( 𝐺 ∩ ( ⊥ ‘ 𝐻 ) ) ) ‘ 𝐴 )
37 8 36 eqtri ( ( proj ‘ ( 𝐺 ∩ ( ⊥ ‘ 𝐻 ) ) ) ‘ ( ( ( proj𝐺 ) ‘ 𝐴 ) − ( ( proj𝐻 ) ‘ 𝐴 ) ) ) = ( ( proj ‘ ( 𝐺 ∩ ( ⊥ ‘ 𝐻 ) ) ) ‘ 𝐴 )
38 3 2 pjclii ( ( proj𝐺 ) ‘ 𝐴 ) ∈ 𝐺
39 ssel ( 𝐻𝐺 → ( ( ( proj𝐻 ) ‘ 𝐴 ) ∈ 𝐻 → ( ( proj𝐻 ) ‘ 𝐴 ) ∈ 𝐺 ) )
40 22 39 mpi ( 𝐻𝐺 → ( ( proj𝐻 ) ‘ 𝐴 ) ∈ 𝐺 )
41 3 chshii 𝐺S
42 shsubcl ( ( 𝐺S ∧ ( ( proj𝐺 ) ‘ 𝐴 ) ∈ 𝐺 ∧ ( ( proj𝐻 ) ‘ 𝐴 ) ∈ 𝐺 ) → ( ( ( proj𝐺 ) ‘ 𝐴 ) − ( ( proj𝐻 ) ‘ 𝐴 ) ) ∈ 𝐺 )
43 41 42 mp3an1 ( ( ( ( proj𝐺 ) ‘ 𝐴 ) ∈ 𝐺 ∧ ( ( proj𝐻 ) ‘ 𝐴 ) ∈ 𝐺 ) → ( ( ( proj𝐺 ) ‘ 𝐴 ) − ( ( proj𝐻 ) ‘ 𝐴 ) ) ∈ 𝐺 )
44 38 40 43 sylancr ( 𝐻𝐺 → ( ( ( proj𝐺 ) ‘ 𝐴 ) − ( ( proj𝐻 ) ‘ 𝐴 ) ) ∈ 𝐺 )
45 1 2 3 pjsslem ( ( ( proj ‘ ( ⊥ ‘ 𝐻 ) ) ‘ 𝐴 ) − ( ( proj ‘ ( ⊥ ‘ 𝐺 ) ) ‘ 𝐴 ) ) = ( ( ( proj𝐺 ) ‘ 𝐴 ) − ( ( proj𝐻 ) ‘ 𝐴 ) )
46 1 3 chsscon3i ( 𝐻𝐺 ↔ ( ⊥ ‘ 𝐺 ) ⊆ ( ⊥ ‘ 𝐻 ) )
47 4 2 pjclii ( ( proj ‘ ( ⊥ ‘ 𝐻 ) ) ‘ 𝐴 ) ∈ ( ⊥ ‘ 𝐻 )
48 3 choccli ( ⊥ ‘ 𝐺 ) ∈ C
49 48 2 pjclii ( ( proj ‘ ( ⊥ ‘ 𝐺 ) ) ‘ 𝐴 ) ∈ ( ⊥ ‘ 𝐺 )
50 ssel ( ( ⊥ ‘ 𝐺 ) ⊆ ( ⊥ ‘ 𝐻 ) → ( ( ( proj ‘ ( ⊥ ‘ 𝐺 ) ) ‘ 𝐴 ) ∈ ( ⊥ ‘ 𝐺 ) → ( ( proj ‘ ( ⊥ ‘ 𝐺 ) ) ‘ 𝐴 ) ∈ ( ⊥ ‘ 𝐻 ) ) )
51 49 50 mpi ( ( ⊥ ‘ 𝐺 ) ⊆ ( ⊥ ‘ 𝐻 ) → ( ( proj ‘ ( ⊥ ‘ 𝐺 ) ) ‘ 𝐴 ) ∈ ( ⊥ ‘ 𝐻 ) )
52 4 chshii ( ⊥ ‘ 𝐻 ) ∈ S
53 shsubcl ( ( ( ⊥ ‘ 𝐻 ) ∈ S ∧ ( ( proj ‘ ( ⊥ ‘ 𝐻 ) ) ‘ 𝐴 ) ∈ ( ⊥ ‘ 𝐻 ) ∧ ( ( proj ‘ ( ⊥ ‘ 𝐺 ) ) ‘ 𝐴 ) ∈ ( ⊥ ‘ 𝐻 ) ) → ( ( ( proj ‘ ( ⊥ ‘ 𝐻 ) ) ‘ 𝐴 ) − ( ( proj ‘ ( ⊥ ‘ 𝐺 ) ) ‘ 𝐴 ) ) ∈ ( ⊥ ‘ 𝐻 ) )
54 52 53 mp3an1 ( ( ( ( proj ‘ ( ⊥ ‘ 𝐻 ) ) ‘ 𝐴 ) ∈ ( ⊥ ‘ 𝐻 ) ∧ ( ( proj ‘ ( ⊥ ‘ 𝐺 ) ) ‘ 𝐴 ) ∈ ( ⊥ ‘ 𝐻 ) ) → ( ( ( proj ‘ ( ⊥ ‘ 𝐻 ) ) ‘ 𝐴 ) − ( ( proj ‘ ( ⊥ ‘ 𝐺 ) ) ‘ 𝐴 ) ) ∈ ( ⊥ ‘ 𝐻 ) )
55 47 51 54 sylancr ( ( ⊥ ‘ 𝐺 ) ⊆ ( ⊥ ‘ 𝐻 ) → ( ( ( proj ‘ ( ⊥ ‘ 𝐻 ) ) ‘ 𝐴 ) − ( ( proj ‘ ( ⊥ ‘ 𝐺 ) ) ‘ 𝐴 ) ) ∈ ( ⊥ ‘ 𝐻 ) )
56 46 55 sylbi ( 𝐻𝐺 → ( ( ( proj ‘ ( ⊥ ‘ 𝐻 ) ) ‘ 𝐴 ) − ( ( proj ‘ ( ⊥ ‘ 𝐺 ) ) ‘ 𝐴 ) ) ∈ ( ⊥ ‘ 𝐻 ) )
57 45 56 eqeltrrid ( 𝐻𝐺 → ( ( ( proj𝐺 ) ‘ 𝐴 ) − ( ( proj𝐻 ) ‘ 𝐴 ) ) ∈ ( ⊥ ‘ 𝐻 ) )
58 44 57 jca ( 𝐻𝐺 → ( ( ( ( proj𝐺 ) ‘ 𝐴 ) − ( ( proj𝐻 ) ‘ 𝐴 ) ) ∈ 𝐺 ∧ ( ( ( proj𝐺 ) ‘ 𝐴 ) − ( ( proj𝐻 ) ‘ 𝐴 ) ) ∈ ( ⊥ ‘ 𝐻 ) ) )
59 elin ( ( ( ( proj𝐺 ) ‘ 𝐴 ) − ( ( proj𝐻 ) ‘ 𝐴 ) ) ∈ ( 𝐺 ∩ ( ⊥ ‘ 𝐻 ) ) ↔ ( ( ( ( proj𝐺 ) ‘ 𝐴 ) − ( ( proj𝐻 ) ‘ 𝐴 ) ) ∈ 𝐺 ∧ ( ( ( proj𝐺 ) ‘ 𝐴 ) − ( ( proj𝐻 ) ‘ 𝐴 ) ) ∈ ( ⊥ ‘ 𝐻 ) ) )
60 6 7 hvsubcli ( ( ( proj𝐺 ) ‘ 𝐴 ) − ( ( proj𝐻 ) ‘ 𝐴 ) ) ∈ ℋ
61 5 60 pjchi ( ( ( ( proj𝐺 ) ‘ 𝐴 ) − ( ( proj𝐻 ) ‘ 𝐴 ) ) ∈ ( 𝐺 ∩ ( ⊥ ‘ 𝐻 ) ) ↔ ( ( proj ‘ ( 𝐺 ∩ ( ⊥ ‘ 𝐻 ) ) ) ‘ ( ( ( proj𝐺 ) ‘ 𝐴 ) − ( ( proj𝐻 ) ‘ 𝐴 ) ) ) = ( ( ( proj𝐺 ) ‘ 𝐴 ) − ( ( proj𝐻 ) ‘ 𝐴 ) ) )
62 59 61 bitr3i ( ( ( ( ( proj𝐺 ) ‘ 𝐴 ) − ( ( proj𝐻 ) ‘ 𝐴 ) ) ∈ 𝐺 ∧ ( ( ( proj𝐺 ) ‘ 𝐴 ) − ( ( proj𝐻 ) ‘ 𝐴 ) ) ∈ ( ⊥ ‘ 𝐻 ) ) ↔ ( ( proj ‘ ( 𝐺 ∩ ( ⊥ ‘ 𝐻 ) ) ) ‘ ( ( ( proj𝐺 ) ‘ 𝐴 ) − ( ( proj𝐻 ) ‘ 𝐴 ) ) ) = ( ( ( proj𝐺 ) ‘ 𝐴 ) − ( ( proj𝐻 ) ‘ 𝐴 ) ) )
63 58 62 sylib ( 𝐻𝐺 → ( ( proj ‘ ( 𝐺 ∩ ( ⊥ ‘ 𝐻 ) ) ) ‘ ( ( ( proj𝐺 ) ‘ 𝐴 ) − ( ( proj𝐻 ) ‘ 𝐴 ) ) ) = ( ( ( proj𝐺 ) ‘ 𝐴 ) − ( ( proj𝐻 ) ‘ 𝐴 ) ) )
64 37 63 syl5reqr ( 𝐻𝐺 → ( ( ( proj𝐺 ) ‘ 𝐴 ) − ( ( proj𝐻 ) ‘ 𝐴 ) ) = ( ( proj ‘ ( 𝐺 ∩ ( ⊥ ‘ 𝐻 ) ) ) ‘ 𝐴 ) )