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

Theorem tendoex 38726
Description: Generalization of Lemma K of [Crawley] p. 118, cdlemk 38725. TODO: can this be used to shorten uses of cdlemk 38725? (Contributed by NM, 15-Oct-2013.)
Hypotheses
Ref Expression
tendoex.l = (le‘𝐾)
tendoex.h 𝐻 = (LHyp‘𝐾)
tendoex.t 𝑇 = ((LTrn‘𝐾)‘𝑊)
tendoex.r 𝑅 = ((trL‘𝐾)‘𝑊)
tendoex.e 𝐸 = ((TEndo‘𝐾)‘𝑊)
Assertion
Ref Expression
tendoex (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝐹𝑇𝑁𝑇) ∧ (𝑅𝑁) (𝑅𝐹)) → ∃𝑢𝐸 (𝑢𝐹) = 𝑁)
Distinct variable groups:   𝑢,𝐸   𝑢,𝐹   𝑢,𝐾   𝑢,𝑁   𝑢,𝑅   𝑢,𝑇   𝑢,𝑊
Allowed substitution hints:   𝐻(𝑢)   (𝑢)

Proof of Theorem tendoex
Dummy variable is distinct from all other variables.
StepHypRef Expression
1 simpl1l 1226 . . . . . . 7 ((((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝐹𝑇𝑁𝑇) ∧ (𝑅𝑁) (𝑅𝐹)) ∧ (𝑅𝐹) ∈ (Atoms‘𝐾)) → 𝐾 ∈ HL)
2 hlop 37113 . . . . . . 7 (𝐾 ∈ HL → 𝐾 ∈ OP)
31, 2syl 17 . . . . . 6 ((((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝐹𝑇𝑁𝑇) ∧ (𝑅𝑁) (𝑅𝐹)) ∧ (𝑅𝐹) ∈ (Atoms‘𝐾)) → 𝐾 ∈ OP)
4 simpl1 1193 . . . . . . 7 ((((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝐹𝑇𝑁𝑇) ∧ (𝑅𝑁) (𝑅𝐹)) ∧ (𝑅𝐹) ∈ (Atoms‘𝐾)) → (𝐾 ∈ HL ∧ 𝑊𝐻))
5 simpl2r 1229 . . . . . . 7 ((((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝐹𝑇𝑁𝑇) ∧ (𝑅𝑁) (𝑅𝐹)) ∧ (𝑅𝐹) ∈ (Atoms‘𝐾)) → 𝑁𝑇)
6 eqid 2737 . . . . . . . 8 (Base‘𝐾) = (Base‘𝐾)
7 tendoex.h . . . . . . . 8 𝐻 = (LHyp‘𝐾)
8 tendoex.t . . . . . . . 8 𝑇 = ((LTrn‘𝐾)‘𝑊)
9 tendoex.r . . . . . . . 8 𝑅 = ((trL‘𝐾)‘𝑊)
106, 7, 8, 9trlcl 37915 . . . . . . 7 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ 𝑁𝑇) → (𝑅𝑁) ∈ (Base‘𝐾))
114, 5, 10syl2anc 587 . . . . . 6 ((((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝐹𝑇𝑁𝑇) ∧ (𝑅𝑁) (𝑅𝐹)) ∧ (𝑅𝐹) ∈ (Atoms‘𝐾)) → (𝑅𝑁) ∈ (Base‘𝐾))
12 simpr 488 . . . . . 6 ((((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝐹𝑇𝑁𝑇) ∧ (𝑅𝑁) (𝑅𝐹)) ∧ (𝑅𝐹) ∈ (Atoms‘𝐾)) → (𝑅𝐹) ∈ (Atoms‘𝐾))
13 simpl3 1195 . . . . . 6 ((((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝐹𝑇𝑁𝑇) ∧ (𝑅𝑁) (𝑅𝐹)) ∧ (𝑅𝐹) ∈ (Atoms‘𝐾)) → (𝑅𝑁) (𝑅𝐹))
14 tendoex.l . . . . . . 7 = (le‘𝐾)
15 eqid 2737 . . . . . . 7 (0.‘𝐾) = (0.‘𝐾)
16 eqid 2737 . . . . . . 7 (Atoms‘𝐾) = (Atoms‘𝐾)
176, 14, 15, 16leat 37044 . . . . . 6 (((𝐾 ∈ OP ∧ (𝑅𝑁) ∈ (Base‘𝐾) ∧ (𝑅𝐹) ∈ (Atoms‘𝐾)) ∧ (𝑅𝑁) (𝑅𝐹)) → ((𝑅𝑁) = (𝑅𝐹) ∨ (𝑅𝑁) = (0.‘𝐾)))
183, 11, 12, 13, 17syl31anc 1375 . . . . 5 ((((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝐹𝑇𝑁𝑇) ∧ (𝑅𝑁) (𝑅𝐹)) ∧ (𝑅𝐹) ∈ (Atoms‘𝐾)) → ((𝑅𝑁) = (𝑅𝐹) ∨ (𝑅𝑁) = (0.‘𝐾)))
19 simp3 1140 . . . . . . . . 9 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝐹𝑇𝑁𝑇) ∧ (𝑅𝑁) (𝑅𝐹)) → (𝑅𝑁) (𝑅𝐹))
20 breq2 5057 . . . . . . . . 9 ((𝑅𝐹) = (0.‘𝐾) → ((𝑅𝑁) (𝑅𝐹) ↔ (𝑅𝑁) (0.‘𝐾)))
2119, 20syl5ibcom 248 . . . . . . . 8 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝐹𝑇𝑁𝑇) ∧ (𝑅𝑁) (𝑅𝐹)) → ((𝑅𝐹) = (0.‘𝐾) → (𝑅𝑁) (0.‘𝐾)))
2221imp 410 . . . . . . 7 ((((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝐹𝑇𝑁𝑇) ∧ (𝑅𝑁) (𝑅𝐹)) ∧ (𝑅𝐹) = (0.‘𝐾)) → (𝑅𝑁) (0.‘𝐾))
23 simpl1l 1226 . . . . . . . . 9 ((((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝐹𝑇𝑁𝑇) ∧ (𝑅𝑁) (𝑅𝐹)) ∧ (𝑅𝐹) = (0.‘𝐾)) → 𝐾 ∈ HL)
2423, 2syl 17 . . . . . . . 8 ((((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝐹𝑇𝑁𝑇) ∧ (𝑅𝑁) (𝑅𝐹)) ∧ (𝑅𝐹) = (0.‘𝐾)) → 𝐾 ∈ OP)
25 simpl1 1193 . . . . . . . . 9 ((((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝐹𝑇𝑁𝑇) ∧ (𝑅𝑁) (𝑅𝐹)) ∧ (𝑅𝐹) = (0.‘𝐾)) → (𝐾 ∈ HL ∧ 𝑊𝐻))
26 simpl2r 1229 . . . . . . . . 9 ((((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝐹𝑇𝑁𝑇) ∧ (𝑅𝑁) (𝑅𝐹)) ∧ (𝑅𝐹) = (0.‘𝐾)) → 𝑁𝑇)
2725, 26, 10syl2anc 587 . . . . . . . 8 ((((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝐹𝑇𝑁𝑇) ∧ (𝑅𝑁) (𝑅𝐹)) ∧ (𝑅𝐹) = (0.‘𝐾)) → (𝑅𝑁) ∈ (Base‘𝐾))
286, 14, 15ople0 36938 . . . . . . . 8 ((𝐾 ∈ OP ∧ (𝑅𝑁) ∈ (Base‘𝐾)) → ((𝑅𝑁) (0.‘𝐾) ↔ (𝑅𝑁) = (0.‘𝐾)))
2924, 27, 28syl2anc 587 . . . . . . 7 ((((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝐹𝑇𝑁𝑇) ∧ (𝑅𝑁) (𝑅𝐹)) ∧ (𝑅𝐹) = (0.‘𝐾)) → ((𝑅𝑁) (0.‘𝐾) ↔ (𝑅𝑁) = (0.‘𝐾)))
3022, 29mpbid 235 . . . . . 6 ((((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝐹𝑇𝑁𝑇) ∧ (𝑅𝑁) (𝑅𝐹)) ∧ (𝑅𝐹) = (0.‘𝐾)) → (𝑅𝑁) = (0.‘𝐾))
3130olcd 874 . . . . 5 ((((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝐹𝑇𝑁𝑇) ∧ (𝑅𝑁) (𝑅𝐹)) ∧ (𝑅𝐹) = (0.‘𝐾)) → ((𝑅𝑁) = (𝑅𝐹) ∨ (𝑅𝑁) = (0.‘𝐾)))
32 simp1 1138 . . . . . 6 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝐹𝑇𝑁𝑇) ∧ (𝑅𝑁) (𝑅𝐹)) → (𝐾 ∈ HL ∧ 𝑊𝐻))
33 simp2l 1201 . . . . . 6 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝐹𝑇𝑁𝑇) ∧ (𝑅𝑁) (𝑅𝐹)) → 𝐹𝑇)
3415, 16, 7, 8, 9trlator0 37922 . . . . . 6 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ 𝐹𝑇) → ((𝑅𝐹) ∈ (Atoms‘𝐾) ∨ (𝑅𝐹) = (0.‘𝐾)))
3532, 33, 34syl2anc 587 . . . . 5 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝐹𝑇𝑁𝑇) ∧ (𝑅𝑁) (𝑅𝐹)) → ((𝑅𝐹) ∈ (Atoms‘𝐾) ∨ (𝑅𝐹) = (0.‘𝐾)))
3618, 31, 35mpjaodan 959 . . . 4 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝐹𝑇𝑁𝑇) ∧ (𝑅𝑁) (𝑅𝐹)) → ((𝑅𝑁) = (𝑅𝐹) ∨ (𝑅𝑁) = (0.‘𝐾)))
37363expa 1120 . . 3 ((((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝐹𝑇𝑁𝑇)) ∧ (𝑅𝑁) (𝑅𝐹)) → ((𝑅𝑁) = (𝑅𝐹) ∨ (𝑅𝑁) = (0.‘𝐾)))
38 eqcom 2744 . . . . 5 ((𝑅𝑁) = (𝑅𝐹) ↔ (𝑅𝐹) = (𝑅𝑁))
39 tendoex.e . . . . . . 7 𝐸 = ((TEndo‘𝐾)‘𝑊)
407, 8, 9, 39cdlemk 38725 . . . . . 6 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝐹𝑇𝑁𝑇) ∧ (𝑅𝐹) = (𝑅𝑁)) → ∃𝑢𝐸 (𝑢𝐹) = 𝑁)
41403expa 1120 . . . . 5 ((((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝐹𝑇𝑁𝑇)) ∧ (𝑅𝐹) = (𝑅𝑁)) → ∃𝑢𝐸 (𝑢𝐹) = 𝑁)
4238, 41sylan2b 597 . . . 4 ((((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝐹𝑇𝑁𝑇)) ∧ (𝑅𝑁) = (𝑅𝐹)) → ∃𝑢𝐸 (𝑢𝐹) = 𝑁)
43 eqid 2737 . . . . . . 7 (𝑇 ↦ ( I ↾ (Base‘𝐾))) = (𝑇 ↦ ( I ↾ (Base‘𝐾)))
446, 7, 8, 39, 43tendo0cl 38541 . . . . . 6 ((𝐾 ∈ HL ∧ 𝑊𝐻) → (𝑇 ↦ ( I ↾ (Base‘𝐾))) ∈ 𝐸)
4544ad2antrr 726 . . . . 5 ((((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝐹𝑇𝑁𝑇)) ∧ (𝑅𝑁) = (0.‘𝐾)) → (𝑇 ↦ ( I ↾ (Base‘𝐾))) ∈ 𝐸)
46 simplrl 777 . . . . . . 7 ((((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝐹𝑇𝑁𝑇)) ∧ (𝑅𝑁) = (0.‘𝐾)) → 𝐹𝑇)
4743, 6tendo02 38538 . . . . . . 7 (𝐹𝑇 → ((𝑇 ↦ ( I ↾ (Base‘𝐾)))‘𝐹) = ( I ↾ (Base‘𝐾)))
4846, 47syl 17 . . . . . 6 ((((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝐹𝑇𝑁𝑇)) ∧ (𝑅𝑁) = (0.‘𝐾)) → ((𝑇 ↦ ( I ↾ (Base‘𝐾)))‘𝐹) = ( I ↾ (Base‘𝐾)))
496, 15, 7, 8, 9trlid0b 37929 . . . . . . . 8 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ 𝑁𝑇) → (𝑁 = ( I ↾ (Base‘𝐾)) ↔ (𝑅𝑁) = (0.‘𝐾)))
5049adantrl 716 . . . . . . 7 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝐹𝑇𝑁𝑇)) → (𝑁 = ( I ↾ (Base‘𝐾)) ↔ (𝑅𝑁) = (0.‘𝐾)))
5150biimpar 481 . . . . . 6 ((((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝐹𝑇𝑁𝑇)) ∧ (𝑅𝑁) = (0.‘𝐾)) → 𝑁 = ( I ↾ (Base‘𝐾)))
5248, 51eqtr4d 2780 . . . . 5 ((((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝐹𝑇𝑁𝑇)) ∧ (𝑅𝑁) = (0.‘𝐾)) → ((𝑇 ↦ ( I ↾ (Base‘𝐾)))‘𝐹) = 𝑁)
53 fveq1 6716 . . . . . . 7 (𝑢 = (𝑇 ↦ ( I ↾ (Base‘𝐾))) → (𝑢𝐹) = ((𝑇 ↦ ( I ↾ (Base‘𝐾)))‘𝐹))
5453eqeq1d 2739 . . . . . 6 (𝑢 = (𝑇 ↦ ( I ↾ (Base‘𝐾))) → ((𝑢𝐹) = 𝑁 ↔ ((𝑇 ↦ ( I ↾ (Base‘𝐾)))‘𝐹) = 𝑁))
5554rspcev 3537 . . . . 5 (((𝑇 ↦ ( I ↾ (Base‘𝐾))) ∈ 𝐸 ∧ ((𝑇 ↦ ( I ↾ (Base‘𝐾)))‘𝐹) = 𝑁) → ∃𝑢𝐸 (𝑢𝐹) = 𝑁)
5645, 52, 55syl2anc 587 . . . 4 ((((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝐹𝑇𝑁𝑇)) ∧ (𝑅𝑁) = (0.‘𝐾)) → ∃𝑢𝐸 (𝑢𝐹) = 𝑁)
5742, 56jaodan 958 . . 3 ((((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝐹𝑇𝑁𝑇)) ∧ ((𝑅𝑁) = (𝑅𝐹) ∨ (𝑅𝑁) = (0.‘𝐾))) → ∃𝑢𝐸 (𝑢𝐹) = 𝑁)
5837, 57syldan 594 . 2 ((((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝐹𝑇𝑁𝑇)) ∧ (𝑅𝑁) (𝑅𝐹)) → ∃𝑢𝐸 (𝑢𝐹) = 𝑁)
59583impa 1112 1 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝐹𝑇𝑁𝑇) ∧ (𝑅𝑁) (𝑅𝐹)) → ∃𝑢𝐸 (𝑢𝐹) = 𝑁)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 209  wa 399  wo 847  w3a 1089   = wceq 1543  wcel 2110  wrex 3062   class class class wbr 5053  cmpt 5135   I cid 5454  cres 5553  cfv 6380  Basecbs 16760  lecple 16809  0.cp0 17929  OPcops 36923  Atomscatm 37014  HLchlt 37101  LHypclh 37735  LTrncltrn 37852  trLctrl 37909  TEndoctendo 38503
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1803  ax-4 1817  ax-5 1918  ax-6 1976  ax-7 2016  ax-8 2112  ax-9 2120  ax-10 2141  ax-11 2158  ax-12 2175  ax-ext 2708  ax-rep 5179  ax-sep 5192  ax-nul 5199  ax-pow 5258  ax-pr 5322  ax-un 7523  ax-riotaBAD 36704
This theorem depends on definitions:  df-bi 210  df-an 400  df-or 848  df-3or 1090  df-3an 1091  df-tru 1546  df-fal 1556  df-ex 1788  df-nf 1792  df-sb 2071  df-mo 2539  df-eu 2568  df-clab 2715  df-cleq 2729  df-clel 2816  df-nfc 2886  df-ne 2941  df-ral 3066  df-rex 3067  df-reu 3068  df-rmo 3069  df-rab 3070  df-v 3410  df-sbc 3695  df-csb 3812  df-dif 3869  df-un 3871  df-in 3873  df-ss 3883  df-nul 4238  df-if 4440  df-pw 4515  df-sn 4542  df-pr 4544  df-op 4548  df-uni 4820  df-iun 4906  df-iin 4907  df-br 5054  df-opab 5116  df-mpt 5136  df-id 5455  df-xp 5557  df-rel 5558  df-cnv 5559  df-co 5560  df-dm 5561  df-rn 5562  df-res 5563  df-ima 5564  df-iota 6338  df-fun 6382  df-fn 6383  df-f 6384  df-f1 6385  df-fo 6386  df-f1o 6387  df-fv 6388  df-riota 7170  df-ov 7216  df-oprab 7217  df-mpo 7218  df-1st 7761  df-2nd 7762  df-undef 8015  df-map 8510  df-proset 17802  df-poset 17820  df-plt 17836  df-lub 17852  df-glb 17853  df-join 17854  df-meet 17855  df-p0 17931  df-p1 17932  df-lat 17938  df-clat 18005  df-oposet 36927  df-ol 36929  df-oml 36930  df-covers 37017  df-ats 37018  df-atl 37049  df-cvlat 37073  df-hlat 37102  df-llines 37249  df-lplanes 37250  df-lvols 37251  df-lines 37252  df-psubsp 37254  df-pmap 37255  df-padd 37547  df-lhyp 37739  df-laut 37740  df-ldil 37855  df-ltrn 37856  df-trl 37910  df-tendo 38506
This theorem is referenced by:  dva1dim  38736  dihjatcclem4  39172
  Copyright terms: Public domain W3C validator