trlcoat

Description: The trace of a composition of two translations is an atom if their traces are different. (Contributed by NM, 15-Jun-2013)

	Ref	Expression
Hypotheses	trlcoat.a	$⊢ A = Atoms (K)$
	trlcoat.h	$⊢ H = LHyp (K)$
	trlcoat.t	$⊢ T = LTrn (K) (W)$
	trlcoat.r	$⊢ R = trL (K) (W)$
Assertion	trlcoat	$⊢ ((K \in HL \land W \in H) \land (F \in T \land G \in T) \land R (F) \neq R (G)) \to R (F \circ G) \in A$

Proof

Step	Hyp	Ref	Expression
1		trlcoat.a	$⊢ A = Atoms (K)$
2		trlcoat.h	$⊢ H = LHyp (K)$
3		trlcoat.t	$⊢ T = LTrn (K) (W)$
4		trlcoat.r	$⊢ R = trL (K) (W)$
5	2 3	ltrnco	$⊢ ((K \in HL \land W \in H) \land F \in T \land G \in T) \to F \circ G \in T$
6	5	3expb	$⊢ ((K \in HL \land W \in H) \land (F \in T \land G \in T)) \to F \circ G \in T$
7		eqid	$⊢ {Base}_{K} = {Base}_{K}$
8		eqid	$⊢ 0. (K) = 0. (K)$
9	7 8 2 3 4	trlid0b	$⊢ ((K \in HL \land W \in H) \land F \circ G \in T) \to (F \circ G = {I ↾}_{{Base}_{K}} \leftrightarrow R (F \circ G) = 0. (K))$
10	6 9	syldan	$⊢ ((K \in HL \land W \in H) \land (F \in T \land G \in T)) \to (F \circ G = {I ↾}_{{Base}_{K}} \leftrightarrow R (F \circ G) = 0. (K))$
11		coass	$⊢ (F^{-1} \circ F) \circ G = F^{-1} \circ (F \circ G)$
12		simpll	$⊢ (((K \in HL \land W \in H) \land (F \in T \land G \in T)) \land F \circ G = {I ↾}_{{Base}_{K}}) \to (K \in HL \land W \in H)$
13		simplrl	$⊢ (((K \in HL \land W \in H) \land (F \in T \land G \in T)) \land F \circ G = {I ↾}_{{Base}_{K}}) \to F \in T$
14	7 2 3	ltrn1o	$⊢ ((K \in HL \land W \in H) \land F \in T) \to F : {Base}_{K} \underset{1-1 onto}{⟶} {Base}_{K}$
15	12 13 14	syl2anc	$⊢ (((K \in HL \land W \in H) \land (F \in T \land G \in T)) \land F \circ G = {I ↾}_{{Base}_{K}}) \to F : {Base}_{K} \underset{1-1 onto}{⟶} {Base}_{K}$
16		f1ococnv1	$⊢ F : {Base}_{K} \underset{1-1 onto}{⟶} {Base}_{K} \to F^{-1} \circ F = {I ↾}_{{Base}_{K}}$
17	15 16	syl	$⊢ (((K \in HL \land W \in H) \land (F \in T \land G \in T)) \land F \circ G = {I ↾}_{{Base}_{K}}) \to F^{-1} \circ F = {I ↾}_{{Base}_{K}}$
18	17	coeq1d	$⊢ (((K \in HL \land W \in H) \land (F \in T \land G \in T)) \land F \circ G = {I ↾}_{{Base}_{K}}) \to (F^{-1} \circ F) \circ G = ({I ↾}_{{Base}_{K}}) \circ G$
19		coeq2	$⊢ F \circ G = {I ↾}_{{Base}_{K}} \to F^{-1} \circ (F \circ G) = F^{-1} \circ ({I ↾}_{{Base}_{K}})$
20	19	adantl	$⊢ (((K \in HL \land W \in H) \land (F \in T \land G \in T)) \land F \circ G = {I ↾}_{{Base}_{K}}) \to F^{-1} \circ (F \circ G) = F^{-1} \circ ({I ↾}_{{Base}_{K}})$
21	11 18 20	3eqtr3a	$⊢ (((K \in HL \land W \in H) \land (F \in T \land G \in T)) \land F \circ G = {I ↾}_{{Base}_{K}}) \to ({I ↾}_{{Base}_{K}}) \circ G = F^{-1} \circ ({I ↾}_{{Base}_{K}})$
22		simplrr	$⊢ (((K \in HL \land W \in H) \land (F \in T \land G \in T)) \land F \circ G = {I ↾}_{{Base}_{K}}) \to G \in T$
23	7 2 3	ltrn1o	$⊢ ((K \in HL \land W \in H) \land G \in T) \to G : {Base}_{K} \underset{1-1 onto}{⟶} {Base}_{K}$
24	12 22 23	syl2anc	$⊢ (((K \in HL \land W \in H) \land (F \in T \land G \in T)) \land F \circ G = {I ↾}_{{Base}_{K}}) \to G : {Base}_{K} \underset{1-1 onto}{⟶} {Base}_{K}$
25		f1of	$⊢ G : {Base}_{K} \underset{1-1 onto}{⟶} {Base}_{K} \to G : {Base}_{K} ⟶ {Base}_{K}$
26		fcoi2	$⊢ G : {Base}_{K} ⟶ {Base}_{K} \to ({I ↾}_{{Base}_{K}}) \circ G = G$
27	24 25 26	3syl	$⊢ (((K \in HL \land W \in H) \land (F \in T \land G \in T)) \land F \circ G = {I ↾}_{{Base}_{K}}) \to ({I ↾}_{{Base}_{K}}) \circ G = G$
28	2 3	ltrncnv	$⊢ ((K \in HL \land W \in H) \land F \in T) \to F^{-1} \in T$
29	12 13 28	syl2anc	$⊢ (((K \in HL \land W \in H) \land (F \in T \land G \in T)) \land F \circ G = {I ↾}_{{Base}_{K}}) \to F^{-1} \in T$
30	7 2 3	ltrn1o	$⊢ ((K \in HL \land W \in H) \land F^{-1} \in T) \to F^{-1} : {Base}_{K} \underset{1-1 onto}{⟶} {Base}_{K}$
31	12 29 30	syl2anc	$⊢ (((K \in HL \land W \in H) \land (F \in T \land G \in T)) \land F \circ G = {I ↾}_{{Base}_{K}}) \to F^{-1} : {Base}_{K} \underset{1-1 onto}{⟶} {Base}_{K}$
32		f1of	$⊢ F^{-1} : {Base}_{K} \underset{1-1 onto}{⟶} {Base}_{K} \to F^{-1} : {Base}_{K} ⟶ {Base}_{K}$
33		fcoi1	$⊢ F^{-1} : {Base}_{K} ⟶ {Base}_{K} \to F^{-1} \circ ({I ↾}_{{Base}_{K}}) = F^{-1}$
34	31 32 33	3syl	$⊢ (((K \in HL \land W \in H) \land (F \in T \land G \in T)) \land F \circ G = {I ↾}_{{Base}_{K}}) \to F^{-1} \circ ({I ↾}_{{Base}_{K}}) = F^{-1}$
35	21 27 34	3eqtr3d	$⊢ (((K \in HL \land W \in H) \land (F \in T \land G \in T)) \land F \circ G = {I ↾}_{{Base}_{K}}) \to G = F^{-1}$
36	35	fveq2d	$⊢ (((K \in HL \land W \in H) \land (F \in T \land G \in T)) \land F \circ G = {I ↾}_{{Base}_{K}}) \to R (G) = R (F^{-1})$
37	2 3 4	trlcnv	$⊢ ((K \in HL \land W \in H) \land F \in T) \to R (F^{-1}) = R (F)$
38	12 13 37	syl2anc	$⊢ (((K \in HL \land W \in H) \land (F \in T \land G \in T)) \land F \circ G = {I ↾}_{{Base}_{K}}) \to R (F^{-1}) = R (F)$
39	36 38	eqtr2d	$⊢ (((K \in HL \land W \in H) \land (F \in T \land G \in T)) \land F \circ G = {I ↾}_{{Base}_{K}}) \to R (F) = R (G)$
40	39	ex	$⊢ ((K \in HL \land W \in H) \land (F \in T \land G \in T)) \to (F \circ G = {I ↾}_{{Base}_{K}} \to R (F) = R (G))$
41	10 40	sylbird	$⊢ ((K \in HL \land W \in H) \land (F \in T \land G \in T)) \to (R (F \circ G) = 0. (K) \to R (F) = R (G))$
42	41	necon3d	$⊢ ((K \in HL \land W \in H) \land (F \in T \land G \in T)) \to (R (F) \neq R (G) \to R (F \circ G) \neq 0. (K))$
43	8 1 2 3 4	trlatn0	$⊢ ((K \in HL \land W \in H) \land F \circ G \in T) \to (R (F \circ G) \in A \leftrightarrow R (F \circ G) \neq 0. (K))$
44	6 43	syldan	$⊢ ((K \in HL \land W \in H) \land (F \in T \land G \in T)) \to (R (F \circ G) \in A \leftrightarrow R (F \circ G) \neq 0. (K))$
45	42 44	sylibrd	$⊢ ((K \in HL \land W \in H) \land (F \in T \land G \in T)) \to (R (F) \neq R (G) \to R (F \circ G) \in A)$
46	45	3impia	$⊢ ((K \in HL \land W \in H) \land (F \in T \land G \in T) \land R (F) \neq R (G)) \to R (F \circ G) \in A$

Metamath Proof Explorer

Theorem trlcoat

Proof