Theorem djhlsmcl

Description: A closed subspace sum equals subspace join. ( shjshseli analog.) (Contributed by NM, 13-Aug-2014)

	Ref	Expression
Hypotheses	djhlsmcl.h	$$⊢H=\mathrm{LHyp}\left(K\right)$$
	djhlsmcl.u	$$⊢U=\mathrm{DVecH}\left(K\right)\left(W\right)$$
	djhlsmcl.v	$$⊢V={\mathrm{Base}}_U$$
	djhlsmcl.s	$$⊢S=\mathrm{LSubSp}\left(U\right)$$
	djhlsmcl.p	$$⊢\underset{\dot{}}{\oplus }=\mathrm{LSSum}\left(U\right)$$
	djhlsmcl.i	$$⊢I=\mathrm{DIsoH}\left(K\right)\left(W\right)$$
	djhlsmcl.j	$$⊢\underset{\dot{}}{\vee }=\mathrm{joinH}\left(K\right)\left(W\right)$$
	djhlsmcl.k	$$⊢\phi \to \left(K\in \mathrm{HL}\wedge W\in H\right)$$
	djhlsmcl.x	$$⊢\phi \to X\in S$$
	djhlsmcl.y	$$⊢\phi \to Y\in S$$
Assertion	djhlsmcl	$$⊢\phi \to \left(X\underset{\dot{}}{\oplus }Y\in \mathrm{ran}I\leftrightarrow X\underset{\dot{}}{\oplus }Y=X\underset{\dot{}}{\vee }Y\right)$$

Proof

