djhlsmat

Description: The sum of two subspace atoms equals their join. TODO: seems convoluted to go via dihprrn ; should we directly use dihjat ? (Contributed by NM, 13-Aug-2014)

	Ref	Expression
Hypotheses	djhlsmat.h	$⊢ H = LHyp (K)$
	djhlsmat.u	$⊢ U = DVecH (K) (W)$
	djhlsmat.v	$⊢ V = {Base}_{U}$
	djhlsmat.p	$⊢ \underset{˙}{\oplus} = LSSum (U)$
	djhlsmat.n	$⊢ N = LSpan (U)$
	djhlsmat.i	$⊢ I = DIsoH (K) (W)$
	djhlsmat.j	$⊢ \underset{˙}{\lor} = joinH (K) (W)$
	djhlsmat.k	$⊢ φ \to (K \in HL \land W \in H)$
	djhlsmat.x	$⊢ φ \to X \in V$
	djhlsmat.y	$⊢ φ \to Y \in V$
Assertion	djhlsmat	$⊢ φ \to N (\{X\}) \underset{˙}{\oplus} N (\{Y\}) = N (\{X\}) \underset{˙}{\lor} N (\{Y\})$

Proof

Step	Hyp	Ref	Expression
1		djhlsmat.h	$⊢ H = LHyp (K)$
2		djhlsmat.u	$⊢ U = DVecH (K) (W)$
3		djhlsmat.v	$⊢ V = {Base}_{U}$
4		djhlsmat.p	$⊢ \underset{˙}{\oplus} = LSSum (U)$
5		djhlsmat.n	$⊢ N = LSpan (U)$
6		djhlsmat.i	$⊢ I = DIsoH (K) (W)$
7		djhlsmat.j	$⊢ \underset{˙}{\lor} = joinH (K) (W)$
8		djhlsmat.k	$⊢ φ \to (K \in HL \land W \in H)$
9		djhlsmat.x	$⊢ φ \to X \in V$
10		djhlsmat.y	$⊢ φ \to Y \in V$
11	1 2 8	dvhlmod	$⊢ φ \to U \in LMod$
12	9	snssd	$⊢ φ \to \{X\} \subseteq V$
13	10	snssd	$⊢ φ \to \{Y\} \subseteq V$
14	3 5 4	lsmsp2	$⊢ (U \in LMod \land \{X\} \subseteq V \land \{Y\} \subseteq V) \to N (\{X\}) \underset{˙}{\oplus} N (\{Y\}) = N (\{X\} \cup \{Y\})$
15	11 12 13 14	syl3anc	$⊢ φ \to N (\{X\}) \underset{˙}{\oplus} N (\{Y\}) = N (\{X\} \cup \{Y\})$
16		df-pr	$⊢ \{X, Y\} = \{X\} \cup \{Y\}$
17	16	fveq2i	$⊢ N (\{X, Y\}) = N (\{X\} \cup \{Y\})$
18	15 17	eqtr4di	$⊢ φ \to N (\{X\}) \underset{˙}{\oplus} N (\{Y\}) = N (\{X, Y\})$
19	1 2 3 5 6 8 9 10	dihprrn	$⊢ φ \to N (\{X, Y\}) \in ran I$
20	18 19	eqeltrd	$⊢ φ \to N (\{X\}) \underset{˙}{\oplus} N (\{Y\}) \in ran I$
21		eqid	$⊢ LSubSp (U) = LSubSp (U)$
22	3 21 5	lspsncl	$⊢ (U \in LMod \land X \in V) \to N (\{X\}) \in LSubSp (U)$
23	11 9 22	syl2anc	$⊢ φ \to N (\{X\}) \in LSubSp (U)$
24	3 21 5	lspsncl	$⊢ (U \in LMod \land Y \in V) \to N (\{Y\}) \in LSubSp (U)$
25	11 10 24	syl2anc	$⊢ φ \to N (\{Y\}) \in LSubSp (U)$
26	1 2 3 21 4 6 7 8 23 25	djhlsmcl	$⊢ φ \to (N (\{X\}) \underset{˙}{\oplus} N (\{Y\}) \in ran I \leftrightarrow N (\{X\}) \underset{˙}{\oplus} N (\{Y\}) = N (\{X\}) \underset{˙}{\lor} N (\{Y\}))$
27	20 26	mpbid	$⊢ φ \to N (\{X\}) \underset{˙}{\oplus} N (\{Y\}) = N (\{X\}) \underset{˙}{\lor} N (\{Y\})$

Metamath Proof Explorer

Theorem djhlsmat

Proof