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	biimtrid	⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑈 ∈ 𝐸 ∧ 𝑉 ∈ 𝐸 ) ) → ( ( ∀ 𝑓 ∈ 𝑇 ( 𝑓 = ( I ↾ 𝐵 ) → ( 𝑈 ‘ 𝑓 ) = ( 𝑉 ‘ 𝑓 ) ) ∧ ∀ 𝑓 ∈ 𝑇 ( 𝑓 ≠ ( I ↾ 𝐵 ) → ( 𝑈 ‘ 𝑓 ) = ( 𝑉 ‘ 𝑓 ) ) ) → 𝑈 = 𝑉 ) )
26	14 25	mpand	⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑈 ∈ 𝐸 ∧ 𝑉 ∈ 𝐸 ) ) → ( ∀ 𝑓 ∈ 𝑇 ( 𝑓 ≠ ( I ↾ 𝐵 ) → ( 𝑈 ‘ 𝑓 ) = ( 𝑉 ‘ 𝑓 ) ) → 𝑈 = 𝑉 ) )
27	26	3impia	⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑈 ∈ 𝐸 ∧ 𝑉 ∈ 𝐸 ) ∧ ∀ 𝑓 ∈ 𝑇 ( 𝑓 ≠ ( I ↾ 𝐵 ) → ( 𝑈 ‘ 𝑓 ) = ( 𝑉 ‘ 𝑓 ) ) ) → 𝑈 = 𝑉 )

Metamath Proof Explorer

Theorem tendoeq2

Proof