Metamath Proof Explorer

Theorem tendoeq2

Description: Condition determining equality of two trace-preserving endomorphisms, showing it is unnecessary to consider the identity translation. In tendocan , we show that we only need to consider a single non-identity translation. (Contributed by NM, 21-Jun-2013)

Ref Expression
Hypotheses tendoeq2.b ⊢B=BaseK
tendoeq2.h ⊢H=LHyp⁡K
tendoeq2.t ⊢T=LTrn⁡K⁡W
tendoeq2.e ⊢E=TEndo⁡K⁡W
Assertion tendoeq2 ⊢K∈HL∧W∈H∧U∈E∧V∈E∧∀f∈Tf≠I↾B→U⁡f=V⁡f→U=V

Proof

Step Hyp Ref Expression
1 tendoeq2.b ⊢B=BaseK
2 tendoeq2.h ⊢H=LHyp⁡K
3 tendoeq2.t ⊢T=LTrn⁡K⁡W
4 tendoeq2.e ⊢E=TEndo⁡K⁡W
5 1 2 4 tendoid ⊢K∈HL∧W∈H∧U∈E→U⁡I↾B=I↾B
6 5 adantrr ⊢K∈HL∧W∈H∧U∈E∧V∈E→U⁡I↾B=I↾B
7 1 2 4 tendoid ⊢K∈HL∧W∈H∧V∈E→V⁡I↾B=I↾B
8 7 adantrl ⊢K∈HL∧W∈H∧U∈E∧V∈E→V⁡I↾B=I↾B
9 6 8 eqtr4d ⊢K∈HL∧W∈H∧U∈E∧V∈E→U⁡I↾B=V⁡I↾B
10 fveq2 ⊢f=I↾B→U⁡f=U⁡I↾B
11 fveq2 ⊢f=I↾B→V⁡f=V⁡I↾B
12 10 11 eqeq12d ⊢f=I↾B→U⁡f=V⁡f↔U⁡I↾B=V⁡I↾B
13 9 12 syl5ibrcom ⊢K∈HL∧W∈H∧U∈E∧V∈E→f=I↾B→U⁡f=V⁡f
14 13 ralrimivw ⊢K∈HL∧W∈H∧U∈E∧V∈E→∀f∈Tf=I↾B→U⁡f=V⁡f
15 r19.26 ⊢∀f∈Tf=I↾B→U⁡f=V⁡f∧f≠I↾B→U⁡f=V⁡f↔∀f∈Tf=I↾B→U⁡f=V⁡f∧∀f∈Tf≠I↾B→U⁡f=V⁡f
16 jaob ⊢f=I↾B∨f≠I↾B→U⁡f=V⁡f↔f=I↾B→U⁡f=V⁡f∧f≠I↾B→U⁡f=V⁡f
17 exmidne ⊢f=I↾B∨f≠I↾B
18 pm5.5 ⊢f=I↾B∨f≠I↾B→f=I↾B∨f≠I↾B→U⁡f=V⁡f↔U⁡f=V⁡f
19 17 18 ax-mp ⊢f=I↾B∨f≠I↾B→U⁡f=V⁡f↔U⁡f=V⁡f
20 16 19 bitr3i ⊢f=I↾B→U⁡f=V⁡f∧f≠I↾B→U⁡f=V⁡f↔U⁡f=V⁡f
21 20 ralbii ⊢∀f∈Tf=I↾B→U⁡f=V⁡f∧f≠I↾B→U⁡f=V⁡f↔∀f∈TU⁡f=V⁡f
22 15 21 bitr3i ⊢∀f∈Tf=I↾B→U⁡f=V⁡f∧∀f∈Tf≠I↾B→U⁡f=V⁡f↔∀f∈TU⁡f=V⁡f
23 2 3 4 tendoeq1 ⊢K∈HL∧W∈H∧U∈E∧V∈E∧∀f∈TU⁡f=V⁡f→U=V
24 23 3expia ⊢K∈HL∧W∈H∧U∈E∧V∈E→∀f∈TU⁡f=V⁡f→U=V
25 22 24 biimtrid ⊢K∈HL∧W∈H∧U∈E∧V∈E→∀f∈Tf=I↾B→U⁡f=V⁡f∧∀f∈Tf≠I↾B→U⁡f=V⁡f→U=V
26 14 25 mpand ⊢K∈HL∧W∈H∧U∈E∧V∈E→∀f∈Tf≠I↾B→U⁡f=V⁡f→U=V
27 26 3impia ⊢K∈HL∧W∈H∧U∈E∧V∈E∧∀f∈Tf≠I↾B→U⁡f=V⁡f→U=V