tendopltp

Description: Trace-preserving property of endomorphism sum operation P , based on Theorems trlco . Part of remark in Crawley p. 118, 2nd line, "it is clear from the second part of G (our trlco ) that Delta is a subring of E." (In our development, we will bypass their E and go directly to their Delta, whose base set is our ( TEndoK )W .) (Contributed by NM, 9-Jun-2013)

	Ref	Expression
Hypotheses	tendopl.h	$⊢ H = LHyp (K)$
	tendopl.t	$⊢ T = LTrn (K) (W)$
	tendopl.e	$⊢ E = TEndo (K) (W)$
	tendopl.p	$⊢ P = (s \in E, t \in E ⟼ (f \in T ⟼ s (f) \circ t (f)))$
	tendopltp.l	$⊢ \underset{˙}{\leq} = \leq_{K}$
	tendopltp.r	$⊢ R = trL (K) (W)$
Assertion	tendopltp	$⊢ ((K \in HL \land W \in H) \land (U \in E \land V \in E) \land F \in T) \to R ((U P V) (F)) \underset{˙}{\leq} R (F)$

Proof

Step	Hyp	Ref	Expression
1		tendopl.h	$⊢ H = LHyp (K)$
2		tendopl.t	$⊢ T = LTrn (K) (W)$
3		tendopl.e	$⊢ E = TEndo (K) (W)$
4		tendopl.p	$⊢ P = (s \in E, t \in E ⟼ (f \in T ⟼ s (f) \circ t (f)))$
5		tendopltp.l	$⊢ \underset{˙}{\leq} = \leq_{K}$
6		tendopltp.r	$⊢ R = trL (K) (W)$
7		eqid	$⊢ {Base}_{K} = {Base}_{K}$
8		simp1l	$⊢ ((K \in HL \land W \in H) \land (U \in E \land V \in E) \land F \in T) \to K \in HL$
9	8	hllatd	$⊢ ((K \in HL \land W \in H) \land (U \in E \land V \in E) \land F \in T) \to K \in Lat$
10		simp1	$⊢ ((K \in HL \land W \in H) \land (U \in E \land V \in E) \land F \in T) \to (K \in HL \land W \in H)$
11	1 2 3 4	tendoplcl2	$⊢ ((K \in HL \land W \in H) \land (U \in E \land V \in E) \land F \in T) \to (U P V) (F) \in T$
12	7 1 2 6	trlcl	$⊢ ((K \in HL \land W \in H) \land (U P V) (F) \in T) \to R ((U P V) (F)) \in {Base}_{K}$
13	10 11 12	syl2anc	$⊢ ((K \in HL \land W \in H) \land (U \in E \land V \in E) \land F \in T) \to R ((U P V) (F)) \in {Base}_{K}$
14	1 2 3	tendocl	$⊢ ((K \in HL \land W \in H) \land U \in E \land F \in T) \to U (F) \in T$
15	14	3adant2r	$⊢ ((K \in HL \land W \in H) \land (U \in E \land V \in E) \land F \in T) \to U (F) \in T$
16	7 1 2 6	trlcl	$⊢ ((K \in HL \land W \in H) \land U (F) \in T) \to R (U (F)) \in {Base}_{K}$
17	10 15 16	syl2anc	$⊢ ((K \in HL \land W \in H) \land (U \in E \land V \in E) \land F \in T) \to R (U (F)) \in {Base}_{K}$
18	1 2 3	tendocl	$⊢ ((K \in HL \land W \in H) \land V \in E \land F \in T) \to V (F) \in T$
19	18	3adant2l	$⊢ ((K \in HL \land W \in H) \land (U \in E \land V \in E) \land F \in T) \to V (F) \in T$
20	7 1 2 6	trlcl	$⊢ ((K \in HL \land W \in H) \land V (F) \in T) \to R (V (F)) \in {Base}_{K}$
21	10 19 20	syl2anc	$⊢ ((K \in HL \land W \in H) \land (U \in E \land V \in E) \land F \in T) \to R (V (F)) \in {Base}_{K}$
22		eqid	$⊢ join (K) = join (K)$
23	7 22	latjcl	$⊢ (K \in Lat \land R (U (F)) \in {Base}_{K} \land R (V (F)) \in {Base}_{K}) \to R (U (F)) join (K) R (V (F)) \in {Base}_{K}$
24	9 17 21 23	syl3anc	$⊢ ((K \in HL \land W \in H) \land (U \in E \land V \in E) \land F \in T) \to R (U (F)) join (K) R (V (F)) \in {Base}_{K}$
25		simp3	$⊢ ((K \in HL \land W \in H) \land (U \in E \land V \in E) \land F \in T) \to F \in T$
26	7 1 2 6	trlcl	$⊢ ((K \in HL \land W \in H) \land F \in T) \to R (F) \in {Base}_{K}$
27	10 25 26	syl2anc	$⊢ ((K \in HL \land W \in H) \land (U \in E \land V \in E) \land F \in T) \to R (F) \in {Base}_{K}$
28		simp2l	$⊢ ((K \in HL \land W \in H) \land (U \in E \land V \in E) \land F \in T) \to U \in E$
29		simp2r	$⊢ ((K \in HL \land W \in H) \land (U \in E \land V \in E) \land F \in T) \to V \in E$
30	4 2	tendopl2	$⊢ (U \in E \land V \in E \land F \in T) \to (U P V) (F) = U (F) \circ V (F)$
31	28 29 25 30	syl3anc	$⊢ ((K \in HL \land W \in H) \land (U \in E \land V \in E) \land F \in T) \to (U P V) (F) = U (F) \circ V (F)$
32	31	fveq2d	$⊢ ((K \in HL \land W \in H) \land (U \in E \land V \in E) \land F \in T) \to R ((U P V) (F)) = R (U (F) \circ V (F))$
33	5 22 1 2 6	trlco	$⊢ ((K \in HL \land W \in H) \land U (F) \in T \land V (F) \in T) \to R (U (F) \circ V (F)) \underset{˙}{\leq} (R (U (F)) join (K) R (V (F)))$
34	10 15 19 33	syl3anc	$⊢ ((K \in HL \land W \in H) \land (U \in E \land V \in E) \land F \in T) \to R (U (F) \circ V (F)) \underset{˙}{\leq} (R (U (F)) join (K) R (V (F)))$
35	32 34	eqbrtrd	$⊢ ((K \in HL \land W \in H) \land (U \in E \land V \in E) \land F \in T) \to R ((U P V) (F)) \underset{˙}{\leq} (R (U (F)) join (K) R (V (F)))$
36	5 1 2 6 3	tendotp	$⊢ ((K \in HL \land W \in H) \land U \in E \land F \in T) \to R (U (F)) \underset{˙}{\leq} R (F)$
37	36	3adant2r	$⊢ ((K \in HL \land W \in H) \land (U \in E \land V \in E) \land F \in T) \to R (U (F)) \underset{˙}{\leq} R (F)$
38	5 1 2 6 3	tendotp	$⊢ ((K \in HL \land W \in H) \land V \in E \land F \in T) \to R (V (F)) \underset{˙}{\leq} R (F)$
39	38	3adant2l	$⊢ ((K \in HL \land W \in H) \land (U \in E \land V \in E) \land F \in T) \to R (V (F)) \underset{˙}{\leq} R (F)$
40	7 5 22	latjle12	$⊢ (K \in Lat \land (R (U (F)) \in {Base}_{K} \land R (V (F)) \in {Base}_{K} \land R (F) \in {Base}_{K})) \to ((R (U (F)) \underset{˙}{\leq} R (F) \land R (V (F)) \underset{˙}{\leq} R (F)) \leftrightarrow (R (U (F)) join (K) R (V (F))) \underset{˙}{\leq} R (F))$
41	9 17 21 27 40	syl13anc	$⊢ ((K \in HL \land W \in H) \land (U \in E \land V \in E) \land F \in T) \to ((R (U (F)) \underset{˙}{\leq} R (F) \land R (V (F)) \underset{˙}{\leq} R (F)) \leftrightarrow (R (U (F)) join (K) R (V (F))) \underset{˙}{\leq} R (F))$
42	37 39 41	mpbi2and	$⊢ ((K \in HL \land W \in H) \land (U \in E \land V \in E) \land F \in T) \to (R (U (F)) join (K) R (V (F))) \underset{˙}{\leq} R (F)$
43	7 5 9 13 24 27 35 42	lattrd	$⊢ ((K \in HL \land W \in H) \land (U \in E \land V \in E) \land F \in T) \to R ((U P V) (F)) \underset{˙}{\leq} R (F)$

Metamath Proof Explorer

Theorem tendopltp

Proof