dicssdvh

Description: The partial isomorphism C maps to a set of vectors in full vector space H. (Contributed by NM, 19-Jan-2014)

	Ref	Expression
Hypotheses	dicssdvh.l	$⊢ \underset{˙}{\leq} = \leq_{K}$
	dicssdvh.a	$⊢ A = Atoms (K)$
	dicssdvh.h	$⊢ H = LHyp (K)$
	dicssdvh.i	$⊢ I = DIsoC (K) (W)$
	dicssdvh.u	$⊢ U = DVecH (K) (W)$
	dicssdvh.v	$⊢ V = {Base}_{U}$
Assertion	dicssdvh	$⊢ ((K \in HL \land W \in H) \land (Q \in A \land \neg Q \underset{˙}{\leq} W)) \to I (Q) \subseteq V$

Proof

Step	Hyp	Ref	Expression
1		dicssdvh.l	$⊢ \underset{˙}{\leq} = \leq_{K}$
2		dicssdvh.a	$⊢ A = Atoms (K)$
3		dicssdvh.h	$⊢ H = LHyp (K)$
4		dicssdvh.i	$⊢ I = DIsoC (K) (W)$
5		dicssdvh.u	$⊢ U = DVecH (K) (W)$
6		dicssdvh.v	$⊢ V = {Base}_{U}$
7		simprl	$⊢ (((K \in HL \land W \in H) \land (Q \in A \land \neg Q \underset{˙}{\leq} W)) \land (f = s ((ι g \in LTrn (K) (W) \| g (oc (K) (W)) = Q)) \land s \in TEndo (K) (W))) \to f = s ((ι g \in LTrn (K) (W) \| g (oc (K) (W)) = Q))$
8		simpll	$⊢ (((K \in HL \land W \in H) \land (Q \in A \land \neg Q \underset{˙}{\leq} W)) \land (f = s ((ι g \in LTrn (K) (W) \| g (oc (K) (W)) = Q)) \land s \in TEndo (K) (W))) \to (K \in HL \land W \in H)$
9		simprr	$⊢ (((K \in HL \land W \in H) \land (Q \in A \land \neg Q \underset{˙}{\leq} W)) \land (f = s ((ι g \in LTrn (K) (W) \| g (oc (K) (W)) = Q)) \land s \in TEndo (K) (W))) \to s \in TEndo (K) (W)$
10		eqid	$⊢ oc (K) = oc (K)$
11	1 10 2 3	lhpocnel	$⊢ (K \in HL \land W \in H) \to (oc (K) (W) \in A \land \neg oc (K) (W) \underset{˙}{\leq} W)$
12	11	ad2antrr	$⊢ (((K \in HL \land W \in H) \land (Q \in A \land \neg Q \underset{˙}{\leq} W)) \land (f = s ((ι g \in LTrn (K) (W) \| g (oc (K) (W)) = Q)) \land s \in TEndo (K) (W))) \to (oc (K) (W) \in A \land \neg oc (K) (W) \underset{˙}{\leq} W)$
13		simplr	$⊢ (((K \in HL \land W \in H) \land (Q \in A \land \neg Q \underset{˙}{\leq} W)) \land (f = s ((ι g \in LTrn (K) (W) \| g (oc (K) (W)) = Q)) \land s \in TEndo (K) (W))) \to (Q \in A \land \neg Q \underset{˙}{\leq} W)$
14		eqid	$⊢ LTrn (K) (W) = LTrn (K) (W)$
15		eqid	$⊢ (ι g \in LTrn (K) (W) \| g (oc (K) (W)) = Q) = (ι g \in LTrn (K) (W) \| g (oc (K) (W)) = Q)$
16	1 2 3 14 15	ltrniotacl	$⊢ ((K \in HL \land W \in H) \land (oc (K) (W) \in A \land \neg oc (K) (W) \underset{˙}{\leq} W) \land (Q \in A \land \neg Q \underset{˙}{\leq} W)) \to (ι g \in LTrn (K) (W) \| g (oc (K) (W)) = Q) \in LTrn (K) (W)$
17	8 12 13 16	syl3anc	$⊢ (((K \in HL \land W \in H) \land (Q \in A \land \neg Q \underset{˙}{\leq} W)) \land (f = s ((ι g \in LTrn (K) (W) \| g (oc (K) (W)) = Q)) \land s \in TEndo (K) (W))) \to (ι g \in LTrn (K) (W) \| g (oc (K) (W)) = Q) \in LTrn (K) (W)$
18		eqid	$⊢ TEndo (K) (W) = TEndo (K) (W)$
19	3 14 18	tendocl	$⊢ ((K \in HL \land W \in H) \land s \in TEndo (K) (W) \land (ι g \in LTrn (K) (W) \| g (oc (K) (W)) = Q) \in LTrn (K) (W)) \to s ((ι g \in LTrn (K) (W) \| g (oc (K) (W)) = Q)) \in LTrn (K) (W)$
20	8 9 17 19	syl3anc	$⊢ (((K \in HL \land W \in H) \land (Q \in A \land \neg Q \underset{˙}{\leq} W)) \land (f = s ((ι g \in LTrn (K) (W) \| g (oc (K) (W)) = Q)) \land s \in TEndo (K) (W))) \to s ((ι g \in LTrn (K) (W) \| g (oc (K) (W)) = Q)) \in LTrn (K) (W)$
21	7 20	eqeltrd	$⊢ (((K \in HL \land W \in H) \land (Q \in A \land \neg Q \underset{˙}{\leq} W)) \land (f = s ((ι g \in LTrn (K) (W) \| g (oc (K) (W)) = Q)) \land s \in TEndo (K) (W))) \to f \in LTrn (K) (W)$
22	21 9 9	jca31	$⊢ (((K \in HL \land W \in H) \land (Q \in A \land \neg Q \underset{˙}{\leq} W)) \land (f = s ((ι g \in LTrn (K) (W) \| g (oc (K) (W)) = Q)) \land s \in TEndo (K) (W))) \to ((f \in LTrn (K) (W) \land s \in TEndo (K) (W)) \land s \in TEndo (K) (W))$
23	22	ex	$⊢ ((K \in HL \land W \in H) \land (Q \in A \land \neg Q \underset{˙}{\leq} W)) \to ((f = s ((ι g \in LTrn (K) (W) \| g (oc (K) (W)) = Q)) \land s \in TEndo (K) (W)) \to ((f \in LTrn (K) (W) \land s \in TEndo (K) (W)) \land s \in TEndo (K) (W)))$
24	23	ssopab2dv	$⊢ ((K \in HL \land W \in H) \land (Q \in A \land \neg Q \underset{˙}{\leq} W)) \to \{⟨f, s⟩ \| (f = s ((ι g \in LTrn (K) (W) \| g (oc (K) (W)) = Q)) \land s \in TEndo (K) (W))\} \subseteq \{⟨f, s⟩ \| ((f \in LTrn (K) (W) \land s \in TEndo (K) (W)) \land s \in TEndo (K) (W))\}$
25		opabssxp	$⊢ \{⟨f, s⟩ \| ((f \in LTrn (K) (W) \land s \in TEndo (K) (W)) \land s \in TEndo (K) (W))\} \subseteq LTrn (K) (W) \times TEndo (K) (W)$
26	24 25	sstrdi	$⊢ ((K \in HL \land W \in H) \land (Q \in A \land \neg Q \underset{˙}{\leq} W)) \to \{⟨f, s⟩ \| (f = s ((ι g \in LTrn (K) (W) \| g (oc (K) (W)) = Q)) \land s \in TEndo (K) (W))\} \subseteq LTrn (K) (W) \times TEndo (K) (W)$
27		eqid	$⊢ oc (K) (W) = oc (K) (W)$
28	1 2 3 27 14 18 4	dicval	$⊢ ((K \in HL \land W \in H) \land (Q \in A \land \neg Q \underset{˙}{\leq} W)) \to I (Q) = \{⟨f, s⟩ \| (f = s ((ι g \in LTrn (K) (W) \| g (oc (K) (W)) = Q)) \land s \in TEndo (K) (W))\}$
29	3 14 18 5 6	dvhvbase	$⊢ (K \in HL \land W \in H) \to V = LTrn (K) (W) \times TEndo (K) (W)$
30	29	adantr	$⊢ ((K \in HL \land W \in H) \land (Q \in A \land \neg Q \underset{˙}{\leq} W)) \to V = LTrn (K) (W) \times TEndo (K) (W)$
31	26 28 30	3sstr4d	$⊢ ((K \in HL \land W \in H) \land (Q \in A \land \neg Q \underset{˙}{\leq} W)) \to I (Q) \subseteq V$

Metamath Proof Explorer

Theorem dicssdvh

Proof