tendotr

Description: The trace of the value of a nonzero trace-preserving endomorphism equals the trace of the argument. (Contributed by NM, 11-Aug-2013)

	Ref	Expression
Hypotheses	tendotr.b	$⊢ B = {Base}_{K}$
	tendotr.h	$⊢ H = LHyp (K)$
	tendotr.t	$⊢ T = LTrn (K) (W)$
	tendotr.r	$⊢ R = trL (K) (W)$
	tendotr.e	$⊢ E = TEndo (K) (W)$
	tendotr.o	$⊢ O = (f \in T ⟼ {I ↾}_{B})$
Assertion	tendotr	$⊢ ((K \in HL \land W \in H) \land (U \in E \land U \neq O) \land F \in T) \to R (U (F)) = R (F)$

Proof

Step	Hyp	Ref	Expression
1		tendotr.b	$⊢ B = {Base}_{K}$
2		tendotr.h	$⊢ H = LHyp (K)$
3		tendotr.t	$⊢ T = LTrn (K) (W)$
4		tendotr.r	$⊢ R = trL (K) (W)$
5		tendotr.e	$⊢ E = TEndo (K) (W)$
6		tendotr.o	$⊢ O = (f \in T ⟼ {I ↾}_{B})$
7		simpl1	$⊢ (((K \in HL \land W \in H) \land (U \in E \land U \neq O) \land F \in T) \land F = {I ↾}_{B}) \to (K \in HL \land W \in H)$
8		simpl2l	$⊢ (((K \in HL \land W \in H) \land (U \in E \land U \neq O) \land F \in T) \land F = {I ↾}_{B}) \to U \in E$
9	1 2 5	tendoid	$⊢ ((K \in HL \land W \in H) \land U \in E) \to U ({I ↾}_{B}) = {I ↾}_{B}$
10	7 8 9	syl2anc	$⊢ (((K \in HL \land W \in H) \land (U \in E \land U \neq O) \land F \in T) \land F = {I ↾}_{B}) \to U ({I ↾}_{B}) = {I ↾}_{B}$
11		simpr	$⊢ (((K \in HL \land W \in H) \land (U \in E \land U \neq O) \land F \in T) \land F = {I ↾}_{B}) \to F = {I ↾}_{B}$
12	11	fveq2d	$⊢ (((K \in HL \land W \in H) \land (U \in E \land U \neq O) \land F \in T) \land F = {I ↾}_{B}) \to U (F) = U ({I ↾}_{B})$
13	10 12 11	3eqtr4d	$⊢ (((K \in HL \land W \in H) \land (U \in E \land U \neq O) \land F \in T) \land F = {I ↾}_{B}) \to U (F) = F$
14	13	fveq2d	$⊢ (((K \in HL \land W \in H) \land (U \in E \land U \neq O) \land F \in T) \land F = {I ↾}_{B}) \to R (U (F)) = R (F)$
15		simpl1	$⊢ (((K \in HL \land W \in H) \land (U \in E \land U \neq O) \land F \in T) \land F \neq {I ↾}_{B}) \to (K \in HL \land W \in H)$
16		simpl2l	$⊢ (((K \in HL \land W \in H) \land (U \in E \land U \neq O) \land F \in T) \land F \neq {I ↾}_{B}) \to U \in E$
17		simpl3	$⊢ (((K \in HL \land W \in H) \land (U \in E \land U \neq O) \land F \in T) \land F \neq {I ↾}_{B}) \to F \in T$
18		eqid	$⊢ \leq_{K} = \leq_{K}$
19	18 2 3 4 5	tendotp	$⊢ ((K \in HL \land W \in H) \land U \in E \land F \in T) \to R (U (F)) \leq_{K} R (F)$
20	15 16 17 19	syl3anc	$⊢ (((K \in HL \land W \in H) \land (U \in E \land U \neq O) \land F \in T) \land F \neq {I ↾}_{B}) \to R (U (F)) \leq_{K} R (F)$
21		simpl1l	$⊢ (((K \in HL \land W \in H) \land (U \in E \land U \neq O) \land F \in T) \land F \neq {I ↾}_{B}) \to K \in HL$
22		hlatl	$⊢ K \in HL \to K \in AtLat$
23	21 22	syl	$⊢ (((K \in HL \land W \in H) \land (U \in E \land U \neq O) \land F \in T) \land F \neq {I ↾}_{B}) \to K \in AtLat$
24	2 3 5	tendocl	$⊢ ((K \in HL \land W \in H) \land U \in E \land F \in T) \to U (F) \in T$
25	15 16 17 24	syl3anc	$⊢ (((K \in HL \land W \in H) \land (U \in E \land U \neq O) \land F \in T) \land F \neq {I ↾}_{B}) \to U (F) \in T$
26		simpl2r	$⊢ (((K \in HL \land W \in H) \land (U \in E \land U \neq O) \land F \in T) \land F \neq {I ↾}_{B}) \to U \neq O$
27		simpr	$⊢ (((K \in HL \land W \in H) \land (U \in E \land U \neq O) \land F \in T) \land F \neq {I ↾}_{B}) \to F \neq {I ↾}_{B}$
28	1 2 3 5 6	tendoid0	$⊢ ((K \in HL \land W \in H) \land U \in E \land (F \in T \land F \neq {I ↾}_{B})) \to (U (F) = {I ↾}_{B} \leftrightarrow U = O)$
29	15 16 17 27 28	syl112anc	$⊢ (((K \in HL \land W \in H) \land (U \in E \land U \neq O) \land F \in T) \land F \neq {I ↾}_{B}) \to (U (F) = {I ↾}_{B} \leftrightarrow U = O)$
30	29	necon3bid	$⊢ (((K \in HL \land W \in H) \land (U \in E \land U \neq O) \land F \in T) \land F \neq {I ↾}_{B}) \to (U (F) \neq {I ↾}_{B} \leftrightarrow U \neq O)$
31	26 30	mpbird	$⊢ (((K \in HL \land W \in H) \land (U \in E \land U \neq O) \land F \in T) \land F \neq {I ↾}_{B}) \to U (F) \neq {I ↾}_{B}$
32		eqid	$⊢ Atoms (K) = Atoms (K)$
33	1 32 2 3 4	trlnidat	$⊢ ((K \in HL \land W \in H) \land U (F) \in T \land U (F) \neq {I ↾}_{B}) \to R (U (F)) \in Atoms (K)$
34	15 25 31 33	syl3anc	$⊢ (((K \in HL \land W \in H) \land (U \in E \land U \neq O) \land F \in T) \land F \neq {I ↾}_{B}) \to R (U (F)) \in Atoms (K)$
35	1 32 2 3 4	trlnidat	$⊢ ((K \in HL \land W \in H) \land F \in T \land F \neq {I ↾}_{B}) \to R (F) \in Atoms (K)$
36	15 17 27 35	syl3anc	$⊢ (((K \in HL \land W \in H) \land (U \in E \land U \neq O) \land F \in T) \land F \neq {I ↾}_{B}) \to R (F) \in Atoms (K)$
37	18 32	atcmp	$⊢ (K \in AtLat \land R (U (F)) \in Atoms (K) \land R (F) \in Atoms (K)) \to (R (U (F)) \leq_{K} R (F) \leftrightarrow R (U (F)) = R (F))$
38	23 34 36 37	syl3anc	$⊢ (((K \in HL \land W \in H) \land (U \in E \land U \neq O) \land F \in T) \land F \neq {I ↾}_{B}) \to (R (U (F)) \leq_{K} R (F) \leftrightarrow R (U (F)) = R (F))$
39	20 38	mpbid	$⊢ (((K \in HL \land W \in H) \land (U \in E \land U \neq O) \land F \in T) \land F \neq {I ↾}_{B}) \to R (U (F)) = R (F)$
40	14 39	pm2.61dane	$⊢ ((K \in HL \land W \in H) \land (U \in E \land U \neq O) \land F \in T) \to R (U (F)) = R (F)$

Metamath Proof Explorer

Theorem tendotr

Proof