djaclN

Description: Closure of subspace join for DVecA partial vector space. (Contributed by NM, 5-Dec-2013) (New usage is discouraged.)

	Ref	Expression
Hypotheses	djacl.h	$⊢ H = LHyp (K)$
	djacl.t	$⊢ T = LTrn (K) (W)$
	djacl.i	$⊢ I = DIsoA (K) (W)$
	djacl.j	$⊢ J = vA (K) (W)$
Assertion	djaclN	$⊢ ((K \in HL \land W \in H) \land (X \subseteq T \land Y \subseteq T)) \to X J Y \in ran I$

Step	Hyp	Ref	Expression
1		djacl.h	$⊢ H = LHyp (K)$
2		djacl.t	$⊢ T = LTrn (K) (W)$
3		djacl.i	$⊢ I = DIsoA (K) (W)$
4		djacl.j	$⊢ J = vA (K) (W)$
5		eqid	$⊢ ocA (K) (W) = ocA (K) (W)$
6	1 2 3 5 4	djavalN	$⊢ ((K \in HL \land W \in H) \land (X \subseteq T \land Y \subseteq T)) \to X J Y = ocA (K) (W) (ocA (K) (W) (X) \cap ocA (K) (W) (Y))$
7		inss1	$⊢ ocA (K) (W) (X) \cap ocA (K) (W) (Y) \subseteq ocA (K) (W) (X)$
8	1 2 3 5	docaclN	$⊢ ((K \in HL \land W \in H) \land X \subseteq T) \to ocA (K) (W) (X) \in ran I$
9	8	adantrr	$⊢ ((K \in HL \land W \in H) \land (X \subseteq T \land Y \subseteq T)) \to ocA (K) (W) (X) \in ran I$
10	1 2 3	diaelrnN	$⊢ ((K \in HL \land W \in H) \land ocA (K) (W) (X) \in ran I) \to ocA (K) (W) (X) \subseteq T$
11	9 10	syldan	$⊢ ((K \in HL \land W \in H) \land (X \subseteq T \land Y \subseteq T)) \to ocA (K) (W) (X) \subseteq T$
12	7 11	sstrid	$⊢ ((K \in HL \land W \in H) \land (X \subseteq T \land Y \subseteq T)) \to ocA (K) (W) (X) \cap ocA (K) (W) (Y) \subseteq T$
13	1 2 3 5	docaclN	$⊢ ((K \in HL \land W \in H) \land ocA (K) (W) (X) \cap ocA (K) (W) (Y) \subseteq T) \to ocA (K) (W) (ocA (K) (W) (X) \cap ocA (K) (W) (Y)) \in ran I$
14	12 13	syldan	$⊢ ((K \in HL \land W \in H) \land (X \subseteq T \land Y \subseteq T)) \to ocA (K) (W) (ocA (K) (W) (X) \cap ocA (K) (W) (Y)) \in ran I$
15	6 14	eqeltrd	$⊢ ((K \in HL \land W \in H) \land (X \subseteq T \land Y \subseteq T)) \to X J Y \in ran I$

Metamath Proof Explorer