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

Theorem dva1dim 35094
Description: Two expressions for the 1-dimensional subspaces of partial vector space A. Remark in [Crawley] p. 120 line 21, but using a non-identity translation (nonzero vector) 𝐹 whose trace is 𝑃 rather than 𝑃 itself; 𝐹 exists by cdlemf 34672. 𝐸 is the division ring base by erngdv 35102, and 𝑠𝐹 is the scalar product by dvavsca 35126. 𝐹 must be a non-identity translation for the expression to be a 1-dimensional subspace, although the theorem doesn't require it. (Contributed by NM, 14-Oct-2013.)
Hypotheses
Ref Expression
dva1dim.l = (le‘𝐾)
dva1dim.h 𝐻 = (LHyp‘𝐾)
dva1dim.t 𝑇 = ((LTrn‘𝐾)‘𝑊)
dva1dim.r 𝑅 = ((trL‘𝐾)‘𝑊)
dva1dim.e 𝐸 = ((TEndo‘𝐾)‘𝑊)
Assertion
Ref Expression
dva1dim (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ 𝐹𝑇) → {𝑔 ∣ ∃𝑠𝐸 𝑔 = (𝑠𝐹)} = {𝑔𝑇 ∣ (𝑅𝑔) (𝑅𝐹)})
Distinct variable groups:   ,𝑠   𝐸,𝑠   𝑔,𝑠,𝐹   𝑔,𝐻,𝑠   𝑔,𝐾,𝑠   𝑅,𝑠   𝑇,𝑔,𝑠   𝑔,𝑊,𝑠
Allowed substitution hints:   𝑅(𝑔)   𝐸(𝑔)   (𝑔)

