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	|- .<_ = ( le ` K )
	dihjatb.h	|- H = ( LHyp ` K )
	dihjatb.j	|- .\/ = ( join ` K )
	dihjatb.a	|- A = ( Atoms ` K )
	dihjatb.u	|- U = ( ( DVecH ` K ) ` W )
	dihjatb.s	|- .(+) = ( LSSum ` U )
	dihjatb.i	|- I = ( ( DIsoH ` K ) ` W )
	dihjatb.k	|- ( ph -> ( K e. HL /\ W e. H ) )
	dihjatb.p	|- ( ph -> ( P e. A /\ P .<_ W ) )
	dihjatb.q	|- ( ph -> ( Q e. A /\ Q .<_ W ) )
Assertion	dihjatb	|- ( ph -> ( I ` ( P .\/ Q ) ) = ( ( I ` P ) .(+) ( I ` Q ) ) )

Proof

Step	Hyp	Ref	Expression
1		dihjatb.l	|- .<_ = ( le ` K )
2		dihjatb.h	|- H = ( LHyp ` K )
3		dihjatb.j	|- .\/ = ( join ` K )
4		dihjatb.a	|- A = ( Atoms ` K )
5		dihjatb.u	|- U = ( ( DVecH ` K ) ` W )
6		dihjatb.s	|- .(+) = ( LSSum ` U )
7		dihjatb.i	|- I = ( ( DIsoH ` K ) ` W )
8		dihjatb.k	|- ( ph -> ( K e. HL /\ W e. H ) )
9		dihjatb.p	|- ( ph -> ( P e. A /\ P .<_ W ) )
10		dihjatb.q	|- ( ph -> ( Q e. A /\ Q .<_ W ) )
11	1 3 4 2 5 6 7 8 9 10	dih2dimb	|- ( ph -> ( I ` ( P .\/ Q ) ) C_ ( ( I ` P ) .(+) ( I ` Q ) ) )
12		eqid	|- ( Base ` K ) = ( Base ` K )
13	9	simpld	|- ( ph -> P e. A )
14	12 4	atbase	|- ( P e. A -> P e. ( Base ` K ) )
15	13 14	syl	|- ( ph -> P e. ( Base ` K ) )
16	10	simpld	|- ( ph -> Q e. A )
17	12 4	atbase	|- ( Q e. A -> Q e. ( Base ` K ) )
18	16 17	syl	|- ( ph -> Q e. ( Base ` K ) )
19	12 2 3 5 6 7 8 15 18	dihsumssj	|- ( ph -> ( ( I ` P ) .(+) ( I ` Q ) ) C_ ( I ` ( P .\/ Q ) ) )
20	11 19	eqssd	|- ( ph -> ( I ` ( P .\/ Q ) ) = ( ( I ` P ) .(+) ( I ` Q ) ) )