Theorem dia2dimlem13

Description: Lemma for dia2dim . Eliminate U =/= V condition. (Contributed by NM, 8-Sep-2014)

	Ref	Expression
Hypotheses	dia2dimlem12.l	$$⊢\underset{\dot{}}{\le }={\le }_K$$
	dia2dimlem12.j	$$⊢\underset{\dot{}}{\vee }=\mathrm{join}\left(K\right)$$
	dia2dimlem12.m	$$⊢\underset{\dot{}}{\wedge }=\mathrm{meet}\left(K\right)$$
	dia2dimlem12.a	$$⊢A=\mathrm{Atoms}\left(K\right)$$
	dia2dimlem12.h	$$⊢H=\mathrm{LHyp}\left(K\right)$$
	dia2dimlem12.t	$$⊢T=\mathrm{LTrn}\left(K\right)\left(W\right)$$
	dia2dimlem12.r	$$⊢R=\mathrm{trL}\left(K\right)\left(W\right)$$
	dia2dimlem12.y	$$⊢Y=\mathrm{DVecA}\left(K\right)\left(W\right)$$
	dia2dimlem12.s	$$⊢S=\mathrm{LSubSp}\left(Y\right)$$
	dia2dimlem12.pl	$$⊢\underset{\dot{}}{\oplus }=\mathrm{LSSum}\left(Y\right)$$
	dia2dimlem12.n	$$⊢N=\mathrm{LSpan}\left(Y\right)$$
	dia2dimlem12.i	$$⊢I=\mathrm{DIsoA}\left(K\right)\left(W\right)$$
	dia2dimlem12.k	$$⊢\phi \to \left(K\in \mathrm{HL}\wedge W\in H\right)$$
	dia2dimlem12.u	$$⊢\phi \to \left(U\in A\wedge U\underset{\dot{}}{\le }W\right)$$
	dia2dimlem12.v	$$⊢\phi \to \left(V\in A\wedge V\underset{\dot{}}{\le }W\right)$$
Assertion	dia2dimlem13	$$⊢\phi \to I\left(U\underset{\dot{}}{\vee }V\right)\subseteq I\left(U\right)\underset{\dot{}}{\oplus }I\left(V\right)$$

Proof

