trljco

Description: Trace joined with trace of composition. (Contributed by NM, 15-Jun-2013)

	Ref	Expression
Hypotheses	trljco.j	$⊢ \underset{˙}{\lor} = join (K)$
	trljco.h	$⊢ H = LHyp (K)$
	trljco.t	$⊢ T = LTrn (K) (W)$
	trljco.r	$⊢ R = trL (K) (W)$
Assertion	trljco	$⊢ ((K \in HL \land W \in H) \land F \in T \land G \in T) \to R (F) \underset{˙}{\lor} R (F \circ G) = R (F) \underset{˙}{\lor} R (G)$

Proof

Step	Hyp	Ref	Expression
1		trljco.j	$⊢ \underset{˙}{\lor} = join (K)$
2		trljco.h	$⊢ H = LHyp (K)$
3		trljco.t	$⊢ T = LTrn (K) (W)$
4		trljco.r	$⊢ R = trL (K) (W)$
5		coeq1	$⊢ F = {I ↾}_{{Base}_{K}} \to F \circ G = ({I ↾}_{{Base}_{K}}) \circ G$
6		eqid	$⊢ {Base}_{K} = {Base}_{K}$
7	6 2 3	ltrn1o	$⊢ ((K \in HL \land W \in H) \land G \in T) \to G : {Base}_{K} \underset{1-1 onto}{⟶} {Base}_{K}$
8	7	3adant2	$⊢ ((K \in HL \land W \in H) \land F \in T \land G \in T) \to G : {Base}_{K} \underset{1-1 onto}{⟶} {Base}_{K}$
9		f1of	$⊢ G : {Base}_{K} \underset{1-1 onto}{⟶} {Base}_{K} \to G : {Base}_{K} ⟶ {Base}_{K}$
10		fcoi2	$⊢ G : {Base}_{K} ⟶ {Base}_{K} \to ({I ↾}_{{Base}_{K}}) \circ G = G$
11	8 9 10	3syl	$⊢ ((K \in HL \land W \in H) \land F \in T \land G \in T) \to ({I ↾}_{{Base}_{K}}) \circ G = G$
12	5 11	sylan9eqr	$⊢ (((K \in HL \land W \in H) \land F \in T \land G \in T) \land F = {I ↾}_{{Base}_{K}}) \to F \circ G = G$
13	12	fveq2d	$⊢ (((K \in HL \land W \in H) \land F \in T \land G \in T) \land F = {I ↾}_{{Base}_{K}}) \to R (F \circ G) = R (G)$
14	13	oveq2d	$⊢ (((K \in HL \land W \in H) \land F \in T \land G \in T) \land F = {I ↾}_{{Base}_{K}}) \to R (F) \underset{˙}{\lor} R (F \circ G) = R (F) \underset{˙}{\lor} R (G)$
15		simp1l	$⊢ ((K \in HL \land W \in H) \land F \in T \land G \in T) \to K \in HL$
16	15	hllatd	$⊢ ((K \in HL \land W \in H) \land F \in T \land G \in T) \to K \in Lat$
17	6 2 3 4	trlcl	$⊢ ((K \in HL \land W \in H) \land F \in T) \to R (F) \in {Base}_{K}$
18	17	3adant3	$⊢ ((K \in HL \land W \in H) \land F \in T \land G \in T) \to R (F) \in {Base}_{K}$
19	6 1	latjidm	$⊢ (K \in Lat \land R (F) \in {Base}_{K}) \to R (F) \underset{˙}{\lor} R (F) = R (F)$
20	16 18 19	syl2anc	$⊢ ((K \in HL \land W \in H) \land F \in T \land G \in T) \to R (F) \underset{˙}{\lor} R (F) = R (F)$
21		hlol	$⊢ K \in HL \to K \in OL$
22	15 21	syl	$⊢ ((K \in HL \land W \in H) \land F \in T \land G \in T) \to K \in OL$
23		eqid	$⊢ 0. (K) = 0. (K)$
24	6 1 23	olj01	$⊢ (K \in OL \land R (F) \in {Base}_{K}) \to R (F) \underset{˙}{\lor} 0. (K) = R (F)$
25	22 18 24	syl2anc	$⊢ ((K \in HL \land W \in H) \land F \in T \land G \in T) \to R (F) \underset{˙}{\lor} 0. (K) = R (F)$
26	20 25	eqtr4d	$⊢ ((K \in HL \land W \in H) \land F \in T \land G \in T) \to R (F) \underset{˙}{\lor} R (F) = R (F) \underset{˙}{\lor} 0. (K)$
27	26	adantr	$⊢ (((K \in HL \land W \in H) \land F \in T \land G \in T) \land G = {I ↾}_{{Base}_{K}}) \to R (F) \underset{˙}{\lor} R (F) = R (F) \underset{˙}{\lor} 0. (K)$
28		coeq2	$⊢ G = {I ↾}_{{Base}_{K}} \to F \circ G = F \circ ({I ↾}_{{Base}_{K}})$
29	6 2 3	ltrn1o	$⊢ ((K \in HL \land W \in H) \land F \in T) \to F : {Base}_{K} \underset{1-1 onto}{⟶} {Base}_{K}$
30	29	3adant3	$⊢ ((K \in HL \land W \in H) \land F \in T \land G \in T) \to F : {Base}_{K} \underset{1-1 onto}{⟶} {Base}_{K}$
31		f1of	$⊢ F : {Base}_{K} \underset{1-1 onto}{⟶} {Base}_{K} \to F : {Base}_{K} ⟶ {Base}_{K}$
32		fcoi1	$⊢ F : {Base}_{K} ⟶ {Base}_{K} \to F \circ ({I ↾}_{{Base}_{K}}) = F$
33	30 31 32	3syl	$⊢ ((K \in HL \land W \in H) \land F \in T \land G \in T) \to F \circ ({I ↾}_{{Base}_{K}}) = F$
34	28 33	sylan9eqr	$⊢ (((K \in HL \land W \in H) \land F \in T \land G \in T) \land G = {I ↾}_{{Base}_{K}}) \to F \circ G = F$
35	34	fveq2d	$⊢ (((K \in HL \land W \in H) \land F \in T \land G \in T) \land G = {I ↾}_{{Base}_{K}}) \to R (F \circ G) = R (F)$
36	35	oveq2d	$⊢ (((K \in HL \land W \in H) \land F \in T \land G \in T) \land G = {I ↾}_{{Base}_{K}}) \to R (F) \underset{˙}{\lor} R (F \circ G) = R (F) \underset{˙}{\lor} R (F)$
37	6 23 2 3 4	trlid0b	$⊢ ((K \in HL \land W \in H) \land G \in T) \to (G = {I ↾}_{{Base}_{K}} \leftrightarrow R (G) = 0. (K))$
38	37	3adant2	$⊢ ((K \in HL \land W \in H) \land F \in T \land G \in T) \to (G = {I ↾}_{{Base}_{K}} \leftrightarrow R (G) = 0. (K))$
39	38	biimpa	$⊢ (((K \in HL \land W \in H) \land F \in T \land G \in T) \land G = {I ↾}_{{Base}_{K}}) \to R (G) = 0. (K)$
40	39	oveq2d	$⊢ (((K \in HL \land W \in H) \land F \in T \land G \in T) \land G = {I ↾}_{{Base}_{K}}) \to R (F) \underset{˙}{\lor} R (G) = R (F) \underset{˙}{\lor} 0. (K)$
41	27 36 40	3eqtr4d	$⊢ (((K \in HL \land W \in H) \land F \in T \land G \in T) \land G = {I ↾}_{{Base}_{K}}) \to R (F) \underset{˙}{\lor} R (F \circ G) = R (F) \underset{˙}{\lor} R (G)$
42		eqid	$⊢ \leq_{K} = \leq_{K}$
43	16	adantr	$⊢ (((K \in HL \land W \in H) \land F \in T \land G \in T) \land R (F) = R (G)) \to K \in Lat$
44		simp1	$⊢ ((K \in HL \land W \in H) \land F \in T \land G \in T) \to (K \in HL \land W \in H)$
45	2 3	ltrnco	$⊢ ((K \in HL \land W \in H) \land F \in T \land G \in T) \to F \circ G \in T$
46	6 2 3 4	trlcl	$⊢ ((K \in HL \land W \in H) \land F \circ G \in T) \to R (F \circ G) \in {Base}_{K}$
47	44 45 46	syl2anc	$⊢ ((K \in HL \land W \in H) \land F \in T \land G \in T) \to R (F \circ G) \in {Base}_{K}$
48	6 1	latjcl	$⊢ (K \in Lat \land R (F) \in {Base}_{K} \land R (F \circ G) \in {Base}_{K}) \to R (F) \underset{˙}{\lor} R (F \circ G) \in {Base}_{K}$
49	16 18 47 48	syl3anc	$⊢ ((K \in HL \land W \in H) \land F \in T \land G \in T) \to R (F) \underset{˙}{\lor} R (F \circ G) \in {Base}_{K}$
50	49	adantr	$⊢ (((K \in HL \land W \in H) \land F \in T \land G \in T) \land R (F) = R (G)) \to R (F) \underset{˙}{\lor} R (F \circ G) \in {Base}_{K}$
51	6 2 3 4	trlcl	$⊢ ((K \in HL \land W \in H) \land G \in T) \to R (G) \in {Base}_{K}$
52	51	3adant2	$⊢ ((K \in HL \land W \in H) \land F \in T \land G \in T) \to R (G) \in {Base}_{K}$
53	6 1	latjcl	$⊢ (K \in Lat \land R (F) \in {Base}_{K} \land R (G) \in {Base}_{K}) \to R (F) \underset{˙}{\lor} R (G) \in {Base}_{K}$
54	16 18 52 53	syl3anc	$⊢ ((K \in HL \land W \in H) \land F \in T \land G \in T) \to R (F) \underset{˙}{\lor} R (G) \in {Base}_{K}$
55	54	adantr	$⊢ (((K \in HL \land W \in H) \land F \in T \land G \in T) \land R (F) = R (G)) \to R (F) \underset{˙}{\lor} R (G) \in {Base}_{K}$
56	6 42 1	latlej1	$⊢ (K \in Lat \land R (F) \in {Base}_{K} \land R (G) \in {Base}_{K}) \to R (F) \leq_{K} (R (F) \underset{˙}{\lor} R (G))$
57	16 18 52 56	syl3anc	$⊢ ((K \in HL \land W \in H) \land F \in T \land G \in T) \to R (F) \leq_{K} (R (F) \underset{˙}{\lor} R (G))$
58	42 1 2 3 4	trlco	$⊢ ((K \in HL \land W \in H) \land F \in T \land G \in T) \to R (F \circ G) \leq_{K} (R (F) \underset{˙}{\lor} R (G))$
59	6 42 1	latjle12	$⊢ (K \in Lat \land (R (F) \in {Base}_{K} \land R (F \circ G) \in {Base}_{K} \land R (F) \underset{˙}{\lor} R (G) \in {Base}_{K})) \to ((R (F) \leq_{K} (R (F) \underset{˙}{\lor} R (G)) \land R (F \circ G) \leq_{K} (R (F) \underset{˙}{\lor} R (G))) \leftrightarrow (R (F) \underset{˙}{\lor} R (F \circ G)) \leq_{K} (R (F) \underset{˙}{\lor} R (G)))$
60	16 18 47 54 59	syl13anc	$⊢ ((K \in HL \land W \in H) \land F \in T \land G \in T) \to ((R (F) \leq_{K} (R (F) \underset{˙}{\lor} R (G)) \land R (F \circ G) \leq_{K} (R (F) \underset{˙}{\lor} R (G))) \leftrightarrow (R (F) \underset{˙}{\lor} R (F \circ G)) \leq_{K} (R (F) \underset{˙}{\lor} R (G)))$
61	57 58 60	mpbi2and	$⊢ ((K \in HL \land W \in H) \land F \in T \land G \in T) \to (R (F) \underset{˙}{\lor} R (F \circ G)) \leq_{K} (R (F) \underset{˙}{\lor} R (G))$
62	61	adantr	$⊢ (((K \in HL \land W \in H) \land F \in T \land G \in T) \land R (F) = R (G)) \to (R (F) \underset{˙}{\lor} R (F \circ G)) \leq_{K} (R (F) \underset{˙}{\lor} R (G))$
63		simpr	$⊢ (((K \in HL \land W \in H) \land F \in T \land G \in T) \land R (F) = R (G)) \to R (F) = R (G)$
64	63	oveq2d	$⊢ (((K \in HL \land W \in H) \land F \in T \land G \in T) \land R (F) = R (G)) \to R (F) \underset{˙}{\lor} R (F) = R (F) \underset{˙}{\lor} R (G)$
65	6 42 1	latlej1	$⊢ (K \in Lat \land R (F) \in {Base}_{K} \land R (F \circ G) \in {Base}_{K}) \to R (F) \leq_{K} (R (F) \underset{˙}{\lor} R (F \circ G))$
66	16 18 47 65	syl3anc	$⊢ ((K \in HL \land W \in H) \land F \in T \land G \in T) \to R (F) \leq_{K} (R (F) \underset{˙}{\lor} R (F \circ G))$
67	20 66	eqbrtrd	$⊢ ((K \in HL \land W \in H) \land F \in T \land G \in T) \to (R (F) \underset{˙}{\lor} R (F)) \leq_{K} (R (F) \underset{˙}{\lor} R (F \circ G))$
68	67	adantr	$⊢ (((K \in HL \land W \in H) \land F \in T \land G \in T) \land R (F) = R (G)) \to (R (F) \underset{˙}{\lor} R (F)) \leq_{K} (R (F) \underset{˙}{\lor} R (F \circ G))$
69	64 68	eqbrtrrd	$⊢ (((K \in HL \land W \in H) \land F \in T \land G \in T) \land R (F) = R (G)) \to (R (F) \underset{˙}{\lor} R (G)) \leq_{K} (R (F) \underset{˙}{\lor} R (F \circ G))$
70	6 42 43 50 55 62 69	latasymd	$⊢ (((K \in HL \land W \in H) \land F \in T \land G \in T) \land R (F) = R (G)) \to R (F) \underset{˙}{\lor} R (F \circ G) = R (F) \underset{˙}{\lor} R (G)$
71	61	adantr	$⊢ (((K \in HL \land W \in H) \land F \in T \land G \in T) \land (F \neq {I ↾}_{{Base}_{K}} \land G \neq {I ↾}_{{Base}_{K}} \land R (F) \neq R (G))) \to (R (F) \underset{˙}{\lor} R (F \circ G)) \leq_{K} (R (F) \underset{˙}{\lor} R (G))$
72		simpl1l	$⊢ (((K \in HL \land W \in H) \land F \in T \land G \in T) \land (F \neq {I ↾}_{{Base}_{K}} \land G \neq {I ↾}_{{Base}_{K}} \land R (F) \neq R (G))) \to K \in HL$
73		simpl1	$⊢ (((K \in HL \land W \in H) \land F \in T \land G \in T) \land (F \neq {I ↾}_{{Base}_{K}} \land G \neq {I ↾}_{{Base}_{K}} \land R (F) \neq R (G))) \to (K \in HL \land W \in H)$
74		simpl2	$⊢ (((K \in HL \land W \in H) \land F \in T \land G \in T) \land (F \neq {I ↾}_{{Base}_{K}} \land G \neq {I ↾}_{{Base}_{K}} \land R (F) \neq R (G))) \to F \in T$
75		simpr1	$⊢ (((K \in HL \land W \in H) \land F \in T \land G \in T) \land (F \neq {I ↾}_{{Base}_{K}} \land G \neq {I ↾}_{{Base}_{K}} \land R (F) \neq R (G))) \to F \neq {I ↾}_{{Base}_{K}}$
76		eqid	$⊢ Atoms (K) = Atoms (K)$
77	6 76 2 3 4	trlnidat	$⊢ ((K \in HL \land W \in H) \land F \in T \land F \neq {I ↾}_{{Base}_{K}}) \to R (F) \in Atoms (K)$
78	73 74 75 77	syl3anc	$⊢ (((K \in HL \land W \in H) \land F \in T \land G \in T) \land (F \neq {I ↾}_{{Base}_{K}} \land G \neq {I ↾}_{{Base}_{K}} \land R (F) \neq R (G))) \to R (F) \in Atoms (K)$
79		simpl3	$⊢ (((K \in HL \land W \in H) \land F \in T \land G \in T) \land (F \neq {I ↾}_{{Base}_{K}} \land G \neq {I ↾}_{{Base}_{K}} \land R (F) \neq R (G))) \to G \in T$
80	74 79	jca	$⊢ (((K \in HL \land W \in H) \land F \in T \land G \in T) \land (F \neq {I ↾}_{{Base}_{K}} \land G \neq {I ↾}_{{Base}_{K}} \land R (F) \neq R (G))) \to (F \in T \land G \in T)$
81		simpr3	$⊢ (((K \in HL \land W \in H) \land F \in T \land G \in T) \land (F \neq {I ↾}_{{Base}_{K}} \land G \neq {I ↾}_{{Base}_{K}} \land R (F) \neq R (G))) \to R (F) \neq R (G)$
82	76 2 3 4	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 Atoms (K)$
83	73 80 81 82	syl3anc	$⊢ (((K \in HL \land W \in H) \land F \in T \land G \in T) \land (F \neq {I ↾}_{{Base}_{K}} \land G \neq {I ↾}_{{Base}_{K}} \land R (F) \neq R (G))) \to R (F \circ G) \in Atoms (K)$
84		simpr2	$⊢ (((K \in HL \land W \in H) \land F \in T \land G \in T) \land (F \neq {I ↾}_{{Base}_{K}} \land G \neq {I ↾}_{{Base}_{K}} \land R (F) \neq R (G))) \to G \neq {I ↾}_{{Base}_{K}}$
85	6 2 3 4	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 ↾}_{{Base}_{K}})) \to R (F) \neq R (F \circ G)$
86	73 80 81 84 85	syl112anc	$⊢ (((K \in HL \land W \in H) \land F \in T \land G \in T) \land (F \neq {I ↾}_{{Base}_{K}} \land G \neq {I ↾}_{{Base}_{K}} \land R (F) \neq R (G))) \to R (F) \neq R (F \circ G)$
87	6 76 2 3 4	trlnidat	$⊢ ((K \in HL \land W \in H) \land G \in T \land G \neq {I ↾}_{{Base}_{K}}) \to R (G) \in Atoms (K)$
88	73 79 84 87	syl3anc	$⊢ (((K \in HL \land W \in H) \land F \in T \land G \in T) \land (F \neq {I ↾}_{{Base}_{K}} \land G \neq {I ↾}_{{Base}_{K}} \land R (F) \neq R (G))) \to R (G) \in Atoms (K)$
89	42 1 76	ps-1	$⊢ (K \in HL \land (R (F) \in Atoms (K) \land R (F \circ G) \in Atoms (K) \land R (F) \neq R (F \circ G)) \land (R (F) \in Atoms (K) \land R (G) \in Atoms (K))) \to ((R (F) \underset{˙}{\lor} R (F \circ G)) \leq_{K} (R (F) \underset{˙}{\lor} R (G)) \leftrightarrow R (F) \underset{˙}{\lor} R (F \circ G) = R (F) \underset{˙}{\lor} R (G))$
90	72 78 83 86 78 88 89	syl132anc	$⊢ (((K \in HL \land W \in H) \land F \in T \land G \in T) \land (F \neq {I ↾}_{{Base}_{K}} \land G \neq {I ↾}_{{Base}_{K}} \land R (F) \neq R (G))) \to ((R (F) \underset{˙}{\lor} R (F \circ G)) \leq_{K} (R (F) \underset{˙}{\lor} R (G)) \leftrightarrow R (F) \underset{˙}{\lor} R (F \circ G) = R (F) \underset{˙}{\lor} R (G))$
91	71 90	mpbid	$⊢ (((K \in HL \land W \in H) \land F \in T \land G \in T) \land (F \neq {I ↾}_{{Base}_{K}} \land G \neq {I ↾}_{{Base}_{K}} \land R (F) \neq R (G))) \to R (F) \underset{˙}{\lor} R (F \circ G) = R (F) \underset{˙}{\lor} R (G)$
92	14 41 70 91	pm2.61da3ne	$⊢ ((K \in HL \land W \in H) \land F \in T \land G \in T) \to R (F) \underset{˙}{\lor} R (F \circ G) = R (F) \underset{˙}{\lor} R (G)$

Metamath Proof Explorer

Theorem trljco

Proof