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

Theorem tendoplcl 36855
Description: Endomorphism sum is a trace-preserving endomorphism. (Contributed by NM, 10-Jun-2013.)
Hypotheses
Ref Expression
tendopl.h 𝐻 = (LHyp‘𝐾)
tendopl.t 𝑇 = ((LTrn‘𝐾)‘𝑊)
tendopl.e 𝐸 = ((TEndo‘𝐾)‘𝑊)
tendopl.p 𝑃 = (𝑠𝐸, 𝑡𝐸 ↦ (𝑓𝑇 ↦ ((𝑠𝑓) ∘ (𝑡𝑓))))
Assertion
Ref Expression
tendoplcl (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ 𝑈𝐸𝑉𝐸) → (𝑈𝑃𝑉) ∈ 𝐸)
Distinct variable groups:   𝑡,𝑠,𝐸   𝑓,𝑠,𝑡,𝑇   𝑓,𝑊,𝑠,𝑡
Allowed substitution hints:   𝑃(𝑡,𝑓,𝑠)   𝑈(𝑡,𝑓,𝑠)   𝐸(𝑓)   𝐻(𝑡,𝑓,𝑠)   𝐾(𝑡,𝑓,𝑠)   𝑉(𝑡,𝑓,𝑠)

Proof of Theorem tendoplcl
Dummy variables 𝑔 𝑖 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 eqid 2824 . 2 (le‘𝐾) = (le‘𝐾)
2 tendopl.h . 2 𝐻 = (LHyp‘𝐾)
3 tendopl.t . 2 𝑇 = ((LTrn‘𝐾)‘𝑊)
4 eqid 2824 . 2 ((trL‘𝐾)‘𝑊) = ((trL‘𝐾)‘𝑊)
5 tendopl.e . 2 𝐸 = ((TEndo‘𝐾)‘𝑊)
6 simp1 1172 . 2 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ 𝑈𝐸𝑉𝐸) → (𝐾 ∈ HL ∧ 𝑊𝐻))
7 simpl1 1248 . . . . 5 ((((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ 𝑈𝐸𝑉𝐸) ∧ 𝑔𝑇) → (𝐾 ∈ HL ∧ 𝑊𝐻))
8 simpl2 1250 . . . . . 6 ((((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ 𝑈𝐸𝑉𝐸) ∧ 𝑔𝑇) → 𝑈𝐸)
9 simpr 479 . . . . . 6 ((((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ 𝑈𝐸𝑉𝐸) ∧ 𝑔𝑇) → 𝑔𝑇)
102, 3, 5tendocl 36841 . . . . . 6 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ 𝑈𝐸𝑔𝑇) → (𝑈𝑔) ∈ 𝑇)
117, 8, 9, 10syl3anc 1496 . . . . 5 ((((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ 𝑈𝐸𝑉𝐸) ∧ 𝑔𝑇) → (𝑈𝑔) ∈ 𝑇)
12 simpl3 1252 . . . . . 6 ((((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ 𝑈𝐸𝑉𝐸) ∧ 𝑔𝑇) → 𝑉𝐸)
132, 3, 5tendocl 36841 . . . . . 6 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ 𝑉𝐸𝑔𝑇) → (𝑉𝑔) ∈ 𝑇)
147, 12, 9, 13syl3anc 1496 . . . . 5 ((((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ 𝑈𝐸𝑉𝐸) ∧ 𝑔𝑇) → (𝑉𝑔) ∈ 𝑇)
152, 3ltrnco 36793 . . . . 5 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑈𝑔) ∈ 𝑇 ∧ (𝑉𝑔) ∈ 𝑇) → ((𝑈𝑔) ∘ (𝑉𝑔)) ∈ 𝑇)
167, 11, 14, 15syl3anc 1496 . . . 4 ((((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ 𝑈𝐸𝑉𝐸) ∧ 𝑔𝑇) → ((𝑈𝑔) ∘ (𝑉𝑔)) ∈ 𝑇)
1716fmpttd 6633 . . 3 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ 𝑈𝐸𝑉𝐸) → (𝑔𝑇 ↦ ((𝑈𝑔) ∘ (𝑉𝑔))):𝑇𝑇)
18 tendopl.p . . . . . 6 𝑃 = (𝑠𝐸, 𝑡𝐸 ↦ (𝑓𝑇 ↦ ((𝑠𝑓) ∘ (𝑡𝑓))))
1918, 3tendopl 36850 . . . . 5 ((𝑈𝐸𝑉𝐸) → (𝑈𝑃𝑉) = (𝑔𝑇 ↦ ((𝑈𝑔) ∘ (𝑉𝑔))))
20193adant1 1166 . . . 4 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ 𝑈𝐸𝑉𝐸) → (𝑈𝑃𝑉) = (𝑔𝑇 ↦ ((𝑈𝑔) ∘ (𝑉𝑔))))
2120feq1d 6262 . . 3 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ 𝑈𝐸𝑉𝐸) → ((𝑈𝑃𝑉):𝑇𝑇 ↔ (𝑔𝑇 ↦ ((𝑈𝑔) ∘ (𝑉𝑔))):𝑇𝑇))
2217, 21mpbird 249 . 2 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ 𝑈𝐸𝑉𝐸) → (𝑈𝑃𝑉):𝑇𝑇)
23 simp11 1266 . . 3 ((((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ 𝑈𝐸𝑉𝐸) ∧ 𝑇𝑖𝑇) → (𝐾 ∈ HL ∧ 𝑊𝐻))
24 simp12 1267 . . 3 ((((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ 𝑈𝐸𝑉𝐸) ∧ 𝑇𝑖𝑇) → 𝑈𝐸)
25 simp13 1268 . . 3 ((((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ 𝑈𝐸𝑉𝐸) ∧ 𝑇𝑖𝑇) → 𝑉𝐸)
26 3simpc 1188 . . 3 ((((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ 𝑈𝐸𝑉𝐸) ∧ 𝑇𝑖𝑇) → (𝑇𝑖𝑇))
272, 3, 5, 18tendoplco2 36853 . . 3 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑈𝐸𝑉𝐸) ∧ (𝑇𝑖𝑇)) → ((𝑈𝑃𝑉)‘(𝑖)) = (((𝑈𝑃𝑉)‘) ∘ ((𝑈𝑃𝑉)‘𝑖)))
2823, 24, 25, 26, 27syl121anc 1500 . 2 ((((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ 𝑈𝐸𝑉𝐸) ∧ 𝑇𝑖𝑇) → ((𝑈𝑃𝑉)‘(𝑖)) = (((𝑈𝑃𝑉)‘) ∘ ((𝑈𝑃𝑉)‘𝑖)))
29 simpl1 1248 . . 3 ((((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ 𝑈𝐸𝑉𝐸) ∧ 𝑇) → (𝐾 ∈ HL ∧ 𝑊𝐻))
30 simpl2 1250 . . 3 ((((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ 𝑈𝐸𝑉𝐸) ∧ 𝑇) → 𝑈𝐸)
31 simpl3 1252 . . 3 ((((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ 𝑈𝐸𝑉𝐸) ∧ 𝑇) → 𝑉𝐸)
32 simpr 479 . . 3 ((((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ 𝑈𝐸𝑉𝐸) ∧ 𝑇) → 𝑇)
332, 3, 5, 18, 1, 4tendopltp 36854 . . 3 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑈𝐸𝑉𝐸) ∧ 𝑇) → (((trL‘𝐾)‘𝑊)‘((𝑈𝑃𝑉)‘))(le‘𝐾)(((trL‘𝐾)‘𝑊)‘))
3429, 30, 31, 32, 33syl121anc 1500 . 2 ((((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ 𝑈𝐸𝑉𝐸) ∧ 𝑇) → (((trL‘𝐾)‘𝑊)‘((𝑈𝑃𝑉)‘))(le‘𝐾)(((trL‘𝐾)‘𝑊)‘))
351, 2, 3, 4, 5, 6, 22, 28, 34istendod 36836 1 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ 𝑈𝐸𝑉𝐸) → (𝑈𝑃𝑉) ∈ 𝐸)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 386  w3a 1113   = wceq 1658  wcel 2166   class class class wbr 4872  cmpt 4951  ccom 5345  wf 6118  cfv 6122  (class class class)co 6904  cmpt2 6906  lecple 16311  HLchlt 35424  LHypclh 36058  LTrncltrn 36175  trLctrl 36232  TEndoctendo 36826
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 2390  ax-ext 2802  ax-rep 4993  ax-sep 5004  ax-nul 5012  ax-pow 5064  ax-pr 5126  ax-un 7208  ax-riotaBAD 35027
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 2604  df-eu 2639  df-clab 2811  df-cleq 2817  df-clel 2820  df-nfc 2957  df-ne 2999  df-nel 3102  df-ral 3121  df-rex 3122  df-reu 3123  df-rmo 3124  df-rab 3125  df-v 3415  df-sbc 3662  df-csb 3757  df-dif 3800  df-un 3802  df-in 3804  df-ss 3811  df-nul 4144  df-if 4306  df-pw 4379  df-sn 4397  df-pr 4399  df-op 4403  df-uni 4658  df-iun 4741  df-iin 4742  df-br 4873  df-opab 4935  df-mpt 4952  df-id 5249  df-xp 5347  df-rel 5348  df-cnv 5349  df-co 5350  df-dm 5351  df-rn 5352  df-res 5353  df-ima 5354  df-iota 6085  df-fun 6124  df-fn 6125  df-f 6126  df-f1 6127  df-fo 6128  df-f1o 6129  df-fv 6130  df-riota 6865  df-ov 6907  df-oprab 6908  df-mpt2 6909  df-1st 7427  df-2nd 7428  df-undef 7663  df-map 8123  df-proset 17280  df-poset 17298  df-plt 17310  df-lub 17326  df-glb 17327  df-join 17328  df-meet 17329  df-p0 17391  df-p1 17392  df-lat 17398  df-clat 17460  df-oposet 35250  df-ol 35252  df-oml 35253  df-covers 35340  df-ats 35341  df-atl 35372  df-cvlat 35396  df-hlat 35425  df-llines 35572  df-lplanes 35573  df-lvols 35574  df-lines 35575  df-psubsp 35577  df-pmap 35578  df-padd 35870  df-lhyp 36062  df-laut 36063  df-ldil 36178  df-ltrn 36179  df-trl 36233  df-tendo 36829
This theorem is referenced by:  tendoplcom  36856  tendoplass  36857  tendodi1  36858  tendodi2  36859  tendo0pl  36865  tendoipl  36871  erngdvlem1  37062  erngdvlem3  37064  erngdvlem1-rN  37070  erngdvlem3-rN  37072  dvalveclem  37099  dvhvaddcl  37169  dicvaddcl  37264
  Copyright terms: Public domain W3C validator