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}\in {\mathbf{C}}_{ℋ}$
pjidm.2 ${⊢}{A}\in ℋ$
pjsslem.1 ${⊢}{G}\in {\mathbf{C}}_{ℋ}$
Assertion pjssmii ${⊢}{H}\subseteq {G}\to {\mathrm{proj}}_{ℎ}\left({G}\right)\left({A}\right){-}_{ℎ}{\mathrm{proj}}_{ℎ}\left({H}\right)\left({A}\right)={\mathrm{proj}}_{ℎ}\left({G}\cap \perp \left({H}\right)\right)\left({A}\right)$

Proof

Step Hyp Ref Expression
1 pjidm.1 ${⊢}{H}\in {\mathbf{C}}_{ℋ}$
2 pjidm.2 ${⊢}{A}\in ℋ$
3 pjsslem.1 ${⊢}{G}\in {\mathbf{C}}_{ℋ}$
4 1 choccli ${⊢}\perp \left({H}\right)\in {\mathbf{C}}_{ℋ}$
5 3 4 chincli ${⊢}{G}\cap \perp \left({H}\right)\in {\mathbf{C}}_{ℋ}$
6 3 2 pjhclii ${⊢}{\mathrm{proj}}_{ℎ}\left({G}\right)\left({A}\right)\in ℋ$
7 1 2 pjhclii ${⊢}{\mathrm{proj}}_{ℎ}\left({H}\right)\left({A}\right)\in ℋ$
8 5 6 7 pjsubii ${⊢}{\mathrm{proj}}_{ℎ}\left({G}\cap \perp \left({H}\right)\right)\left({\mathrm{proj}}_{ℎ}\left({G}\right)\left({A}\right){-}_{ℎ}{\mathrm{proj}}_{ℎ}\left({H}\right)\left({A}\right)\right)={\mathrm{proj}}_{ℎ}\left({G}\cap \perp \left({H}\right)\right)\left({\mathrm{proj}}_{ℎ}\left({G}\right)\left({A}\right)\right){-}_{ℎ}{\mathrm{proj}}_{ℎ}\left({G}\cap \perp \left({H}\right)\right)\left({\mathrm{proj}}_{ℎ}\left({H}\right)\left({A}\right)\right)$
9 5 6 pjhclii ${⊢}{\mathrm{proj}}_{ℎ}\left({G}\cap \perp \left({H}\right)\right)\left({\mathrm{proj}}_{ℎ}\left({G}\right)\left({A}\right)\right)\in ℋ$
10 5 7 pjhclii ${⊢}{\mathrm{proj}}_{ℎ}\left({G}\cap \perp \left({H}\right)\right)\left({\mathrm{proj}}_{ℎ}\left({H}\right)\left({A}\right)\right)\in ℋ$
11 9 10 hvsubvali ${⊢}{\mathrm{proj}}_{ℎ}\left({G}\cap \perp \left({H}\right)\right)\left({\mathrm{proj}}_{ℎ}\left({G}\right)\left({A}\right)\right){-}_{ℎ}{\mathrm{proj}}_{ℎ}\left({G}\cap \perp \left({H}\right)\right)\left({\mathrm{proj}}_{ℎ}\left({H}\right)\left({A}\right)\right)={\mathrm{proj}}_{ℎ}\left({G}\cap \perp \left({H}\right)\right)\left({\mathrm{proj}}_{ℎ}\left({G}\right)\left({A}\right)\right){+}_{ℎ}\left(-1{\cdot }_{ℎ}{\mathrm{proj}}_{ℎ}\left({G}\cap \perp \left({H}\right)\right)\left({\mathrm{proj}}_{ℎ}\left({H}\right)\left({A}\right)\right)\right)$
12 inss1 ${⊢}{G}\cap \perp \left({H}\right)\subseteq {G}$
13 5 2 3 pjss2i ${⊢}{G}\cap \perp \left({H}\right)\subseteq {G}\to {\mathrm{proj}}_{ℎ}\left({G}\cap \perp \left({H}\right)\right)\left({\mathrm{proj}}_{ℎ}\left({G}\right)\left({A}\right)\right)={\mathrm{proj}}_{ℎ}\left({G}\cap \perp \left({H}\right)\right)\left({A}\right)$
14 12 13 ax-mp ${⊢}{\mathrm{proj}}_{ℎ}\left({G}\cap \perp \left({H}\right)\right)\left({\mathrm{proj}}_{ℎ}\left({G}\right)\left({A}\right)\right)={\mathrm{proj}}_{ℎ}\left({G}\cap \perp \left({H}\right)\right)\left({A}\right)$
15 1 chshii ${⊢}{H}\in {\mathbf{S}}_{ℋ}$
16 shococss ${⊢}{H}\in {\mathbf{S}}_{ℋ}\to {H}\subseteq \perp \left(\perp \left({H}\right)\right)$
17 15 16 ax-mp ${⊢}{H}\subseteq \perp \left(\perp \left({H}\right)\right)$
18 inss2 ${⊢}{G}\cap \perp \left({H}\right)\subseteq \perp \left({H}\right)$
19 5 4 chsscon3i ${⊢}{G}\cap \perp \left({H}\right)\subseteq \perp \left({H}\right)↔\perp \left(\perp \left({H}\right)\right)\subseteq \perp \left({G}\cap \perp \left({H}\right)\right)$
20 18 19 mpbi ${⊢}\perp \left(\perp \left({H}\right)\right)\subseteq \perp \left({G}\cap \perp \left({H}\right)\right)$
21 17 20 sstri ${⊢}{H}\subseteq \perp \left({G}\cap \perp \left({H}\right)\right)$
22 1 2 pjclii ${⊢}{\mathrm{proj}}_{ℎ}\left({H}\right)\left({A}\right)\in {H}$
23 21 22 sselii ${⊢}{\mathrm{proj}}_{ℎ}\left({H}\right)\left({A}\right)\in \perp \left({G}\cap \perp \left({H}\right)\right)$
24 5 7 pjoc2i ${⊢}{\mathrm{proj}}_{ℎ}\left({H}\right)\left({A}\right)\in \perp \left({G}\cap \perp \left({H}\right)\right)↔{\mathrm{proj}}_{ℎ}\left({G}\cap \perp \left({H}\right)\right)\left({\mathrm{proj}}_{ℎ}\left({H}\right)\left({A}\right)\right)={0}_{ℎ}$
25 23 24 mpbi ${⊢}{\mathrm{proj}}_{ℎ}\left({G}\cap \perp \left({H}\right)\right)\left({\mathrm{proj}}_{ℎ}\left({H}\right)\left({A}\right)\right)={0}_{ℎ}$
26 25 oveq2i ${⊢}-1{\cdot }_{ℎ}{\mathrm{proj}}_{ℎ}\left({G}\cap \perp \left({H}\right)\right)\left({\mathrm{proj}}_{ℎ}\left({H}\right)\left({A}\right)\right)=-1{\cdot }_{ℎ}{0}_{ℎ}$
27 neg1cn ${⊢}-1\in ℂ$
28 hvmul0 ${⊢}-1\in ℂ\to -1{\cdot }_{ℎ}{0}_{ℎ}={0}_{ℎ}$
29 27 28 ax-mp ${⊢}-1{\cdot }_{ℎ}{0}_{ℎ}={0}_{ℎ}$
30 26 29 eqtri ${⊢}-1{\cdot }_{ℎ}{\mathrm{proj}}_{ℎ}\left({G}\cap \perp \left({H}\right)\right)\left({\mathrm{proj}}_{ℎ}\left({H}\right)\left({A}\right)\right)={0}_{ℎ}$
31 14 30 oveq12i ${⊢}{\mathrm{proj}}_{ℎ}\left({G}\cap \perp \left({H}\right)\right)\left({\mathrm{proj}}_{ℎ}\left({G}\right)\left({A}\right)\right){+}_{ℎ}\left(-1{\cdot }_{ℎ}{\mathrm{proj}}_{ℎ}\left({G}\cap \perp \left({H}\right)\right)\left({\mathrm{proj}}_{ℎ}\left({H}\right)\left({A}\right)\right)\right)={\mathrm{proj}}_{ℎ}\left({G}\cap \perp \left({H}\right)\right)\left({A}\right){+}_{ℎ}{0}_{ℎ}$
32 5 2 pjhclii ${⊢}{\mathrm{proj}}_{ℎ}\left({G}\cap \perp \left({H}\right)\right)\left({A}\right)\in ℋ$
33 ax-hvaddid ${⊢}{\mathrm{proj}}_{ℎ}\left({G}\cap \perp \left({H}\right)\right)\left({A}\right)\in ℋ\to {\mathrm{proj}}_{ℎ}\left({G}\cap \perp \left({H}\right)\right)\left({A}\right){+}_{ℎ}{0}_{ℎ}={\mathrm{proj}}_{ℎ}\left({G}\cap \perp \left({H}\right)\right)\left({A}\right)$
34 32 33 ax-mp ${⊢}{\mathrm{proj}}_{ℎ}\left({G}\cap \perp \left({H}\right)\right)\left({A}\right){+}_{ℎ}{0}_{ℎ}={\mathrm{proj}}_{ℎ}\left({G}\cap \perp \left({H}\right)\right)\left({A}\right)$
35 31 34 eqtri ${⊢}{\mathrm{proj}}_{ℎ}\left({G}\cap \perp \left({H}\right)\right)\left({\mathrm{proj}}_{ℎ}\left({G}\right)\left({A}\right)\right){+}_{ℎ}\left(-1{\cdot }_{ℎ}{\mathrm{proj}}_{ℎ}\left({G}\cap \perp \left({H}\right)\right)\left({\mathrm{proj}}_{ℎ}\left({H}\right)\left({A}\right)\right)\right)={\mathrm{proj}}_{ℎ}\left({G}\cap \perp \left({H}\right)\right)\left({A}\right)$
36 11 35 eqtri ${⊢}{\mathrm{proj}}_{ℎ}\left({G}\cap \perp \left({H}\right)\right)\left({\mathrm{proj}}_{ℎ}\left({G}\right)\left({A}\right)\right){-}_{ℎ}{\mathrm{proj}}_{ℎ}\left({G}\cap \perp \left({H}\right)\right)\left({\mathrm{proj}}_{ℎ}\left({H}\right)\left({A}\right)\right)={\mathrm{proj}}_{ℎ}\left({G}\cap \perp \left({H}\right)\right)\left({A}\right)$
37 8 36 eqtri ${⊢}{\mathrm{proj}}_{ℎ}\left({G}\cap \perp \left({H}\right)\right)\left({\mathrm{proj}}_{ℎ}\left({G}\right)\left({A}\right){-}_{ℎ}{\mathrm{proj}}_{ℎ}\left({H}\right)\left({A}\right)\right)={\mathrm{proj}}_{ℎ}\left({G}\cap \perp \left({H}\right)\right)\left({A}\right)$
38 3 2 pjclii ${⊢}{\mathrm{proj}}_{ℎ}\left({G}\right)\left({A}\right)\in {G}$
39 ssel ${⊢}{H}\subseteq {G}\to \left({\mathrm{proj}}_{ℎ}\left({H}\right)\left({A}\right)\in {H}\to {\mathrm{proj}}_{ℎ}\left({H}\right)\left({A}\right)\in {G}\right)$
40 22 39 mpi ${⊢}{H}\subseteq {G}\to {\mathrm{proj}}_{ℎ}\left({H}\right)\left({A}\right)\in {G}$
41 3 chshii ${⊢}{G}\in {\mathbf{S}}_{ℋ}$
42 shsubcl ${⊢}\left({G}\in {\mathbf{S}}_{ℋ}\wedge {\mathrm{proj}}_{ℎ}\left({G}\right)\left({A}\right)\in {G}\wedge {\mathrm{proj}}_{ℎ}\left({H}\right)\left({A}\right)\in {G}\right)\to {\mathrm{proj}}_{ℎ}\left({G}\right)\left({A}\right){-}_{ℎ}{\mathrm{proj}}_{ℎ}\left({H}\right)\left({A}\right)\in {G}$
43 41 42 mp3an1 ${⊢}\left({\mathrm{proj}}_{ℎ}\left({G}\right)\left({A}\right)\in {G}\wedge {\mathrm{proj}}_{ℎ}\left({H}\right)\left({A}\right)\in {G}\right)\to {\mathrm{proj}}_{ℎ}\left({G}\right)\left({A}\right){-}_{ℎ}{\mathrm{proj}}_{ℎ}\left({H}\right)\left({A}\right)\in {G}$
44 38 40 43 sylancr ${⊢}{H}\subseteq {G}\to {\mathrm{proj}}_{ℎ}\left({G}\right)\left({A}\right){-}_{ℎ}{\mathrm{proj}}_{ℎ}\left({H}\right)\left({A}\right)\in {G}$
45 1 2 3 pjsslem ${⊢}{\mathrm{proj}}_{ℎ}\left(\perp \left({H}\right)\right)\left({A}\right){-}_{ℎ}{\mathrm{proj}}_{ℎ}\left(\perp \left({G}\right)\right)\left({A}\right)={\mathrm{proj}}_{ℎ}\left({G}\right)\left({A}\right){-}_{ℎ}{\mathrm{proj}}_{ℎ}\left({H}\right)\left({A}\right)$
46 1 3 chsscon3i ${⊢}{H}\subseteq {G}↔\perp \left({G}\right)\subseteq \perp \left({H}\right)$
47 4 2 pjclii ${⊢}{\mathrm{proj}}_{ℎ}\left(\perp \left({H}\right)\right)\left({A}\right)\in \perp \left({H}\right)$
48 3 choccli ${⊢}\perp \left({G}\right)\in {\mathbf{C}}_{ℋ}$
49 48 2 pjclii ${⊢}{\mathrm{proj}}_{ℎ}\left(\perp \left({G}\right)\right)\left({A}\right)\in \perp \left({G}\right)$
50 ssel ${⊢}\perp \left({G}\right)\subseteq \perp \left({H}\right)\to \left({\mathrm{proj}}_{ℎ}\left(\perp \left({G}\right)\right)\left({A}\right)\in \perp \left({G}\right)\to {\mathrm{proj}}_{ℎ}\left(\perp \left({G}\right)\right)\left({A}\right)\in \perp \left({H}\right)\right)$
51 49 50 mpi ${⊢}\perp \left({G}\right)\subseteq \perp \left({H}\right)\to {\mathrm{proj}}_{ℎ}\left(\perp \left({G}\right)\right)\left({A}\right)\in \perp \left({H}\right)$
52 4 chshii ${⊢}\perp \left({H}\right)\in {\mathbf{S}}_{ℋ}$
53 shsubcl ${⊢}\left(\perp \left({H}\right)\in {\mathbf{S}}_{ℋ}\wedge {\mathrm{proj}}_{ℎ}\left(\perp \left({H}\right)\right)\left({A}\right)\in \perp \left({H}\right)\wedge {\mathrm{proj}}_{ℎ}\left(\perp \left({G}\right)\right)\left({A}\right)\in \perp \left({H}\right)\right)\to {\mathrm{proj}}_{ℎ}\left(\perp \left({H}\right)\right)\left({A}\right){-}_{ℎ}{\mathrm{proj}}_{ℎ}\left(\perp \left({G}\right)\right)\left({A}\right)\in \perp \left({H}\right)$
54 52 53 mp3an1 ${⊢}\left({\mathrm{proj}}_{ℎ}\left(\perp \left({H}\right)\right)\left({A}\right)\in \perp \left({H}\right)\wedge {\mathrm{proj}}_{ℎ}\left(\perp \left({G}\right)\right)\left({A}\right)\in \perp \left({H}\right)\right)\to {\mathrm{proj}}_{ℎ}\left(\perp \left({H}\right)\right)\left({A}\right){-}_{ℎ}{\mathrm{proj}}_{ℎ}\left(\perp \left({G}\right)\right)\left({A}\right)\in \perp \left({H}\right)$
55 47 51 54 sylancr ${⊢}\perp \left({G}\right)\subseteq \perp \left({H}\right)\to {\mathrm{proj}}_{ℎ}\left(\perp \left({H}\right)\right)\left({A}\right){-}_{ℎ}{\mathrm{proj}}_{ℎ}\left(\perp \left({G}\right)\right)\left({A}\right)\in \perp \left({H}\right)$
56 46 55 sylbi ${⊢}{H}\subseteq {G}\to {\mathrm{proj}}_{ℎ}\left(\perp \left({H}\right)\right)\left({A}\right){-}_{ℎ}{\mathrm{proj}}_{ℎ}\left(\perp \left({G}\right)\right)\left({A}\right)\in \perp \left({H}\right)$
57 45 56 eqeltrrid ${⊢}{H}\subseteq {G}\to {\mathrm{proj}}_{ℎ}\left({G}\right)\left({A}\right){-}_{ℎ}{\mathrm{proj}}_{ℎ}\left({H}\right)\left({A}\right)\in \perp \left({H}\right)$
58 44 57 jca ${⊢}{H}\subseteq {G}\to \left({\mathrm{proj}}_{ℎ}\left({G}\right)\left({A}\right){-}_{ℎ}{\mathrm{proj}}_{ℎ}\left({H}\right)\left({A}\right)\in {G}\wedge {\mathrm{proj}}_{ℎ}\left({G}\right)\left({A}\right){-}_{ℎ}{\mathrm{proj}}_{ℎ}\left({H}\right)\left({A}\right)\in \perp \left({H}\right)\right)$
59 elin ${⊢}{\mathrm{proj}}_{ℎ}\left({G}\right)\left({A}\right){-}_{ℎ}{\mathrm{proj}}_{ℎ}\left({H}\right)\left({A}\right)\in \left({G}\cap \perp \left({H}\right)\right)↔\left({\mathrm{proj}}_{ℎ}\left({G}\right)\left({A}\right){-}_{ℎ}{\mathrm{proj}}_{ℎ}\left({H}\right)\left({A}\right)\in {G}\wedge {\mathrm{proj}}_{ℎ}\left({G}\right)\left({A}\right){-}_{ℎ}{\mathrm{proj}}_{ℎ}\left({H}\right)\left({A}\right)\in \perp \left({H}\right)\right)$
60 6 7 hvsubcli ${⊢}{\mathrm{proj}}_{ℎ}\left({G}\right)\left({A}\right){-}_{ℎ}{\mathrm{proj}}_{ℎ}\left({H}\right)\left({A}\right)\in ℋ$
61 5 60 pjchi ${⊢}{\mathrm{proj}}_{ℎ}\left({G}\right)\left({A}\right){-}_{ℎ}{\mathrm{proj}}_{ℎ}\left({H}\right)\left({A}\right)\in \left({G}\cap \perp \left({H}\right)\right)↔{\mathrm{proj}}_{ℎ}\left({G}\cap \perp \left({H}\right)\right)\left({\mathrm{proj}}_{ℎ}\left({G}\right)\left({A}\right){-}_{ℎ}{\mathrm{proj}}_{ℎ}\left({H}\right)\left({A}\right)\right)={\mathrm{proj}}_{ℎ}\left({G}\right)\left({A}\right){-}_{ℎ}{\mathrm{proj}}_{ℎ}\left({H}\right)\left({A}\right)$
62 59 61 bitr3i ${⊢}\left({\mathrm{proj}}_{ℎ}\left({G}\right)\left({A}\right){-}_{ℎ}{\mathrm{proj}}_{ℎ}\left({H}\right)\left({A}\right)\in {G}\wedge {\mathrm{proj}}_{ℎ}\left({G}\right)\left({A}\right){-}_{ℎ}{\mathrm{proj}}_{ℎ}\left({H}\right)\left({A}\right)\in \perp \left({H}\right)\right)↔{\mathrm{proj}}_{ℎ}\left({G}\cap \perp \left({H}\right)\right)\left({\mathrm{proj}}_{ℎ}\left({G}\right)\left({A}\right){-}_{ℎ}{\mathrm{proj}}_{ℎ}\left({H}\right)\left({A}\right)\right)={\mathrm{proj}}_{ℎ}\left({G}\right)\left({A}\right){-}_{ℎ}{\mathrm{proj}}_{ℎ}\left({H}\right)\left({A}\right)$
63 58 62 sylib ${⊢}{H}\subseteq {G}\to {\mathrm{proj}}_{ℎ}\left({G}\cap \perp \left({H}\right)\right)\left({\mathrm{proj}}_{ℎ}\left({G}\right)\left({A}\right){-}_{ℎ}{\mathrm{proj}}_{ℎ}\left({H}\right)\left({A}\right)\right)={\mathrm{proj}}_{ℎ}\left({G}\right)\left({A}\right){-}_{ℎ}{\mathrm{proj}}_{ℎ}\left({H}\right)\left({A}\right)$
64 37 63 syl5reqr ${⊢}{H}\subseteq {G}\to {\mathrm{proj}}_{ℎ}\left({G}\right)\left({A}\right){-}_{ℎ}{\mathrm{proj}}_{ℎ}\left({H}\right)\left({A}\right)={\mathrm{proj}}_{ℎ}\left({G}\cap \perp \left({H}\right)\right)\left({A}\right)$