Theorem dihjatb

Description: Isomorphism H of lattice join of two atoms under the fiducial hyperplane. (Contributed by NM, 23-Sep-2014)

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

Proof

Step	Hyp	Ref	Expression
1		dihjatb.l	$$⊢\underset{\dot{}}{\le }={\le }_K$$
2		dihjatb.h	$$⊢H=\mathrm{LHyp}\left(K\right)$$
3		dihjatb.j	$$⊢\underset{\dot{}}{\vee }=\mathrm{join}\left(K\right)$$
4		dihjatb.a	$$⊢A=\mathrm{Atoms}\left(K\right)$$
5		dihjatb.u	$$⊢U=\mathrm{DVecH}\left(K\right)\left(W\right)$$
6		dihjatb.s	$$⊢\underset{\dot{}}{\oplus }=\mathrm{LSSum}\left(U\right)$$
7		dihjatb.i	$$⊢I=\mathrm{DIsoH}\left(K\right)\left(W\right)$$
8		dihjatb.k	$$⊢\phi \to \left(K\in \mathrm{HL}\wedge W\in H\right)$$
9		dihjatb.p	$$⊢\phi \to \left(P\in A\wedge P\underset{\dot{}}{\le }W\right)$$
10		dihjatb.q	$$⊢\phi \to \left(Q\in A\wedge Q\underset{\dot{}}{\le }W\right)$$
11	1 3 4 2 5 6 7 8 9 10	dih2dimb	$$⊢\phi \to I\left(P\underset{\dot{}}{\vee }Q\right)\subseteq I\left(P\right)\underset{\dot{}}{\oplus }I\left(Q\right)$$
12		eqid	$$⊢{\mathrm{Base}}_K={\mathrm{Base}}_K$$
13	9	simpld	$$⊢\phi \to P\in A$$
14	12 4	atbase	$$⊢P\in A\to P\in {\mathrm{Base}}_K$$
15	13 14	syl	$$⊢\phi \to P\in {\mathrm{Base}}_K$$
16	10	simpld	$$⊢\phi \to Q\in A$$
17	12 4	atbase	$$⊢Q\in A\to Q\in {\mathrm{Base}}_K$$
18	16 17	syl	$$⊢\phi \to Q\in {\mathrm{Base}}_K$$
19	12 2 3 5 6 7 8 15 18	dihsumssj	$$⊢\phi \to I\left(P\right)\underset{\dot{}}{\oplus }I\left(Q\right)\subseteq I\left(P\underset{\dot{}}{\vee }Q\right)$$
20	11 19	eqssd	$$⊢\phi \to I\left(P\underset{\dot{}}{\vee }Q\right)=I\left(P\right)\underset{\dot{}}{\oplus }I\left(Q\right)$$