Metamath Proof Explorer

Theorem tendo0mulr

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

Ref Expression
Hypotheses tendoid0.b ⊢ 𝐵 = ( Base ‘ 𝐾 )
tendoid0.h ⊢ 𝐻 = ( LHyp ‘ 𝐾 )
tendoid0.t ⊢ 𝑇 = ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 )
tendoid0.e ⊢ 𝐸 = ( ( TEndo ‘ 𝐾 ) ‘ 𝑊 )
tendoid0.o ⊢ 𝑂 = ( 𝑓 ∈ 𝑇 ↦ ( I ↾ 𝐵 ) )
Assertion tendo0mulr ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝑈 ∈ 𝐸 ) → ( 𝑈 ∘ 𝑂 ) = 𝑂 )

Proof

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