diblss

Description: The value of partial isomorphism B is a subspace of partial vector space H. TODO: use dib* specific theorems instead of dia* ones to shorten proof? (Contributed by NM, 11-Feb-2014)

	Ref	Expression
Hypotheses	diblss.b	$⊢ B = {Base}_{K}$
	diblss.l	$⊢ \underset{˙}{\leq} = \leq_{K}$
	diblss.h	$⊢ H = LHyp (K)$
	diblss.u	$⊢ U = DVecH (K) (W)$
	diblss.i	$⊢ I = DIsoB (K) (W)$
	diblss.s	$⊢ S = LSubSp (U)$
Assertion	diblss	$⊢ ((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		diblss.b	$⊢ B = {Base}_{K}$
2		diblss.l	$⊢ \underset{˙}{\leq} = \leq_{K}$
3		diblss.h	$⊢ H = LHyp (K)$
4		diblss.u	$⊢ U = DVecH (K) (W)$
5		diblss.i	$⊢ I = DIsoB (K) (W)$
6		diblss.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	dvhbase	$⊢ (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 8 4 15	dvhvbase	$⊢ (K \in HL \land W \in H) \to {Base}_{U} = LTrn (K) (W) \times TEndo (K) (W)$
17	16	eqcomd	$⊢ (K \in HL \land W \in H) \to LTrn (K) (W) \times TEndo (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) \times TEndo (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 5 4 15	dibss	$⊢ ((K \in HL \land W \in H) \land (X \in B \land X \underset{˙}{\leq} W)) \to I (X) \subseteq {Base}_{U}$
23	22 18	sseqtrrd	$⊢ ((K \in HL \land W \in H) \land (X \in B \land X \underset{˙}{\leq} W)) \to I (X) \subseteq LTrn (K) (W) \times TEndo (K) (W)$
24	1 2 3 5	dibn0	$⊢ ((K \in HL \land W \in H) \land (X \in B \land X \underset{˙}{\leq} W)) \to I (X) \neq \emptyset$
25		fvex	$⊢ x (1^{st} (a)) \in V$
26		vex	$⊢ x \in V$
27		fvex	$⊢ 2^{nd} (a) \in V$
28	26 27	coex	$⊢ x \circ 2^{nd} (a) \in V$
29	25 28	op1st	$⊢ 1^{st} (⟨x (1^{st} (a)), x \circ 2^{nd} (a)⟩) = x (1^{st} (a))$
30	29	coeq1i	$⊢ 1^{st} (⟨x (1^{st} (a)), x \circ 2^{nd} (a)⟩) \circ 1^{st} (b) = x (1^{st} (a)) \circ 1^{st} (b)$
31		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)$
32		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)$
33		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)$
34		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)$
35	1 2 3 14 5	dibelval1st1	$⊢ ((K \in HL \land W \in H) \land (X \in B \land X \underset{˙}{\leq} W) \land a \in I (X)) \to 1^{st} (a) \in LTrn (K) (W)$
36	31 33 34 35	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 1^{st} (a) \in LTrn (K) (W)$
37	3 14 8	tendocl	$⊢ ((K \in HL \land W \in H) \land x \in TEndo (K) (W) \land 1^{st} (a) \in LTrn (K) (W)) \to x (1^{st} (a)) \in LTrn (K) (W)$
38	31 32 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 x (1^{st} (a)) \in LTrn (K) (W)$
39		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)$
40	1 2 3 14 5	dibelval1st1	$⊢ ((K \in HL \land W \in H) \land (X \in B \land X \underset{˙}{\leq} W) \land b \in I (X)) \to 1^{st} (b) \in LTrn (K) (W)$
41	31 33 39 40	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 1^{st} (b) \in LTrn (K) (W)$
42	3 14	ltrnco	$⊢ ((K \in HL \land W \in H) \land x (1^{st} (a)) \in LTrn (K) (W) \land 1^{st} (b) \in LTrn (K) (W)) \to x (1^{st} (a)) \circ 1^{st} (b) \in LTrn (K) (W)$
43	31 38 41 42	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 (1^{st} (a)) \circ 1^{st} (b) \in LTrn (K) (W)$
44		simplll	$⊢ (((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$
45	44	hllatd	$⊢ (((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$
46		eqid	$⊢ trL (K) (W) = trL (K) (W)$
47	1 3 14 46	trlcl	$⊢ ((K \in HL \land W \in H) \land x (1^{st} (a)) \circ 1^{st} (b) \in LTrn (K) (W)) \to trL (K) (W) (x (1^{st} (a)) \circ 1^{st} (b)) \in B$
48	31 43 47	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 (1^{st} (a)) \circ 1^{st} (b)) \in B$
49	1 3 14 46	trlcl	$⊢ ((K \in HL \land W \in H) \land x (1^{st} (a)) \in LTrn (K) (W)) \to trL (K) (W) (x (1^{st} (a))) \in B$
50	31 38 49	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 (1^{st} (a))) \in B$
51	1 3 14 46	trlcl	$⊢ ((K \in HL \land W \in H) \land 1^{st} (b) \in LTrn (K) (W)) \to trL (K) (W) (1^{st} (b)) \in B$
52	31 41 51	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) (1^{st} (b)) \in B$
53		eqid	$⊢ join (K) = join (K)$
54	1 53	latjcl	$⊢ (K \in Lat \land trL (K) (W) (x (1^{st} (a))) \in B \land trL (K) (W) (1^{st} (b)) \in B) \to trL (K) (W) (x (1^{st} (a))) join (K) trL (K) (W) (1^{st} (b)) \in B$
55	45 50 52 54	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 (1^{st} (a))) join (K) trL (K) (W) (1^{st} (b)) \in B$
56		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$
57	2 53 3 14 46	trlco	$⊢ ((K \in HL \land W \in H) \land x (1^{st} (a)) \in LTrn (K) (W) \land 1^{st} (b) \in LTrn (K) (W)) \to trL (K) (W) (x (1^{st} (a)) \circ 1^{st} (b)) \underset{˙}{\leq} (trL (K) (W) (x (1^{st} (a))) join (K) trL (K) (W) (1^{st} (b)))$
58	31 38 41 57	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 (1^{st} (a)) \circ 1^{st} (b)) \underset{˙}{\leq} (trL (K) (W) (x (1^{st} (a))) join (K) trL (K) (W) (1^{st} (b)))$
59	1 3 14 46	trlcl	$⊢ ((K \in HL \land W \in H) \land 1^{st} (a) \in LTrn (K) (W)) \to trL (K) (W) (1^{st} (a)) \in B$
60	31 36 59	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) (1^{st} (a)) \in B$
61	2 3 14 46 8	tendotp	$⊢ ((K \in HL \land W \in H) \land x \in TEndo (K) (W) \land 1^{st} (a) \in LTrn (K) (W)) \to trL (K) (W) (x (1^{st} (a))) \underset{˙}{\leq} trL (K) (W) (1^{st} (a))$
62	31 32 36 61	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 (1^{st} (a))) \underset{˙}{\leq} trL (K) (W) (1^{st} (a))$
63		eqid	$⊢ DIsoA (K) (W) = DIsoA (K) (W)$
64	1 2 3 63 5	dibelval1st	$⊢ ((K \in HL \land W \in H) \land (X \in B \land X \underset{˙}{\leq} W) \land a \in I (X)) \to 1^{st} (a) \in DIsoA (K) (W) (X)$
65	31 33 34 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 1^{st} (a) \in DIsoA (K) (W) (X)$
66	1 2 3 14 46 63	diatrl	$⊢ ((K \in HL \land W \in H) \land (X \in B \land X \underset{˙}{\leq} W) \land 1^{st} (a) \in DIsoA (K) (W) (X)) \to trL (K) (W) (1^{st} (a)) \underset{˙}{\leq} X$
67	31 33 65 66	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) (1^{st} (a)) \underset{˙}{\leq} X$
68	1 2 45 50 60 56 62 67	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 (1^{st} (a))) \underset{˙}{\leq} X$
69	1 2 3 63 5	dibelval1st	$⊢ ((K \in HL \land W \in H) \land (X \in B \land X \underset{˙}{\leq} W) \land b \in I (X)) \to 1^{st} (b) \in DIsoA (K) (W) (X)$
70	31 33 39 69	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 1^{st} (b) \in DIsoA (K) (W) (X)$
71	1 2 3 14 46 63	diatrl	$⊢ ((K \in HL \land W \in H) \land (X \in B \land X \underset{˙}{\leq} W) \land 1^{st} (b) \in DIsoA (K) (W) (X)) \to trL (K) (W) (1^{st} (b)) \underset{˙}{\leq} X$
72	31 33 70 71	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) (1^{st} (b)) \underset{˙}{\leq} X$
73	1 2 53	latjle12	$⊢ (K \in Lat \land (trL (K) (W) (x (1^{st} (a))) \in B \land trL (K) (W) (1^{st} (b)) \in B \land X \in B)) \to ((trL (K) (W) (x (1^{st} (a))) \underset{˙}{\leq} X \land trL (K) (W) (1^{st} (b)) \underset{˙}{\leq} X) \leftrightarrow (trL (K) (W) (x (1^{st} (a))) join (K) trL (K) (W) (1^{st} (b))) \underset{˙}{\leq} X)$
74	45 50 52 56 73	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 (1^{st} (a))) \underset{˙}{\leq} X \land trL (K) (W) (1^{st} (b)) \underset{˙}{\leq} X) \leftrightarrow (trL (K) (W) (x (1^{st} (a))) join (K) trL (K) (W) (1^{st} (b))) \underset{˙}{\leq} X)$
75	68 72 74	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 (1^{st} (a))) join (K) trL (K) (W) (1^{st} (b))) \underset{˙}{\leq} X$
76	1 2 45 48 55 56 58 75	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 (1^{st} (a)) \circ 1^{st} (b)) \underset{˙}{\leq} X$
77	1 2 3 14 46 63	diaelval	$⊢ ((K \in HL \land W \in H) \land (X \in B \land X \underset{˙}{\leq} W)) \to (x (1^{st} (a)) \circ 1^{st} (b) \in DIsoA (K) (W) (X) \leftrightarrow (x (1^{st} (a)) \circ 1^{st} (b) \in LTrn (K) (W) \land trL (K) (W) (x (1^{st} (a)) \circ 1^{st} (b)) \underset{˙}{\leq} X))$
78	77	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 (1^{st} (a)) \circ 1^{st} (b) \in DIsoA (K) (W) (X) \leftrightarrow (x (1^{st} (a)) \circ 1^{st} (b) \in LTrn (K) (W) \land trL (K) (W) (x (1^{st} (a)) \circ 1^{st} (b)) \underset{˙}{\leq} X))$
79	43 76 78	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 (1^{st} (a)) \circ 1^{st} (b) \in DIsoA (K) (W) (X)$
80	30 79	eqeltrid	$⊢ (((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 1^{st} (⟨x (1^{st} (a)), x \circ 2^{nd} (a)⟩) \circ 1^{st} (b) \in DIsoA (K) (W) (X)$
81		eqid	$⊢ (s \in TEndo (K) (W), t \in TEndo (K) (W) ⟼ (h \in LTrn (K) (W) ⟼ s (h) \circ t (h))) = (s \in TEndo (K) (W), t \in TEndo (K) (W) ⟼ (h \in LTrn (K) (W) ⟼ s (h) \circ t (h)))$
82		eqid	$⊢ +_{Scalar (U)} = +_{Scalar (U)}$
83	3 14 8 4 9 81 82	dvhfplusr	$⊢ (K \in HL \land W \in H) \to +_{Scalar (U)} = (s \in TEndo (K) (W), t \in TEndo (K) (W) ⟼ (h \in LTrn (K) (W) ⟼ s (h) \circ t (h)))$
84	83	ad2antrr	$⊢ (((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 +_{Scalar (U)} = (s \in TEndo (K) (W), t \in TEndo (K) (W) ⟼ (h \in LTrn (K) (W) ⟼ s (h) \circ t (h)))$
85	25 28	op2nd	$⊢ 2^{nd} (⟨x (1^{st} (a)), x \circ 2^{nd} (a)⟩) = x \circ 2^{nd} (a)$
86		eqid	$⊢ (h \in LTrn (K) (W) ⟼ {I ↾}_{B}) = (h \in LTrn (K) (W) ⟼ {I ↾}_{B})$
87	1 2 3 14 86 5	dibelval2nd	$⊢ ((K \in HL \land W \in H) \land (X \in B \land X \underset{˙}{\leq} W) \land a \in I (X)) \to 2^{nd} (a) = (h \in LTrn (K) (W) ⟼ {I ↾}_{B})$
88	31 33 34 87	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 2^{nd} (a) = (h \in LTrn (K) (W) ⟼ {I ↾}_{B})$
89	88	coeq2d	$⊢ (((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 \circ 2^{nd} (a) = x \circ (h \in LTrn (K) (W) ⟼ {I ↾}_{B})$
90	1 3 14 8 86	tendo0mulr	$⊢ ((K \in HL \land W \in H) \land x \in TEndo (K) (W)) \to x \circ (h \in LTrn (K) (W) ⟼ {I ↾}_{B}) = (h \in LTrn (K) (W) ⟼ {I ↾}_{B})$
91	31 32 90	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 x \circ (h \in LTrn (K) (W) ⟼ {I ↾}_{B}) = (h \in LTrn (K) (W) ⟼ {I ↾}_{B})$
92	89 91	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 \circ 2^{nd} (a) = (h \in LTrn (K) (W) ⟼ {I ↾}_{B})$
93	85 92	syl5eq	$⊢ (((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 2^{nd} (⟨x (1^{st} (a)), x \circ 2^{nd} (a)⟩) = (h \in LTrn (K) (W) ⟼ {I ↾}_{B})$
94	1 2 3 14 86 5	dibelval2nd	$⊢ ((K \in HL \land W \in H) \land (X \in B \land X \underset{˙}{\leq} W) \land b \in I (X)) \to 2^{nd} (b) = (h \in LTrn (K) (W) ⟼ {I ↾}_{B})$
95	31 33 39 94	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 2^{nd} (b) = (h \in LTrn (K) (W) ⟼ {I ↾}_{B})$
96	84 93 95	oveq123d	$⊢ (((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 2^{nd} (⟨x (1^{st} (a)), x \circ 2^{nd} (a)⟩) +_{Scalar (U)} 2^{nd} (b) = (h \in LTrn (K) (W) ⟼ {I ↾}_{B}) (s \in TEndo (K) (W), t \in TEndo (K) (W) ⟼ (h \in LTrn (K) (W) ⟼ s (h) \circ t (h))) (h \in LTrn (K) (W) ⟼ {I ↾}_{B})$
97		simpllr	$⊢ (((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 W \in H$
98	1 3 14 8 86	tendo0cl	$⊢ (K \in HL \land W \in H) \to (h \in LTrn (K) (W) ⟼ {I ↾}_{B}) \in TEndo (K) (W)$
99	98	ad2antrr	$⊢ (((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 (h \in LTrn (K) (W) ⟼ {I ↾}_{B}) \in TEndo (K) (W)$
100	1 3 14 8 86 81	tendo0pl	$⊢ ((K \in HL \land W \in H) \land (h \in LTrn (K) (W) ⟼ {I ↾}_{B}) \in TEndo (K) (W)) \to (h \in LTrn (K) (W) ⟼ {I ↾}_{B}) (s \in TEndo (K) (W), t \in TEndo (K) (W) ⟼ (h \in LTrn (K) (W) ⟼ s (h) \circ t (h))) (h \in LTrn (K) (W) ⟼ {I ↾}_{B}) = (h \in LTrn (K) (W) ⟼ {I ↾}_{B})$
101	44 97 99 100	syl21anc	$⊢ (((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 (h \in LTrn (K) (W) ⟼ {I ↾}_{B}) (s \in TEndo (K) (W), t \in TEndo (K) (W) ⟼ (h \in LTrn (K) (W) ⟼ s (h) \circ t (h))) (h \in LTrn (K) (W) ⟼ {I ↾}_{B}) = (h \in LTrn (K) (W) ⟼ {I ↾}_{B})$
102	96 101	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 2^{nd} (⟨x (1^{st} (a)), x \circ 2^{nd} (a)⟩) +_{Scalar (U)} 2^{nd} (b) = (h \in LTrn (K) (W) ⟼ {I ↾}_{B})$
103		ovex	$⊢ 2^{nd} (⟨x (1^{st} (a)), x \circ 2^{nd} (a)⟩) +_{Scalar (U)} 2^{nd} (b) \in V$
104	103	elsn	$⊢ 2^{nd} (⟨x (1^{st} (a)), x \circ 2^{nd} (a)⟩) +_{Scalar (U)} 2^{nd} (b) \in \{(h \in LTrn (K) (W) ⟼ {I ↾}_{B})\} \leftrightarrow 2^{nd} (⟨x (1^{st} (a)), x \circ 2^{nd} (a)⟩) +_{Scalar (U)} 2^{nd} (b) = (h \in LTrn (K) (W) ⟼ {I ↾}_{B})$
105	102 104	sylibr	$⊢ (((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 2^{nd} (⟨x (1^{st} (a)), x \circ 2^{nd} (a)⟩) +_{Scalar (U)} 2^{nd} (b) \in \{(h \in LTrn (K) (W) ⟼ {I ↾}_{B})\}$
106		opelxpi	$⊢ (1^{st} (⟨x (1^{st} (a)), x \circ 2^{nd} (a)⟩) \circ 1^{st} (b) \in DIsoA (K) (W) (X) \land 2^{nd} (⟨x (1^{st} (a)), x \circ 2^{nd} (a)⟩) +_{Scalar (U)} 2^{nd} (b) \in \{(h \in LTrn (K) (W) ⟼ {I ↾}_{B})\}) \to ⟨1^{st} (⟨x (1^{st} (a)), x \circ 2^{nd} (a)⟩) \circ 1^{st} (b), 2^{nd} (⟨x (1^{st} (a)), x \circ 2^{nd} (a)⟩) +_{Scalar (U)} 2^{nd} (b)⟩ \in (DIsoA (K) (W) (X) \times \{(h \in LTrn (K) (W) ⟼ {I ↾}_{B})\})$
107	80 105 106	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 ⟨1^{st} (⟨x (1^{st} (a)), x \circ 2^{nd} (a)⟩) \circ 1^{st} (b), 2^{nd} (⟨x (1^{st} (a)), x \circ 2^{nd} (a)⟩) +_{Scalar (U)} 2^{nd} (b)⟩ \in (DIsoA (K) (W) (X) \times \{(h \in LTrn (K) (W) ⟼ {I ↾}_{B})\})$
108	23	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 I (X) \subseteq LTrn (K) (W) \times TEndo (K) (W)$
109	108 34	sseldd	$⊢ (((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) \times TEndo (K) (W))$
110		eqid	$⊢ \cdot_{U} = \cdot_{U}$
111	3 14 8 4 110	dvhvsca	$⊢ ((K \in HL \land W \in H) \land (x \in TEndo (K) (W) \land a \in (LTrn (K) (W) \times TEndo (K) (W)))) \to x \cdot_{U} a = ⟨x (1^{st} (a)), x \circ 2^{nd} (a)⟩$
112	31 32 109 111	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 (1^{st} (a)), x \circ 2^{nd} (a)⟩$
113	112	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 (1^{st} (a)), x \circ 2^{nd} (a)⟩ +_{U} b$
114	88 99	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 2^{nd} (a) \in TEndo (K) (W)$
115	3 8	tendococl	$⊢ ((K \in HL \land W \in H) \land x \in TEndo (K) (W) \land 2^{nd} (a) \in TEndo (K) (W)) \to x \circ 2^{nd} (a) \in TEndo (K) (W)$
116	31 32 114 115	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 \circ 2^{nd} (a) \in TEndo (K) (W)$
117		opelxpi	$⊢ (x (1^{st} (a)) \in LTrn (K) (W) \land x \circ 2^{nd} (a) \in TEndo (K) (W)) \to ⟨x (1^{st} (a)), x \circ 2^{nd} (a)⟩ \in (LTrn (K) (W) \times TEndo (K) (W))$
118	38 116 117	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 ⟨x (1^{st} (a)), x \circ 2^{nd} (a)⟩ \in (LTrn (K) (W) \times TEndo (K) (W))$
119	108 39	sseldd	$⊢ (((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) \times TEndo (K) (W))$
120		eqid	$⊢ +_{U} = +_{U}$
121	3 14 8 4 9 120 82	dvhvadd	$⊢ ((K \in HL \land W \in H) \land (⟨x (1^{st} (a)), x \circ 2^{nd} (a)⟩ \in (LTrn (K) (W) \times TEndo (K) (W)) \land b \in (LTrn (K) (W) \times TEndo (K) (W)))) \to ⟨x (1^{st} (a)), x \circ 2^{nd} (a)⟩ +_{U} b = ⟨1^{st} (⟨x (1^{st} (a)), x \circ 2^{nd} (a)⟩) \circ 1^{st} (b), 2^{nd} (⟨x (1^{st} (a)), x \circ 2^{nd} (a)⟩) +_{Scalar (U)} 2^{nd} (b)⟩$
122	31 118 119 121	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 (1^{st} (a)), x \circ 2^{nd} (a)⟩ +_{U} b = ⟨1^{st} (⟨x (1^{st} (a)), x \circ 2^{nd} (a)⟩) \circ 1^{st} (b), 2^{nd} (⟨x (1^{st} (a)), x \circ 2^{nd} (a)⟩) +_{Scalar (U)} 2^{nd} (b)⟩$
123	113 122	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 = ⟨1^{st} (⟨x (1^{st} (a)), x \circ 2^{nd} (a)⟩) \circ 1^{st} (b), 2^{nd} (⟨x (1^{st} (a)), x \circ 2^{nd} (a)⟩) +_{Scalar (U)} 2^{nd} (b)⟩$
124	1 2 3 14 86 63 5	dibval2	$⊢ ((K \in HL \land W \in H) \land (X \in B \land X \underset{˙}{\leq} W)) \to I (X) = DIsoA (K) (W) (X) \times \{(h \in LTrn (K) (W) ⟼ {I ↾}_{B})\}$
125	124	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 I (X) = DIsoA (K) (W) (X) \times \{(h \in LTrn (K) (W) ⟼ {I ↾}_{B})\}$
126	107 123 125	3eltr4d	$⊢ (((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)$
127	7 13 18 19 20 21 23 24 126	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 diblss

Proof