Metamath Proof Explorer


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 ‘ 𝐾 )
dia2dimlem4.a 𝐴 = ( Atoms ‘ 𝐾 )
dia2dimlem4.h 𝐻 = ( LHyp ‘ 𝐾 )
dia2dimlem4.t 𝑇 = ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 )
dia2dimlem4.k ( 𝜑 → ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) )
dia2dimlem4.p ( 𝜑 → ( 𝑃𝐴 ∧ ¬ 𝑃 𝑊 ) )
dia2dimlem4.f ( 𝜑𝐹𝑇 )
dia2dimlem4.g ( 𝜑𝐺𝑇 )
dia2dimlem4.gv ( 𝜑 → ( 𝐺𝑃 ) = 𝑄 )
dia2dimlem4.d ( 𝜑𝐷𝑇 )
dia2dimlem4.dv ( 𝜑 → ( 𝐷𝑄 ) = ( 𝐹𝑃 ) )
Assertion dia2dimlem4 ( 𝜑 → ( 𝐷𝐺 ) = 𝐹 )

Proof

Step Hyp Ref Expression
1 dia2dimlem4.l = ( le ‘ 𝐾 )
2 dia2dimlem4.a 𝐴 = ( Atoms ‘ 𝐾 )
3 dia2dimlem4.h 𝐻 = ( LHyp ‘ 𝐾 )
4 dia2dimlem4.t 𝑇 = ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 )
5 dia2dimlem4.k ( 𝜑 → ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) )
6 dia2dimlem4.p ( 𝜑 → ( 𝑃𝐴 ∧ ¬ 𝑃 𝑊 ) )
7 dia2dimlem4.f ( 𝜑𝐹𝑇 )
8 dia2dimlem4.g ( 𝜑𝐺𝑇 )
9 dia2dimlem4.gv ( 𝜑 → ( 𝐺𝑃 ) = 𝑄 )
10 dia2dimlem4.d ( 𝜑𝐷𝑇 )
11 dia2dimlem4.dv ( 𝜑 → ( 𝐷𝑄 ) = ( 𝐹𝑃 ) )
12 3 4 ltrnco ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ 𝐷𝑇𝐺𝑇 ) → ( 𝐷𝐺 ) ∈ 𝑇 )
13 5 10 8 12 syl3anc ( 𝜑 → ( 𝐷𝐺 ) ∈ 𝑇 )
14 6 simpld ( 𝜑𝑃𝐴 )
15 1 2 3 4 ltrncoval ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( 𝐷𝑇𝐺𝑇 ) ∧ 𝑃𝐴 ) → ( ( 𝐷𝐺 ) ‘ 𝑃 ) = ( 𝐷 ‘ ( 𝐺𝑃 ) ) )
16 5 10 8 14 15 syl121anc ( 𝜑 → ( ( 𝐷𝐺 ) ‘ 𝑃 ) = ( 𝐷 ‘ ( 𝐺𝑃 ) ) )
17 9 fveq2d ( 𝜑 → ( 𝐷 ‘ ( 𝐺𝑃 ) ) = ( 𝐷𝑄 ) )
18 16 17 11 3eqtrd ( 𝜑 → ( ( 𝐷𝐺 ) ‘ 𝑃 ) = ( 𝐹𝑃 ) )
19 1 2 3 4 cdlemd ( ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( 𝐷𝐺 ) ∈ 𝑇𝐹𝑇 ) ∧ ( 𝑃𝐴 ∧ ¬ 𝑃 𝑊 ) ∧ ( ( 𝐷𝐺 ) ‘ 𝑃 ) = ( 𝐹𝑃 ) ) → ( 𝐷𝐺 ) = 𝐹 )
20 5 13 7 6 18 19 syl311anc ( 𝜑 → ( 𝐷𝐺 ) = 𝐹 )