trlcone

Description: If two translations have different traces, the trace of their composition is also different. (Contributed by NM, 14-Jun-2013)

	Ref	Expression
Hypotheses	trlcone.b	$⊢ B = {Base}_{K}$
	trlcone.h	$⊢ H = LHyp (K)$
	trlcone.t	$⊢ T = LTrn (K) (W)$
	trlcone.r	$⊢ R = trL (K) (W)$
Assertion	trlcone	$⊢ ((K \in HL \land W \in H) \land (F \in T \land G \in T) \land (R (F) \neq R (G) \land G \neq {I ↾}_{B})) \to R (F) \neq R (F \circ G)$

Proof

Step	Hyp	Ref	Expression
1		trlcone.b	$⊢ B = {Base}_{K}$
2		trlcone.h	$⊢ H = LHyp (K)$
3		trlcone.t	$⊢ T = LTrn (K) (W)$
4		trlcone.r	$⊢ R = trL (K) (W)$
5		simpl3l	$⊢ (((K \in HL \land W \in H) \land (F \in T \land G \in T) \land (R (F) \neq R (G) \land G \neq {I ↾}_{B})) \land R (F) \in Atoms (K)) \to R (F) \neq R (G)$
6		simp11	$⊢ (((K \in HL \land W \in H) \land (F \in T \land G \in T) \land (R (F) \neq R (G) \land G \neq {I ↾}_{B})) \land R (F) \in Atoms (K) \land R (F) = R (F \circ G)) \to (K \in HL \land W \in H)$
7		simp12l	$⊢ (((K \in HL \land W \in H) \land (F \in T \land G \in T) \land (R (F) \neq R (G) \land G \neq {I ↾}_{B})) \land R (F) \in Atoms (K) \land R (F) = R (F \circ G)) \to F \in T$
8	2 3	ltrncnv	$⊢ ((K \in HL \land W \in H) \land F \in T) \to F^{-1} \in T$
9	6 7 8	syl2anc	$⊢ (((K \in HL \land W \in H) \land (F \in T \land G \in T) \land (R (F) \neq R (G) \land G \neq {I ↾}_{B})) \land R (F) \in Atoms (K) \land R (F) = R (F \circ G)) \to F^{-1} \in T$
10		simp12r	$⊢ (((K \in HL \land W \in H) \land (F \in T \land G \in T) \land (R (F) \neq R (G) \land G \neq {I ↾}_{B})) \land R (F) \in Atoms (K) \land R (F) = R (F \circ G)) \to G \in T$
11	2 3	ltrnco	$⊢ ((K \in HL \land W \in H) \land F \in T \land G \in T) \to F \circ G \in T$
12	6 7 10 11	syl3anc	$⊢ (((K \in HL \land W \in H) \land (F \in T \land G \in T) \land (R (F) \neq R (G) \land G \neq {I ↾}_{B})) \land R (F) \in Atoms (K) \land R (F) = R (F \circ G)) \to F \circ G \in T$
13		eqid	$⊢ \leq_{K} = \leq_{K}$
14		eqid	$⊢ join (K) = join (K)$
15	13 14 2 3 4	trlco	$⊢ ((K \in HL \land W \in H) \land F^{-1} \in T \land F \circ G \in T) \to R (F^{-1} \circ (F \circ G)) \leq_{K} (R (F^{-1}) join (K) R (F \circ G))$
16	6 9 12 15	syl3anc	$⊢ (((K \in HL \land W \in H) \land (F \in T \land G \in T) \land (R (F) \neq R (G) \land G \neq {I ↾}_{B})) \land R (F) \in Atoms (K) \land R (F) = R (F \circ G)) \to R (F^{-1} \circ (F \circ G)) \leq_{K} (R (F^{-1}) join (K) R (F \circ G))$
17		coass	$⊢ (F^{-1} \circ F) \circ G = F^{-1} \circ (F \circ G)$
18	1 2 3	ltrn1o	$⊢ ((K \in HL \land W \in H) \land F \in T) \to F : B \underset{1-1 onto}{⟶} B$
19	6 7 18	syl2anc	$⊢ (((K \in HL \land W \in H) \land (F \in T \land G \in T) \land (R (F) \neq R (G) \land G \neq {I ↾}_{B})) \land R (F) \in Atoms (K) \land R (F) = R (F \circ G)) \to F : B \underset{1-1 onto}{⟶} B$
20		f1ococnv1	$⊢ F : B \underset{1-1 onto}{⟶} B \to F^{-1} \circ F = {I ↾}_{B}$
21	19 20	syl	$⊢ (((K \in HL \land W \in H) \land (F \in T \land G \in T) \land (R (F) \neq R (G) \land G \neq {I ↾}_{B})) \land R (F) \in Atoms (K) \land R (F) = R (F \circ G)) \to F^{-1} \circ F = {I ↾}_{B}$
22	21	coeq1d	$⊢ (((K \in HL \land W \in H) \land (F \in T \land G \in T) \land (R (F) \neq R (G) \land G \neq {I ↾}_{B})) \land R (F) \in Atoms (K) \land R (F) = R (F \circ G)) \to (F^{-1} \circ F) \circ G = ({I ↾}_{B}) \circ G$
23	1 2 3	ltrn1o	$⊢ ((K \in HL \land W \in H) \land G \in T) \to G : B \underset{1-1 onto}{⟶} B$
24	6 10 23	syl2anc	$⊢ (((K \in HL \land W \in H) \land (F \in T \land G \in T) \land (R (F) \neq R (G) \land G \neq {I ↾}_{B})) \land R (F) \in Atoms (K) \land R (F) = R (F \circ G)) \to G : B \underset{1-1 onto}{⟶} B$
25		f1of	$⊢ G : B \underset{1-1 onto}{⟶} B \to G : B ⟶ B$
26		fcoi2	$⊢ G : B ⟶ B \to ({I ↾}_{B}) \circ G = G$
27	24 25 26	3syl	$⊢ (((K \in HL \land W \in H) \land (F \in T \land G \in T) \land (R (F) \neq R (G) \land G \neq {I ↾}_{B})) \land R (F) \in Atoms (K) \land R (F) = R (F \circ G)) \to ({I ↾}_{B}) \circ G = G$
28	22 27	eqtrd	$⊢ (((K \in HL \land W \in H) \land (F \in T \land G \in T) \land (R (F) \neq R (G) \land G \neq {I ↾}_{B})) \land R (F) \in Atoms (K) \land R (F) = R (F \circ G)) \to (F^{-1} \circ F) \circ G = G$
29	17 28	syl5reqr	$⊢ (((K \in HL \land W \in H) \land (F \in T \land G \in T) \land (R (F) \neq R (G) \land G \neq {I ↾}_{B})) \land R (F) \in Atoms (K) \land R (F) = R (F \circ G)) \to G = F^{-1} \circ (F \circ G)$
30	29	fveq2d	$⊢ (((K \in HL \land W \in H) \land (F \in T \land G \in T) \land (R (F) \neq R (G) \land G \neq {I ↾}_{B})) \land R (F) \in Atoms (K) \land R (F) = R (F \circ G)) \to R (G) = R (F^{-1} \circ (F \circ G))$
31		simp11l	$⊢ (((K \in HL \land W \in H) \land (F \in T \land G \in T) \land (R (F) \neq R (G) \land G \neq {I ↾}_{B})) \land R (F) \in Atoms (K) \land R (F) = R (F \circ G)) \to K \in HL$
32		simp2	$⊢ (((K \in HL \land W \in H) \land (F \in T \land G \in T) \land (R (F) \neq R (G) \land G \neq {I ↾}_{B})) \land R (F) \in Atoms (K) \land R (F) = R (F \circ G)) \to R (F) \in Atoms (K)$
33		eqid	$⊢ Atoms (K) = Atoms (K)$
34	14 33	hlatjidm	$⊢ (K \in HL \land R (F) \in Atoms (K)) \to R (F) join (K) R (F) = R (F)$
35	31 32 34	syl2anc	$⊢ (((K \in HL \land W \in H) \land (F \in T \land G \in T) \land (R (F) \neq R (G) \land G \neq {I ↾}_{B})) \land R (F) \in Atoms (K) \land R (F) = R (F \circ G)) \to R (F) join (K) R (F) = R (F)$
36	2 3 4	trlcnv	$⊢ ((K \in HL \land W \in H) \land F \in T) \to R (F^{-1}) = R (F)$
37	6 7 36	syl2anc	$⊢ (((K \in HL \land W \in H) \land (F \in T \land G \in T) \land (R (F) \neq R (G) \land G \neq {I ↾}_{B})) \land R (F) \in Atoms (K) \land R (F) = R (F \circ G)) \to R (F^{-1}) = R (F)$
38	37	eqcomd	$⊢ (((K \in HL \land W \in H) \land (F \in T \land G \in T) \land (R (F) \neq R (G) \land G \neq {I ↾}_{B})) \land R (F) \in Atoms (K) \land R (F) = R (F \circ G)) \to R (F) = R (F^{-1})$
39		simp3	$⊢ (((K \in HL \land W \in H) \land (F \in T \land G \in T) \land (R (F) \neq R (G) \land G \neq {I ↾}_{B})) \land R (F) \in Atoms (K) \land R (F) = R (F \circ G)) \to R (F) = R (F \circ G)$
40	38 39	oveq12d	$⊢ (((K \in HL \land W \in H) \land (F \in T \land G \in T) \land (R (F) \neq R (G) \land G \neq {I ↾}_{B})) \land R (F) \in Atoms (K) \land R (F) = R (F \circ G)) \to R (F) join (K) R (F) = R (F^{-1}) join (K) R (F \circ G)$
41	35 40	eqtr3d	$⊢ (((K \in HL \land W \in H) \land (F \in T \land G \in T) \land (R (F) \neq R (G) \land G \neq {I ↾}_{B})) \land R (F) \in Atoms (K) \land R (F) = R (F \circ G)) \to R (F) = R (F^{-1}) join (K) R (F \circ G)$
42	16 30 41	3brtr4d	$⊢ (((K \in HL \land W \in H) \land (F \in T \land G \in T) \land (R (F) \neq R (G) \land G \neq {I ↾}_{B})) \land R (F) \in Atoms (K) \land R (F) = R (F \circ G)) \to R (G) \leq_{K} R (F)$
43		hlatl	$⊢ K \in HL \to K \in AtLat$
44	31 43	syl	$⊢ (((K \in HL \land W \in H) \land (F \in T \land G \in T) \land (R (F) \neq R (G) \land G \neq {I ↾}_{B})) \land R (F) \in Atoms (K) \land R (F) = R (F \circ G)) \to K \in AtLat$
45		simp13r	$⊢ (((K \in HL \land W \in H) \land (F \in T \land G \in T) \land (R (F) \neq R (G) \land G \neq {I ↾}_{B})) \land R (F) \in Atoms (K) \land R (F) = R (F \circ G)) \to G \neq {I ↾}_{B}$
46	1 33 2 3 4	trlnidat	$⊢ ((K \in HL \land W \in H) \land G \in T \land G \neq {I ↾}_{B}) \to R (G) \in Atoms (K)$
47	6 10 45 46	syl3anc	$⊢ (((K \in HL \land W \in H) \land (F \in T \land G \in T) \land (R (F) \neq R (G) \land G \neq {I ↾}_{B})) \land R (F) \in Atoms (K) \land R (F) = R (F \circ G)) \to R (G) \in Atoms (K)$
48	13 33	atcmp	$⊢ (K \in AtLat \land R (G) \in Atoms (K) \land R (F) \in Atoms (K)) \to (R (G) \leq_{K} R (F) \leftrightarrow R (G) = R (F))$
49	44 47 32 48	syl3anc	$⊢ (((K \in HL \land W \in H) \land (F \in T \land G \in T) \land (R (F) \neq R (G) \land G \neq {I ↾}_{B})) \land R (F) \in Atoms (K) \land R (F) = R (F \circ G)) \to (R (G) \leq_{K} R (F) \leftrightarrow R (G) = R (F))$
50	42 49	mpbid	$⊢ (((K \in HL \land W \in H) \land (F \in T \land G \in T) \land (R (F) \neq R (G) \land G \neq {I ↾}_{B})) \land R (F) \in Atoms (K) \land R (F) = R (F \circ G)) \to R (G) = R (F)$
51	50	eqcomd	$⊢ (((K \in HL \land W \in H) \land (F \in T \land G \in T) \land (R (F) \neq R (G) \land G \neq {I ↾}_{B})) \land R (F) \in Atoms (K) \land R (F) = R (F \circ G)) \to R (F) = R (G)$
52	51	3expia	$⊢ (((K \in HL \land W \in H) \land (F \in T \land G \in T) \land (R (F) \neq R (G) \land G \neq {I ↾}_{B})) \land R (F) \in Atoms (K)) \to (R (F) = R (F \circ G) \to R (F) = R (G))$
53	52	necon3d	$⊢ (((K \in HL \land W \in H) \land (F \in T \land G \in T) \land (R (F) \neq R (G) \land G \neq {I ↾}_{B})) \land R (F) \in Atoms (K)) \to (R (F) \neq R (G) \to R (F) \neq R (F \circ G))$
54	5 53	mpd	$⊢ (((K \in HL \land W \in H) \land (F \in T \land G \in T) \land (R (F) \neq R (G) \land G \neq {I ↾}_{B})) \land R (F) \in Atoms (K)) \to R (F) \neq R (F \circ G)$
55		simpl3r	$⊢ (((K \in HL \land W \in H) \land (F \in T \land G \in T) \land (R (F) \neq R (G) \land G \neq {I ↾}_{B})) \land R (F) = 0. (K)) \to G \neq {I ↾}_{B}$
56		simpl1	$⊢ (((K \in HL \land W \in H) \land (F \in T \land G \in T) \land (R (F) \neq R (G) \land G \neq {I ↾}_{B})) \land R (F) = 0. (K)) \to (K \in HL \land W \in H)$
57		simpl2r	$⊢ (((K \in HL \land W \in H) \land (F \in T \land G \in T) \land (R (F) \neq R (G) \land G \neq {I ↾}_{B})) \land R (F) = 0. (K)) \to G \in T$
58		eqid	$⊢ 0. (K) = 0. (K)$
59	1 58 2 3 4	trlid0b	$⊢ ((K \in HL \land W \in H) \land G \in T) \to (G = {I ↾}_{B} \leftrightarrow R (G) = 0. (K))$
60	56 57 59	syl2anc	$⊢ (((K \in HL \land W \in H) \land (F \in T \land G \in T) \land (R (F) \neq R (G) \land G \neq {I ↾}_{B})) \land R (F) = 0. (K)) \to (G = {I ↾}_{B} \leftrightarrow R (G) = 0. (K))$
61	60	necon3bid	$⊢ (((K \in HL \land W \in H) \land (F \in T \land G \in T) \land (R (F) \neq R (G) \land G \neq {I ↾}_{B})) \land R (F) = 0. (K)) \to (G \neq {I ↾}_{B} \leftrightarrow R (G) \neq 0. (K))$
62	55 61	mpbid	$⊢ (((K \in HL \land W \in H) \land (F \in T \land G \in T) \land (R (F) \neq R (G) \land G \neq {I ↾}_{B})) \land R (F) = 0. (K)) \to R (G) \neq 0. (K)$
63	62	necomd	$⊢ (((K \in HL \land W \in H) \land (F \in T \land G \in T) \land (R (F) \neq R (G) \land G \neq {I ↾}_{B})) \land R (F) = 0. (K)) \to 0. (K) \neq R (G)$
64		simpr	$⊢ (((K \in HL \land W \in H) \land (F \in T \land G \in T) \land (R (F) \neq R (G) \land G \neq {I ↾}_{B})) \land R (F) = 0. (K)) \to R (F) = 0. (K)$
65		simpl2l	$⊢ (((K \in HL \land W \in H) \land (F \in T \land G \in T) \land (R (F) \neq R (G) \land G \neq {I ↾}_{B})) \land R (F) = 0. (K)) \to F \in T$
66	1 58 2 3 4	trlid0b	$⊢ ((K \in HL \land W \in H) \land F \in T) \to (F = {I ↾}_{B} \leftrightarrow R (F) = 0. (K))$
67	56 65 66	syl2anc	$⊢ (((K \in HL \land W \in H) \land (F \in T \land G \in T) \land (R (F) \neq R (G) \land G \neq {I ↾}_{B})) \land R (F) = 0. (K)) \to (F = {I ↾}_{B} \leftrightarrow R (F) = 0. (K))$
68	64 67	mpbird	$⊢ (((K \in HL \land W \in H) \land (F \in T \land G \in T) \land (R (F) \neq R (G) \land G \neq {I ↾}_{B})) \land R (F) = 0. (K)) \to F = {I ↾}_{B}$
69	68	coeq1d	$⊢ (((K \in HL \land W \in H) \land (F \in T \land G \in T) \land (R (F) \neq R (G) \land G \neq {I ↾}_{B})) \land R (F) = 0. (K)) \to F \circ G = ({I ↾}_{B}) \circ G$
70	56 57 23	syl2anc	$⊢ (((K \in HL \land W \in H) \land (F \in T \land G \in T) \land (R (F) \neq R (G) \land G \neq {I ↾}_{B})) \land R (F) = 0. (K)) \to G : B \underset{1-1 onto}{⟶} B$
71	70 25 26	3syl	$⊢ (((K \in HL \land W \in H) \land (F \in T \land G \in T) \land (R (F) \neq R (G) \land G \neq {I ↾}_{B})) \land R (F) = 0. (K)) \to ({I ↾}_{B}) \circ G = G$
72	69 71	eqtrd	$⊢ (((K \in HL \land W \in H) \land (F \in T \land G \in T) \land (R (F) \neq R (G) \land G \neq {I ↾}_{B})) \land R (F) = 0. (K)) \to F \circ G = G$
73	72	fveq2d	$⊢ (((K \in HL \land W \in H) \land (F \in T \land G \in T) \land (R (F) \neq R (G) \land G \neq {I ↾}_{B})) \land R (F) = 0. (K)) \to R (F \circ G) = R (G)$
74	63 64 73	3netr4d	$⊢ (((K \in HL \land W \in H) \land (F \in T \land G \in T) \land (R (F) \neq R (G) \land G \neq {I ↾}_{B})) \land R (F) = 0. (K)) \to R (F) \neq R (F \circ G)$
75		simp1	$⊢ ((K \in HL \land W \in H) \land (F \in T \land G \in T) \land (R (F) \neq R (G) \land G \neq {I ↾}_{B})) \to (K \in HL \land W \in H)$
76		simp2l	$⊢ ((K \in HL \land W \in H) \land (F \in T \land G \in T) \land (R (F) \neq R (G) \land G \neq {I ↾}_{B})) \to F \in T$
77	58 33 2 3 4	trlator0	$⊢ ((K \in HL \land W \in H) \land F \in T) \to (R (F) \in Atoms (K) \lor R (F) = 0. (K))$
78	75 76 77	syl2anc	$⊢ ((K \in HL \land W \in H) \land (F \in T \land G \in T) \land (R (F) \neq R (G) \land G \neq {I ↾}_{B})) \to (R (F) \in Atoms (K) \lor R (F) = 0. (K))$
79	54 74 78	mpjaodan	$⊢ ((K \in HL \land W \in H) \land (F \in T \land G \in T) \land (R (F) \neq R (G) \land G \neq {I ↾}_{B})) \to R (F) \neq R (F \circ G)$

Metamath Proof Explorer

Theorem trlcone

Proof