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