Metamath Proof Explorer

Theorem tendoeq1

Description: Condition determining equality of two trace-preserving endomorphisms. (Contributed by NM, 11-Jun-2013)

Ref Expression
Hypotheses tendof.h ⊢ H = LHyp ⁡ K
tendof.t ⊢ T = LTrn ⁡ K ⁡ W
tendof.e ⊢ E = TEndo ⁡ K ⁡ W
Assertion tendoeq1 ⊢ K ∈ HL ∧ W ∈ H ∧ U ∈ E ∧ V ∈ E ∧ ∀ f ∈ T U ⁡ f = V ⁡ f → U = V

Proof

Step Hyp Ref Expression
1 tendof.h ⊢ H = LHyp ⁡ K
2 tendof.t ⊢ T = LTrn ⁡ K ⁡ W
3 tendof.e ⊢ E = TEndo ⁡ K ⁡ W
4 simp3 ⊢ K ∈ HL ∧ W ∈ H ∧ U ∈ E ∧ V ∈ E ∧ ∀ f ∈ T U ⁡ f = V ⁡ f → ∀ f ∈ T U ⁡ f = V ⁡ f
5 simp1 ⊢ K ∈ HL ∧ W ∈ H ∧ U ∈ E ∧ V ∈ E ∧ ∀ f ∈ T U ⁡ f = V ⁡ f → K ∈ HL ∧ W ∈ H
6 simp2l ⊢ K ∈ HL ∧ W ∈ H ∧ U ∈ E ∧ V ∈ E ∧ ∀ f ∈ T U ⁡ f = V ⁡ f → U ∈ E
7 1 2 3 tendof ⊢ K ∈ HL ∧ W ∈ H ∧ U ∈ E → U : T ⟶ T
8 5 6 7 syl2anc ⊢ K ∈ HL ∧ W ∈ H ∧ U ∈ E ∧ V ∈ E ∧ ∀ f ∈ T U ⁡ f = V ⁡ f → U : T ⟶ T
9 8 ffnd ⊢ K ∈ HL ∧ W ∈ H ∧ U ∈ E ∧ V ∈ E ∧ ∀ f ∈ T U ⁡ f = V ⁡ f → U Fn T
10 simp2r ⊢ K ∈ HL ∧ W ∈ H ∧ U ∈ E ∧ V ∈ E ∧ ∀ f ∈ T U ⁡ f = V ⁡ f → V ∈ E
11 1 2 3 tendof ⊢ K ∈ HL ∧ W ∈ H ∧ V ∈ E → V : T ⟶ T
12 5 10 11 syl2anc ⊢ K ∈ HL ∧ W ∈ H ∧ U ∈ E ∧ V ∈ E ∧ ∀ f ∈ T U ⁡ f = V ⁡ f → V : T ⟶ T
13 12 ffnd ⊢ K ∈ HL ∧ W ∈ H ∧ U ∈ E ∧ V ∈ E ∧ ∀ f ∈ T U ⁡ f = V ⁡ f → V Fn T
14 eqfnfv ⊢ U Fn T ∧ V Fn T → U = V ↔ ∀ f ∈ T U ⁡ f = V ⁡ f
15 9 13 14 syl2anc ⊢ K ∈ HL ∧ W ∈ H ∧ U ∈ E ∧ V ∈ E ∧ ∀ f ∈ T U ⁡ f = V ⁡ f → U = V ↔ ∀ f ∈ T U ⁡ f = V ⁡ f
16 4 15 mpbird ⊢ K ∈ HL ∧ W ∈ H ∧ U ∈ E ∧ V ∈ E ∧ ∀ f ∈ T U ⁡ f = V ⁡ f → U = V