Theorem tendo0mulr 39088

Description: Additive identity multiplied by a trace-preserving endomorphism. (Contributed by NM, 13-Feb-2014.)

Hypotheses

Ref	Expression
tendoid0.b	⊢ 𝐵 = (Base‘𝐾)
tendoid0.h	⊢ 𝐻 = (LHyp‘𝐾)
tendoid0.t	⊢ 𝑇 = ((LTrn‘𝐾)‘𝑊)
tendoid0.e	⊢ 𝐸 = ((TEndo‘𝐾)‘𝑊)
tendoid0.o	⊢ 𝑂 = (𝑓 ∈ 𝑇 ↦ ( I ↾ 𝐵))

Assertion

Ref	Expression
tendo0mulr	⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝑈 ∈ 𝐸) → (𝑈 ∘ 𝑂) = 𝑂)

Distinct variable groups:   𝐵,𝑓   𝑇,𝑓

Allowed substitution hints:   𝑈(𝑓)   𝐸(𝑓)   𝐻(𝑓)   𝐾(𝑓)   𝑂(𝑓)   𝑊(𝑓)

Proof of Theorem tendo0mulr

Dummy variable 𝑔 is distinct from all other variables.

Step	Hyp	Ref	Expression
1		tendoid0.b	. . . 4 ⊢ 𝐵 = (Base‘𝐾)
2		tendoid0.h	. . . 4 ⊢ 𝐻 = (LHyp‘𝐾)
3		tendoid0.t	. . . 4 ⊢ 𝑇 = ((LTrn‘𝐾)‘𝑊)
4	1, 2, 3	cdlemftr0 38829	. . 3 ⊢ ((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) → ∃𝑔 ∈ 𝑇 𝑔 ≠ ( I ↾ 𝐵))
5	4	adantr 481	. 2 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝑈 ∈ 𝐸) → ∃𝑔 ∈ 𝑇 𝑔 ≠ ( I ↾ 𝐵))
6		simpll 764	. . 3 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝑈 ∈ 𝐸) ∧ (𝑔 ∈ 𝑇 ∧ 𝑔 ≠ ( I ↾ 𝐵))) → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻))
7		simplr 766	. . . 4 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝑈 ∈ 𝐸) ∧ (𝑔 ∈ 𝑇 ∧ 𝑔 ≠ ( I ↾ 𝐵))) → 𝑈 ∈ 𝐸)
8		tendoid0.e	. . . . . 6 ⊢ 𝐸 = ((TEndo‘𝐾)‘𝑊)
9		tendoid0.o	. . . . . 6 ⊢ 𝑂 = (𝑓 ∈ 𝑇 ↦ ( I ↾ 𝐵))
10	1, 2, 3, 8, 9	tendo0cl 39051	. . . . 5 ⊢ ((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) → 𝑂 ∈ 𝐸)
11	10	ad2antrr 723	. . . 4 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝑈 ∈ 𝐸) ∧ (𝑔 ∈ 𝑇 ∧ 𝑔 ≠ ( I ↾ 𝐵))) → 𝑂 ∈ 𝐸)
12	2, 8	tendococl 39033	. . . 4 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝑈 ∈ 𝐸 ∧ 𝑂 ∈ 𝐸) → (𝑈 ∘ 𝑂) ∈ 𝐸)
13	6, 7, 11, 12	syl3anc 1370	. . 3 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝑈 ∈ 𝐸) ∧ (𝑔 ∈ 𝑇 ∧ 𝑔 ≠ ( I ↾ 𝐵))) → (𝑈 ∘ 𝑂) ∈ 𝐸)
14	9, 1	tendo02 39048	. . . . . . 7 ⊢ (𝑔 ∈ 𝑇 → (𝑂‘𝑔) = ( I ↾ 𝐵))
15	14	ad2antrl 725	. . . . . 6 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝑈 ∈ 𝐸) ∧ (𝑔 ∈ 𝑇 ∧ 𝑔 ≠ ( I ↾ 𝐵))) → (𝑂‘𝑔) = ( I ↾ 𝐵))
16	15	fveq2d 6823	. . . . 5 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝑈 ∈ 𝐸) ∧ (𝑔 ∈ 𝑇 ∧ 𝑔 ≠ ( I ↾ 𝐵))) → (𝑈‘(𝑂‘𝑔)) = (𝑈‘( I ↾ 𝐵)))
17	1, 2, 8	tendoid 39034	. . . . . 6 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝑈 ∈ 𝐸) → (𝑈‘( I ↾ 𝐵)) = ( I ↾ 𝐵))
18	17	adantr 481	. . . . 5 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝑈 ∈ 𝐸) ∧ (𝑔 ∈ 𝑇 ∧ 𝑔 ≠ ( I ↾ 𝐵))) → (𝑈‘( I ↾ 𝐵)) = ( I ↾ 𝐵))
19	16, 18	eqtrd 2776	. . . 4 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝑈 ∈ 𝐸) ∧ (𝑔 ∈ 𝑇 ∧ 𝑔 ≠ ( I ↾ 𝐵))) → (𝑈‘(𝑂‘𝑔)) = ( I ↾ 𝐵))
20		simprl 768	. . . . 5 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝑈 ∈ 𝐸) ∧ (𝑔 ∈ 𝑇 ∧ 𝑔 ≠ ( I ↾ 𝐵))) → 𝑔 ∈ 𝑇)
21	2, 3, 8	tendocoval 39027	. . . . 5 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑈 ∈ 𝐸 ∧ 𝑂 ∈ 𝐸) ∧ 𝑔 ∈ 𝑇) → ((𝑈 ∘ 𝑂)‘𝑔) = (𝑈‘(𝑂‘𝑔)))
22	6, 7, 11, 20, 21	syl121anc 1374	. . . 4 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝑈 ∈ 𝐸) ∧ (𝑔 ∈ 𝑇 ∧ 𝑔 ≠ ( I ↾ 𝐵))) → ((𝑈 ∘ 𝑂)‘𝑔) = (𝑈‘(𝑂‘𝑔)))
23	19, 22, 15	3eqtr4d 2786	. . 3 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝑈 ∈ 𝐸) ∧ (𝑔 ∈ 𝑇 ∧ 𝑔 ≠ ( I ↾ 𝐵))) → ((𝑈 ∘ 𝑂)‘𝑔) = (𝑂‘𝑔))
24		simpr 485	. . 3 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝑈 ∈ 𝐸) ∧ (𝑔 ∈ 𝑇 ∧ 𝑔 ≠ ( I ↾ 𝐵))) → (𝑔 ∈ 𝑇 ∧ 𝑔 ≠ ( I ↾ 𝐵)))
25	1, 2, 3, 8	tendocan 39085	. . 3 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ ((𝑈 ∘ 𝑂) ∈ 𝐸 ∧ 𝑂 ∈ 𝐸 ∧ ((𝑈 ∘ 𝑂)‘𝑔) = (𝑂‘𝑔)) ∧ (𝑔 ∈ 𝑇 ∧ 𝑔 ≠ ( I ↾ 𝐵))) → (𝑈 ∘ 𝑂) = 𝑂)
26	6, 13, 11, 23, 24, 25	syl131anc 1382	. 2 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝑈 ∈ 𝐸) ∧ (𝑔 ∈ 𝑇 ∧ 𝑔 ≠ ( I ↾ 𝐵))) → (𝑈 ∘ 𝑂) = 𝑂)
27	5, 26	rexlimddv 3154	1 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝑈 ∈ 𝐸) → (𝑈 ∘ 𝑂) = 𝑂)

