# 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}={\mathrm{Base}}_{{K}}$
tendoeq2.h ${⊢}{H}=\mathrm{LHyp}\left({K}\right)$
tendoeq2.t ${⊢}{T}=\mathrm{LTrn}\left({K}\right)\left({W}\right)$
tendoeq2.e ${⊢}{E}=\mathrm{TEndo}\left({K}\right)\left({W}\right)$
Assertion tendoeq2 ${⊢}\left(\left({K}\in \mathrm{HL}\wedge {W}\in {H}\right)\wedge \left({U}\in {E}\wedge {V}\in {E}\right)\wedge \forall {f}\in {T}\phantom{\rule{.4em}{0ex}}\left({f}\ne {\mathrm{I}↾}_{{B}}\to {U}\left({f}\right)={V}\left({f}\right)\right)\right)\to {U}={V}$

### Proof

Step Hyp Ref Expression
1 tendoeq2.b ${⊢}{B}={\mathrm{Base}}_{{K}}$
2 tendoeq2.h ${⊢}{H}=\mathrm{LHyp}\left({K}\right)$
3 tendoeq2.t ${⊢}{T}=\mathrm{LTrn}\left({K}\right)\left({W}\right)$
4 tendoeq2.e ${⊢}{E}=\mathrm{TEndo}\left({K}\right)\left({W}\right)$
5 1 2 4 tendoid ${⊢}\left(\left({K}\in \mathrm{HL}\wedge {W}\in {H}\right)\wedge {U}\in {E}\right)\to {U}\left({\mathrm{I}↾}_{{B}}\right)={\mathrm{I}↾}_{{B}}$
6 5 adantrr ${⊢}\left(\left({K}\in \mathrm{HL}\wedge {W}\in {H}\right)\wedge \left({U}\in {E}\wedge {V}\in {E}\right)\right)\to {U}\left({\mathrm{I}↾}_{{B}}\right)={\mathrm{I}↾}_{{B}}$
7 1 2 4 tendoid ${⊢}\left(\left({K}\in \mathrm{HL}\wedge {W}\in {H}\right)\wedge {V}\in {E}\right)\to {V}\left({\mathrm{I}↾}_{{B}}\right)={\mathrm{I}↾}_{{B}}$
8 7 adantrl ${⊢}\left(\left({K}\in \mathrm{HL}\wedge {W}\in {H}\right)\wedge \left({U}\in {E}\wedge {V}\in {E}\right)\right)\to {V}\left({\mathrm{I}↾}_{{B}}\right)={\mathrm{I}↾}_{{B}}$
9 6 8 eqtr4d ${⊢}\left(\left({K}\in \mathrm{HL}\wedge {W}\in {H}\right)\wedge \left({U}\in {E}\wedge {V}\in {E}\right)\right)\to {U}\left({\mathrm{I}↾}_{{B}}\right)={V}\left({\mathrm{I}↾}_{{B}}\right)$
10 fveq2 ${⊢}{f}={\mathrm{I}↾}_{{B}}\to {U}\left({f}\right)={U}\left({\mathrm{I}↾}_{{B}}\right)$
11 fveq2 ${⊢}{f}={\mathrm{I}↾}_{{B}}\to {V}\left({f}\right)={V}\left({\mathrm{I}↾}_{{B}}\right)$
12 10 11 eqeq12d ${⊢}{f}={\mathrm{I}↾}_{{B}}\to \left({U}\left({f}\right)={V}\left({f}\right)↔{U}\left({\mathrm{I}↾}_{{B}}\right)={V}\left({\mathrm{I}↾}_{{B}}\right)\right)$
13 9 12 syl5ibrcom ${⊢}\left(\left({K}\in \mathrm{HL}\wedge {W}\in {H}\right)\wedge \left({U}\in {E}\wedge {V}\in {E}\right)\right)\to \left({f}={\mathrm{I}↾}_{{B}}\to {U}\left({f}\right)={V}\left({f}\right)\right)$
14 13 ralrimivw ${⊢}\left(\left({K}\in \mathrm{HL}\wedge {W}\in {H}\right)\wedge \left({U}\in {E}\wedge {V}\in {E}\right)\right)\to \forall {f}\in {T}\phantom{\rule{.4em}{0ex}}\left({f}={\mathrm{I}↾}_{{B}}\to {U}\left({f}\right)={V}\left({f}\right)\right)$
15 r19.26 ${⊢}\forall {f}\in {T}\phantom{\rule{.4em}{0ex}}\left(\left({f}={\mathrm{I}↾}_{{B}}\to {U}\left({f}\right)={V}\left({f}\right)\right)\wedge \left({f}\ne {\mathrm{I}↾}_{{B}}\to {U}\left({f}\right)={V}\left({f}\right)\right)\right)↔\left(\forall {f}\in {T}\phantom{\rule{.4em}{0ex}}\left({f}={\mathrm{I}↾}_{{B}}\to {U}\left({f}\right)={V}\left({f}\right)\right)\wedge \forall {f}\in {T}\phantom{\rule{.4em}{0ex}}\left({f}\ne {\mathrm{I}↾}_{{B}}\to {U}\left({f}\right)={V}\left({f}\right)\right)\right)$
16 jaob ${⊢}\left(\left({f}={\mathrm{I}↾}_{{B}}\vee {f}\ne {\mathrm{I}↾}_{{B}}\right)\to {U}\left({f}\right)={V}\left({f}\right)\right)↔\left(\left({f}={\mathrm{I}↾}_{{B}}\to {U}\left({f}\right)={V}\left({f}\right)\right)\wedge \left({f}\ne {\mathrm{I}↾}_{{B}}\to {U}\left({f}\right)={V}\left({f}\right)\right)\right)$
17 exmidne ${⊢}\left({f}={\mathrm{I}↾}_{{B}}\vee {f}\ne {\mathrm{I}↾}_{{B}}\right)$
18 pm5.5 ${⊢}\left({f}={\mathrm{I}↾}_{{B}}\vee {f}\ne {\mathrm{I}↾}_{{B}}\right)\to \left(\left(\left({f}={\mathrm{I}↾}_{{B}}\vee {f}\ne {\mathrm{I}↾}_{{B}}\right)\to {U}\left({f}\right)={V}\left({f}\right)\right)↔{U}\left({f}\right)={V}\left({f}\right)\right)$
19 17 18 ax-mp ${⊢}\left(\left({f}={\mathrm{I}↾}_{{B}}\vee {f}\ne {\mathrm{I}↾}_{{B}}\right)\to {U}\left({f}\right)={V}\left({f}\right)\right)↔{U}\left({f}\right)={V}\left({f}\right)$
20 16 19 bitr3i ${⊢}\left(\left({f}={\mathrm{I}↾}_{{B}}\to {U}\left({f}\right)={V}\left({f}\right)\right)\wedge \left({f}\ne {\mathrm{I}↾}_{{B}}\to {U}\left({f}\right)={V}\left({f}\right)\right)\right)↔{U}\left({f}\right)={V}\left({f}\right)$
21 20 ralbii ${⊢}\forall {f}\in {T}\phantom{\rule{.4em}{0ex}}\left(\left({f}={\mathrm{I}↾}_{{B}}\to {U}\left({f}\right)={V}\left({f}\right)\right)\wedge \left({f}\ne {\mathrm{I}↾}_{{B}}\to {U}\left({f}\right)={V}\left({f}\right)\right)\right)↔\forall {f}\in {T}\phantom{\rule{.4em}{0ex}}{U}\left({f}\right)={V}\left({f}\right)$
22 15 21 bitr3i ${⊢}\left(\forall {f}\in {T}\phantom{\rule{.4em}{0ex}}\left({f}={\mathrm{I}↾}_{{B}}\to {U}\left({f}\right)={V}\left({f}\right)\right)\wedge \forall {f}\in {T}\phantom{\rule{.4em}{0ex}}\left({f}\ne {\mathrm{I}↾}_{{B}}\to {U}\left({f}\right)={V}\left({f}\right)\right)\right)↔\forall {f}\in {T}\phantom{\rule{.4em}{0ex}}{U}\left({f}\right)={V}\left({f}\right)$
23 2 3 4 tendoeq1 ${⊢}\left(\left({K}\in \mathrm{HL}\wedge {W}\in {H}\right)\wedge \left({U}\in {E}\wedge {V}\in {E}\right)\wedge \forall {f}\in {T}\phantom{\rule{.4em}{0ex}}{U}\left({f}\right)={V}\left({f}\right)\right)\to {U}={V}$
24 23 3expia ${⊢}\left(\left({K}\in \mathrm{HL}\wedge {W}\in {H}\right)\wedge \left({U}\in {E}\wedge {V}\in {E}\right)\right)\to \left(\forall {f}\in {T}\phantom{\rule{.4em}{0ex}}{U}\left({f}\right)={V}\left({f}\right)\to {U}={V}\right)$
25 22 24 syl5bi ${⊢}\left(\left({K}\in \mathrm{HL}\wedge {W}\in {H}\right)\wedge \left({U}\in {E}\wedge {V}\in {E}\right)\right)\to \left(\left(\forall {f}\in {T}\phantom{\rule{.4em}{0ex}}\left({f}={\mathrm{I}↾}_{{B}}\to {U}\left({f}\right)={V}\left({f}\right)\right)\wedge \forall {f}\in {T}\phantom{\rule{.4em}{0ex}}\left({f}\ne {\mathrm{I}↾}_{{B}}\to {U}\left({f}\right)={V}\left({f}\right)\right)\right)\to {U}={V}\right)$
26 14 25 mpand ${⊢}\left(\left({K}\in \mathrm{HL}\wedge {W}\in {H}\right)\wedge \left({U}\in {E}\wedge {V}\in {E}\right)\right)\to \left(\forall {f}\in {T}\phantom{\rule{.4em}{0ex}}\left({f}\ne {\mathrm{I}↾}_{{B}}\to {U}\left({f}\right)={V}\left({f}\right)\right)\to {U}={V}\right)$
27 26 3impia ${⊢}\left(\left({K}\in \mathrm{HL}\wedge {W}\in {H}\right)\wedge \left({U}\in {E}\wedge {V}\in {E}\right)\wedge \forall {f}\in {T}\phantom{\rule{.4em}{0ex}}\left({f}\ne {\mathrm{I}↾}_{{B}}\to {U}\left({f}\right)={V}\left({f}\right)\right)\right)\to {U}={V}$