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 ⊢H∈Cℋ
pjidm.2 ⊢A∈ℋ
pjsslem.1 ⊢G∈Cℋ
Assertion pjssmii ⊢H⊆G→projℎ⁡G⁡A-ℎprojℎ⁡H⁡A=projℎ⁡G∩⊥⁡H⁡A

Proof

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