tendocnv

Description: Converse of a trace-preserving endomorphism value. (Contributed by NM, 7-Apr-2014)

	Ref	Expression
Hypotheses	tendosp.h	$⊢ H = LHyp (K)$
	tendosp.t	$⊢ T = LTrn (K) (W)$
	tendosp.e	$⊢ E = TEndo (K) (W)$
Assertion	tendocnv	$⊢ ((K \in HL \land W \in H) \land S \in E \land F \in T) \to {S (F)}^{-1} = S (F^{-1})$

Proof

Step	Hyp	Ref	Expression
1		tendosp.h	$⊢ H = LHyp (K)$
2		tendosp.t	$⊢ T = LTrn (K) (W)$
3		tendosp.e	$⊢ E = TEndo (K) (W)$
4		simp1	$⊢ ((K \in HL \land W \in H) \land S \in E \land F \in T) \to (K \in HL \land W \in H)$
5	1 2 3	tendocl	$⊢ ((K \in HL \land W \in H) \land S \in E \land F \in T) \to S (F) \in T$
6		eqid	$⊢ {Base}_{K} = {Base}_{K}$
7	6 1 2	ltrn1o	$⊢ ((K \in HL \land W \in H) \land S (F) \in T) \to S (F) : {Base}_{K} \underset{1-1 onto}{⟶} {Base}_{K}$
8	4 5 7	syl2anc	$⊢ ((K \in HL \land W \in H) \land S \in E \land F \in T) \to S (F) : {Base}_{K} \underset{1-1 onto}{⟶} {Base}_{K}$
9		f1ococnv1	$⊢ S (F) : {Base}_{K} \underset{1-1 onto}{⟶} {Base}_{K} \to {S (F)}^{-1} \circ S (F) = {I ↾}_{{Base}_{K}}$
10	8 9	syl	$⊢ ((K \in HL \land W \in H) \land S \in E \land F \in T) \to {S (F)}^{-1} \circ S (F) = {I ↾}_{{Base}_{K}}$
11	10	coeq1d	$⊢ ((K \in HL \land W \in H) \land S \in E \land F \in T) \to ({S (F)}^{-1} \circ S (F)) \circ {S (F)}^{-1} = ({I ↾}_{{Base}_{K}}) \circ {S (F)}^{-1}$
12		simp2	$⊢ ((K \in HL \land W \in H) \land S \in E \land F \in T) \to S \in E$
13	6 1 3	tendoid	$⊢ ((K \in HL \land W \in H) \land S \in E) \to S ({I ↾}_{{Base}_{K}}) = {I ↾}_{{Base}_{K}}$
14	4 12 13	syl2anc	$⊢ ((K \in HL \land W \in H) \land S \in E \land F \in T) \to S ({I ↾}_{{Base}_{K}}) = {I ↾}_{{Base}_{K}}$
15	6 1 2	ltrn1o	$⊢ ((K \in HL \land W \in H) \land F \in T) \to F : {Base}_{K} \underset{1-1 onto}{⟶} {Base}_{K}$
16	15	3adant2	$⊢ ((K \in HL \land W \in H) \land S \in E \land F \in T) \to F : {Base}_{K} \underset{1-1 onto}{⟶} {Base}_{K}$
17		f1ococnv2	$⊢ F : {Base}_{K} \underset{1-1 onto}{⟶} {Base}_{K} \to F \circ F^{-1} = {I ↾}_{{Base}_{K}}$
18	16 17	syl	$⊢ ((K \in HL \land W \in H) \land S \in E \land F \in T) \to F \circ F^{-1} = {I ↾}_{{Base}_{K}}$
19	18	fveq2d	$⊢ ((K \in HL \land W \in H) \land S \in E \land F \in T) \to S (F \circ F^{-1}) = S ({I ↾}_{{Base}_{K}})$
20		f1ococnv2	$⊢ S (F) : {Base}_{K} \underset{1-1 onto}{⟶} {Base}_{K} \to S (F) \circ {S (F)}^{-1} = {I ↾}_{{Base}_{K}}$
21	8 20	syl	$⊢ ((K \in HL \land W \in H) \land S \in E \land F \in T) \to S (F) \circ {S (F)}^{-1} = {I ↾}_{{Base}_{K}}$
22	14 19 21	3eqtr4rd	$⊢ ((K \in HL \land W \in H) \land S \in E \land F \in T) \to S (F) \circ {S (F)}^{-1} = S (F \circ F^{-1})$
23		simp3	$⊢ ((K \in HL \land W \in H) \land S \in E \land F \in T) \to F \in T$
24	1 2	ltrncnv	$⊢ ((K \in HL \land W \in H) \land F \in T) \to F^{-1} \in T$
25	24	3adant2	$⊢ ((K \in HL \land W \in H) \land S \in E \land F \in T) \to F^{-1} \in T$
26	1 2 3	tendospdi1	$⊢ ((K \in HL \land W \in H) \land (S \in E \land F \in T \land F^{-1} \in T)) \to S (F \circ F^{-1}) = S (F) \circ S (F^{-1})$
27	4 12 23 25 26	syl13anc	$⊢ ((K \in HL \land W \in H) \land S \in E \land F \in T) \to S (F \circ F^{-1}) = S (F) \circ S (F^{-1})$
28	22 27	eqtrd	$⊢ ((K \in HL \land W \in H) \land S \in E \land F \in T) \to S (F) \circ {S (F)}^{-1} = S (F) \circ S (F^{-1})$
29	28	coeq2d	$⊢ ((K \in HL \land W \in H) \land S \in E \land F \in T) \to {S (F)}^{-1} \circ (S (F) \circ {S (F)}^{-1}) = {S (F)}^{-1} \circ (S (F) \circ S (F^{-1}))$
30		coass	$⊢ ({S (F)}^{-1} \circ S (F)) \circ {S (F)}^{-1} = {S (F)}^{-1} \circ (S (F) \circ {S (F)}^{-1})$
31		coass	$⊢ ({S (F)}^{-1} \circ S (F)) \circ S (F^{-1}) = {S (F)}^{-1} \circ (S (F) \circ S (F^{-1}))$
32	29 30 31	3eqtr4g	$⊢ ((K \in HL \land W \in H) \land S \in E \land F \in T) \to ({S (F)}^{-1} \circ S (F)) \circ {S (F)}^{-1} = ({S (F)}^{-1} \circ S (F)) \circ S (F^{-1})$
33	10	coeq1d	$⊢ ((K \in HL \land W \in H) \land S \in E \land F \in T) \to ({S (F)}^{-1} \circ S (F)) \circ S (F^{-1}) = ({I ↾}_{{Base}_{K}}) \circ S (F^{-1})$
34	1 2 3	tendocl	$⊢ ((K \in HL \land W \in H) \land S \in E \land F^{-1} \in T) \to S (F^{-1}) \in T$
35	25 34	syld3an3	$⊢ ((K \in HL \land W \in H) \land S \in E \land F \in T) \to S (F^{-1}) \in T$
36	6 1 2	ltrn1o	$⊢ ((K \in HL \land W \in H) \land S (F^{-1}) \in T) \to S (F^{-1}) : {Base}_{K} \underset{1-1 onto}{⟶} {Base}_{K}$
37	4 35 36	syl2anc	$⊢ ((K \in HL \land W \in H) \land S \in E \land F \in T) \to S (F^{-1}) : {Base}_{K} \underset{1-1 onto}{⟶} {Base}_{K}$
38		f1of	$⊢ S (F^{-1}) : {Base}_{K} \underset{1-1 onto}{⟶} {Base}_{K} \to S (F^{-1}) : {Base}_{K} ⟶ {Base}_{K}$
39		fcoi2	$⊢ S (F^{-1}) : {Base}_{K} ⟶ {Base}_{K} \to ({I ↾}_{{Base}_{K}}) \circ S (F^{-1}) = S (F^{-1})$
40	37 38 39	3syl	$⊢ ((K \in HL \land W \in H) \land S \in E \land F \in T) \to ({I ↾}_{{Base}_{K}}) \circ S (F^{-1}) = S (F^{-1})$
41	32 33 40	3eqtrd	$⊢ ((K \in HL \land W \in H) \land S \in E \land F \in T) \to ({S (F)}^{-1} \circ S (F)) \circ {S (F)}^{-1} = S (F^{-1})$
42	1 2	ltrncnv	$⊢ ((K \in HL \land W \in H) \land S (F) \in T) \to {S (F)}^{-1} \in T$
43	4 5 42	syl2anc	$⊢ ((K \in HL \land W \in H) \land S \in E \land F \in T) \to {S (F)}^{-1} \in T$
44	6 1 2	ltrn1o	$⊢ ((K \in HL \land W \in H) \land {S (F)}^{-1} \in T) \to {S (F)}^{-1} : {Base}_{K} \underset{1-1 onto}{⟶} {Base}_{K}$
45	4 43 44	syl2anc	$⊢ ((K \in HL \land W \in H) \land S \in E \land F \in T) \to {S (F)}^{-1} : {Base}_{K} \underset{1-1 onto}{⟶} {Base}_{K}$
46		f1of	$⊢ {S (F)}^{-1} : {Base}_{K} \underset{1-1 onto}{⟶} {Base}_{K} \to {S (F)}^{-1} : {Base}_{K} ⟶ {Base}_{K}$
47		fcoi2	$⊢ {S (F)}^{-1} : {Base}_{K} ⟶ {Base}_{K} \to ({I ↾}_{{Base}_{K}}) \circ {S (F)}^{-1} = {S (F)}^{-1}$
48	45 46 47	3syl	$⊢ ((K \in HL \land W \in H) \land S \in E \land F \in T) \to ({I ↾}_{{Base}_{K}}) \circ {S (F)}^{-1} = {S (F)}^{-1}$
49	11 41 48	3eqtr3rd	$⊢ ((K \in HL \land W \in H) \land S \in E \land F \in T) \to {S (F)}^{-1} = S (F^{-1})$

Metamath Proof Explorer

Theorem tendocnv

Proof