Theorem dia2dimlem4

Description: Lemma for dia2dim . Show that the composition (sum) of translations (vectors) G and D equals F . Part of proof of Lemma M in Crawley p. 121 line 5. (Contributed by NM, 8-Sep-2014)

	Ref	Expression
Hypotheses	dia2dimlem4.l	|- .<_ = ( le ` K )
	dia2dimlem4.a	|- A = ( Atoms ` K )
	dia2dimlem4.h	|- H = ( LHyp ` K )
	dia2dimlem4.t	|- T = ( ( LTrn ` K ) ` W )
	dia2dimlem4.k	|- ( ph -> ( K e. HL /\ W e. H ) )
	dia2dimlem4.p	|- ( ph -> ( P e. A /\ -. P .<_ W ) )
	dia2dimlem4.f	|- ( ph -> F e. T )
	dia2dimlem4.g	|- ( ph -> G e. T )
	dia2dimlem4.gv	|- ( ph -> ( G ` P ) = Q )
	dia2dimlem4.d	|- ( ph -> D e. T )
	dia2dimlem4.dv	|- ( ph -> ( D ` Q ) = ( F ` P ) )
Assertion	dia2dimlem4	|- ( ph -> ( D o. G ) = F )

Proof

Step	Hyp	Ref	Expression
1		dia2dimlem4.l	|- .<_ = ( le ` K )
2		dia2dimlem4.a	|- A = ( Atoms ` K )
3		dia2dimlem4.h	|- H = ( LHyp ` K )
4		dia2dimlem4.t	|- T = ( ( LTrn ` K ) ` W )
5		dia2dimlem4.k	|- ( ph -> ( K e. HL /\ W e. H ) )
6		dia2dimlem4.p	|- ( ph -> ( P e. A /\ -. P .<_ W ) )
7		dia2dimlem4.f	|- ( ph -> F e. T )
8		dia2dimlem4.g	|- ( ph -> G e. T )
9		dia2dimlem4.gv	|- ( ph -> ( G ` P ) = Q )
10		dia2dimlem4.d	|- ( ph -> D e. T )
11		dia2dimlem4.dv	|- ( ph -> ( D ` Q ) = ( F ` P ) )
12	3 4	ltrnco	|- ( ( ( K e. HL /\ W e. H ) /\ D e. T /\ G e. T ) -> ( D o. G ) e. T )
13	5 10 8 12	syl3anc	|- ( ph -> ( D o. G ) e. T )
14	6	simpld	|- ( ph -> P e. A )
15	1 2 3 4	ltrncoval	|- ( ( ( K e. HL /\ W e. H ) /\ ( D e. T /\ G e. T ) /\ P e. A ) -> ( ( D o. G ) ` P ) = ( D ` ( G ` P ) ) )
16	5 10 8 14 15	syl121anc	|- ( ph -> ( ( D o. G ) ` P ) = ( D ` ( G ` P ) ) )
17	9	fveq2d	|- ( ph -> ( D ` ( G ` P ) ) = ( D ` Q ) )
18	16 17 11	3eqtrd	|- ( ph -> ( ( D o. G ) ` P ) = ( F ` P ) )
19	1 2 3 4	cdlemd	|- ( ( ( ( K e. HL /\ W e. H ) /\ ( D o. G ) e. T /\ F e. T ) /\ ( P e. A /\ -. P .<_ W ) /\ ( ( D o. G ) ` P ) = ( F ` P ) ) -> ( D o. G ) = F )
20	5 13 7 6 18 19	syl311anc	|- ( ph -> ( D o. G ) = F )