Syntax hints:   → wi 4   ∧ wa 396   = wceq 1540   ∈ wcel 2105   ≠ wne 2940  ∃wrex 3070   ↦ cmpt 5172   I cid 5511   ↾ cres 5616   ∘ ccom 5618  ‘cfv 6473  Basecbs 17001  HLchlt 37610  LHypclh 38245  LTrncltrn 38362  TEndoctendo 39013

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1912  ax-6 1970  ax-7 2010  ax-8 2107  ax-9 2115  ax-10 2136  ax-11 2153  ax-12 2170  ax-ext 2707  ax-rep 5226  ax-sep 5240  ax-nul 5247  ax-pow 5305  ax-pr 5369  ax-un 7642  ax-riotaBAD 37213

This theorem depends on definitions:  df-bi 206  df-an 397  df-or 845  df-3or 1087  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1781  df-nf 1785  df-sb 2067  df-mo 2538  df-eu 2567  df-clab 2714  df-cleq 2728  df-clel 2814  df-nfc 2886  df-ne 2941  df-ral 3062  df-rex 3071  df-rmo 3349  df-reu 3350  df-rab 3404  df-v 3443  df-sbc 3727  df-csb 3843  df-dif 3900  df-un 3902  df-in 3904  df-ss 3914  df-nul 4269  df-if 4473  df-pw 4548  df-sn 4573  df-pr 4575  df-op 4579  df-uni 4852  df-iun 4940  df-iin 4941  df-br 5090  df-opab 5152  df-mpt 5173  df-id 5512  df-xp 5620  df-rel 5621  df-cnv 5622  df-co 5623  df-dm 5624  df-rn 5625  df-res 5626  df-ima 5627  df-iota 6425  df-fun 6475  df-fn 6476  df-f 6477  df-f1 6478  df-fo 6479  df-f1o 6480  df-fv 6481  df-riota 7286  df-ov 7332  df-oprab 7333  df-mpo 7334  df-1st 7891  df-2nd 7892  df-undef 8151  df-map 8680  df-proset 18102  df-poset 18120  df-plt 18137  df-lub 18153  df-glb 18154  df-join 18155  df-meet 18156  df-p0 18232  df-p1 18233  df-lat 18239  df-clat 18306  df-oposet 37436  df-ol 37438  df-oml 37439  df-covers 37526  df-ats 37527  df-atl 37558  df-cvlat 37582  df-hlat 37611  df-llines 37759  df-lplanes 37760  df-lvols 37761  df-lines 37762  df-psubsp 37764  df-pmap 37765  df-padd 38057  df-lhyp 38249  df-laut 38250  df-ldil 38365  df-ltrn 38366  df-trl 38420  df-tendo 39016

This theorem is referenced by:  dib1dim2  39429  diblss  39431