cdlemg46

Description: Part of proof of Lemma G of Crawley p. 116, seventh line of third paragraph on p. 117: "hf and f have different traces." (Contributed by NM, 5-Jun-2013)

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

Proof

Step	Hyp	Ref	Expression
1		cdlemg46.b	$⊢ B = {Base}_{K}$
2		cdlemg46.h	$⊢ H = LHyp (K)$
3		cdlemg46.t	$⊢ T = LTrn (K) (W)$
4		cdlemg46.r	$⊢ R = trL (K) (W)$
5		simpl1l	$⊢ (((K \in HL \land W \in H) \land (F \in T \land h \in T) \land (F \neq {I ↾}_{B} \land h \neq {I ↾}_{B} \land R (h) \neq R (F))) \land R (h \circ F) \in Atoms (K)) \to K \in HL$
6		simp1	$⊢ ((K \in HL \land W \in H) \land (F \in T \land h \in T) \land (F \neq {I ↾}_{B} \land h \neq {I ↾}_{B} \land R (h) \neq R (F))) \to (K \in HL \land W \in H)$
7		simp2r	$⊢ ((K \in HL \land W \in H) \land (F \in T \land h \in T) \land (F \neq {I ↾}_{B} \land h \neq {I ↾}_{B} \land R (h) \neq R (F))) \to h \in T$
8		simp32	$⊢ ((K \in HL \land W \in H) \land (F \in T \land h \in T) \land (F \neq {I ↾}_{B} \land h \neq {I ↾}_{B} \land R (h) \neq R (F))) \to h \neq {I ↾}_{B}$
9		eqid	$⊢ Atoms (K) = Atoms (K)$
10	1 9 2 3 4	trlnidat	$⊢ ((K \in HL \land W \in H) \land h \in T \land h \neq {I ↾}_{B}) \to R (h) \in Atoms (K)$
11	6 7 8 10	syl3anc	$⊢ ((K \in HL \land W \in H) \land (F \in T \land h \in T) \land (F \neq {I ↾}_{B} \land h \neq {I ↾}_{B} \land R (h) \neq R (F))) \to R (h) \in Atoms (K)$
12	11	adantr	$⊢ (((K \in HL \land W \in H) \land (F \in T \land h \in T) \land (F \neq {I ↾}_{B} \land h \neq {I ↾}_{B} \land R (h) \neq R (F))) \land R (h \circ F) \in Atoms (K)) \to R (h) \in Atoms (K)$
13		simp2l	$⊢ ((K \in HL \land W \in H) \land (F \in T \land h \in T) \land (F \neq {I ↾}_{B} \land h \neq {I ↾}_{B} \land R (h) \neq R (F))) \to F \in T$
14		simp31	$⊢ ((K \in HL \land W \in H) \land (F \in T \land h \in T) \land (F \neq {I ↾}_{B} \land h \neq {I ↾}_{B} \land R (h) \neq R (F))) \to F \neq {I ↾}_{B}$
15	1 9 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)$
16	6 13 14 15	syl3anc	$⊢ ((K \in HL \land W \in H) \land (F \in T \land h \in T) \land (F \neq {I ↾}_{B} \land h \neq {I ↾}_{B} \land R (h) \neq R (F))) \to R (F) \in Atoms (K)$
17	16	adantr	$⊢ (((K \in HL \land W \in H) \land (F \in T \land h \in T) \land (F \neq {I ↾}_{B} \land h \neq {I ↾}_{B} \land R (h) \neq R (F))) \land R (h \circ F) \in Atoms (K)) \to R (F) \in Atoms (K)$
18		simpl33	$⊢ (((K \in HL \land W \in H) \land (F \in T \land h \in T) \land (F \neq {I ↾}_{B} \land h \neq {I ↾}_{B} \land R (h) \neq R (F))) \land R (h \circ F) \in Atoms (K)) \to R (h) \neq R (F)$
19		simpr	$⊢ (((K \in HL \land W \in H) \land (F \in T \land h \in T) \land (F \neq {I ↾}_{B} \land h \neq {I ↾}_{B} \land R (h) \neq R (F))) \land R (h \circ F) \in Atoms (K)) \to R (h \circ F) \in Atoms (K)$
20	2 3	ltrnco	$⊢ ((K \in HL \land W \in H) \land h \in T \land F \in T) \to h \circ F \in T$
21	6 7 13 20	syl3anc	$⊢ ((K \in HL \land W \in H) \land (F \in T \land h \in T) \land (F \neq {I ↾}_{B} \land h \neq {I ↾}_{B} \land R (h) \neq R (F))) \to h \circ F \in T$
22	2 3	ltrncnv	$⊢ ((K \in HL \land W \in H) \land F \in T) \to F^{-1} \in T$
23	6 13 22	syl2anc	$⊢ ((K \in HL \land W \in H) \land (F \in T \land h \in T) \land (F \neq {I ↾}_{B} \land h \neq {I ↾}_{B} \land R (h) \neq R (F))) \to F^{-1} \in T$
24		eqid	$⊢ \leq_{K} = \leq_{K}$
25		eqid	$⊢ join (K) = join (K)$
26	24 25 2 3 4	trlco	$⊢ ((K \in HL \land W \in H) \land h \circ F \in T \land F^{-1} \in T) \to R ((h \circ F) \circ F^{-1}) \leq_{K} (R (h \circ F) join (K) R (F^{-1}))$
27	6 21 23 26	syl3anc	$⊢ ((K \in HL \land W \in H) \land (F \in T \land h \in T) \land (F \neq {I ↾}_{B} \land h \neq {I ↾}_{B} \land R (h) \neq R (F))) \to R ((h \circ F) \circ F^{-1}) \leq_{K} (R (h \circ F) join (K) R (F^{-1}))$
28		coass	$⊢ (h \circ F) \circ F^{-1} = h \circ (F \circ F^{-1})$
29	1 2 3	ltrn1o	$⊢ ((K \in HL \land W \in H) \land F \in T) \to F : B \underset{1-1 onto}{⟶} B$
30	6 13 29	syl2anc	$⊢ ((K \in HL \land W \in H) \land (F \in T \land h \in T) \land (F \neq {I ↾}_{B} \land h \neq {I ↾}_{B} \land R (h) \neq R (F))) \to F : B \underset{1-1 onto}{⟶} B$
31		f1ococnv2	$⊢ F : B \underset{1-1 onto}{⟶} B \to F \circ F^{-1} = {I ↾}_{B}$
32	30 31	syl	$⊢ ((K \in HL \land W \in H) \land (F \in T \land h \in T) \land (F \neq {I ↾}_{B} \land h \neq {I ↾}_{B} \land R (h) \neq R (F))) \to F \circ F^{-1} = {I ↾}_{B}$
33	32	coeq2d	$⊢ ((K \in HL \land W \in H) \land (F \in T \land h \in T) \land (F \neq {I ↾}_{B} \land h \neq {I ↾}_{B} \land R (h) \neq R (F))) \to h \circ (F \circ F^{-1}) = h \circ ({I ↾}_{B})$
34	1 2 3	ltrn1o	$⊢ ((K \in HL \land W \in H) \land h \in T) \to h : B \underset{1-1 onto}{⟶} B$
35	6 7 34	syl2anc	$⊢ ((K \in HL \land W \in H) \land (F \in T \land h \in T) \land (F \neq {I ↾}_{B} \land h \neq {I ↾}_{B} \land R (h) \neq R (F))) \to h : B \underset{1-1 onto}{⟶} B$
36		f1of	$⊢ h : B \underset{1-1 onto}{⟶} B \to h : B ⟶ B$
37		fcoi1	$⊢ h : B ⟶ B \to h \circ ({I ↾}_{B}) = h$
38	35 36 37	3syl	$⊢ ((K \in HL \land W \in H) \land (F \in T \land h \in T) \land (F \neq {I ↾}_{B} \land h \neq {I ↾}_{B} \land R (h) \neq R (F))) \to h \circ ({I ↾}_{B}) = h$
39	33 38	eqtrd	$⊢ ((K \in HL \land W \in H) \land (F \in T \land h \in T) \land (F \neq {I ↾}_{B} \land h \neq {I ↾}_{B} \land R (h) \neq R (F))) \to h \circ (F \circ F^{-1}) = h$
40	28 39	syl5eq	$⊢ ((K \in HL \land W \in H) \land (F \in T \land h \in T) \land (F \neq {I ↾}_{B} \land h \neq {I ↾}_{B} \land R (h) \neq R (F))) \to (h \circ F) \circ F^{-1} = h$
41	40	fveq2d	$⊢ ((K \in HL \land W \in H) \land (F \in T \land h \in T) \land (F \neq {I ↾}_{B} \land h \neq {I ↾}_{B} \land R (h) \neq R (F))) \to R ((h \circ F) \circ F^{-1}) = R (h)$
42	2 3 4	trlcnv	$⊢ ((K \in HL \land W \in H) \land F \in T) \to R (F^{-1}) = R (F)$
43	6 13 42	syl2anc	$⊢ ((K \in HL \land W \in H) \land (F \in T \land h \in T) \land (F \neq {I ↾}_{B} \land h \neq {I ↾}_{B} \land R (h) \neq R (F))) \to R (F^{-1}) = R (F)$
44	43	oveq2d	$⊢ ((K \in HL \land W \in H) \land (F \in T \land h \in T) \land (F \neq {I ↾}_{B} \land h \neq {I ↾}_{B} \land R (h) \neq R (F))) \to R (h \circ F) join (K) R (F^{-1}) = R (h \circ F) join (K) R (F)$
45	27 41 44	3brtr3d	$⊢ ((K \in HL \land W \in H) \land (F \in T \land h \in T) \land (F \neq {I ↾}_{B} \land h \neq {I ↾}_{B} \land R (h) \neq R (F))) \to R (h) \leq_{K} (R (h \circ F) join (K) R (F))$
46	45	adantr	$⊢ (((K \in HL \land W \in H) \land (F \in T \land h \in T) \land (F \neq {I ↾}_{B} \land h \neq {I ↾}_{B} \land R (h) \neq R (F))) \land R (h \circ F) \in Atoms (K)) \to R (h) \leq_{K} (R (h \circ F) join (K) R (F))$
47	24 25 9	hlatlej2	$⊢ (K \in HL \land R (h \circ F) \in Atoms (K) \land R (F) \in Atoms (K)) \to R (F) \leq_{K} (R (h \circ F) join (K) R (F))$
48	5 19 17 47	syl3anc	$⊢ (((K \in HL \land W \in H) \land (F \in T \land h \in T) \land (F \neq {I ↾}_{B} \land h \neq {I ↾}_{B} \land R (h) \neq R (F))) \land R (h \circ F) \in Atoms (K)) \to R (F) \leq_{K} (R (h \circ F) join (K) R (F))$
49	5	hllatd	$⊢ (((K \in HL \land W \in H) \land (F \in T \land h \in T) \land (F \neq {I ↾}_{B} \land h \neq {I ↾}_{B} \land R (h) \neq R (F))) \land R (h \circ F) \in Atoms (K)) \to K \in Lat$
50	1 9	atbase	$⊢ R (h) \in Atoms (K) \to R (h) \in B$
51	12 50	syl	$⊢ (((K \in HL \land W \in H) \land (F \in T \land h \in T) \land (F \neq {I ↾}_{B} \land h \neq {I ↾}_{B} \land R (h) \neq R (F))) \land R (h \circ F) \in Atoms (K)) \to R (h) \in B$
52	1 9	atbase	$⊢ R (F) \in Atoms (K) \to R (F) \in B$
53	17 52	syl	$⊢ (((K \in HL \land W \in H) \land (F \in T \land h \in T) \land (F \neq {I ↾}_{B} \land h \neq {I ↾}_{B} \land R (h) \neq R (F))) \land R (h \circ F) \in Atoms (K)) \to R (F) \in B$
54	1 25 9	hlatjcl	$⊢ (K \in HL \land R (h \circ F) \in Atoms (K) \land R (F) \in Atoms (K)) \to R (h \circ F) join (K) R (F) \in B$
55	5 19 17 54	syl3anc	$⊢ (((K \in HL \land W \in H) \land (F \in T \land h \in T) \land (F \neq {I ↾}_{B} \land h \neq {I ↾}_{B} \land R (h) \neq R (F))) \land R (h \circ F) \in Atoms (K)) \to R (h \circ F) join (K) R (F) \in B$
56	1 24 25	latjle12	$⊢ (K \in Lat \land (R (h) \in B \land R (F) \in B \land R (h \circ F) join (K) R (F) \in B)) \to ((R (h) \leq_{K} (R (h \circ F) join (K) R (F)) \land R (F) \leq_{K} (R (h \circ F) join (K) R (F))) \leftrightarrow (R (h) join (K) R (F)) \leq_{K} (R (h \circ F) join (K) R (F)))$
57	49 51 53 55 56	syl13anc	$⊢ (((K \in HL \land W \in H) \land (F \in T \land h \in T) \land (F \neq {I ↾}_{B} \land h \neq {I ↾}_{B} \land R (h) \neq R (F))) \land R (h \circ F) \in Atoms (K)) \to ((R (h) \leq_{K} (R (h \circ F) join (K) R (F)) \land R (F) \leq_{K} (R (h \circ F) join (K) R (F))) \leftrightarrow (R (h) join (K) R (F)) \leq_{K} (R (h \circ F) join (K) R (F)))$
58	46 48 57	mpbi2and	$⊢ (((K \in HL \land W \in H) \land (F \in T \land h \in T) \land (F \neq {I ↾}_{B} \land h \neq {I ↾}_{B} \land R (h) \neq R (F))) \land R (h \circ F) \in Atoms (K)) \to (R (h) join (K) R (F)) \leq_{K} (R (h \circ F) join (K) R (F))$
59	24 25 9	2atjlej	$⊢ (K \in HL \land (R (h) \in Atoms (K) \land R (F) \in Atoms (K) \land R (h) \neq R (F)) \land (R (h \circ F) \in Atoms (K) \land R (F) \in Atoms (K) \land (R (h) join (K) R (F)) \leq_{K} (R (h \circ F) join (K) R (F)))) \to R (h \circ F) \neq R (F)$
60	5 12 17 18 19 17 58 59	syl133anc	$⊢ (((K \in HL \land W \in H) \land (F \in T \land h \in T) \land (F \neq {I ↾}_{B} \land h \neq {I ↾}_{B} \land R (h) \neq R (F))) \land R (h \circ F) \in Atoms (K)) \to R (h \circ F) \neq R (F)$
61		nelne2	$⊢ (R (F) \in Atoms (K) \land \neg R (h \circ F) \in Atoms (K)) \to R (F) \neq R (h \circ F)$
62	61	necomd	$⊢ (R (F) \in Atoms (K) \land \neg R (h \circ F) \in Atoms (K)) \to R (h \circ F) \neq R (F)$
63	16 62	sylan	$⊢ (((K \in HL \land W \in H) \land (F \in T \land h \in T) \land (F \neq {I ↾}_{B} \land h \neq {I ↾}_{B} \land R (h) \neq R (F))) \land \neg R (h \circ F) \in Atoms (K)) \to R (h \circ F) \neq R (F)$
64	60 63	pm2.61dan	$⊢ ((K \in HL \land W \in H) \land (F \in T \land h \in T) \land (F \neq {I ↾}_{B} \land h \neq {I ↾}_{B} \land R (h) \neq R (F))) \to R (h \circ F) \neq R (F)$

Metamath Proof Explorer

Theorem cdlemg46

Proof