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 = Base K
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 ∈ T f ≠ I ↾ B → U ⁡ f = V ⁡ f → U = V

Proof

Step Hyp Ref Expression
1 tendoeq2.b ⊢ B = Base K
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 ∈ T f = I ↾ B → U ⁡ f = V ⁡ f
15 r19.26 ⊢ ∀ f ∈ T f = I ↾ B → U ⁡ f = V ⁡ f ∧ f ≠ I ↾ B → U ⁡ f = V ⁡ f ↔ ∀ f ∈ T f = I ↾ B → U ⁡ f = V ⁡ f ∧ ∀ f ∈ T f ≠ 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 ∈ T f = I ↾ B → U ⁡ f = V ⁡ f ∧ f ≠ I ↾ B → U ⁡ f = V ⁡ f ↔ ∀ f ∈ T U ⁡ f = V ⁡ f
22 15 21 bitr3i ⊢ ∀ f ∈ T f = I ↾ B → U ⁡ f = V ⁡ f ∧ ∀ f ∈ T f ≠ I ↾ B → U ⁡ f = V ⁡ f ↔ ∀ f ∈ T U ⁡ f = V ⁡ f
23 2 3 4 tendoeq1 ⊢ K ∈ HL ∧ W ∈ H ∧ U ∈ E ∧ V ∈ E ∧ ∀ f ∈ T U ⁡ f = V ⁡ f → U = V
24 23 3expia ⊢ K ∈ HL ∧ W ∈ H ∧ U ∈ E ∧ V ∈ E → ∀ f ∈ T U ⁡ f = V ⁡ f → U = V
25 22 24 biimtrid ⊢ K ∈ HL ∧ W ∈ H ∧ U ∈ E ∧ V ∈ E → ∀ f ∈ T f = I ↾ B → U ⁡ f = V ⁡ f ∧ ∀ f ∈ T f ≠ I ↾ B → U ⁡ f = V ⁡ f → U = V
26 14 25 mpand ⊢ K ∈ HL ∧ W ∈ H ∧ U ∈ E ∧ V ∈ E → ∀ f ∈ T f ≠ I ↾ B → U ⁡ f = V ⁡ f → U = V
27 26 3impia ⊢ K ∈ HL ∧ W ∈ H ∧ U ∈ E ∧ V ∈ E ∧ ∀ f ∈ T f ≠ I ↾ B → U ⁡ f = V ⁡ f → U = V