djhcl

Description: Closure of subspace join for DVecH vector space. (Contributed by NM, 19-Jul-2014)

	Ref	Expression
Hypotheses	djhcl.h	$⊢ H = LHyp (K)$
	djhcl.i	$⊢ I = DIsoH (K) (W)$
	djhcl.u	$⊢ U = DVecH (K) (W)$
	djhcl.v	$⊢ V = {Base}_{U}$
	djhcl.j	$⊢ \underset{˙}{\lor} = joinH (K) (W)$
Assertion	djhcl	$⊢ ((K \in HL \land W \in H) \land (X \subseteq V \land Y \subseteq V)) \to X \underset{˙}{\lor} Y \in ran I$

Step	Hyp	Ref	Expression
1		djhcl.h	$⊢ H = LHyp (K)$
2		djhcl.i	$⊢ I = DIsoH (K) (W)$
3		djhcl.u	$⊢ U = DVecH (K) (W)$
4		djhcl.v	$⊢ V = {Base}_{U}$
5		djhcl.j	$⊢ \underset{˙}{\lor} = joinH (K) (W)$
6		eqid	$⊢ ocH (K) (W) = ocH (K) (W)$
7	1 3 4 6 5	djhval	$⊢ ((K \in HL \land W \in H) \land (X \subseteq V \land Y \subseteq V)) \to X \underset{˙}{\lor} Y = ocH (K) (W) (ocH (K) (W) (X) \cap ocH (K) (W) (Y))$
8		inss1	$⊢ ocH (K) (W) (X) \cap ocH (K) (W) (Y) \subseteq ocH (K) (W) (X)$
9	1 2 3 4 6	dochcl	$⊢ ((K \in HL \land W \in H) \land X \subseteq V) \to ocH (K) (W) (X) \in ran I$
10	9	adantrr	$⊢ ((K \in HL \land W \in H) \land (X \subseteq V \land Y \subseteq V)) \to ocH (K) (W) (X) \in ran I$
11	1 3 2 4	dihrnss	$⊢ ((K \in HL \land W \in H) \land ocH (K) (W) (X) \in ran I) \to ocH (K) (W) (X) \subseteq V$
12	10 11	syldan	$⊢ ((K \in HL \land W \in H) \land (X \subseteq V \land Y \subseteq V)) \to ocH (K) (W) (X) \subseteq V$
13	8 12	sstrid	$⊢ ((K \in HL \land W \in H) \land (X \subseteq V \land Y \subseteq V)) \to ocH (K) (W) (X) \cap ocH (K) (W) (Y) \subseteq V$
14	1 2 3 4 6	dochcl	$⊢ ((K \in HL \land W \in H) \land ocH (K) (W) (X) \cap ocH (K) (W) (Y) \subseteq V) \to ocH (K) (W) (ocH (K) (W) (X) \cap ocH (K) (W) (Y)) \in ran I$
15	13 14	syldan	$⊢ ((K \in HL \land W \in H) \land (X \subseteq V \land Y \subseteq V)) \to ocH (K) (W) (ocH (K) (W) (X) \cap ocH (K) (W) (Y)) \in ran I$
16	7 15	eqeltrd	$⊢ ((K \in HL \land W \in H) \land (X \subseteq V \land Y \subseteq V)) \to X \underset{˙}{\lor} Y \in ran I$

Metamath Proof Explorer