Users' Mathboxes Mathbox for Norm Megill < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  dia2dimlem4 Structured version   Visualization version   GIF version

Theorem dia2dimlem4 37143
Description: Lemma for dia2dim 37153. Show that the composition (sum) of translations (vectors) 𝐺 and 𝐷 equals 𝐹. Part of proof of Lemma M in [Crawley] p. 121 line 5. (Contributed by NM, 8-Sep-2014.)
Hypotheses
Ref Expression
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
Ref Expression
dia2dimlem4 (𝜑 → (𝐷𝐺) = 𝐹)

Proof of Theorem dia2dimlem4
StepHypRef Expression
1 dia2dimlem4.k . 2 (𝜑 → (𝐾 ∈ HL ∧ 𝑊𝐻))
2 dia2dimlem4.d . . 3 (𝜑𝐷𝑇)
3 dia2dimlem4.g . . 3 (𝜑𝐺𝑇)
4 dia2dimlem4.h . . . 4 𝐻 = (LHyp‘𝐾)
5 dia2dimlem4.t . . . 4 𝑇 = ((LTrn‘𝐾)‘𝑊)
64, 5ltrnco 36795 . . 3 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ 𝐷𝑇𝐺𝑇) → (𝐷𝐺) ∈ 𝑇)
71, 2, 3, 6syl3anc 1496 . 2 (𝜑 → (𝐷𝐺) ∈ 𝑇)
8 dia2dimlem4.f . 2 (𝜑𝐹𝑇)
9 dia2dimlem4.p . 2 (𝜑 → (𝑃𝐴 ∧ ¬ 𝑃 𝑊))
109simpld 490 . . . 4 (𝜑𝑃𝐴)
11 dia2dimlem4.l . . . . 5 = (le‘𝐾)
12 dia2dimlem4.a . . . . 5 𝐴 = (Atoms‘𝐾)
1311, 12, 4, 5ltrncoval 36221 . . . 4 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝐷𝑇𝐺𝑇) ∧ 𝑃𝐴) → ((𝐷𝐺)‘𝑃) = (𝐷‘(𝐺𝑃)))
141, 2, 3, 10, 13syl121anc 1500 . . 3 (𝜑 → ((𝐷𝐺)‘𝑃) = (𝐷‘(𝐺𝑃)))
15 dia2dimlem4.gv . . . 4 (𝜑 → (𝐺𝑃) = 𝑄)
1615fveq2d 6438 . . 3 (𝜑 → (𝐷‘(𝐺𝑃)) = (𝐷𝑄))
17 dia2dimlem4.dv . . 3 (𝜑 → (𝐷𝑄) = (𝐹𝑃))
1814, 16, 173eqtrd 2866 . 2 (𝜑 → ((𝐷𝐺)‘𝑃) = (𝐹𝑃))
1911, 12, 4, 5cdlemd 36283 . 2 ((((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝐷𝐺) ∈ 𝑇𝐹𝑇) ∧ (𝑃𝐴 ∧ ¬ 𝑃 𝑊) ∧ ((𝐷𝐺)‘𝑃) = (𝐹𝑃)) → (𝐷𝐺) = 𝐹)
201, 7, 8, 9, 18, 19syl311anc 1509 1 (𝜑 → (𝐷𝐺) = 𝐹)
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wa 386   = wceq 1658  wcel 2166   class class class wbr 4874  ccom 5347  cfv 6124  lecple 16313  Atomscatm 35339  HLchlt 35426  LHypclh 36060  LTrncltrn 36177
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1896  ax-4 1910  ax-5 2011  ax-6 2077  ax-7 2114  ax-8 2168  ax-9 2175  ax-10 2194  ax-11 2209  ax-12 2222  ax-13 2391  ax-ext 2804  ax-rep 4995  ax-sep 5006  ax-nul 5014  ax-pow 5066  ax-pr 5128  ax-un 7210  ax-riotaBAD 35029
This theorem depends on definitions:  df-bi 199  df-an 387  df-or 881  df-3or 1114  df-3an 1115  df-tru 1662  df-ex 1881  df-nf 1885  df-sb 2070  df-mo 2606  df-eu 2641  df-clab 2813  df-cleq 2819  df-clel 2822  df-nfc 2959  df-ne 3001  df-nel 3104  df-ral 3123  df-rex 3124  df-reu 3125  df-rmo 3126  df-rab 3127  df-v 3417  df-sbc 3664  df-csb 3759  df-dif 3802  df-un 3804  df-in 3806  df-ss 3813  df-nul 4146  df-if 4308  df-pw 4381  df-sn 4399  df-pr 4401  df-op 4405  df-uni 4660  df-iun 4743  df-iin 4744  df-br 4875  df-opab 4937  df-mpt 4954  df-id 5251  df-xp 5349  df-rel 5350  df-cnv 5351  df-co 5352  df-dm 5353  df-rn 5354  df-res 5355  df-ima 5356  df-iota 6087  df-fun 6126  df-fn 6127  df-f 6128  df-f1 6129  df-fo 6130  df-f1o 6131  df-fv 6132  df-riota 6867  df-ov 6909  df-oprab 6910  df-mpt2 6911  df-1st 7429  df-2nd 7430  df-undef 7665  df-map 8125  df-proset 17282  df-poset 17300  df-plt 17312  df-lub 17328  df-glb 17329  df-join 17330  df-meet 17331  df-p0 17393  df-p1 17394  df-lat 17400  df-clat 17462  df-oposet 35252  df-ol 35254  df-oml 35255  df-covers 35342  df-ats 35343  df-atl 35374  df-cvlat 35398  df-hlat 35427  df-llines 35574  df-lplanes 35575  df-lvols 35576  df-lines 35577  df-psubsp 35579  df-pmap 35580  df-padd 35872  df-lhyp 36064  df-laut 36065  df-ldil 36180  df-ltrn 36181  df-trl 36235
This theorem is referenced by:  dia2dimlem5  37144
  Copyright terms: Public domain W3C validator