Theorem dihjatc

Description: Isomorphism H of lattice join of an element under the fiducial hyperplane with atom not under it. (Contributed by NM, 26-Aug-2014)

	Ref	Expression
Hypotheses	dihjatc.b	$$⊢B={\mathrm{Base}}_K$$
	dihjatc.l	$$⊢\underset{\dot{}}{\le }={\le }_K$$
	dihjatc.h	$$⊢H=\mathrm{LHyp}\left(K\right)$$
	dihjatc.j	$$⊢\underset{\dot{}}{\vee }=\mathrm{join}\left(K\right)$$
	dihjatc.a	$$⊢A=\mathrm{Atoms}\left(K\right)$$
	dihjatc.u	$$⊢U=\mathrm{DVecH}\left(K\right)\left(W\right)$$
	dihjatc.s	$$⊢\underset{\dot{}}{\oplus }=\mathrm{LSSum}\left(U\right)$$
	dihjatc.i	$$⊢I=\mathrm{DIsoH}\left(K\right)\left(W\right)$$
	dihjatc.k	$$⊢\phi \to \left(K\in \mathrm{HL}\wedge W\in H\right)$$
	dihjatc.x	$$⊢\phi \to \left(X\in B\wedge X\underset{\dot{}}{\le }W\right)$$
	dihjatc.p	$$⊢\phi \to \left(P\in A\wedge \neg P\underset{\dot{}}{\le }W\right)$$
Assertion	dihjatc	$$⊢\phi \to I\left(X\underset{\dot{}}{\vee }P\right)=I\left(X\right)\underset{\dot{}}{\oplus }I\left(P\right)$$

Proof

Step	Hyp	Ref	Expression
1		dihjatc.b	$$⊢B={\mathrm{Base}}_K$$
2		dihjatc.l	$$⊢\underset{\dot{}}{\le }={\le }_K$$
3		dihjatc.h	$$⊢H=\mathrm{LHyp}\left(K\right)$$
4		dihjatc.j	$$⊢\underset{\dot{}}{\vee }=\mathrm{join}\left(K\right)$$
5		dihjatc.a	$$⊢A=\mathrm{Atoms}\left(K\right)$$
6		dihjatc.u	$$⊢U=\mathrm{DVecH}\left(K\right)\left(W\right)$$
7		dihjatc.s	$$⊢\underset{\dot{}}{\oplus }=\mathrm{LSSum}\left(U\right)$$
8		dihjatc.i	$$⊢I=\mathrm{DIsoH}\left(K\right)\left(W\right)$$
9		dihjatc.k	$$⊢\phi \to \left(K\in \mathrm{HL}\wedge W\in H\right)$$
10		dihjatc.x	$$⊢\phi \to \left(X\in B\wedge X\underset{\dot{}}{\le }W\right)$$
11		dihjatc.p	$$⊢\phi \to \left(P\in A\wedge \neg P\underset{\dot{}}{\le }W\right)$$
12	9	simpld	$$⊢\phi \to K\in \mathrm{HL}$$
13		hlop	$$⊢K\in \mathrm{HL}\to K\in \mathrm{OP}$$
14	12 13	syl	$$⊢\phi \to K\in \mathrm{OP}$$
15		eqid	$$⊢\mathrm{1.}\left(K\right)=\mathrm{1.}\left(K\right)$$
16	1 15	op1cl	$$⊢K\in \mathrm{OP}\to \mathrm{1.}\left(K\right)\in B$$
17	14 16	syl	$$⊢\phi \to \mathrm{1.}\left(K\right)\in B$$
18	10	simpld	$$⊢\phi \to X\in B$$
19	11	simpld	$$⊢\phi \to P\in A$$
20	1 5	atbase	$$⊢P\in A\to P\in B$$
21	19 20	syl	$$⊢\phi \to P\in B$$
22	1 2 15	ople1	$$⊢\left(K\in \mathrm{OP}\wedge P\in B\right)\to P\underset{\dot{}}{\le }\mathrm{1.}\left(K\right)$$
23	14 21 22	syl2anc	$$⊢\phi \to P\underset{\dot{}}{\le }\mathrm{1.}\left(K\right)$$
24		hlol	$$⊢K\in \mathrm{HL}\to K\in \mathrm{OL}$$
25	12 24	syl	$$⊢\phi \to K\in \mathrm{OL}$$
26		eqid	$$⊢\mathrm{meet}\left(K\right)=\mathrm{meet}\left(K\right)$$
27	1 26 15	olm12	$$⊢\left(K\in \mathrm{OL}\wedge X\in B\right)\to \mathrm{1.}\left(K\right)\mathrm{meet}\left(K\right)X=X$$
28	25 18 27	syl2anc	$$⊢\phi \to \mathrm{1.}\left(K\right)\mathrm{meet}\left(K\right)X=X$$
29	10	simprd	$$⊢\phi \to X\underset{\dot{}}{\le }W$$
30	28 29	eqbrtrd	$$⊢\phi \to \left(\mathrm{1.}\left(K\right)\mathrm{meet}\left(K\right)X\right)\underset{\dot{}}{\le }W$$
31	1 2 3 4 26 5 6 7 8	dihjatc3	$$⊢\left(\left(\left(K\in \mathrm{HL}\wedge W\in H\right)\wedge \mathrm{1.}\left(K\right)\in B\wedge X\in B\right)\wedge \left(P\in A\wedge \neg P\underset{\dot{}}{\le }W\right)\wedge \left(P\underset{\dot{}}{\le }\mathrm{1.}\left(K\right)\wedge \left(\mathrm{1.}\left(K\right)\mathrm{meet}\left(K\right)X\right)\underset{\dot{}}{\le }W\right)\right)\to I\left(\left(\mathrm{1.}\left(K\right)\mathrm{meet}\left(K\right)X\right)\underset{\dot{}}{\vee }P\right)=I\left(\mathrm{1.}\left(K\right)\mathrm{meet}\left(K\right)X\right)\underset{\dot{}}{\oplus }I\left(P\right)$$
32	9 17 18 11 23 30 31	syl312anc	$$⊢\phi \to I\left(\left(\mathrm{1.}\left(K\right)\mathrm{meet}\left(K\right)X\right)\underset{\dot{}}{\vee }P\right)=I\left(\mathrm{1.}\left(K\right)\mathrm{meet}\left(K\right)X\right)\underset{\dot{}}{\oplus }I\left(P\right)$$
33	28	fvoveq1d	$$⊢\phi \to I\left(\left(\mathrm{1.}\left(K\right)\mathrm{meet}\left(K\right)X\right)\underset{\dot{}}{\vee }P\right)=I\left(X\underset{\dot{}}{\vee }P\right)$$
34	28	fveq2d	$$⊢\phi \to I\left(\mathrm{1.}\left(K\right)\mathrm{meet}\left(K\right)X\right)=I\left(X\right)$$
35	34	oveq1d	$$⊢\phi \to I\left(\mathrm{1.}\left(K\right)\mathrm{meet}\left(K\right)X\right)\underset{\dot{}}{\oplus }I\left(P\right)=I\left(X\right)\underset{\dot{}}{\oplus }I\left(P\right)$$
36	32 33 35	3eqtr3d	$$⊢\phi \to I\left(X\underset{\dot{}}{\vee }P\right)=I\left(X\right)\underset{\dot{}}{\oplus }I\left(P\right)$$