Metamath Proof Explorer

Theorem tendo0mul

Description: Additive identity multiplied by a trace-preserving endomorphism. (Contributed by NM, 1-Aug-2013)

Ref Expression
Hypotheses tendoid0.b ⊢ 𝐵 = ( Base ‘ 𝐾 )
tendoid0.h ⊢ 𝐻 = ( LHyp ‘ 𝐾 )
tendoid0.t ⊢ 𝑇 = ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 )
tendoid0.e ⊢ 𝐸 = ( ( TEndo ‘ 𝐾 ) ‘ 𝑊 )
tendoid0.o ⊢ 𝑂 = ( 𝑓 ∈ 𝑇 ↦ ( I ↾ 𝐵 ) )
Assertion tendo0mul ( ( ( 𝐾 ∈ 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 1 2 3 4 5 tendo0cl ⊢ ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) → 𝑂 ∈ 𝐸 )
10 9 ad2antrr ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝑈 ∈ 𝐸 ) ∧ ( 𝑔 ∈ 𝑇 ∧ 𝑔 ≠ ( I ↾ 𝐵 ) ) ) → 𝑂 ∈ 𝐸 )
11 simplr ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝑈 ∈ 𝐸 ) ∧ ( 𝑔 ∈ 𝑇 ∧ 𝑔 ≠ ( I ↾ 𝐵 ) ) ) → 𝑈 ∈ 𝐸 )
12 2 4 tendococl ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝑂 ∈ 𝐸 ∧ 𝑈 ∈ 𝐸 ) → ( 𝑂 ∘ 𝑈 ) ∈ 𝐸 )
13 8 10 11 12 syl3anc ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝑈 ∈ 𝐸 ) ∧ ( 𝑔 ∈ 𝑇 ∧ 𝑔 ≠ ( I ↾ 𝐵 ) ) ) → ( 𝑂 ∘ 𝑈 ) ∈ 𝐸 )
14 simprl ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝑈 ∈ 𝐸 ) ∧ ( 𝑔 ∈ 𝑇 ∧ 𝑔 ≠ ( I ↾ 𝐵 ) ) ) → 𝑔 ∈ 𝑇 )
15 2 3 4 tendocl ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝑈 ∈ 𝐸 ∧ 𝑔 ∈ 𝑇 ) → ( 𝑈 ‘ 𝑔 ) ∈ 𝑇 )
16 8 11 14 15 syl3anc ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝑈 ∈ 𝐸 ) ∧ ( 𝑔 ∈ 𝑇 ∧ 𝑔 ≠ ( I ↾ 𝐵 ) ) ) → ( 𝑈 ‘ 𝑔 ) ∈ 𝑇 )
17 5 1 tendo02 ⊢ ( ( 𝑈 ‘ 𝑔 ) ∈ 𝑇 → ( 𝑂 ‘ ( 𝑈 ‘ 𝑔 ) ) = ( I ↾ 𝐵 ) )
18 16 17 syl ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝑈 ∈ 𝐸 ) ∧ ( 𝑔 ∈ 𝑇 ∧ 𝑔 ≠ ( I ↾ 𝐵 ) ) ) → ( 𝑂 ‘ ( 𝑈 ‘ 𝑔 ) ) = ( I ↾ 𝐵 ) )
19 2 3 4 tendocoval ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑂 ∈ 𝐸 ∧ 𝑈 ∈ 𝐸 ) ∧ 𝑔 ∈ 𝑇 ) → ( ( 𝑂 ∘ 𝑈 ) ‘ 𝑔 ) = ( 𝑂 ‘ ( 𝑈 ‘ 𝑔 ) ) )
20 8 10 11 14 19 syl121anc ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝑈 ∈ 𝐸 ) ∧ ( 𝑔 ∈ 𝑇 ∧ 𝑔 ≠ ( I ↾ 𝐵 ) ) ) → ( ( 𝑂 ∘ 𝑈 ) ‘ 𝑔 ) = ( 𝑂 ‘ ( 𝑈 ‘ 𝑔 ) ) )
21 5 1 tendo02 ⊢ ( 𝑔 ∈ 𝑇 → ( 𝑂 ‘ 𝑔 ) = ( I ↾ 𝐵 ) )
22 21 ad2antrl ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝑈 ∈ 𝐸 ) ∧ ( 𝑔 ∈ 𝑇 ∧ 𝑔 ≠ ( I ↾ 𝐵 ) ) ) → ( 𝑂 ‘ 𝑔 ) = ( I ↾ 𝐵 ) )
23 18 20 22 3eqtr4d ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝑈 ∈ 𝐸 ) ∧ ( 𝑔 ∈ 𝑇 ∧ 𝑔 ≠ ( I ↾ 𝐵 ) ) ) → ( ( 𝑂 ∘ 𝑈 ) ‘ 𝑔 ) = ( 𝑂 ‘ 𝑔 ) )
24 simpr ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝑈 ∈ 𝐸 ) ∧ ( 𝑔 ∈ 𝑇 ∧ 𝑔 ≠ ( I ↾ 𝐵 ) ) ) → ( 𝑔 ∈ 𝑇 ∧ 𝑔 ≠ ( I ↾ 𝐵 ) ) )
25 1 2 3 4 tendocan ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( ( 𝑂 ∘ 𝑈 ) ∈ 𝐸 ∧ 𝑂 ∈ 𝐸 ∧ ( ( 𝑂 ∘ 𝑈 ) ‘ 𝑔 ) = ( 𝑂 ‘ 𝑔 ) ) ∧ ( 𝑔 ∈ 𝑇 ∧ 𝑔 ≠ ( I ↾ 𝐵 ) ) ) → ( 𝑂 ∘ 𝑈 ) = 𝑂 )
26 8 13 10 23 24 25 syl131anc ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝑈 ∈ 𝐸 ) ∧ ( 𝑔 ∈ 𝑇 ∧ 𝑔 ≠ ( I ↾ 𝐵 ) ) ) → ( 𝑂 ∘ 𝑈 ) = 𝑂 )
27 7 26 rexlimddv ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝑈 ∈ 𝐸 ) → ( 𝑂 ∘ 𝑈 ) = 𝑂 )