Mathbox for Norm Megill < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  cdleme50trn3 Structured version   Unicode version

Theorem cdleme50trn3 34038
 Description: Part of proof that is a translation. case. TODO: fix comment. (Contributed by NM, 10-Apr-2013.)
Hypotheses
Ref Expression
cdlemef50.b
cdlemef50.l
cdlemef50.j
cdlemef50.m
cdlemef50.a
cdlemef50.h
cdlemef50.u
cdlemef50.d
cdlemefs50.e
cdlemef50.f
Assertion
Ref Expression
cdleme50trn3
Distinct variable groups:   ,,,,,   ,,,,,   ,,,,,   ,,,,,   ,,,,,   ,,,,   ,,,   ,,,,,   ,,,,,   ,,,,,   ,,,,,   ,,,,,   ,,,,,   ,,,,,
Allowed substitution hints:   ()   (,)   (,,,,)

Proof of Theorem cdleme50trn3
StepHypRef Expression
1 simpl1 1008 . . . . 5
2 simprr 764 . . . . 5
3 cdlemef50.l . . . . . 6
4 cdlemef50.m . . . . . 6
5 eqid 2422 . . . . . 6
6 cdlemef50.a . . . . . 6
7 cdlemef50.h . . . . . 6
83, 4, 5, 6, 7lhpmat 33513 . . . . 5
91, 2, 8syl2anc 665 . . . 4
10 simprrl 772 . . . . . . . . 9
11 cdlemef50.b . . . . . . . . . 10
1211, 6atbase 32773 . . . . . . . . 9
1310, 12syl 17 . . . . . . . 8
14 simprl 762 . . . . . . . 8
15 cdlemef50.f . . . . . . . . 9
1615cdleme31id 33879 . . . . . . . 8
1713, 14, 16syl2anc 665 . . . . . . 7
1817oveq2d 6317 . . . . . 6
19 simpl1l 1056 . . . . . . 7
20 cdlemef50.j . . . . . . . 8
2120, 6hlatjidm 32852 . . . . . . 7
2219, 10, 21syl2anc 665 . . . . . 6
2318, 22eqtrd 2463 . . . . 5
2423oveq1d 6316 . . . 4
25 simpl2 1009 . . . . 5
263, 4, 5, 6, 7lhpmat 33513 . . . . 5
271, 25, 26syl2anc 665 . . . 4
289, 24, 273eqtr4d 2473 . . 3
29 simpl2l 1058 . . . . . 6
3020, 6hlatjidm 32852 . . . . . 6
3119, 29, 30syl2anc 665 . . . . 5
3214oveq2d 6317 . . . . 5
3331, 32eqtr3d 2465 . . . 4
3433oveq1d 6316 . . 3
3528, 34eqtrd 2463 . 2
36 cdlemef50.u . 2
3735, 36syl6eqr 2481 1
 Colors of variables: wff setvar class Syntax hints:   wn 3   wi 4   wa 370   w3a 982   wceq 1437   wcel 1868   wne 2618  wral 2775  csb 3395  cif 3909   class class class wbr 4420   cmpt 4479  cfv 5597  crio 6262  (class class class)co 6301  cbs 15108  cple 15184  cjn 16176  cmee 16177  cp0 16270  catm 32747  chlt 32834  clh 33467 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1665  ax-4 1678  ax-5 1748  ax-6 1794  ax-7 1839  ax-8 1870  ax-9 1872  ax-10 1887  ax-11 1892  ax-12 1905  ax-13 2053  ax-ext 2400  ax-rep 4533  ax-sep 4543  ax-nul 4551  ax-pow 4598  ax-pr 4656  ax-un 6593 This theorem depends on definitions:  df-bi 188  df-or 371  df-an 372  df-3an 984  df-tru 1440  df-ex 1660  df-nf 1664  df-sb 1787  df-eu 2269  df-mo 2270  df-clab 2408  df-cleq 2414  df-clel 2417  df-nfc 2572  df-ne 2620  df-ral 2780  df-rex 2781  df-reu 2782  df-rab 2784  df-v 3083  df-sbc 3300  df-csb 3396  df-dif 3439  df-un 3441  df-in 3443  df-ss 3450  df-nul 3762  df-if 3910  df-pw 3981  df-sn 3997  df-pr 3999  df-op 4003  df-uni 4217  df-iun 4298  df-br 4421  df-opab 4480  df-mpt 4481  df-id 4764  df-xp 4855  df-rel 4856  df-cnv 4857  df-co 4858  df-dm 4859  df-rn 4860  df-res 4861  df-ima 4862  df-iota 5561  df-fun 5599  df-fn 5600  df-f 5601  df-f1 5602  df-fo 5603  df-f1o 5604  df-fv 5605  df-riota 6263  df-ov 6304  df-oprab 6305  df-preset 16160  df-poset 16178  df-plt 16191  df-lub 16207  df-glb 16208  df-join 16209  df-meet 16210  df-p0 16272  df-lat 16279  df-covers 32750  df-ats 32751  df-atl 32782  df-cvlat 32806  df-hlat 32835  df-lhyp 33471 This theorem is referenced by:  cdleme50trn123  34039
 Copyright terms: Public domain W3C validator