Theorem dihjat3

Description: Isomorphism H of lattice join with an atom. (Contributed by NM, 25-Apr-2015)

	Ref	Expression
Hypotheses	dihjat3.b	|- B = ( Base ` K )
	dihjat3.h	|- H = ( LHyp ` K )
	dihjat3.j	|- .\/ = ( join ` K )
	dihjat3.a	|- A = ( Atoms ` K )
	dihjat3.u	|- U = ( ( DVecH ` K ) ` W )
	dihjat3.s	|- .(+) = ( LSSum ` U )
	dihjat3.i	|- I = ( ( DIsoH ` K ) ` W )
	dihjat3.k	|- ( ph -> ( K e. HL /\ W e. H ) )
	dihjat3.x	|- ( ph -> X e. B )
	dihjat3.p	|- ( ph -> P e. A )
Assertion	dihjat3	|- ( ph -> ( I ` ( X .\/ P ) ) = ( ( I ` X ) .(+) ( I ` P ) ) )

Proof

Step	Hyp	Ref	Expression
1		dihjat3.b	|- B = ( Base ` K )
2		dihjat3.h	|- H = ( LHyp ` K )
3		dihjat3.j	|- .\/ = ( join ` K )
4		dihjat3.a	|- A = ( Atoms ` K )
5		dihjat3.u	|- U = ( ( DVecH ` K ) ` W )
6		dihjat3.s	|- .(+) = ( LSSum ` U )
7		dihjat3.i	|- I = ( ( DIsoH ` K ) ` W )
8		dihjat3.k	|- ( ph -> ( K e. HL /\ W e. H ) )
9		dihjat3.x	|- ( ph -> X e. B )
10		dihjat3.p	|- ( ph -> P e. A )
11	1 4	atbase	|- ( P e. A -> P e. B )
12	10 11	syl	|- ( ph -> P e. B )
13		eqid	|- ( ( joinH ` K ) ` W ) = ( ( joinH ` K ) ` W )
14	1 3 2 7 13	djhlj	|- ( ( ( K e. HL /\ W e. H ) /\ ( X e. B /\ P e. B ) ) -> ( I ` ( X .\/ P ) ) = ( ( I ` X ) ( ( joinH ` K ) ` W ) ( I ` P ) ) )
15	8 9 12 14	syl12anc	|- ( ph -> ( I ` ( X .\/ P ) ) = ( ( I ` X ) ( ( joinH ` K ) ` W ) ( I ` P ) ) )
16		eqid	|- ( LSAtoms ` U ) = ( LSAtoms ` U )
17	1 2 7	dihcl	|- ( ( ( K e. HL /\ W e. H ) /\ X e. B ) -> ( I ` X ) e. ran I )
18	8 9 17	syl2anc	|- ( ph -> ( I ` X ) e. ran I )
19	4 2 5 7 16	dihatlat	|- ( ( ( K e. HL /\ W e. H ) /\ P e. A ) -> ( I ` P ) e. ( LSAtoms ` U ) )
20	8 10 19	syl2anc	|- ( ph -> ( I ` P ) e. ( LSAtoms ` U ) )
21	2 7 13 5 6 16 8 18 20	dihjat2	|- ( ph -> ( ( I ` X ) ( ( joinH ` K ) ` W ) ( I ` P ) ) = ( ( I ` X ) .(+) ( I ` P ) ) )
22	15 21	eqtrd	|- ( ph -> ( I ` ( X .\/ P ) ) = ( ( I ` X ) .(+) ( I ` P ) ) )