trlcoabs2N

Description: Absorption of the trace of a composition. (Contributed by NM, 29-Jul-2013) (New usage is discouraged.)

	Ref	Expression
Hypotheses	trlcoabs.l	$⊢ \underset{˙}{\leq} = \leq_{K}$
	trlcoabs.j	$⊢ \underset{˙}{\lor} = join (K)$
	trlcoabs.a	$⊢ A = Atoms (K)$
	trlcoabs.h	$⊢ H = LHyp (K)$
	trlcoabs.t	$⊢ T = LTrn (K) (W)$
	trlcoabs.r	$⊢ R = trL (K) (W)$
Assertion	trlcoabs2N	$⊢ ((K \in HL \land W \in H) \land (F \in T \land G \in T) \land (P \in A \land \neg P \underset{˙}{\leq} W)) \to F (P) \underset{˙}{\lor} R (G \circ F^{-1}) = F (P) \underset{˙}{\lor} G (P)$

Proof

Step	Hyp	Ref	Expression
1		trlcoabs.l	$⊢ \underset{˙}{\leq} = \leq_{K}$
2		trlcoabs.j	$⊢ \underset{˙}{\lor} = join (K)$
3		trlcoabs.a	$⊢ A = Atoms (K)$
4		trlcoabs.h	$⊢ H = LHyp (K)$
5		trlcoabs.t	$⊢ T = LTrn (K) (W)$
6		trlcoabs.r	$⊢ R = trL (K) (W)$
7		simp1	$⊢ ((K \in HL \land W \in H) \land (F \in T \land G \in T) \land (P \in A \land \neg P \underset{˙}{\leq} W)) \to (K \in HL \land W \in H)$
8		simp2r	$⊢ ((K \in HL \land W \in H) \land (F \in T \land G \in T) \land (P \in A \land \neg P \underset{˙}{\leq} W)) \to G \in T$
9		simp2l	$⊢ ((K \in HL \land W \in H) \land (F \in T \land G \in T) \land (P \in A \land \neg P \underset{˙}{\leq} W)) \to F \in T$
10	4 5	ltrncnv	$⊢ ((K \in HL \land W \in H) \land F \in T) \to F^{-1} \in T$
11	7 9 10	syl2anc	$⊢ ((K \in HL \land W \in H) \land (F \in T \land G \in T) \land (P \in A \land \neg P \underset{˙}{\leq} W)) \to F^{-1} \in T$
12	4 5	ltrnco	$⊢ ((K \in HL \land W \in H) \land G \in T \land F^{-1} \in T) \to G \circ F^{-1} \in T$
13	7 8 11 12	syl3anc	$⊢ ((K \in HL \land W \in H) \land (F \in T \land G \in T) \land (P \in A \land \neg P \underset{˙}{\leq} W)) \to G \circ F^{-1} \in T$
14	1 3 4 5	ltrnel	$⊢ ((K \in HL \land W \in H) \land F \in T \land (P \in A \land \neg P \underset{˙}{\leq} W)) \to (F (P) \in A \land \neg F (P) \underset{˙}{\leq} W)$
15	14	3adant2r	$⊢ ((K \in HL \land W \in H) \land (F \in T \land G \in T) \land (P \in A \land \neg P \underset{˙}{\leq} W)) \to (F (P) \in A \land \neg F (P) \underset{˙}{\leq} W)$
16		eqid	$⊢ meet (K) = meet (K)$
17	1 2 16 3 4 5 6	trlval2	$⊢ ((K \in HL \land W \in H) \land G \circ F^{-1} \in T \land (F (P) \in A \land \neg F (P) \underset{˙}{\leq} W)) \to R (G \circ F^{-1}) = (F (P) \underset{˙}{\lor} (G \circ F^{-1}) (F (P))) meet (K) W$
18	7 13 15 17	syl3anc	$⊢ ((K \in HL \land W \in H) \land (F \in T \land G \in T) \land (P \in A \land \neg P \underset{˙}{\leq} W)) \to R (G \circ F^{-1}) = (F (P) \underset{˙}{\lor} (G \circ F^{-1}) (F (P))) meet (K) W$
19	18	oveq2d	$⊢ ((K \in HL \land W \in H) \land (F \in T \land G \in T) \land (P \in A \land \neg P \underset{˙}{\leq} W)) \to F (P) \underset{˙}{\lor} R (G \circ F^{-1}) = F (P) \underset{˙}{\lor} ((F (P) \underset{˙}{\lor} (G \circ F^{-1}) (F (P))) meet (K) W)$
20		simp1l	$⊢ ((K \in HL \land W \in H) \land (F \in T \land G \in T) \land (P \in A \land \neg P \underset{˙}{\leq} W)) \to K \in HL$
21		simp3l	$⊢ ((K \in HL \land W \in H) \land (F \in T \land G \in T) \land (P \in A \land \neg P \underset{˙}{\leq} W)) \to P \in A$
22	1 3 4 5	ltrnat	$⊢ ((K \in HL \land W \in H) \land F \in T \land P \in A) \to F (P) \in A$
23	7 9 21 22	syl3anc	$⊢ ((K \in HL \land W \in H) \land (F \in T \land G \in T) \land (P \in A \land \neg P \underset{˙}{\leq} W)) \to F (P) \in A$
24	1 3 4 5	ltrnat	$⊢ ((K \in HL \land W \in H) \land G \circ F^{-1} \in T \land F (P) \in A) \to (G \circ F^{-1}) (F (P)) \in A$
25	7 13 23 24	syl3anc	$⊢ ((K \in HL \land W \in H) \land (F \in T \land G \in T) \land (P \in A \land \neg P \underset{˙}{\leq} W)) \to (G \circ F^{-1}) (F (P)) \in A$
26		eqid	$⊢ {Base}_{K} = {Base}_{K}$
27	26 2 3	hlatjcl	$⊢ (K \in HL \land F (P) \in A \land (G \circ F^{-1}) (F (P)) \in A) \to F (P) \underset{˙}{\lor} (G \circ F^{-1}) (F (P)) \in {Base}_{K}$
28	20 23 25 27	syl3anc	$⊢ ((K \in HL \land W \in H) \land (F \in T \land G \in T) \land (P \in A \land \neg P \underset{˙}{\leq} W)) \to F (P) \underset{˙}{\lor} (G \circ F^{-1}) (F (P)) \in {Base}_{K}$
29		simp1r	$⊢ ((K \in HL \land W \in H) \land (F \in T \land G \in T) \land (P \in A \land \neg P \underset{˙}{\leq} W)) \to W \in H$
30	26 4	lhpbase	$⊢ W \in H \to W \in {Base}_{K}$
31	29 30	syl	$⊢ ((K \in HL \land W \in H) \land (F \in T \land G \in T) \land (P \in A \land \neg P \underset{˙}{\leq} W)) \to W \in {Base}_{K}$
32	1 2 3	hlatlej1	$⊢ (K \in HL \land F (P) \in A \land (G \circ F^{-1}) (F (P)) \in A) \to F (P) \underset{˙}{\leq} (F (P) \underset{˙}{\lor} (G \circ F^{-1}) (F (P)))$
33	20 23 25 32	syl3anc	$⊢ ((K \in HL \land W \in H) \land (F \in T \land G \in T) \land (P \in A \land \neg P \underset{˙}{\leq} W)) \to F (P) \underset{˙}{\leq} (F (P) \underset{˙}{\lor} (G \circ F^{-1}) (F (P)))$
34	26 1 2 16 3	atmod3i1	$⊢ (K \in HL \land (F (P) \in A \land F (P) \underset{˙}{\lor} (G \circ F^{-1}) (F (P)) \in {Base}_{K} \land W \in {Base}_{K}) \land F (P) \underset{˙}{\leq} (F (P) \underset{˙}{\lor} (G \circ F^{-1}) (F (P)))) \to F (P) \underset{˙}{\lor} ((F (P) \underset{˙}{\lor} (G \circ F^{-1}) (F (P))) meet (K) W) = (F (P) \underset{˙}{\lor} (G \circ F^{-1}) (F (P))) meet (K) (F (P) \underset{˙}{\lor} W)$
35	20 23 28 31 33 34	syl131anc	$⊢ ((K \in HL \land W \in H) \land (F \in T \land G \in T) \land (P \in A \land \neg P \underset{˙}{\leq} W)) \to F (P) \underset{˙}{\lor} ((F (P) \underset{˙}{\lor} (G \circ F^{-1}) (F (P))) meet (K) W) = (F (P) \underset{˙}{\lor} (G \circ F^{-1}) (F (P))) meet (K) (F (P) \underset{˙}{\lor} W)$
36	1 3 4 5	ltrncoval	$⊢ ((K \in HL \land W \in H) \land (G \circ F^{-1} \in T \land F \in T) \land P \in A) \to ((G \circ F^{-1}) \circ F) (P) = (G \circ F^{-1}) (F (P))$
37	7 13 9 21 36	syl121anc	$⊢ ((K \in HL \land W \in H) \land (F \in T \land G \in T) \land (P \in A \land \neg P \underset{˙}{\leq} W)) \to ((G \circ F^{-1}) \circ F) (P) = (G \circ F^{-1}) (F (P))$
38		coass	$⊢ (G \circ F^{-1}) \circ F = G \circ (F^{-1} \circ F)$
39	26 4 5	ltrn1o	$⊢ ((K \in HL \land W \in H) \land F \in T) \to F : {Base}_{K} \underset{1-1 onto}{⟶} {Base}_{K}$
40	7 9 39	syl2anc	$⊢ ((K \in HL \land W \in H) \land (F \in T \land G \in T) \land (P \in A \land \neg P \underset{˙}{\leq} W)) \to F : {Base}_{K} \underset{1-1 onto}{⟶} {Base}_{K}$
41		f1ococnv1	$⊢ F : {Base}_{K} \underset{1-1 onto}{⟶} {Base}_{K} \to F^{-1} \circ F = {I ↾}_{{Base}_{K}}$
42	40 41	syl	$⊢ ((K \in HL \land W \in H) \land (F \in T \land G \in T) \land (P \in A \land \neg P \underset{˙}{\leq} W)) \to F^{-1} \circ F = {I ↾}_{{Base}_{K}}$
43	42	coeq2d	$⊢ ((K \in HL \land W \in H) \land (F \in T \land G \in T) \land (P \in A \land \neg P \underset{˙}{\leq} W)) \to G \circ (F^{-1} \circ F) = G \circ ({I ↾}_{{Base}_{K}})$
44	26 4 5	ltrn1o	$⊢ ((K \in HL \land W \in H) \land G \in T) \to G : {Base}_{K} \underset{1-1 onto}{⟶} {Base}_{K}$
45	7 8 44	syl2anc	$⊢ ((K \in HL \land W \in H) \land (F \in T \land G \in T) \land (P \in A \land \neg P \underset{˙}{\leq} W)) \to G : {Base}_{K} \underset{1-1 onto}{⟶} {Base}_{K}$
46		f1of	$⊢ G : {Base}_{K} \underset{1-1 onto}{⟶} {Base}_{K} \to G : {Base}_{K} ⟶ {Base}_{K}$
47		fcoi1	$⊢ G : {Base}_{K} ⟶ {Base}_{K} \to G \circ ({I ↾}_{{Base}_{K}}) = G$
48	45 46 47	3syl	$⊢ ((K \in HL \land W \in H) \land (F \in T \land G \in T) \land (P \in A \land \neg P \underset{˙}{\leq} W)) \to G \circ ({I ↾}_{{Base}_{K}}) = G$
49	43 48	eqtrd	$⊢ ((K \in HL \land W \in H) \land (F \in T \land G \in T) \land (P \in A \land \neg P \underset{˙}{\leq} W)) \to G \circ (F^{-1} \circ F) = G$
50	38 49	syl5eq	$⊢ ((K \in HL \land W \in H) \land (F \in T \land G \in T) \land (P \in A \land \neg P \underset{˙}{\leq} W)) \to (G \circ F^{-1}) \circ F = G$
51	50	fveq1d	$⊢ ((K \in HL \land W \in H) \land (F \in T \land G \in T) \land (P \in A \land \neg P \underset{˙}{\leq} W)) \to ((G \circ F^{-1}) \circ F) (P) = G (P)$
52	37 51	eqtr3d	$⊢ ((K \in HL \land W \in H) \land (F \in T \land G \in T) \land (P \in A \land \neg P \underset{˙}{\leq} W)) \to (G \circ F^{-1}) (F (P)) = G (P)$
53	52	oveq2d	$⊢ ((K \in HL \land W \in H) \land (F \in T \land G \in T) \land (P \in A \land \neg P \underset{˙}{\leq} W)) \to F (P) \underset{˙}{\lor} (G \circ F^{-1}) (F (P)) = F (P) \underset{˙}{\lor} G (P)$
54		eqid	$⊢ 1. (K) = 1. (K)$
55	1 2 54 3 4	lhpjat2	$⊢ ((K \in HL \land W \in H) \land (F (P) \in A \land \neg F (P) \underset{˙}{\leq} W)) \to F (P) \underset{˙}{\lor} W = 1. (K)$
56	7 15 55	syl2anc	$⊢ ((K \in HL \land W \in H) \land (F \in T \land G \in T) \land (P \in A \land \neg P \underset{˙}{\leq} W)) \to F (P) \underset{˙}{\lor} W = 1. (K)$
57	53 56	oveq12d	$⊢ ((K \in HL \land W \in H) \land (F \in T \land G \in T) \land (P \in A \land \neg P \underset{˙}{\leq} W)) \to (F (P) \underset{˙}{\lor} (G \circ F^{-1}) (F (P))) meet (K) (F (P) \underset{˙}{\lor} W) = (F (P) \underset{˙}{\lor} G (P)) meet (K) 1. (K)$
58		hlol	$⊢ K \in HL \to K \in OL$
59	20 58	syl	$⊢ ((K \in HL \land W \in H) \land (F \in T \land G \in T) \land (P \in A \land \neg P \underset{˙}{\leq} W)) \to K \in OL$
60	1 3 4 5	ltrnat	$⊢ ((K \in HL \land W \in H) \land G \in T \land P \in A) \to G (P) \in A$
61	7 8 21 60	syl3anc	$⊢ ((K \in HL \land W \in H) \land (F \in T \land G \in T) \land (P \in A \land \neg P \underset{˙}{\leq} W)) \to G (P) \in A$
62	26 2 3	hlatjcl	$⊢ (K \in HL \land F (P) \in A \land G (P) \in A) \to F (P) \underset{˙}{\lor} G (P) \in {Base}_{K}$
63	20 23 61 62	syl3anc	$⊢ ((K \in HL \land W \in H) \land (F \in T \land G \in T) \land (P \in A \land \neg P \underset{˙}{\leq} W)) \to F (P) \underset{˙}{\lor} G (P) \in {Base}_{K}$
64	26 16 54	olm11	$⊢ (K \in OL \land F (P) \underset{˙}{\lor} G (P) \in {Base}_{K}) \to (F (P) \underset{˙}{\lor} G (P)) meet (K) 1. (K) = F (P) \underset{˙}{\lor} G (P)$
65	59 63 64	syl2anc	$⊢ ((K \in HL \land W \in H) \land (F \in T \land G \in T) \land (P \in A \land \neg P \underset{˙}{\leq} W)) \to (F (P) \underset{˙}{\lor} G (P)) meet (K) 1. (K) = F (P) \underset{˙}{\lor} G (P)$
66	57 65	eqtrd	$⊢ ((K \in HL \land W \in H) \land (F \in T \land G \in T) \land (P \in A \land \neg P \underset{˙}{\leq} W)) \to (F (P) \underset{˙}{\lor} (G \circ F^{-1}) (F (P))) meet (K) (F (P) \underset{˙}{\lor} W) = F (P) \underset{˙}{\lor} G (P)$
67	19 35 66	3eqtrd	$⊢ ((K \in HL \land W \in H) \land (F \in T \land G \in T) \land (P \in A \land \neg P \underset{˙}{\leq} W)) \to F (P) \underset{˙}{\lor} R (G \circ F^{-1}) = F (P) \underset{˙}{\lor} G (P)$

Metamath Proof Explorer

Theorem trlcoabs2N

Proof