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 ⊢ 𝐵 = ( Base ‘ 𝐾 )
tendoeq2.h ⊢ 𝐻 = ( LHyp ‘ 𝐾 )
tendoeq2.t ⊢ 𝑇 = ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 )
tendoeq2.e ⊢ 𝐸 = ( ( TEndo ‘ 𝐾 ) ‘ 𝑊 )
Assertion tendoeq2 ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑈 ∈ 𝐸 ∧ 𝑉 ∈ 𝐸 ) ∧ ∀ 𝑓 ∈ 𝑇 ( 𝑓 ≠ ( I ↾ 𝐵 ) → ( 𝑈 ‘ 𝑓 ) = ( 𝑉 ‘ 𝑓 ) ) ) → 𝑈 = 𝑉 )

Proof

Step Hyp Ref Expression
1 tendoeq2.b ⊢ 𝐵 = ( Base ‘ 𝐾 )
2 tendoeq2.h ⊢ 𝐻 = ( LHyp ‘ 𝐾 )
3 tendoeq2.t ⊢ 𝑇 = ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 )
4 tendoeq2.e ⊢ 𝐸 = ( ( TEndo ‘ 𝐾 ) ‘ 𝑊 )
5 1 2 4 tendoid ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝑈 ∈ 𝐸 ) → ( 𝑈 ‘ ( I ↾ 𝐵 ) ) = ( I ↾ 𝐵 ) )
6 5 adantrr ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑈 ∈ 𝐸 ∧ 𝑉 ∈ 𝐸 ) ) → ( 𝑈 ‘ ( I ↾ 𝐵 ) ) = ( I ↾ 𝐵 ) )
7 1 2 4 tendoid ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝑉 ∈ 𝐸 ) → ( 𝑉 ‘ ( I ↾ 𝐵 ) ) = ( I ↾ 𝐵 ) )
8 7 adantrl ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑈 ∈ 𝐸 ∧ 𝑉 ∈ 𝐸 ) ) → ( 𝑉 ‘ ( I ↾ 𝐵 ) ) = ( I ↾ 𝐵 ) )
9 6 8 eqtr4d ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑈 ∈ 𝐸 ∧ 𝑉 ∈ 𝐸 ) ) → ( 𝑈 ‘ ( I ↾ 𝐵 ) ) = ( 𝑉 ‘ ( I ↾ 𝐵 ) ) )
10 fveq2 ⊢ ( 𝑓 = ( I ↾ 𝐵 ) → ( 𝑈 ‘ 𝑓 ) = ( 𝑈 ‘ ( I ↾ 𝐵 ) ) )
11 fveq2 ⊢ ( 𝑓 = ( I ↾ 𝐵 ) → ( 𝑉 ‘ 𝑓 ) = ( 𝑉 ‘ ( I ↾ 𝐵 ) ) )
12 10 11 eqeq12d ⊢ ( 𝑓 = ( I ↾ 𝐵 ) → ( ( 𝑈 ‘ 𝑓 ) = ( 𝑉 ‘ 𝑓 ) ↔ ( 𝑈 ‘ ( I ↾ 𝐵 ) ) = ( 𝑉 ‘ ( I ↾ 𝐵 ) ) ) )
13 9 12 syl5ibrcom ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑈 ∈ 𝐸 ∧ 𝑉 ∈ 𝐸 ) ) → ( 𝑓 = ( I ↾ 𝐵 ) → ( 𝑈 ‘ 𝑓 ) = ( 𝑉 ‘ 𝑓 ) ) )
14 13 ralrimivw ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑈 ∈ 𝐸 ∧ 𝑉 ∈ 𝐸 ) ) → ∀ 𝑓 ∈ 𝑇 ( 𝑓 = ( I ↾ 𝐵 ) → ( 𝑈 ‘ 𝑓 ) = ( 𝑉 ‘ 𝑓 ) ) )
15 r19.26 ⊢ ( ∀ 𝑓 ∈ 𝑇 ( ( 𝑓 = ( I ↾ 𝐵 ) → ( 𝑈 ‘ 𝑓 ) = ( 𝑉 ‘ 𝑓 ) ) ∧ ( 𝑓 ≠ ( I ↾ 𝐵 ) → ( 𝑈 ‘ 𝑓 ) = ( 𝑉 ‘ 𝑓 ) ) ) ↔ ( ∀ 𝑓 ∈ 𝑇 ( 𝑓 = ( I ↾ 𝐵 ) → ( 𝑈 ‘ 𝑓 ) = ( 𝑉 ‘ 𝑓 ) ) ∧ ∀ 𝑓 ∈ 𝑇 ( 𝑓 ≠ ( I ↾ 𝐵 ) → ( 𝑈 ‘ 𝑓 ) = ( 𝑉 ‘ 𝑓 ) ) ) )
16 jaob ⊢ ( ( ( 𝑓 = ( I ↾ 𝐵 ) ∨ 𝑓 ≠ ( I ↾ 𝐵 ) ) → ( 𝑈 ‘ 𝑓 ) = ( 𝑉 ‘ 𝑓 ) ) ↔ ( ( 𝑓 = ( I ↾ 𝐵 ) → ( 𝑈 ‘ 𝑓 ) = ( 𝑉 ‘ 𝑓 ) ) ∧ ( 𝑓 ≠ ( I ↾ 𝐵 ) → ( 𝑈 ‘ 𝑓 ) = ( 𝑉 ‘ 𝑓 ) ) ) )
17 exmidne ⊢ ( 𝑓 = ( I ↾ 𝐵 ) ∨ 𝑓 ≠ ( I ↾ 𝐵 ) )
18 pm5.5 ⊢ ( ( 𝑓 = ( I ↾ 𝐵 ) ∨ 𝑓 ≠ ( I ↾ 𝐵 ) ) → ( ( ( 𝑓 = ( I ↾ 𝐵 ) ∨ 𝑓 ≠ ( I ↾ 𝐵 ) ) → ( 𝑈 ‘ 𝑓 ) = ( 𝑉 ‘ 𝑓 ) ) ↔ ( 𝑈 ‘ 𝑓 ) = ( 𝑉 ‘ 𝑓 ) ) )
19 17 18 ax-mp ⊢ ( ( ( 𝑓 = ( I ↾ 𝐵 ) ∨ 𝑓 ≠ ( I ↾ 𝐵 ) ) → ( 𝑈 ‘ 𝑓 ) = ( 𝑉 ‘ 𝑓 ) ) ↔ ( 𝑈 ‘ 𝑓 ) = ( 𝑉 ‘ 𝑓 ) )
20 16 19 bitr3i ⊢ ( ( ( 𝑓 = ( I ↾ 𝐵 ) → ( 𝑈 ‘ 𝑓 ) = ( 𝑉 ‘ 𝑓 ) ) ∧ ( 𝑓 ≠ ( I ↾ 𝐵 ) → ( 𝑈 ‘ 𝑓 ) = ( 𝑉 ‘ 𝑓 ) ) ) ↔ ( 𝑈 ‘ 𝑓 ) = ( 𝑉 ‘ 𝑓 ) )
21 20 ralbii ⊢ ( ∀ 𝑓 ∈ 𝑇 ( ( 𝑓 = ( I ↾ 𝐵 ) → ( 𝑈 ‘ 𝑓 ) = ( 𝑉 ‘ 𝑓 ) ) ∧ ( 𝑓 ≠ ( I ↾ 𝐵 ) → ( 𝑈 ‘ 𝑓 ) = ( 𝑉 ‘ 𝑓 ) ) ) ↔ ∀ 𝑓 ∈ 𝑇 ( 𝑈 ‘ 𝑓 ) = ( 𝑉 ‘ 𝑓 ) )
22 15 21 bitr3i ⊢ ( ( ∀ 𝑓 ∈ 𝑇 ( 𝑓 = ( I ↾ 𝐵 ) → ( 𝑈 ‘ 𝑓 ) = ( 𝑉 ‘ 𝑓 ) ) ∧ ∀ 𝑓 ∈ 𝑇 ( 𝑓 ≠ ( I ↾ 𝐵 ) → ( 𝑈 ‘ 𝑓 ) = ( 𝑉 ‘ 𝑓 ) ) ) ↔ ∀ 𝑓 ∈ 𝑇 ( 𝑈 ‘ 𝑓 ) = ( 𝑉 ‘ 𝑓 ) )
23 2 3 4 tendoeq1 ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑈 ∈ 𝐸 ∧ 𝑉 ∈ 𝐸 ) ∧ ∀ 𝑓 ∈ 𝑇 ( 𝑈 ‘ 𝑓 ) = ( 𝑉 ‘ 𝑓 ) ) → 𝑈 = 𝑉 )
24 23 3expia ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑈 ∈ 𝐸 ∧ 𝑉 ∈ 𝐸 ) ) → ( ∀ 𝑓 ∈ 𝑇 ( 𝑈 ‘ 𝑓 ) = ( 𝑉 ‘ 𝑓 ) → 𝑈 = 𝑉 ) )
25 22 24 syl5bi ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑈 ∈ 𝐸 ∧ 𝑉 ∈ 𝐸 ) ) → ( ( ∀ 𝑓 ∈ 𝑇 ( 𝑓 = ( I ↾ 𝐵 ) → ( 𝑈 ‘ 𝑓 ) = ( 𝑉 ‘ 𝑓 ) ) ∧ ∀ 𝑓 ∈ 𝑇 ( 𝑓 ≠ ( I ↾ 𝐵 ) → ( 𝑈 ‘ 𝑓 ) = ( 𝑉 ‘ 𝑓 ) ) ) → 𝑈 = 𝑉 ) )
26 14 25 mpand ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑈 ∈ 𝐸 ∧ 𝑉 ∈ 𝐸 ) ) → ( ∀ 𝑓 ∈ 𝑇 ( 𝑓 ≠ ( I ↾ 𝐵 ) → ( 𝑈 ‘ 𝑓 ) = ( 𝑉 ‘ 𝑓 ) ) → 𝑈 = 𝑉 ) )
27 26 3impia ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑈 ∈ 𝐸 ∧ 𝑉 ∈ 𝐸 ) ∧ ∀ 𝑓 ∈ 𝑇 ( 𝑓 ≠ ( I ↾ 𝐵 ) → ( 𝑈 ‘ 𝑓 ) = ( 𝑉 ‘ 𝑓 ) ) ) → 𝑈 = 𝑉 )