Theorem cdlemg4b12

Description: TODO: FIX COMMENT. (Contributed by NM, 24-Apr-2013)

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

Proof

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