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	3 2	pjclii	$$⊢{\mathrm{proj}}_{ℎ}\left(G\right)\left(A\right)\in G$$
5	1 2	pjclii	$$⊢{\mathrm{proj}}_{ℎ}\left(H\right)\left(A\right)\in H$$
6		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)$$
7	5 6	mpi	$$⊢H\subseteq G\to {\mathrm{proj}}_{ℎ}\left(H\right)\left(A\right)\in G$$
8	3	chshii	$$⊢G\in {\mathbf{S}}_{\mathscr{H}}$$
9		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$$
10	8 9	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$$
11	4 7 10	sylancr	$$⊢H\subseteq G\to {\mathrm{proj}}_{ℎ}\left(G\right)\left(A\right){-}_{ℎ}{\mathrm{proj}}_{ℎ}\left(H\right)\left(A\right)\in G$$
12	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)$$
13	1 3	chsscon3i	$$⊢H\subseteq G\leftrightarrow \perp \left(G\right)\subseteq \perp \left(H\right)$$
14	1	choccli	$$⊢\perp \left(H\right)\in {\mathbf{C}}_{\mathscr{H}}$$
15	14 2	pjclii	$$⊢{\mathrm{proj}}_{ℎ}\left(\perp \left(H\right)\right)\left(A\right)\in \perp \left(H\right)$$
16	3	choccli	$$⊢\perp \left(G\right)\in {\mathbf{C}}_{\mathscr{H}}$$
17	16 2	pjclii	$$⊢{\mathrm{proj}}_{ℎ}\left(\perp \left(G\right)\right)\left(A\right)\in \perp \left(G\right)$$
18		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)$$
19	17 18	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)$$
20	14	chshii	$$⊢\perp \left(H\right)\in {\mathbf{S}}_{\mathscr{H}}$$
21		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)$$
22	20 21	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)$$
23	15 19 22	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)$$
24	13 23	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)$$
25	12 24	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)$$
26	11 25	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)$$
27		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)$$
28	3 14	chincli	$$⊢G\cap \perp \left(H\right)\in {\mathbf{C}}_{\mathscr{H}}$$
29	3 2	pjhclii	$$⊢{\mathrm{proj}}_{ℎ}\left(G\right)\left(A\right)\in \mathscr{H}$$
30	1 2	pjhclii	$$⊢{\mathrm{proj}}_{ℎ}\left(H\right)\left(A\right)\in \mathscr{H}$$
31	29 30	hvsubcli	$$⊢{\mathrm{proj}}_{ℎ}\left(G\right)\left(A\right){-}_{ℎ}{\mathrm{proj}}_{ℎ}\left(H\right)\left(A\right)\in \mathscr{H}$$
32	28 31	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)$$
33	27 32	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)$$
34	26 33	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)$$
35	28 29 30	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)$$
36	28 29	pjhclii	$$⊢{\mathrm{proj}}_{ℎ}\left(G\cap \perp \left(H\right)\right)\left({\mathrm{proj}}_{ℎ}\left(G\right)\left(A\right)\right)\in \mathscr{H}$$
37	28 30	pjhclii	$$⊢{\mathrm{proj}}_{ℎ}\left(G\cap \perp \left(H\right)\right)\left({\mathrm{proj}}_{ℎ}\left(H\right)\left(A\right)\right)\in \mathscr{H}$$
38	36 37	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)$$
39		inss1	$$⊢G\cap \perp \left(H\right)\subseteq G$$
40	28 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)$$
41	39 40	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)$$
42	1	chshii	$$⊢H\in {\mathbf{S}}_{\mathscr{H}}$$
43		shococss	$$⊢H\in {\mathbf{S}}_{\mathscr{H}}\to H\subseteq \perp \left(\perp \left(H\right)\right)$$
44	42 43	ax-mp	$$⊢H\subseteq \perp \left(\perp \left(H\right)\right)$$
45		inss2	$$⊢G\cap \perp \left(H\right)\subseteq \perp \left(H\right)$$
46	28 14	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)$$
47	45 46	mpbi	$$⊢\perp \left(\perp \left(H\right)\right)\subseteq \perp \left(G\cap \perp \left(H\right)\right)$$
48	44 47	sstri	$$⊢H\subseteq \perp \left(G\cap \perp \left(H\right)\right)$$
49	48 5	sselii	$$⊢{\mathrm{proj}}_{ℎ}\left(H\right)\left(A\right)\in \perp \left(G\cap \perp \left(H\right)\right)$$
50	28 30	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_{ℎ}$$
51	49 50	mpbi	$$⊢{\mathrm{proj}}_{ℎ}\left(G\cap \perp \left(H\right)\right)\left({\mathrm{proj}}_{ℎ}\left(H\right)\left(A\right)\right)=0_{ℎ}$$
52	51	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}_{ℎ}$$
53		neg1cn	$$⊢-1\in ℂ$$
54		hvmul0	$$⊢-1\in ℂ\to -1{\cdot }_{ℎ}{0}_{ℎ}=0_{ℎ}$$
55	53 54	ax-mp	$$⊢-1{\cdot }_{ℎ}{0}_{ℎ}=0_{ℎ}$$
56	52 55	eqtri	$$⊢-1{\cdot }_{ℎ}{\mathrm{proj}}_{ℎ}\left(G\cap \perp \left(H\right)\right)\left({\mathrm{proj}}_{ℎ}\left(H\right)\left(A\right)\right)=0_{ℎ}$$
57	41 56	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}_{ℎ}$$
58	28 2	pjhclii	$$⊢{\mathrm{proj}}_{ℎ}\left(G\cap \perp \left(H\right)\right)\left(A\right)\in \mathscr{H}$$
59		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)$$
60	58 59	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)$$
61	57 60	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)$$
62	38 61	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)$$
63	35 62	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)$$
64	34 63	eqtr3di	$$⊢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)$$