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}}_{\mathscr{H}}$$
	pjidm.2	$$⊢A\in \mathscr{H}$$
	pjsslem.1	$$⊢G\in {\mathbf{C}}_{\mathscr{H}}$$
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}}_{\mathscr{H}}$$
2		pjidm.2	$$⊢A\in \mathscr{H}$$
3		pjsslem.1	$$⊢G\in {\mathbf{C}}_{\mathscr{H}}$$
4	1	choccli	$$⊢\perp \left(H\right)\in {\mathbf{C}}_{\mathscr{H}}$$
5	3 4	chincli	$$⊢G\cap \perp \left(H\right)\in {\mathbf{C}}_{\mathscr{H}}$$
6	3 2	pjhclii	$$⊢{\mathrm{proj}}_{ℎ}\left(G\right)\left(A\right)\in \mathscr{H}$$
7	1 2	pjhclii	$$⊢{\mathrm{proj}}_{ℎ}\left(H\right)\left(A\right)\in \mathscr{H}$$
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 \mathscr{H}$$
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 \mathscr{H}$$
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}}_{\mathscr{H}}$$
16		shococss	$$⊢H\in {\mathbf{S}}_{\mathscr{H}}\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)\leftrightarrow \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)\leftrightarrow {\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 \mathscr{H}$$
33		ax-hvaddid	$$⊢{\mathrm{proj}}_{ℎ}\left(G\cap \perp \left(H\right)\right)\left(A\right)\in \mathscr{H}\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}}_{\mathscr{H}}$$
42		shsubcl	$$⊢\left(G\in {\mathbf{S}}_{\mathscr{H}}\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\leftrightarrow \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}}_{\mathscr{H}}$$
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}}_{\mathscr{H}}$$
53		shsubcl	$$⊢\left(\perp \left(H\right)\in {\mathbf{S}}_{\mathscr{H}}\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)\leftrightarrow \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 \mathscr{H}$$
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)\leftrightarrow {\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)\leftrightarrow {\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)$$