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

Theorem tendoicl 36578
Description: Closure of the additive inverse endomorphism. (Contributed by NM, 12-Jun-2013.)
Hypotheses
Ref Expression
tendoicl.h 𝐻 = (LHyp‘𝐾)
tendoicl.t 𝑇 = ((LTrn‘𝐾)‘𝑊)
tendoicl.e 𝐸 = ((TEndo‘𝐾)‘𝑊)
tendoicl.i 𝐼 = (𝑠𝐸 ↦ (𝑓𝑇(𝑠𝑓)))
Assertion
Ref Expression
tendoicl (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ 𝑆𝐸) → (𝐼𝑆) ∈ 𝐸)
Distinct variable groups:   𝐸,𝑠   𝑓,𝑠,𝑇   𝑓,𝑊,𝑠
Allowed substitution hints:   𝑆(𝑓,𝑠)   𝐸(𝑓)   𝐻(𝑓,𝑠)   𝐼(𝑓,𝑠)   𝐾(𝑓,𝑠)

Proof of Theorem tendoicl
Dummy variables 𝑔 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 eqid 2752 . 2 (le‘𝐾) = (le‘𝐾)
2 tendoicl.h . 2 𝐻 = (LHyp‘𝐾)
3 tendoicl.t . 2 𝑇 = ((LTrn‘𝐾)‘𝑊)
4 eqid 2752 . 2 ((trL‘𝐾)‘𝑊) = ((trL‘𝐾)‘𝑊)
5 tendoicl.e . 2 𝐸 = ((TEndo‘𝐾)‘𝑊)
6 simpl 474 . 2 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ 𝑆𝐸) → (𝐾 ∈ HL ∧ 𝑊𝐻))
7 simpll 807 . . . . 5 ((((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ 𝑆𝐸) ∧ 𝑔𝑇) → (𝐾 ∈ HL ∧ 𝑊𝐻))
82, 3, 5tendocl 36549 . . . . . 6 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ 𝑆𝐸𝑔𝑇) → (𝑆𝑔) ∈ 𝑇)
983expa 1111 . . . . 5 ((((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ 𝑆𝐸) ∧ 𝑔𝑇) → (𝑆𝑔) ∈ 𝑇)
102, 3ltrncnv 35927 . . . . 5 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑆𝑔) ∈ 𝑇) → (𝑆𝑔) ∈ 𝑇)
117, 9, 10syl2anc 696 . . . 4 ((((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ 𝑆𝐸) ∧ 𝑔𝑇) → (𝑆𝑔) ∈ 𝑇)
12 eqid 2752 . . . 4 (𝑔𝑇(𝑆𝑔)) = (𝑔𝑇(𝑆𝑔))
1311, 12fmptd 6540 . . 3 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ 𝑆𝐸) → (𝑔𝑇(𝑆𝑔)):𝑇𝑇)
14 tendoicl.i . . . . . 6 𝐼 = (𝑠𝐸 ↦ (𝑓𝑇(𝑠𝑓)))
1514, 3tendoi 36576 . . . . 5 (𝑆𝐸 → (𝐼𝑆) = (𝑔𝑇(𝑆𝑔)))
1615adantl 473 . . . 4 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ 𝑆𝐸) → (𝐼𝑆) = (𝑔𝑇(𝑆𝑔)))
1716feq1d 6183 . . 3 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ 𝑆𝐸) → ((𝐼𝑆):𝑇𝑇 ↔ (𝑔𝑇(𝑆𝑔)):𝑇𝑇))
1813, 17mpbird 247 . 2 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ 𝑆𝐸) → (𝐼𝑆):𝑇𝑇)
19 simp1r 1238 . . . 4 ((((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ 𝑆𝐸) ∧ 𝑔𝑇𝑇) → 𝑆𝐸)
202, 3ltrnco 36501 . . . . 5 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ 𝑔𝑇𝑇) → (𝑔) ∈ 𝑇)
21203adant1r 1185 . . . 4 ((((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ 𝑆𝐸) ∧ 𝑔𝑇𝑇) → (𝑔) ∈ 𝑇)
2214, 3tendoi2 36577 . . . 4 ((𝑆𝐸 ∧ (𝑔) ∈ 𝑇) → ((𝐼𝑆)‘(𝑔)) = (𝑆‘(𝑔)))
2319, 21, 22syl2anc 696 . . 3 ((((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ 𝑆𝐸) ∧ 𝑔𝑇𝑇) → ((𝐼𝑆)‘(𝑔)) = (𝑆‘(𝑔)))
24 cnvco 5455 . . . 4 ((𝑆) ∘ (𝑆𝑔)) = ((𝑆𝑔) ∘ (𝑆))
252, 3ltrncom 36520 . . . . . . . 8 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ 𝑔𝑇𝑇) → (𝑔) = (𝑔))
26253adant1r 1185 . . . . . . 7 ((((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ 𝑆𝐸) ∧ 𝑔𝑇𝑇) → (𝑔) = (𝑔))
2726fveq2d 6348 . . . . . 6 ((((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ 𝑆𝐸) ∧ 𝑔𝑇𝑇) → (𝑆‘(𝑔)) = (𝑆‘(𝑔)))
28 simp1ll 1300 . . . . . . 7 ((((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ 𝑆𝐸) ∧ 𝑔𝑇𝑇) → 𝐾 ∈ HL)
29 simp1lr 1301 . . . . . . 7 ((((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ 𝑆𝐸) ∧ 𝑔𝑇𝑇) → 𝑊𝐻)
30 simp3 1132 . . . . . . 7 ((((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ 𝑆𝐸) ∧ 𝑔𝑇𝑇) → 𝑇)
31 simp2 1131 . . . . . . 7 ((((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ 𝑆𝐸) ∧ 𝑔𝑇𝑇) → 𝑔𝑇)
322, 3, 5tendovalco 36547 . . . . . . 7 (((𝐾 ∈ HL ∧ 𝑊𝐻𝑆𝐸) ∧ (𝑇𝑔𝑇)) → (𝑆‘(𝑔)) = ((𝑆) ∘ (𝑆𝑔)))
3328, 29, 19, 30, 31, 32syl32anc 1481 . . . . . 6 ((((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ 𝑆𝐸) ∧ 𝑔𝑇𝑇) → (𝑆‘(𝑔)) = ((𝑆) ∘ (𝑆𝑔)))
3427, 33eqtrd 2786 . . . . 5 ((((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ 𝑆𝐸) ∧ 𝑔𝑇𝑇) → (𝑆‘(𝑔)) = ((𝑆) ∘ (𝑆𝑔)))
3534cnveqd 5445 . . . 4 ((((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ 𝑆𝐸) ∧ 𝑔𝑇𝑇) → (𝑆‘(𝑔)) = ((𝑆) ∘ (𝑆𝑔)))
3614, 3tendoi2 36577 . . . . . 6 ((𝑆𝐸𝑔𝑇) → ((𝐼𝑆)‘𝑔) = (𝑆𝑔))
3719, 31, 36syl2anc 696 . . . . 5 ((((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ 𝑆𝐸) ∧ 𝑔𝑇𝑇) → ((𝐼𝑆)‘𝑔) = (𝑆𝑔))
3814, 3tendoi2 36577 . . . . . 6 ((𝑆𝐸𝑇) → ((𝐼𝑆)‘) = (𝑆))
3919, 30, 38syl2anc 696 . . . . 5 ((((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ 𝑆𝐸) ∧ 𝑔𝑇𝑇) → ((𝐼𝑆)‘) = (𝑆))
4037, 39coeq12d 5434 . . . 4 ((((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ 𝑆𝐸) ∧ 𝑔𝑇𝑇) → (((𝐼𝑆)‘𝑔) ∘ ((𝐼𝑆)‘)) = ((𝑆𝑔) ∘ (𝑆)))
4124, 35, 403eqtr4a 2812 . . 3 ((((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ 𝑆𝐸) ∧ 𝑔𝑇𝑇) → (𝑆‘(𝑔)) = (((𝐼𝑆)‘𝑔) ∘ ((𝐼𝑆)‘)))
4223, 41eqtrd 2786 . 2 ((((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ 𝑆𝐸) ∧ 𝑔𝑇𝑇) → ((𝐼𝑆)‘(𝑔)) = (((𝐼𝑆)‘𝑔) ∘ ((𝐼𝑆)‘)))
4336adantll 752 . . . . 5 ((((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ 𝑆𝐸) ∧ 𝑔𝑇) → ((𝐼𝑆)‘𝑔) = (𝑆𝑔))
4443fveq2d 6348 . . . 4 ((((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ 𝑆𝐸) ∧ 𝑔𝑇) → (((trL‘𝐾)‘𝑊)‘((𝐼𝑆)‘𝑔)) = (((trL‘𝐾)‘𝑊)‘(𝑆𝑔)))
452, 3, 4trlcnv 35947 . . . . 5 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑆𝑔) ∈ 𝑇) → (((trL‘𝐾)‘𝑊)‘(𝑆𝑔)) = (((trL‘𝐾)‘𝑊)‘(𝑆𝑔)))
467, 9, 45syl2anc 696 . . . 4 ((((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ 𝑆𝐸) ∧ 𝑔𝑇) → (((trL‘𝐾)‘𝑊)‘(𝑆𝑔)) = (((trL‘𝐾)‘𝑊)‘(𝑆𝑔)))
4744, 46eqtrd 2786 . . 3 ((((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ 𝑆𝐸) ∧ 𝑔𝑇) → (((trL‘𝐾)‘𝑊)‘((𝐼𝑆)‘𝑔)) = (((trL‘𝐾)‘𝑊)‘(𝑆𝑔)))
481, 2, 3, 4, 5tendotp 36543 . . . 4 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ 𝑆𝐸𝑔𝑇) → (((trL‘𝐾)‘𝑊)‘(𝑆𝑔))(le‘𝐾)(((trL‘𝐾)‘𝑊)‘𝑔))
49483expa 1111 . . 3 ((((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ 𝑆𝐸) ∧ 𝑔𝑇) → (((trL‘𝐾)‘𝑊)‘(𝑆𝑔))(le‘𝐾)(((trL‘𝐾)‘𝑊)‘𝑔))
5047, 49eqbrtrd 4818 . 2 ((((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ 𝑆𝐸) ∧ 𝑔𝑇) → (((trL‘𝐾)‘𝑊)‘((𝐼𝑆)‘𝑔))(le‘𝐾)(((trL‘𝐾)‘𝑊)‘𝑔))
511, 2, 3, 4, 5, 6, 18, 42, 50istendod 36544 1 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ 𝑆𝐸) → (𝐼𝑆) ∈ 𝐸)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 383  w3a 1072   = wceq 1624  wcel 2131   class class class wbr 4796  cmpt 4873  ccnv 5257  ccom 5262  wf 6037  cfv 6041  lecple 16142  HLchlt 35132  LHypclh 35765  LTrncltrn 35882  trLctrl 35940  TEndoctendo 36534
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1863  ax-4 1878  ax-5 1980  ax-6 2046  ax-7 2082  ax-8 2133  ax-9 2140  ax-10 2160  ax-11 2175  ax-12 2188  ax-13 2383  ax-ext 2732  ax-rep 4915  ax-sep 4925  ax-nul 4933  ax-pow 4984  ax-pr 5047  ax-un 7106  ax-riotaBAD 34734
This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-3or 1073  df-3an 1074  df-tru 1627  df-ex 1846  df-nf 1851  df-sb 2039  df-eu 2603  df-mo 2604  df-clab 2739  df-cleq 2745  df-clel 2748  df-nfc 2883  df-ne 2925  df-nel 3028  df-ral 3047  df-rex 3048  df-reu 3049  df-rmo 3050  df-rab 3051  df-v 3334  df-sbc 3569  df-csb 3667  df-dif 3710  df-un 3712  df-in 3714  df-ss 3721  df-nul 4051  df-if 4223  df-pw 4296  df-sn 4314  df-pr 4316  df-op 4320  df-uni 4581  df-iun 4666  df-iin 4667  df-br 4797  df-opab 4857  df-mpt 4874  df-id 5166  df-xp 5264  df-rel 5265  df-cnv 5266  df-co 5267  df-dm 5268  df-rn 5269  df-res 5270  df-ima 5271  df-iota 6004  df-fun 6043  df-fn 6044  df-f 6045  df-f1 6046  df-fo 6047  df-f1o 6048  df-fv 6049  df-riota 6766  df-ov 6808  df-oprab 6809  df-mpt2 6810  df-1st 7325  df-2nd 7326  df-undef 7560  df-map 8017  df-preset 17121  df-poset 17139  df-plt 17151  df-lub 17167  df-glb 17168  df-join 17169  df-meet 17170  df-p0 17232  df-p1 17233  df-lat 17239  df-clat 17301  df-oposet 34958  df-ol 34960  df-oml 34961  df-covers 35048  df-ats 35049  df-atl 35080  df-cvlat 35104  df-hlat 35133  df-llines 35279  df-lplanes 35280  df-lvols 35281  df-lines 35282  df-psubsp 35284  df-pmap 35285  df-padd 35577  df-lhyp 35769  df-laut 35770  df-ldil 35885  df-ltrn 35886  df-trl 35941  df-tendo 36537
This theorem is referenced by:  tendoipl  36579  tendoipl2  36580  erngdvlem1  36770  erngdvlem1-rN  36778  dihjatcclem4  37204
  Copyright terms: Public domain W3C validator