Theorem 3dimlem1

Description: Lemma for 3dim1 . (Contributed by NM, 25-Jul-2012)

	Ref	Expression
Hypotheses	3dim0.j	|- .\/ = ( join ` K )
	3dim0.l	|- .<_ = ( le ` K )
	3dim0.a	|- A = ( Atoms ` K )
Assertion	3dimlem1	|- ( ( ( Q =/= R /\ -. S .<_ ( Q .\/ R ) /\ -. T .<_ ( ( Q .\/ R ) .\/ S ) ) /\ P = Q ) -> ( P =/= R /\ -. S .<_ ( P .\/ R ) /\ -. T .<_ ( ( P .\/ R ) .\/ S ) ) )

Proof

Step	Hyp	Ref	Expression
1		3dim0.j	|- .\/ = ( join ` K )
2		3dim0.l	|- .<_ = ( le ` K )
3		3dim0.a	|- A = ( Atoms ` K )
4		neeq1	|- ( P = Q -> ( P =/= R <-> Q =/= R ) )
5		oveq1	|- ( P = Q -> ( P .\/ R ) = ( Q .\/ R ) )
6	5	breq2d	|- ( P = Q -> ( S .<_ ( P .\/ R ) <-> S .<_ ( Q .\/ R ) ) )
7	6	notbid	|- ( P = Q -> ( -. S .<_ ( P .\/ R ) <-> -. S .<_ ( Q .\/ R ) ) )
8	5	oveq1d	|- ( P = Q -> ( ( P .\/ R ) .\/ S ) = ( ( Q .\/ R ) .\/ S ) )
9	8	breq2d	|- ( P = Q -> ( T .<_ ( ( P .\/ R ) .\/ S ) <-> T .<_ ( ( Q .\/ R ) .\/ S ) ) )
10	9	notbid	|- ( P = Q -> ( -. T .<_ ( ( P .\/ R ) .\/ S ) <-> -. T .<_ ( ( Q .\/ R ) .\/ S ) ) )
11	4 7 10	3anbi123d	|- ( P = Q -> ( ( P =/= R /\ -. S .<_ ( P .\/ R ) /\ -. T .<_ ( ( P .\/ R ) .\/ S ) ) <-> ( Q =/= R /\ -. S .<_ ( Q .\/ R ) /\ -. T .<_ ( ( Q .\/ R ) .\/ S ) ) ) )
12	11	biimparc	|- ( ( ( Q =/= R /\ -. S .<_ ( Q .\/ R ) /\ -. T .<_ ( ( Q .\/ R ) .\/ S ) ) /\ P = Q ) -> ( P =/= R /\ -. S .<_ ( P .\/ R ) /\ -. T .<_ ( ( P .\/ R ) .\/ S ) ) )