Theorem dihjust

Description: Part of proof after Lemma N of Crawley p. 122 line 4, "the definition of phi(x) is independent of the atom q." (Contributed by NM, 2-Mar-2014)

	Ref	Expression
Hypotheses	dihjust.b	|- B = ( Base ` K )
	dihjust.l	|- .<_ = ( le ` K )
	dihjust.j	|- .\/ = ( join ` K )
	dihjust.m	|- ./\ = ( meet ` K )
	dihjust.a	|- A = ( Atoms ` K )
	dihjust.h	|- H = ( LHyp ` K )
	dihjust.i	|- I = ( ( DIsoB ` K ) ` W )
	dihjust.J	|- J = ( ( DIsoC ` K ) ` W )
	dihjust.u	|- U = ( ( DVecH ` K ) ` W )
	dihjust.s	|- .(+) = ( LSSum ` U )
Assertion	dihjust	|- ( ( ( K e. HL /\ W e. H ) /\ ( ( Q e. A /\ -. Q .<_ W ) /\ ( R e. A /\ -. R .<_ W ) /\ X e. B ) /\ ( Q .\/ ( X ./\ W ) ) = ( R .\/ ( X ./\ W ) ) ) -> ( ( J ` Q ) .(+) ( I ` ( X ./\ W ) ) ) = ( ( J ` R ) .(+) ( I ` ( X ./\ W ) ) ) )

Proof

Step	Hyp	Ref	Expression
1		dihjust.b	|- B = ( Base ` K )
2		dihjust.l	|- .<_ = ( le ` K )
3		dihjust.j	|- .\/ = ( join ` K )
4		dihjust.m	|- ./\ = ( meet ` K )
5		dihjust.a	|- A = ( Atoms ` K )
6		dihjust.h	|- H = ( LHyp ` K )
7		dihjust.i	|- I = ( ( DIsoB ` K ) ` W )
8		dihjust.J	|- J = ( ( DIsoC ` K ) ` W )
9		dihjust.u	|- U = ( ( DVecH ` K ) ` W )
10		dihjust.s	|- .(+) = ( LSSum ` U )
11	1 2 3 4 5 6 7 8 9 10	dihjustlem	|- ( ( ( K e. HL /\ W e. H ) /\ ( ( Q e. A /\ -. Q .<_ W ) /\ ( R e. A /\ -. R .<_ W ) /\ X e. B ) /\ ( Q .\/ ( X ./\ W ) ) = ( R .\/ ( X ./\ W ) ) ) -> ( ( J ` Q ) .(+) ( I ` ( X ./\ W ) ) ) C_ ( ( J ` R ) .(+) ( I ` ( X ./\ W ) ) ) )
12		simp1	|- ( ( ( K e. HL /\ W e. H ) /\ ( ( Q e. A /\ -. Q .<_ W ) /\ ( R e. A /\ -. R .<_ W ) /\ X e. B ) /\ ( Q .\/ ( X ./\ W ) ) = ( R .\/ ( X ./\ W ) ) ) -> ( K e. HL /\ W e. H ) )
13		simp22	|- ( ( ( K e. HL /\ W e. H ) /\ ( ( Q e. A /\ -. Q .<_ W ) /\ ( R e. A /\ -. R .<_ W ) /\ X e. B ) /\ ( Q .\/ ( X ./\ W ) ) = ( R .\/ ( X ./\ W ) ) ) -> ( R e. A /\ -. R .<_ W ) )
14		simp21	|- ( ( ( K e. HL /\ W e. H ) /\ ( ( Q e. A /\ -. Q .<_ W ) /\ ( R e. A /\ -. R .<_ W ) /\ X e. B ) /\ ( Q .\/ ( X ./\ W ) ) = ( R .\/ ( X ./\ W ) ) ) -> ( Q e. A /\ -. Q .<_ W ) )
15		simp23	|- ( ( ( K e. HL /\ W e. H ) /\ ( ( Q e. A /\ -. Q .<_ W ) /\ ( R e. A /\ -. R .<_ W ) /\ X e. B ) /\ ( Q .\/ ( X ./\ W ) ) = ( R .\/ ( X ./\ W ) ) ) -> X e. B )
16		simp3	|- ( ( ( K e. HL /\ W e. H ) /\ ( ( Q e. A /\ -. Q .<_ W ) /\ ( R e. A /\ -. R .<_ W ) /\ X e. B ) /\ ( Q .\/ ( X ./\ W ) ) = ( R .\/ ( X ./\ W ) ) ) -> ( Q .\/ ( X ./\ W ) ) = ( R .\/ ( X ./\ W ) ) )
17	16	eqcomd	|- ( ( ( K e. HL /\ W e. H ) /\ ( ( Q e. A /\ -. Q .<_ W ) /\ ( R e. A /\ -. R .<_ W ) /\ X e. B ) /\ ( Q .\/ ( X ./\ W ) ) = ( R .\/ ( X ./\ W ) ) ) -> ( R .\/ ( X ./\ W ) ) = ( Q .\/ ( X ./\ W ) ) )
18	1 2 3 4 5 6 7 8 9 10	dihjustlem	|- ( ( ( K e. HL /\ W e. H ) /\ ( ( R e. A /\ -. R .<_ W ) /\ ( Q e. A /\ -. Q .<_ W ) /\ X e. B ) /\ ( R .\/ ( X ./\ W ) ) = ( Q .\/ ( X ./\ W ) ) ) -> ( ( J ` R ) .(+) ( I ` ( X ./\ W ) ) ) C_ ( ( J ` Q ) .(+) ( I ` ( X ./\ W ) ) ) )
19	12 13 14 15 17 18	syl131anc	|- ( ( ( K e. HL /\ W e. H ) /\ ( ( Q e. A /\ -. Q .<_ W ) /\ ( R e. A /\ -. R .<_ W ) /\ X e. B ) /\ ( Q .\/ ( X ./\ W ) ) = ( R .\/ ( X ./\ W ) ) ) -> ( ( J ` R ) .(+) ( I ` ( X ./\ W ) ) ) C_ ( ( J ` Q ) .(+) ( I ` ( X ./\ W ) ) ) )
20	11 19	eqssd	|- ( ( ( K e. HL /\ W e. H ) /\ ( ( Q e. A /\ -. Q .<_ W ) /\ ( R e. A /\ -. R .<_ W ) /\ X e. B ) /\ ( Q .\/ ( X ./\ W ) ) = ( R .\/ ( X ./\ W ) ) ) -> ( ( J ` Q ) .(+) ( I ` ( X ./\ W ) ) ) = ( ( J ` R ) .(+) ( I ` ( X ./\ W ) ) ) )