Theorem trljat3

Description: The value of a translation of an atom P not under the fiducial co-atom W , joined with trace. Equation above Lemma C in Crawley p. 112. (Contributed by NM, 22-May-2012)

	Ref	Expression
Hypotheses	trljat.l	$$⊢\underset{\dot{}}{\le }={\le }_K$$
	trljat.j	$$⊢\underset{\dot{}}{\vee }=\mathrm{join}\left(K\right)$$
	trljat.a	$$⊢A=\mathrm{Atoms}\left(K\right)$$
	trljat.h	$$⊢H=\mathrm{LHyp}\left(K\right)$$
	trljat.t	$$⊢T=\mathrm{LTrn}\left(K\right)\left(W\right)$$
	trljat.r	$$⊢R=\mathrm{trL}\left(K\right)\left(W\right)$$
Assertion	trljat3	$$⊢\left(\left(K\in \mathrm{HL}\wedge W\in H\right)\wedge F\in T\wedge \left(P\in A\wedge \neg P\underset{\dot{}}{\le }W\right)\right)\to P\underset{\dot{}}{\vee }R\left(F\right)=F\left(P\right)\underset{\dot{}}{\vee }R\left(F\right)$$

Proof

Step	Hyp	Ref	Expression
1		trljat.l	$$⊢\underset{\dot{}}{\le }={\le }_K$$
2		trljat.j	$$⊢\underset{\dot{}}{\vee }=\mathrm{join}\left(K\right)$$
3		trljat.a	$$⊢A=\mathrm{Atoms}\left(K\right)$$
4		trljat.h	$$⊢H=\mathrm{LHyp}\left(K\right)$$
5		trljat.t	$$⊢T=\mathrm{LTrn}\left(K\right)\left(W\right)$$
6		trljat.r	$$⊢R=\mathrm{trL}\left(K\right)\left(W\right)$$
7	1 2 3 4 5 6	trljat1	$$⊢\left(\left(K\in \mathrm{HL}\wedge W\in H\right)\wedge F\in T\wedge \left(P\in A\wedge \neg P\underset{\dot{}}{\le }W\right)\right)\to P\underset{\dot{}}{\vee }R\left(F\right)=P\underset{\dot{}}{\vee }F\left(P\right)$$
8	1 2 3 4 5 6	trljat2	$$⊢\left(\left(K\in \mathrm{HL}\wedge W\in H\right)\wedge F\in T\wedge \left(P\in A\wedge \neg P\underset{\dot{}}{\le }W\right)\right)\to F\left(P\right)\underset{\dot{}}{\vee }R\left(F\right)=P\underset{\dot{}}{\vee }F\left(P\right)$$
9	7 8	eqtr4d	$$⊢\left(\left(K\in \mathrm{HL}\wedge W\in H\right)\wedge F\in T\wedge \left(P\in A\wedge \neg P\underset{\dot{}}{\le }W\right)\right)\to P\underset{\dot{}}{\vee }R\left(F\right)=F\left(P\right)\underset{\dot{}}{\vee }R\left(F\right)$$