diclss

Description: The value of partial isomorphism C is a subspace of partial vector space H. (Contributed by NM, 16-Feb-2014)

	Ref	Expression
Hypotheses	diclss.l	$⊢ \underset{˙}{\leq} = \leq_{K}$
	diclss.a	$⊢ A = Atoms (K)$
	diclss.h	$⊢ H = LHyp (K)$
	diclss.u	$⊢ U = DVecH (K) (W)$
	diclss.i	$⊢ I = DIsoC (K) (W)$
	diclss.s	$⊢ S = LSubSp (U)$
Assertion	diclss	$⊢ ((K \in HL \land W \in H) \land (Q \in A \land \neg Q \underset{˙}{\leq} W)) \to I (Q) \in S$

Proof

Step	Hyp	Ref	Expression
1		diclss.l	$⊢ \underset{˙}{\leq} = \leq_{K}$
2		diclss.a	$⊢ A = Atoms (K)$
3		diclss.h	$⊢ H = LHyp (K)$
4		diclss.u	$⊢ U = DVecH (K) (W)$
5		diclss.i	$⊢ I = DIsoC (K) (W)$
6		diclss.s	$⊢ S = LSubSp (U)$
7		eqidd	$⊢ ((K \in HL \land W \in H) \land (Q \in A \land \neg Q \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 (Q \in A \land \neg Q \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 (Q \in A \land \neg Q \underset{˙}{\leq} W)) \to LTrn (K) (W) \times TEndo (K) (W) = {Base}_{U}$
19		eqidd	$⊢ ((K \in HL \land W \in H) \land (Q \in A \land \neg Q \underset{˙}{\leq} W)) \to +_{U} = +_{U}$
20		eqidd	$⊢ ((K \in HL \land W \in H) \land (Q \in A \land \neg Q \underset{˙}{\leq} W)) \to \cdot_{U} = \cdot_{U}$
21	6	a1i	$⊢ ((K \in HL \land W \in H) \land (Q \in A \land \neg Q \underset{˙}{\leq} W)) \to S = LSubSp (U)$
22	1 2 3 5 4 15	dicssdvh	$⊢ ((K \in HL \land W \in H) \land (Q \in A \land \neg Q \underset{˙}{\leq} W)) \to I (Q) \subseteq {Base}_{U}$
23	22 18	sseqtrrd	$⊢ ((K \in HL \land W \in H) \land (Q \in A \land \neg Q \underset{˙}{\leq} W)) \to I (Q) \subseteq LTrn (K) (W) \times TEndo (K) (W)$
24	1 2 3 5	dicn0	$⊢ ((K \in HL \land W \in H) \land (Q \in A \land \neg Q \underset{˙}{\leq} W)) \to I (Q) \neq \emptyset$
25		simpll	$⊢ (((K \in HL \land W \in H) \land (Q \in A \land \neg Q \underset{˙}{\leq} W)) \land (x \in TEndo (K) (W) \land a \in I (Q) \land b \in I (Q))) \to (K \in HL \land W \in H)$
26		simplr	$⊢ (((K \in HL \land W \in H) \land (Q \in A \land \neg Q \underset{˙}{\leq} W)) \land (x \in TEndo (K) (W) \land a \in I (Q) \land b \in I (Q))) \to (Q \in A \land \neg Q \underset{˙}{\leq} W)$
27		simpr1	$⊢ (((K \in HL \land W \in H) \land (Q \in A \land \neg Q \underset{˙}{\leq} W)) \land (x \in TEndo (K) (W) \land a \in I (Q) \land b \in I (Q))) \to x \in TEndo (K) (W)$
28		simpr2	$⊢ (((K \in HL \land W \in H) \land (Q \in A \land \neg Q \underset{˙}{\leq} W)) \land (x \in TEndo (K) (W) \land a \in I (Q) \land b \in I (Q))) \to a \in I (Q)$
29		eqid	$⊢ \cdot_{U} = \cdot_{U}$
30	1 2 3 8 4 5 29	dicvscacl	$⊢ ((K \in HL \land W \in H) \land (Q \in A \land \neg Q \underset{˙}{\leq} W) \land (x \in TEndo (K) (W) \land a \in I (Q))) \to x \cdot_{U} a \in I (Q)$
31	25 26 27 28 30	syl112anc	$⊢ (((K \in HL \land W \in H) \land (Q \in A \land \neg Q \underset{˙}{\leq} W)) \land (x \in TEndo (K) (W) \land a \in I (Q) \land b \in I (Q))) \to x \cdot_{U} a \in I (Q)$
32		simpr3	$⊢ (((K \in HL \land W \in H) \land (Q \in A \land \neg Q \underset{˙}{\leq} W)) \land (x \in TEndo (K) (W) \land a \in I (Q) \land b \in I (Q))) \to b \in I (Q)$
33		eqid	$⊢ +_{U} = +_{U}$
34	1 2 3 4 5 33	dicvaddcl	$⊢ ((K \in HL \land W \in H) \land (Q \in A \land \neg Q \underset{˙}{\leq} W) \land (x \cdot_{U} a \in I (Q) \land b \in I (Q))) \to (x \cdot_{U} a) +_{U} b \in I (Q)$
35	25 26 31 32 34	syl112anc	$⊢ (((K \in HL \land W \in H) \land (Q \in A \land \neg Q \underset{˙}{\leq} W)) \land (x \in TEndo (K) (W) \land a \in I (Q) \land b \in I (Q))) \to (x \cdot_{U} a) +_{U} b \in I (Q)$
36	7 13 18 19 20 21 23 24 35	islssd	$⊢ ((K \in HL \land W \in H) \land (Q \in A \land \neg Q \underset{˙}{\leq} W)) \to I (Q) \in S$

Metamath Proof Explorer

Theorem diclss

Proof