tendocan

Description: Cancellation law: if the values of two trace-preserving endormorphisms are equal, so are the endormorphisms. Lemma J of Crawley p. 118. (Contributed by NM, 21-Jun-2013)

	Ref	Expression
Hypotheses	tendocan.b	$⊢ B = {Base}_{K}$
	tendocan.h	$⊢ H = LHyp (K)$
	tendocan.t	$⊢ T = LTrn (K) (W)$
	tendocan.e	$⊢ E = TEndo (K) (W)$
Assertion	tendocan	$⊢ ((K \in HL \land W \in H) \land (U \in E \land V \in E \land U (F) = V (F)) \land (F \in T \land F \neq {I ↾}_{B})) \to U = V$

Proof

Step	Hyp	Ref	Expression
1		tendocan.b	$⊢ B = {Base}_{K}$
2		tendocan.h	$⊢ H = LHyp (K)$
3		tendocan.t	$⊢ T = LTrn (K) (W)$
4		tendocan.e	$⊢ E = TEndo (K) (W)$
5		simp1l	$⊢ ((K \in HL \land W \in H) \land (U \in E \land V \in E \land U (F) = V (F)) \land (F \in T \land F \neq {I ↾}_{B})) \to K \in HL$
6		simp1r	$⊢ ((K \in HL \land W \in H) \land (U \in E \land V \in E \land U (F) = V (F)) \land (F \in T \land F \neq {I ↾}_{B})) \to W \in H$
7		simp21	$⊢ ((K \in HL \land W \in H) \land (U \in E \land V \in E \land U (F) = V (F)) \land (F \in T \land F \neq {I ↾}_{B})) \to U \in E$
8		simp22	$⊢ ((K \in HL \land W \in H) \land (U \in E \land V \in E \land U (F) = V (F)) \land (F \in T \land F \neq {I ↾}_{B})) \to V \in E$
9		simp11	$⊢ (((K \in HL \land W \in H) \land (U \in E \land V \in E \land U (F) = V (F)) \land (F \in T \land F \neq {I ↾}_{B})) \land h \in T \land h \neq {I ↾}_{B}) \to (K \in HL \land W \in H)$
10		simp12	$⊢ (((K \in HL \land W \in H) \land (U \in E \land V \in E \land U (F) = V (F)) \land (F \in T \land F \neq {I ↾}_{B})) \land h \in T \land h \neq {I ↾}_{B}) \to (U \in E \land V \in E \land U (F) = V (F))$
11		simp13l	$⊢ (((K \in HL \land W \in H) \land (U \in E \land V \in E \land U (F) = V (F)) \land (F \in T \land F \neq {I ↾}_{B})) \land h \in T \land h \neq {I ↾}_{B}) \to F \in T$
12		simp13r	$⊢ (((K \in HL \land W \in H) \land (U \in E \land V \in E \land U (F) = V (F)) \land (F \in T \land F \neq {I ↾}_{B})) \land h \in T \land h \neq {I ↾}_{B}) \to F \neq {I ↾}_{B}$
13		simp2	$⊢ (((K \in HL \land W \in H) \land (U \in E \land V \in E \land U (F) = V (F)) \land (F \in T \land F \neq {I ↾}_{B})) \land h \in T \land h \neq {I ↾}_{B}) \to h \in T$
14	11 12 13	3jca	$⊢ (((K \in HL \land W \in H) \land (U \in E \land V \in E \land U (F) = V (F)) \land (F \in T \land F \neq {I ↾}_{B})) \land h \in T \land h \neq {I ↾}_{B}) \to (F \in T \land F \neq {I ↾}_{B} \land h \in T)$
15		simp3	$⊢ (((K \in HL \land W \in H) \land (U \in E \land V \in E \land U (F) = V (F)) \land (F \in T \land F \neq {I ↾}_{B})) \land h \in T \land h \neq {I ↾}_{B}) \to h \neq {I ↾}_{B}$
16		eqid	$⊢ trL (K) (W) = trL (K) (W)$
17	1 2 3 16 4	cdlemj3	$⊢ (((K \in HL \land W \in H) \land (U \in E \land V \in E \land U (F) = V (F)) \land (F \in T \land F \neq {I ↾}_{B} \land h \in T)) \land h \neq {I ↾}_{B}) \to U (h) = V (h)$
18	9 10 14 15 17	syl31anc	$⊢ (((K \in HL \land W \in H) \land (U \in E \land V \in E \land U (F) = V (F)) \land (F \in T \land F \neq {I ↾}_{B})) \land h \in T \land h \neq {I ↾}_{B}) \to U (h) = V (h)$
19	18	3exp	$⊢ ((K \in HL \land W \in H) \land (U \in E \land V \in E \land U (F) = V (F)) \land (F \in T \land F \neq {I ↾}_{B})) \to (h \in T \to (h \neq {I ↾}_{B} \to U (h) = V (h)))$
20	19	ralrimiv	$⊢ ((K \in HL \land W \in H) \land (U \in E \land V \in E \land U (F) = V (F)) \land (F \in T \land F \neq {I ↾}_{B})) \to \forall h \in T (h \neq {I ↾}_{B} \to U (h) = V (h))$
21	1 2 3 4	tendoeq2	$⊢ ((K \in HL \land W \in H) \land (U \in E \land V \in E) \land \forall h \in T (h \neq {I ↾}_{B} \to U (h) = V (h))) \to U = V$
22	5 6 7 8 20 21	syl221anc	$⊢ ((K \in HL \land W \in H) \land (U \in E \land V \in E \land U (F) = V (F)) \land (F \in T \land F \neq {I ↾}_{B})) \to U = V$

Metamath Proof Explorer

Theorem tendocan

Proof