tendo0tp

Description: Trace-preserving property of endomorphism additive identity. (Contributed by NM, 11-Jun-2013)

	Ref	Expression
Hypotheses	tendo0.b	⊢ 𝐵 = ( Base ‘ 𝐾 )
	tendo0.h	⊢ 𝐻 = ( LHyp ‘ 𝐾 )
	tendo0.t	⊢ 𝑇 = ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 )
	tendo0.e	⊢ 𝐸 = ( ( TEndo ‘ 𝐾 ) ‘ 𝑊 )
	tendo0.o	⊢ 𝑂 = ( 𝑓 ∈ 𝑇 ↦ ( I ↾ 𝐵 ) )
	tendo0tp.l	⊢ ≤ = ( le ‘ 𝐾 )
	tendo0tp.r	⊢ 𝑅 = ( ( trL ‘ 𝐾 ) ‘ 𝑊 )
Assertion	tendo0tp	⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝐹 ∈ 𝑇 ) → ( 𝑅 ‘ ( 𝑂 ‘ 𝐹 ) ) ≤ ( 𝑅 ‘ 𝐹 ) )

Proof

Step	Hyp	Ref	Expression
1		tendo0.b	⊢ 𝐵 = ( Base ‘ 𝐾 )
2		tendo0.h	⊢ 𝐻 = ( LHyp ‘ 𝐾 )
3		tendo0.t	⊢ 𝑇 = ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 )
4		tendo0.e	⊢ 𝐸 = ( ( TEndo ‘ 𝐾 ) ‘ 𝑊 )
5		tendo0.o	⊢ 𝑂 = ( 𝑓 ∈ 𝑇 ↦ ( I ↾ 𝐵 ) )
6		tendo0tp.l	⊢ ≤ = ( le ‘ 𝐾 )
7		tendo0tp.r	⊢ 𝑅 = ( ( trL ‘ 𝐾 ) ‘ 𝑊 )
8	5 1	tendo02	⊢ ( 𝐹 ∈ 𝑇 → ( 𝑂 ‘ 𝐹 ) = ( I ↾ 𝐵 ) )
9	8	adantl	⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝐹 ∈ 𝑇 ) → ( 𝑂 ‘ 𝐹 ) = ( I ↾ 𝐵 ) )
10	9	fveq2d	⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝐹 ∈ 𝑇 ) → ( 𝑅 ‘ ( 𝑂 ‘ 𝐹 ) ) = ( 𝑅 ‘ ( I ↾ 𝐵 ) ) )
11		eqid	⊢ ( 0. ‘ 𝐾 ) = ( 0. ‘ 𝐾 )
12	1 11 2 7	trlid0	⊢ ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) → ( 𝑅 ‘ ( I ↾ 𝐵 ) ) = ( 0. ‘ 𝐾 ) )
13	12	adantr	⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝐹 ∈ 𝑇 ) → ( 𝑅 ‘ ( I ↾ 𝐵 ) ) = ( 0. ‘ 𝐾 ) )
14	10 13	eqtrd	⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝐹 ∈ 𝑇 ) → ( 𝑅 ‘ ( 𝑂 ‘ 𝐹 ) ) = ( 0. ‘ 𝐾 ) )
15		hlop	⊢ ( 𝐾 ∈ HL → 𝐾 ∈ OP )
16	15	ad2antrr	⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝐹 ∈ 𝑇 ) → 𝐾 ∈ OP )
17	1 2 3 7	trlcl	⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝐹 ∈ 𝑇 ) → ( 𝑅 ‘ 𝐹 ) ∈ 𝐵 )
18	1 6 11	op0le	⊢ ( ( 𝐾 ∈ OP ∧ ( 𝑅 ‘ 𝐹 ) ∈ 𝐵 ) → ( 0. ‘ 𝐾 ) ≤ ( 𝑅 ‘ 𝐹 ) )
19	16 17 18	syl2anc	⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝐹 ∈ 𝑇 ) → ( 0. ‘ 𝐾 ) ≤ ( 𝑅 ‘ 𝐹 ) )
20	14 19	eqbrtrd	⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝐹 ∈ 𝑇 ) → ( 𝑅 ‘ ( 𝑂 ‘ 𝐹 ) ) ≤ ( 𝑅 ‘ 𝐹 ) )

Metamath Proof Explorer

Theorem tendo0tp

Proof