trljco2

Description: Trace joined with trace of composition. (Contributed by NM, 16-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	trljco2	$⊢ ((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 (G) \underset{˙}{\lor} R (F \circ 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		simp1l	$⊢ ((K \in HL \land W \in H) \land F \in T \land G \in T) \to K \in HL$
6	5	hllatd	$⊢ ((K \in HL \land W \in H) \land F \in T \land G \in T) \to K \in Lat$
7		eqid	$⊢ {Base}_{K} = {Base}_{K}$
8	7 2 3 4	trlcl	$⊢ ((K \in HL \land W \in H) \land F \in T) \to R (F) \in {Base}_{K}$
9	8	3adant3	$⊢ ((K \in HL \land W \in H) \land F \in T \land G \in T) \to R (F) \in {Base}_{K}$
10	7 2 3 4	trlcl	$⊢ ((K \in HL \land W \in H) \land G \in T) \to R (G) \in {Base}_{K}$
11	10	3adant2	$⊢ ((K \in HL \land W \in H) \land F \in T \land G \in T) \to R (G) \in {Base}_{K}$
12	7 1	latjcom	$⊢ (K \in Lat \land R (F) \in {Base}_{K} \land R (G) \in {Base}_{K}) \to R (F) \underset{˙}{\lor} R (G) = R (G) \underset{˙}{\lor} R (F)$
13	6 9 11 12	syl3anc	$⊢ ((K \in HL \land W \in H) \land F \in T \land G \in T) \to R (F) \underset{˙}{\lor} R (G) = R (G) \underset{˙}{\lor} R (F)$
14	1 2 3 4	trljco	$⊢ ((K \in HL \land W \in H) \land G \in T \land F \in T) \to R (G) \underset{˙}{\lor} R (G \circ F) = R (G) \underset{˙}{\lor} R (F)$
15	14	3com23	$⊢ ((K \in HL \land W \in H) \land F \in T \land G \in T) \to R (G) \underset{˙}{\lor} R (G \circ F) = R (G) \underset{˙}{\lor} R (F)$
16	13 15	eqtr4d	$⊢ ((K \in HL \land W \in H) \land F \in T \land G \in T) \to R (F) \underset{˙}{\lor} R (G) = R (G) \underset{˙}{\lor} R (G \circ F)$
17	1 2 3 4	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)$
18	2 3	ltrncom	$⊢ ((K \in HL \land W \in H) \land F \in T \land G \in T) \to F \circ G = G \circ F$
19	18	fveq2d	$⊢ ((K \in HL \land W \in H) \land F \in T \land G \in T) \to R (F \circ G) = R (G \circ F)$
20	19	oveq2d	$⊢ ((K \in HL \land W \in H) \land F \in T \land G \in T) \to R (G) \underset{˙}{\lor} R (F \circ G) = R (G) \underset{˙}{\lor} R (G \circ F)$
21	16 17 20	3eqtr4d	$⊢ ((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 (G) \underset{˙}{\lor} R (F \circ G)$

Metamath Proof Explorer

Theorem trljco2

Proof