Proof of Theorem dva1dim
StepHypRef Expression
1 dva1dim.h . . . . . . . . . 10 𝐻 = (LHyp‘𝐾)
2 dva1dim.t . . . . . . . . . 10 𝑇 = ((LTrn‘𝐾)‘𝑊)
3 dva1dim.e . . . . . . . . . 10 𝐸 = ((TEndo‘𝐾)‘𝑊)
41, 2, 3tendocl 34876 . . . . . . . . 9 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ 𝑠𝐸𝐹𝑇) → (𝑠𝐹) ∈ 𝑇)
5 dva1dim.l . . . . . . . . . 10 = (le‘𝐾)
6 dva1dim.r . . . . . . . . . 10 𝑅 = ((trL‘𝐾)‘𝑊)
75, 1, 2, 6, 3tendotp 34870 . . . . . . . . 9 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ 𝑠𝐸𝐹𝑇) → (𝑅‘(𝑠𝐹)) (𝑅𝐹))
84, 7jca 552 . . . . . . . 8 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ 𝑠𝐸𝐹𝑇) → ((𝑠𝐹) ∈ 𝑇 ∧ (𝑅‘(𝑠𝐹)) (𝑅𝐹)))
983expb 1257 . . . . . . 7 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑠𝐸𝐹𝑇)) → ((𝑠𝐹) ∈ 𝑇 ∧ (𝑅‘(𝑠𝐹)) (𝑅𝐹)))
109anass1rs 844 . . . . . 6 ((((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ 𝐹𝑇) ∧ 𝑠𝐸) → ((𝑠𝐹) ∈ 𝑇 ∧ (𝑅‘(𝑠𝐹)) (𝑅𝐹)))
11 eleq1 2675 . . . . . . 7 (𝑔 = (𝑠𝐹) → (𝑔𝑇 ↔ (𝑠𝐹) ∈ 𝑇))
12 fveq2 6088 . . . . . . . 8 (𝑔 = (𝑠𝐹) → (𝑅𝑔) = (𝑅‘(𝑠𝐹)))
1312breq1d 4587 . . . . . . 7 (𝑔 = (𝑠𝐹) → ((𝑅𝑔) (𝑅𝐹) ↔ (𝑅‘(𝑠𝐹)) (𝑅𝐹)))
1411, 13anbi12d 742 . . . . . 6 (𝑔 = (𝑠𝐹) → ((𝑔𝑇 ∧ (𝑅𝑔) (𝑅𝐹)) ↔ ((𝑠𝐹) ∈ 𝑇 ∧ (𝑅‘(𝑠𝐹)) (𝑅𝐹))))
1510, 14syl5ibrcom 235 . . . . 5 ((((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ 𝐹𝑇) ∧ 𝑠𝐸) → (𝑔 = (𝑠𝐹) → (𝑔𝑇 ∧ (𝑅𝑔) (𝑅𝐹))))
1615rexlimdva 3012 . . . 4 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ 𝐹𝑇) → (∃𝑠𝐸 𝑔 = (𝑠𝐹) → (𝑔𝑇 ∧ (𝑅𝑔) (𝑅𝐹))))
17 simpll 785 . . . . . . 7 ((((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ 𝐹𝑇) ∧ (𝑔𝑇 ∧ (𝑅𝑔) (𝑅𝐹))) → (𝐾 ∈ HL ∧ 𝑊𝐻))
18 simplr 787 . . . . . . 7 ((((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ 𝐹𝑇) ∧ (𝑔𝑇 ∧ (𝑅𝑔) (𝑅𝐹))) → 𝐹𝑇)
19 simprl 789 . . . . . . 7 ((((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ 𝐹𝑇) ∧ (𝑔𝑇 ∧ (𝑅𝑔) (𝑅𝐹))) → 𝑔𝑇)
20 simprr 791 . . . . . . 7 ((((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ 𝐹𝑇) ∧ (𝑔𝑇 ∧ (𝑅𝑔) (𝑅𝐹))) → (𝑅𝑔) (𝑅𝐹))
215, 1, 2, 6, 3tendoex 35084 . . . . . . 7 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝐹𝑇𝑔𝑇) ∧ (𝑅𝑔) (𝑅𝐹)) → ∃𝑠𝐸 (𝑠𝐹) = 𝑔)
2217, 18, 19, 20, 21syl121anc 1322 . . . . . 6 ((((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ 𝐹𝑇) ∧ (𝑔𝑇 ∧ (𝑅𝑔) (𝑅𝐹))) → ∃𝑠𝐸 (𝑠𝐹) = 𝑔)
23 eqcom 2616 . . . . . . 7 ((𝑠𝐹) = 𝑔𝑔 = (𝑠𝐹))
2423rexbii 3022 . . . . . 6 (∃𝑠𝐸 (𝑠𝐹) = 𝑔 ↔ ∃𝑠𝐸 𝑔 = (𝑠𝐹))
2522, 24sylib 206 . . . . 5 ((((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ 𝐹𝑇) ∧ (𝑔𝑇 ∧ (𝑅𝑔) (𝑅𝐹))) → ∃𝑠𝐸 𝑔 = (𝑠𝐹))
2625ex 448 . . . 4 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ 𝐹𝑇) → ((𝑔𝑇 ∧ (𝑅𝑔) (𝑅𝐹)) → ∃𝑠𝐸 𝑔 = (𝑠𝐹)))
2716, 26impbid 200 . . 3 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ 𝐹𝑇) → (∃𝑠𝐸 𝑔 = (𝑠𝐹) ↔ (𝑔𝑇 ∧ (𝑅𝑔) (𝑅𝐹))))
2827abbidv 2727 . 2 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ 𝐹𝑇) → {𝑔 ∣ ∃𝑠𝐸 𝑔 = (𝑠𝐹)} = {𝑔 ∣ (𝑔𝑇 ∧ (𝑅𝑔) (𝑅𝐹))})
29 df-rab 2904 . 2 {𝑔𝑇 ∣ (𝑅𝑔) (𝑅𝐹)} = {𝑔 ∣ (𝑔𝑇 ∧ (𝑅𝑔) (𝑅𝐹))}
3028, 29syl6eqr 2661 1 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ 𝐹𝑇) → {𝑔 ∣ ∃𝑠𝐸 𝑔 = (𝑠𝐹)} = {𝑔𝑇 ∣ (𝑅𝑔) (𝑅𝐹)})
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 382  w3a 1030   = wceq 1474  wcel 1976  {cab 2595  wrex 2896  {crab 2899   class class class wbr 4577  cfv 5790  lecple 15721  HLchlt 33458  LHypclh 34091  LTrncltrn 34208  trLctrl 34266  TEndoctendo 34861
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1712  ax-4 1727  ax-5 1826  ax-6 1874  ax-7 1921  ax-8 1978  ax-9 1985  ax-10 2005  ax-11 2020  ax-12 2032  ax-13 2232  ax-ext 2589  ax-rep 4693  ax-sep 4703  ax-nul 4712  ax-pow 4764  ax-pr 4828  ax-un 6824  ax-riotaBAD 33060
This theorem depends on definitions:  df-bi 195  df-or 383  df-an 384  df-3or 1031  df-3an 1032  df-tru 1477  df-fal 1480  df-ex 1695  df-nf 1700  df-sb 1867  df-eu 2461  df-mo 2462  df-clab 2596  df-cleq 2602  df-clel 2605  df-nfc 2739  df-ne 2781  df-nel 2782  df-ral 2900  df-rex 2901  df-reu 2902  df-rmo 2903  df-rab 2904  df-v 3174  df-sbc 3402  df-csb 3499  df-dif 3542  df-un 3544  df-in 3546  df-ss 3553  df-nul 3874  df-if 4036  df-pw 4109  df-sn 4125  df-pr 4127  df-op 4131  df-uni 4367  df-iun 4451  df-iin 4452  df-br 4578  df-opab 4638  df-mpt 4639  df-id 4943  df-xp 5034  df-rel 5035  df-cnv 5036  df-co 5037  df-dm 5038  df-rn 5039  df-res 5040  df-ima 5041  df-iota 5754  df-fun 5792  df-fn 5793  df-f 5794  df-f1 5795  df-fo 5796  df-f1o 5797  df-fv 5798  df-riota 6489  df-ov 6530  df-oprab 6531  df-mpt2 6532  df-1st 7036  df-2nd 7037  df-undef 7263  df-map 7723  df-preset 16697  df-poset 16715  df-plt 16727  df-lub 16743  df-glb 16744  df-join 16745  df-meet 16746  df-p0 16808  df-p1 16809  df-lat 16815  df-clat 16877  df-oposet 33284  df-ol 33286  df-oml 33287  df-covers 33374  df-ats 33375  df-atl 33406  df-cvlat 33430  df-hlat 33459  df-llines 33605  df-lplanes 33606  df-lvols 33607  df-lines 33608  df-psubsp 33610  df-pmap 33611  df-padd 33903  df-lhyp 34095  df-laut 34096  df-ldil 34211  df-ltrn 34212  df-trl 34267  df-tendo 34864
This theorem is referenced by:  dvhb1dimN  35095  dia1dim  35171
  Copyright terms: Public domain W3C validator