dialss

Description: The value of partial isomorphism A is a subspace of partial vector space A. Part of Lemma M of Crawley p. 120 line 26. (Contributed by NM, 17-Jan-2014) (Revised by Mario Carneiro, 23-Jun-2014)

	Ref	Expression
Hypotheses	dialss.b	$⊢ B = {Base}_{K}$
	dialss.l	$⊢ \underset{˙}{\leq} = \leq_{K}$
	dialss.h	$⊢ H = LHyp (K)$
	dialss.u	$⊢ U = DVecA (K) (W)$
	dialss.i	$⊢ I = DIsoA (K) (W)$
	dialss.s	$⊢ S = LSubSp (U)$
Assertion	dialss	$⊢ ((K \in HL \land W \in H) \land (X \in B \land X \underset{˙}{\leq} W)) \to I (X) \in S$

Proof

Step	Hyp	Ref	Expression
1		dialss.b	$⊢ B = {Base}_{K}$
2		dialss.l	$⊢ \underset{˙}{\leq} = \leq_{K}$
3		dialss.h	$⊢ H = LHyp (K)$
4		dialss.u	$⊢ U = DVecA (K) (W)$
5		dialss.i	$⊢ I = DIsoA (K) (W)$
6		dialss.s	$⊢ S = LSubSp (U)$
7		eqidd	$⊢ ((K \in HL \land W \in H) \land (X \in B \land X \underset{˙}{\leq} W)) \to Scalar (U) = Scalar (U)$
8		eqid	$⊢ TEndo (K) (W) = TEndo (K) (W)$
9		eqid	$⊢ Scalar (U) = Scalar (U)$
10		eqid	$⊢ {Base}_{Scalar (U)} = {Base}_{Scalar (U)}$
11	3 8 4 9 10	dvabase	$⊢ (K \in HL \land W \in H) \to {Base}_{Scalar (U)} = TEndo (K) (W)$
12	11	eqcomd	$⊢ (K \in HL \land W \in H) \to TEndo (K) (W) = {Base}_{Scalar (U)}$
13	12	adantr	$⊢ ((K \in HL \land W \in H) \land (X \in B \land X \underset{˙}{\leq} W)) \to TEndo (K) (W) = {Base}_{Scalar (U)}$
14		eqid	$⊢ LTrn (K) (W) = LTrn (K) (W)$
15		eqid	$⊢ {Base}_{U} = {Base}_{U}$
16	3 14 4 15	dvavbase	$⊢ (K \in HL \land W \in H) \to {Base}_{U} = LTrn (K) (W)$
17	16	eqcomd	$⊢ (K \in HL \land W \in H) \to LTrn (K) (W) = {Base}_{U}$
18	17	adantr	$⊢ ((K \in HL \land W \in H) \land (X \in B \land X \underset{˙}{\leq} W)) \to LTrn (K) (W) = {Base}_{U}$
19		eqidd	$⊢ ((K \in HL \land W \in H) \land (X \in B \land X \underset{˙}{\leq} W)) \to +_{U} = +_{U}$
20		eqidd	$⊢ ((K \in HL \land W \in H) \land (X \in B \land X \underset{˙}{\leq} W)) \to \cdot_{U} = \cdot_{U}$
21	6	a1i	$⊢ ((K \in HL \land W \in H) \land (X \in B \land X \underset{˙}{\leq} W)) \to S = LSubSp (U)$
22	1 2 3 14 5	diass	$⊢ ((K \in HL \land W \in H) \land (X \in B \land X \underset{˙}{\leq} W)) \to I (X) \subseteq LTrn (K) (W)$
23	1 2 3 5	dian0	$⊢ ((K \in HL \land W \in H) \land (X \in B \land X \underset{˙}{\leq} W)) \to I (X) \neq \emptyset$
24		simpll	$⊢ (((K \in HL \land W \in H) \land (X \in B \land X \underset{˙}{\leq} W)) \land (x \in TEndo (K) (W) \land a \in I (X) \land b \in I (X))) \to (K \in HL \land W \in H)$
25		simpr1	$⊢ (((K \in HL \land W \in H) \land (X \in B \land X \underset{˙}{\leq} W)) \land (x \in TEndo (K) (W) \land a \in I (X) \land b \in I (X))) \to x \in TEndo (K) (W)$
26		simplr	$⊢ (((K \in HL \land W \in H) \land (X \in B \land X \underset{˙}{\leq} W)) \land (x \in TEndo (K) (W) \land a \in I (X) \land b \in I (X))) \to (X \in B \land X \underset{˙}{\leq} W)$
27		simpr2	$⊢ (((K \in HL \land W \in H) \land (X \in B \land X \underset{˙}{\leq} W)) \land (x \in TEndo (K) (W) \land a \in I (X) \land b \in I (X))) \to a \in I (X)$
28	1 2 3 14 5	diael	$⊢ ((K \in HL \land W \in H) \land (X \in B \land X \underset{˙}{\leq} W) \land a \in I (X)) \to a \in LTrn (K) (W)$
29	24 26 27 28	syl3anc	$⊢ (((K \in HL \land W \in H) \land (X \in B \land X \underset{˙}{\leq} W)) \land (x \in TEndo (K) (W) \land a \in I (X) \land b \in I (X))) \to a \in LTrn (K) (W)$
30		eqid	$⊢ \cdot_{U} = \cdot_{U}$
31	3 14 8 4 30	dvavsca	$⊢ ((K \in HL \land W \in H) \land (x \in TEndo (K) (W) \land a \in LTrn (K) (W))) \to x \cdot_{U} a = x (a)$
32	24 25 29 31	syl12anc	$⊢ (((K \in HL \land W \in H) \land (X \in B \land X \underset{˙}{\leq} W)) \land (x \in TEndo (K) (W) \land a \in I (X) \land b \in I (X))) \to x \cdot_{U} a = x (a)$
33	32	oveq1d	$⊢ (((K \in HL \land W \in H) \land (X \in B \land X \underset{˙}{\leq} W)) \land (x \in TEndo (K) (W) \land a \in I (X) \land b \in I (X))) \to (x \cdot_{U} a) +_{U} b = x (a) +_{U} b$
34	3 14 8	tendocl	$⊢ ((K \in HL \land W \in H) \land x \in TEndo (K) (W) \land a \in LTrn (K) (W)) \to x (a) \in LTrn (K) (W)$
35	24 25 29 34	syl3anc	$⊢ (((K \in HL \land W \in H) \land (X \in B \land X \underset{˙}{\leq} W)) \land (x \in TEndo (K) (W) \land a \in I (X) \land b \in I (X))) \to x (a) \in LTrn (K) (W)$
36		simpr3	$⊢ (((K \in HL \land W \in H) \land (X \in B \land X \underset{˙}{\leq} W)) \land (x \in TEndo (K) (W) \land a \in I (X) \land b \in I (X))) \to b \in I (X)$
37	1 2 3 14 5	diael	$⊢ ((K \in HL \land W \in H) \land (X \in B \land X \underset{˙}{\leq} W) \land b \in I (X)) \to b \in LTrn (K) (W)$
38	24 26 36 37	syl3anc	$⊢ (((K \in HL \land W \in H) \land (X \in B \land X \underset{˙}{\leq} W)) \land (x \in TEndo (K) (W) \land a \in I (X) \land b \in I (X))) \to b \in LTrn (K) (W)$
39		eqid	$⊢ +_{U} = +_{U}$
40	3 14 4 39	dvavadd	$⊢ ((K \in HL \land W \in H) \land (x (a) \in LTrn (K) (W) \land b \in LTrn (K) (W))) \to x (a) +_{U} b = x (a) \circ b$
41	24 35 38 40	syl12anc	$⊢ (((K \in HL \land W \in H) \land (X \in B \land X \underset{˙}{\leq} W)) \land (x \in TEndo (K) (W) \land a \in I (X) \land b \in I (X))) \to x (a) +_{U} b = x (a) \circ b$
42	33 41	eqtrd	$⊢ (((K \in HL \land W \in H) \land (X \in B \land X \underset{˙}{\leq} W)) \land (x \in TEndo (K) (W) \land a \in I (X) \land b \in I (X))) \to (x \cdot_{U} a) +_{U} b = x (a) \circ b$
43	3 14	ltrnco	$⊢ ((K \in HL \land W \in H) \land x (a) \in LTrn (K) (W) \land b \in LTrn (K) (W)) \to x (a) \circ b \in LTrn (K) (W)$
44	24 35 38 43	syl3anc	$⊢ (((K \in HL \land W \in H) \land (X \in B \land X \underset{˙}{\leq} W)) \land (x \in TEndo (K) (W) \land a \in I (X) \land b \in I (X))) \to x (a) \circ b \in LTrn (K) (W)$
45		hllat	$⊢ K \in HL \to K \in Lat$
46	45	ad3antrrr	$⊢ (((K \in HL \land W \in H) \land (X \in B \land X \underset{˙}{\leq} W)) \land (x \in TEndo (K) (W) \land a \in I (X) \land b \in I (X))) \to K \in Lat$
47		eqid	$⊢ trL (K) (W) = trL (K) (W)$
48	1 3 14 47	trlcl	$⊢ ((K \in HL \land W \in H) \land x (a) \circ b \in LTrn (K) (W)) \to trL (K) (W) (x (a) \circ b) \in B$
49	24 44 48	syl2anc	$⊢ (((K \in HL \land W \in H) \land (X \in B \land X \underset{˙}{\leq} W)) \land (x \in TEndo (K) (W) \land a \in I (X) \land b \in I (X))) \to trL (K) (W) (x (a) \circ b) \in B$
50	1 3 14 47	trlcl	$⊢ ((K \in HL \land W \in H) \land x (a) \in LTrn (K) (W)) \to trL (K) (W) (x (a)) \in B$
51	24 35 50	syl2anc	$⊢ (((K \in HL \land W \in H) \land (X \in B \land X \underset{˙}{\leq} W)) \land (x \in TEndo (K) (W) \land a \in I (X) \land b \in I (X))) \to trL (K) (W) (x (a)) \in B$
52	1 3 14 47	trlcl	$⊢ ((K \in HL \land W \in H) \land b \in LTrn (K) (W)) \to trL (K) (W) (b) \in B$
53	24 38 52	syl2anc	$⊢ (((K \in HL \land W \in H) \land (X \in B \land X \underset{˙}{\leq} W)) \land (x \in TEndo (K) (W) \land a \in I (X) \land b \in I (X))) \to trL (K) (W) (b) \in B$
54		eqid	$⊢ join (K) = join (K)$
55	1 54	latjcl	$⊢ (K \in Lat \land trL (K) (W) (x (a)) \in B \land trL (K) (W) (b) \in B) \to trL (K) (W) (x (a)) join (K) trL (K) (W) (b) \in B$
56	46 51 53 55	syl3anc	$⊢ (((K \in HL \land W \in H) \land (X \in B \land X \underset{˙}{\leq} W)) \land (x \in TEndo (K) (W) \land a \in I (X) \land b \in I (X))) \to trL (K) (W) (x (a)) join (K) trL (K) (W) (b) \in B$
57		simplrl	$⊢ (((K \in HL \land W \in H) \land (X \in B \land X \underset{˙}{\leq} W)) \land (x \in TEndo (K) (W) \land a \in I (X) \land b \in I (X))) \to X \in B$
58	2 54 3 14 47	trlco	$⊢ ((K \in HL \land W \in H) \land x (a) \in LTrn (K) (W) \land b \in LTrn (K) (W)) \to trL (K) (W) (x (a) \circ b) \underset{˙}{\leq} (trL (K) (W) (x (a)) join (K) trL (K) (W) (b))$
59	24 35 38 58	syl3anc	$⊢ (((K \in HL \land W \in H) \land (X \in B \land X \underset{˙}{\leq} W)) \land (x \in TEndo (K) (W) \land a \in I (X) \land b \in I (X))) \to trL (K) (W) (x (a) \circ b) \underset{˙}{\leq} (trL (K) (W) (x (a)) join (K) trL (K) (W) (b))$
60	1 3 14 47	trlcl	$⊢ ((K \in HL \land W \in H) \land a \in LTrn (K) (W)) \to trL (K) (W) (a) \in B$
61	24 29 60	syl2anc	$⊢ (((K \in HL \land W \in H) \land (X \in B \land X \underset{˙}{\leq} W)) \land (x \in TEndo (K) (W) \land a \in I (X) \land b \in I (X))) \to trL (K) (W) (a) \in B$
62	2 3 14 47 8	tendotp	$⊢ ((K \in HL \land W \in H) \land x \in TEndo (K) (W) \land a \in LTrn (K) (W)) \to trL (K) (W) (x (a)) \underset{˙}{\leq} trL (K) (W) (a)$
63	24 25 29 62	syl3anc	$⊢ (((K \in HL \land W \in H) \land (X \in B \land X \underset{˙}{\leq} W)) \land (x \in TEndo (K) (W) \land a \in I (X) \land b \in I (X))) \to trL (K) (W) (x (a)) \underset{˙}{\leq} trL (K) (W) (a)$
64	1 2 3 14 47 5	diatrl	$⊢ ((K \in HL \land W \in H) \land (X \in B \land X \underset{˙}{\leq} W) \land a \in I (X)) \to trL (K) (W) (a) \underset{˙}{\leq} X$
65	24 26 27 64	syl3anc	$⊢ (((K \in HL \land W \in H) \land (X \in B \land X \underset{˙}{\leq} W)) \land (x \in TEndo (K) (W) \land a \in I (X) \land b \in I (X))) \to trL (K) (W) (a) \underset{˙}{\leq} X$
66	1 2 46 51 61 57 63 65	lattrd	$⊢ (((K \in HL \land W \in H) \land (X \in B \land X \underset{˙}{\leq} W)) \land (x \in TEndo (K) (W) \land a \in I (X) \land b \in I (X))) \to trL (K) (W) (x (a)) \underset{˙}{\leq} X$
67	1 2 3 14 47 5	diatrl	$⊢ ((K \in HL \land W \in H) \land (X \in B \land X \underset{˙}{\leq} W) \land b \in I (X)) \to trL (K) (W) (b) \underset{˙}{\leq} X$
68	24 26 36 67	syl3anc	$⊢ (((K \in HL \land W \in H) \land (X \in B \land X \underset{˙}{\leq} W)) \land (x \in TEndo (K) (W) \land a \in I (X) \land b \in I (X))) \to trL (K) (W) (b) \underset{˙}{\leq} X$
69	1 2 54	latjle12	$⊢ (K \in Lat \land (trL (K) (W) (x (a)) \in B \land trL (K) (W) (b) \in B \land X \in B)) \to ((trL (K) (W) (x (a)) \underset{˙}{\leq} X \land trL (K) (W) (b) \underset{˙}{\leq} X) \leftrightarrow (trL (K) (W) (x (a)) join (K) trL (K) (W) (b)) \underset{˙}{\leq} X)$
70	46 51 53 57 69	syl13anc	$⊢ (((K \in HL \land W \in H) \land (X \in B \land X \underset{˙}{\leq} W)) \land (x \in TEndo (K) (W) \land a \in I (X) \land b \in I (X))) \to ((trL (K) (W) (x (a)) \underset{˙}{\leq} X \land trL (K) (W) (b) \underset{˙}{\leq} X) \leftrightarrow (trL (K) (W) (x (a)) join (K) trL (K) (W) (b)) \underset{˙}{\leq} X)$
71	66 68 70	mpbi2and	$⊢ (((K \in HL \land W \in H) \land (X \in B \land X \underset{˙}{\leq} W)) \land (x \in TEndo (K) (W) \land a \in I (X) \land b \in I (X))) \to (trL (K) (W) (x (a)) join (K) trL (K) (W) (b)) \underset{˙}{\leq} X$
72	1 2 46 49 56 57 59 71	lattrd	$⊢ (((K \in HL \land W \in H) \land (X \in B \land X \underset{˙}{\leq} W)) \land (x \in TEndo (K) (W) \land a \in I (X) \land b \in I (X))) \to trL (K) (W) (x (a) \circ b) \underset{˙}{\leq} X$
73	1 2 3 14 47 5	diaelval	$⊢ ((K \in HL \land W \in H) \land (X \in B \land X \underset{˙}{\leq} W)) \to (x (a) \circ b \in I (X) \leftrightarrow (x (a) \circ b \in LTrn (K) (W) \land trL (K) (W) (x (a) \circ b) \underset{˙}{\leq} X))$
74	73	adantr	$⊢ (((K \in HL \land W \in H) \land (X \in B \land X \underset{˙}{\leq} W)) \land (x \in TEndo (K) (W) \land a \in I (X) \land b \in I (X))) \to (x (a) \circ b \in I (X) \leftrightarrow (x (a) \circ b \in LTrn (K) (W) \land trL (K) (W) (x (a) \circ b) \underset{˙}{\leq} X))$
75	44 72 74	mpbir2and	$⊢ (((K \in HL \land W \in H) \land (X \in B \land X \underset{˙}{\leq} W)) \land (x \in TEndo (K) (W) \land a \in I (X) \land b \in I (X))) \to x (a) \circ b \in I (X)$
76	42 75	eqeltrd	$⊢ (((K \in HL \land W \in H) \land (X \in B \land X \underset{˙}{\leq} W)) \land (x \in TEndo (K) (W) \land a \in I (X) \land b \in I (X))) \to (x \cdot_{U} a) +_{U} b \in I (X)$
77	7 13 18 19 20 21 22 23 76	islssd	$⊢ ((K \in HL \land W \in H) \land (X \in B \land X \underset{˙}{\leq} W)) \to I (X) \in S$

Metamath Proof Explorer

Theorem dialss

Proof