Step	Hyp	Ref	Expression
1		dia2dimlem12.l	$$⊢\underset{\dot{}}{\le }={\le }_K$$
2		dia2dimlem12.j	$$⊢\underset{\dot{}}{\vee }=\mathrm{join}\left(K\right)$$
3		dia2dimlem12.m	$$⊢\underset{\dot{}}{\wedge }=\mathrm{meet}\left(K\right)$$
4		dia2dimlem12.a	$$⊢A=\mathrm{Atoms}\left(K\right)$$
5		dia2dimlem12.h	$$⊢H=\mathrm{LHyp}\left(K\right)$$
6		dia2dimlem12.t	$$⊢T=\mathrm{LTrn}\left(K\right)\left(W\right)$$
7		dia2dimlem12.r	$$⊢R=\mathrm{trL}\left(K\right)\left(W\right)$$
8		dia2dimlem12.y	$$⊢Y=\mathrm{DVecA}\left(K\right)\left(W\right)$$
9		dia2dimlem12.s	$$⊢S=\mathrm{LSubSp}\left(Y\right)$$
10		dia2dimlem12.pl	$$⊢\underset{\dot{}}{\oplus }=\mathrm{LSSum}\left(Y\right)$$
11		dia2dimlem12.n	$$⊢N=\mathrm{LSpan}\left(Y\right)$$
12		dia2dimlem12.i	$$⊢I=\mathrm{DIsoA}\left(K\right)\left(W\right)$$
13		dia2dimlem12.k	$$⊢\phi \to \left(K\in \mathrm{HL}\wedge W\in H\right)$$
14		dia2dimlem12.u	$$⊢\phi \to \left(U\in A\wedge U\underset{\dot{}}{\le }W\right)$$
15		dia2dimlem12.v	$$⊢\phi \to \left(V\in A\wedge V\underset{\dot{}}{\le }W\right)$$
16		oveq2	$$⊢U=V\to U\underset{\dot{}}{\vee }U=U\underset{\dot{}}{\vee }V$$
17	16	adantl	$$⊢\left(\phi \wedge U=V\right)\to U\underset{\dot{}}{\vee }U=U\underset{\dot{}}{\vee }V$$
18	13	simpld	$$⊢\phi \to K\in \mathrm{HL}$$
19	14	simpld	$$⊢\phi \to U\in A$$
20	2 4	hlatjidm	$$⊢\left(K\in \mathrm{HL}\wedge U\in A\right)\to U\underset{\dot{}}{\vee }U=U$$
21	18 19 20	syl2anc	$$⊢\phi \to U\underset{\dot{}}{\vee }U=U$$
22	21	adantr	$$⊢\left(\phi \wedge U=V\right)\to U\underset{\dot{}}{\vee }U=U$$
23	17 22	eqtr3d	$$⊢\left(\phi \wedge U=V\right)\to U\underset{\dot{}}{\vee }V=U$$
24	23	fveq2d	$$⊢\left(\phi \wedge U=V\right)\to I\left(U\underset{\dot{}}{\vee }V\right)=I\left(U\right)$$
25		ssid	$$⊢I\left(U\right)\subseteq I\left(U\right)$$
26	24 25	eqsstrdi	$$⊢\left(\phi \wedge U=V\right)\to I\left(U\underset{\dot{}}{\vee }V\right)\subseteq I\left(U\right)$$
27	5 8	dvalvec	$$⊢\left(K\in \mathrm{HL}\wedge W\in H\right)\to Y\in \mathrm{LVec}$$
28		lveclmod	$$⊢Y\in \mathrm{LVec}\to Y\in \mathrm{LMod}$$
29	13 27 28	3syl	$$⊢\phi \to Y\in \mathrm{LMod}$$
30		eqid	$$⊢{\mathrm{Base}}_K={\mathrm{Base}}_K$$
31	30 4	atbase	$$⊢U\in A\to U\in {\mathrm{Base}}_K$$
32	19 31	syl	$$⊢\phi \to U\in {\mathrm{Base}}_K$$
33	14	simprd	$$⊢\phi \to U\underset{\dot{}}{\le }W$$
34	30 1 5 8 12 9	dialss	$$⊢\left(\left(K\in \mathrm{HL}\wedge W\in H\right)\wedge \left(U\in {\mathrm{Base}}_K\wedge U\underset{\dot{}}{\le }W\right)\right)\to I\left(U\right)\in S$$
35	13 32 33 34	syl12anc	$$⊢\phi \to I\left(U\right)\in S$$
36	9	lsssubg	$$⊢\left(Y\in \mathrm{LMod}\wedge I\left(U\right)\in S\right)\to I\left(U\right)\in \mathrm{SubGrp}\left(Y\right)$$
37	29 35 36	syl2anc	$$⊢\phi \to I\left(U\right)\in \mathrm{SubGrp}\left(Y\right)$$
38	10	lsmidm	$$⊢I\left(U\right)\in \mathrm{SubGrp}\left(Y\right)\to I\left(U\right)\underset{\dot{}}{\oplus }I\left(U\right)=I\left(U\right)$$
39	37 38	syl	$$⊢\phi \to I\left(U\right)\underset{\dot{}}{\oplus }I\left(U\right)=I\left(U\right)$$
40		fveq2	$$⊢U=V\to I\left(U\right)=I\left(V\right)$$
41	40	oveq2d	$$⊢U=V\to I\left(U\right)\underset{\dot{}}{\oplus }I\left(U\right)=I\left(U\right)\underset{\dot{}}{\oplus }I\left(V\right)$$
42	39 41	sylan9req	$$⊢\left(\phi \wedge U=V\right)\to I\left(U\right)=I\left(U\right)\underset{\dot{}}{\oplus }I\left(V\right)$$
43	26 42	sseqtrd	$$⊢\left(\phi \wedge U=V\right)\to I\left(U\underset{\dot{}}{\vee }V\right)\subseteq I\left(U\right)\underset{\dot{}}{\oplus }I\left(V\right)$$
44	13	adantr	$$⊢\left(\phi \wedge U\ne V\right)\to \left(K\in \mathrm{HL}\wedge W\in H\right)$$
45	14	adantr	$$⊢\left(\phi \wedge U\ne V\right)\to \left(U\in A\wedge U\underset{\dot{}}{\le }W\right)$$
46	15	adantr	$$⊢\left(\phi \wedge U\ne V\right)\to \left(V\in A\wedge V\underset{\dot{}}{\le }W\right)$$
47		simpr	$$⊢\left(\phi \wedge U\ne V\right)\to U\ne V$$
48	1 2 3 4 5 6 7 8 9 10 11 12 44 45 46 47	dia2dimlem12	$$⊢\left(\phi \wedge U\ne V\right)\to I\left(U\underset{\dot{}}{\vee }V\right)\subseteq I\left(U\right)\underset{\dot{}}{\oplus }I\left(V\right)$$
49	43 48	pm2.61dane	$$⊢\phi \to I\left(U\underset{\dot{}}{\vee }V\right)\subseteq I\left(U\right)\underset{\dot{}}{\oplus }I\left(V\right)$$