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ℎ ‘ ( 𝐺 ∩ ( ⊥ ‘ 𝐻 ) ) ) ‘ 𝐴 ) )