Step	Hyp	Ref	Expression
1		djhlsmcl.h	$$⊢H=\mathrm{LHyp}\left(K\right)$$
2		djhlsmcl.u	$$⊢U=\mathrm{DVecH}\left(K\right)\left(W\right)$$
3		djhlsmcl.v	$$⊢V={\mathrm{Base}}_U$$
4		djhlsmcl.s	$$⊢S=\mathrm{LSubSp}\left(U\right)$$
5		djhlsmcl.p	$$⊢\underset{\dot{}}{\oplus }=\mathrm{LSSum}\left(U\right)$$
6		djhlsmcl.i	$$⊢I=\mathrm{DIsoH}\left(K\right)\left(W\right)$$
7		djhlsmcl.j	$$⊢\underset{\dot{}}{\vee }=\mathrm{joinH}\left(K\right)\left(W\right)$$
8		djhlsmcl.k	$$⊢\phi \to \left(K\in \mathrm{HL}\wedge W\in H\right)$$
9		djhlsmcl.x	$$⊢\phi \to X\in S$$
10		djhlsmcl.y	$$⊢\phi \to Y\in S$$
11	8	adantr	$$⊢\left(\phi \wedge X\underset{\dot{}}{\oplus }Y\in \mathrm{ran}I\right)\to \left(K\in \mathrm{HL}\wedge W\in H\right)$$
12	3 4	lssss	$$⊢X\in S\to X\subseteq V$$
13	9 12	syl	$$⊢\phi \to X\subseteq V$$
14	13	adantr	$$⊢\left(\phi \wedge X\underset{\dot{}}{\oplus }Y\in \mathrm{ran}I\right)\to X\subseteq V$$
15	3 4	lssss	$$⊢Y\in S\to Y\subseteq V$$
16	10 15	syl	$$⊢\phi \to Y\subseteq V$$
17	16	adantr	$$⊢\left(\phi \wedge X\underset{\dot{}}{\oplus }Y\in \mathrm{ran}I\right)\to Y\subseteq V$$
18		eqid	$$⊢\mathrm{ocH}\left(K\right)\left(W\right)=\mathrm{ocH}\left(K\right)\left(W\right)$$
19	1 2 3 18 7	djhval2	$$⊢\left(\left(K\in \mathrm{HL}\wedge W\in H\right)\wedge X\subseteq V\wedge Y\subseteq V\right)\to X\underset{\dot{}}{\vee }Y=\mathrm{ocH}\left(K\right)\left(W\right)\left(\mathrm{ocH}\left(K\right)\left(W\right)\left(X\cup Y\right)\right)$$
20	11 14 17 19	syl3anc	$$⊢\left(\phi \wedge X\underset{\dot{}}{\oplus }Y\in \mathrm{ran}I\right)\to X\underset{\dot{}}{\vee }Y=\mathrm{ocH}\left(K\right)\left(W\right)\left(\mathrm{ocH}\left(K\right)\left(W\right)\left(X\cup Y\right)\right)$$
21	1 2 8	dvhlmod	$$⊢\phi \to U\in \mathrm{LMod}$$
22	21	adantr	$$⊢\left(\phi \wedge X\underset{\dot{}}{\oplus }Y\in \mathrm{ran}I\right)\to U\in \mathrm{LMod}$$
23	9	adantr	$$⊢\left(\phi \wedge X\underset{\dot{}}{\oplus }Y\in \mathrm{ran}I\right)\to X\in S$$
24	10	adantr	$$⊢\left(\phi \wedge X\underset{\dot{}}{\oplus }Y\in \mathrm{ran}I\right)\to Y\in S$$
25		eqid	$$⊢\mathrm{LSpan}\left(U\right)=\mathrm{LSpan}\left(U\right)$$
26	4 25 5	lsmsp	$$⊢\left(U\in \mathrm{LMod}\wedge X\in S\wedge Y\in S\right)\to X\underset{\dot{}}{\oplus }Y=\mathrm{LSpan}\left(U\right)\left(X\cup Y\right)$$
27	22 23 24 26	syl3anc	$$⊢\left(\phi \wedge X\underset{\dot{}}{\oplus }Y\in \mathrm{ran}I\right)\to X\underset{\dot{}}{\oplus }Y=\mathrm{LSpan}\left(U\right)\left(X\cup Y\right)$$
28	27	fveq2d	$$⊢\left(\phi \wedge X\underset{\dot{}}{\oplus }Y\in \mathrm{ran}I\right)\to \mathrm{ocH}\left(K\right)\left(W\right)\left(X\underset{\dot{}}{\oplus }Y\right)=\mathrm{ocH}\left(K\right)\left(W\right)\left(\mathrm{LSpan}\left(U\right)\left(X\cup Y\right)\right)$$
29	13 16	unssd	$$⊢\phi \to X\cup Y\subseteq V$$
30	29	adantr	$$⊢\left(\phi \wedge X\underset{\dot{}}{\oplus }Y\in \mathrm{ran}I\right)\to X\cup Y\subseteq V$$
31	1 2 18 3 25 11 30	dochocsp	$$⊢\left(\phi \wedge X\underset{\dot{}}{\oplus }Y\in \mathrm{ran}I\right)\to \mathrm{ocH}\left(K\right)\left(W\right)\left(\mathrm{LSpan}\left(U\right)\left(X\cup Y\right)\right)=\mathrm{ocH}\left(K\right)\left(W\right)\left(X\cup Y\right)$$
32	28 31	eqtrd	$$⊢\left(\phi \wedge X\underset{\dot{}}{\oplus }Y\in \mathrm{ran}I\right)\to \mathrm{ocH}\left(K\right)\left(W\right)\left(X\underset{\dot{}}{\oplus }Y\right)=\mathrm{ocH}\left(K\right)\left(W\right)\left(X\cup Y\right)$$
33	32	fveq2d	$$⊢\left(\phi \wedge X\underset{\dot{}}{\oplus }Y\in \mathrm{ran}I\right)\to \mathrm{ocH}\left(K\right)\left(W\right)\left(\mathrm{ocH}\left(K\right)\left(W\right)\left(X\underset{\dot{}}{\oplus }Y\right)\right)=\mathrm{ocH}\left(K\right)\left(W\right)\left(\mathrm{ocH}\left(K\right)\left(W\right)\left(X\cup Y\right)\right)$$
34	1 6 18	dochoc	$$⊢\left(\left(K\in \mathrm{HL}\wedge W\in H\right)\wedge X\underset{\dot{}}{\oplus }Y\in \mathrm{ran}I\right)\to \mathrm{ocH}\left(K\right)\left(W\right)\left(\mathrm{ocH}\left(K\right)\left(W\right)\left(X\underset{\dot{}}{\oplus }Y\right)\right)=X\underset{\dot{}}{\oplus }Y$$
35	8 34	sylan	$$⊢\left(\phi \wedge X\underset{\dot{}}{\oplus }Y\in \mathrm{ran}I\right)\to \mathrm{ocH}\left(K\right)\left(W\right)\left(\mathrm{ocH}\left(K\right)\left(W\right)\left(X\underset{\dot{}}{\oplus }Y\right)\right)=X\underset{\dot{}}{\oplus }Y$$
36	20 33 35	3eqtr2rd	$$⊢\left(\phi \wedge X\underset{\dot{}}{\oplus }Y\in \mathrm{ran}I\right)\to X\underset{\dot{}}{\oplus }Y=X\underset{\dot{}}{\vee }Y$$
37	36	ex	$$⊢\phi \to \left(X\underset{\dot{}}{\oplus }Y\in \mathrm{ran}I\to X\underset{\dot{}}{\oplus }Y=X\underset{\dot{}}{\vee }Y\right)$$
38	1 6 2 3 7	djhcl	$$⊢\left(\left(K\in \mathrm{HL}\wedge W\in H\right)\wedge \left(X\subseteq V\wedge Y\subseteq V\right)\right)\to X\underset{\dot{}}{\vee }Y\in \mathrm{ran}I$$
39	8 13 16 38	syl12anc	$$⊢\phi \to X\underset{\dot{}}{\vee }Y\in \mathrm{ran}I$$
40		eleq1a	$$⊢X\underset{\dot{}}{\vee }Y\in \mathrm{ran}I\to \left(X\underset{\dot{}}{\oplus }Y=X\underset{\dot{}}{\vee }Y\to X\underset{\dot{}}{\oplus }Y\in \mathrm{ran}I\right)$$
41	39 40	syl	$$⊢\phi \to \left(X\underset{\dot{}}{\oplus }Y=X\underset{\dot{}}{\vee }Y\to X\underset{\dot{}}{\oplus }Y\in \mathrm{ran}I\right)$$
42	37 41	impbid	$$⊢\phi \to \left(X\underset{\dot{}}{\oplus }Y\in \mathrm{ran}I\leftrightarrow X\underset{\dot{}}{\oplus }Y=X\underset{\dot{}}{\vee }Y\right)$$