Theorem dia2dimlem7

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

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

Proof

Step	Hyp	Ref	Expression
1		dia2dimlem7.l	$$⊢\underset{\dot{}}{\le }={\le }_K$$
2		dia2dimlem7.j	$$⊢\underset{\dot{}}{\vee }=\mathrm{join}\left(K\right)$$
3		dia2dimlem7.m	$$⊢\underset{\dot{}}{\wedge }=\mathrm{meet}\left(K\right)$$
4		dia2dimlem7.a	$$⊢A=\mathrm{Atoms}\left(K\right)$$
5		dia2dimlem7.h	$$⊢H=\mathrm{LHyp}\left(K\right)$$
6		dia2dimlem7.t	$$⊢T=\mathrm{LTrn}\left(K\right)\left(W\right)$$
7		dia2dimlem7.r	$$⊢R=\mathrm{trL}\left(K\right)\left(W\right)$$
8		dia2dimlem7.y	$$⊢Y=\mathrm{DVecA}\left(K\right)\left(W\right)$$
9		dia2dimlem7.s	$$⊢S=\mathrm{LSubSp}\left(Y\right)$$
10		dia2dimlem7.pl	$$⊢\underset{\dot{}}{\oplus }=\mathrm{LSSum}\left(Y\right)$$
11		dia2dimlem7.n	$$⊢N=\mathrm{LSpan}\left(Y\right)$$
12		dia2dimlem7.i	$$⊢I=\mathrm{DIsoA}\left(K\right)\left(W\right)$$
13		dia2dimlem7.q	$$⊢Q=\left(P\underset{\dot{}}{\vee }U\right)\underset{\dot{}}{\wedge }\left(F\left(P\right)\underset{\dot{}}{\vee }V\right)$$
14		dia2dimlem7.k	$$⊢\phi \to \left(K\in \mathrm{HL}\wedge W\in H\right)$$
15		dia2dimlem7.u	$$⊢\phi \to \left(U\in A\wedge U\underset{\dot{}}{\le }W\right)$$
16		dia2dimlem7.v	$$⊢\phi \to \left(V\in A\wedge V\underset{\dot{}}{\le }W\right)$$
17		dia2dimlem7.p	$$⊢\phi \to \left(P\in A\wedge \neg P\underset{\dot{}}{\le }W\right)$$
18		dia2dimlem7.f	$$⊢\phi \to F\in T$$
19		dia2dimlem7.rf	$$⊢\phi \to R\left(F\right)\underset{\dot{}}{\le }\left(U\underset{\dot{}}{\vee }V\right)$$
20		dia2dimlem7.uv	$$⊢\phi \to U\ne V$$
21		dia2dimlem7.ru	$$⊢\phi \to R\left(F\right)\ne U$$
22		dia2dimlem7.rv	$$⊢\phi \to R\left(F\right)\ne V$$
23		eqid	$$⊢{\mathrm{Base}}_K={\mathrm{Base}}_K$$
24	23 1 4 5 6	ltrnideq	$$⊢\left(\left(K\in \mathrm{HL}\wedge W\in H\right)\wedge F\in T\wedge \left(P\in A\wedge \neg P\underset{\dot{}}{\le }W\right)\right)\to \left(F={\mathrm{I}\upharpoonright }_{{\mathrm{Base}}_K}\leftrightarrow F\left(P\right)=P\right)$$
25	14 18 17 24	syl3anc	$$⊢\phi \to \left(F={\mathrm{I}\upharpoonright }_{{\mathrm{Base}}_K}\leftrightarrow F\left(P\right)=P\right)$$
26		eqid	$$⊢0_Y=0_Y$$
27	23 5 6 8 26	dva0g	$$⊢\left(K\in \mathrm{HL}\wedge W\in H\right)\to 0_Y={\mathrm{I}\upharpoonright }_{{\mathrm{Base}}_K}$$
28	14 27	syl	$$⊢\phi \to 0_Y={\mathrm{I}\upharpoonright }_{{\mathrm{Base}}_K}$$
29	5 8	dvalvec	$$⊢\left(K\in \mathrm{HL}\wedge W\in H\right)\to Y\in \mathrm{LVec}$$
30		lveclmod	$$⊢Y\in \mathrm{LVec}\to Y\in \mathrm{LMod}$$
31	14 29 30	3syl	$$⊢\phi \to Y\in \mathrm{LMod}$$
32	15	simpld	$$⊢\phi \to U\in A$$
33	23 4	atbase	$$⊢U\in A\to U\in {\mathrm{Base}}_K$$
34	32 33	syl	$$⊢\phi \to U\in {\mathrm{Base}}_K$$
35	15	simprd	$$⊢\phi \to U\underset{\dot{}}{\le }W$$
36	23 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$$
37	14 34 35 36	syl12anc	$$⊢\phi \to I\left(U\right)\in S$$
38	16	simpld	$$⊢\phi \to V\in A$$
39	23 4	atbase	$$⊢V\in A\to V\in {\mathrm{Base}}_K$$
40	38 39	syl	$$⊢\phi \to V\in {\mathrm{Base}}_K$$
41	16	simprd	$$⊢\phi \to V\underset{\dot{}}{\le }W$$
42	23 1 5 8 12 9	dialss	$$⊢\left(\left(K\in \mathrm{HL}\wedge W\in H\right)\wedge \left(V\in {\mathrm{Base}}_K\wedge V\underset{\dot{}}{\le }W\right)\right)\to I\left(V\right)\in S$$
43	14 40 41 42	syl12anc	$$⊢\phi \to I\left(V\right)\in S$$
44	9 10	lsmcl	$$⊢\left(Y\in \mathrm{LMod}\wedge I\left(U\right)\in S\wedge I\left(V\right)\in S\right)\to I\left(U\right)\underset{\dot{}}{\oplus }I\left(V\right)\in S$$
45	31 37 43 44	syl3anc	$$⊢\phi \to I\left(U\right)\underset{\dot{}}{\oplus }I\left(V\right)\in S$$
46	26 9	lss0cl	$$⊢\left(Y\in \mathrm{LMod}\wedge I\left(U\right)\underset{\dot{}}{\oplus }I\left(V\right)\in S\right)\to 0_Y\in \left(I\left(U\right)\underset{\dot{}}{\oplus }I\left(V\right)\right)$$
47	31 45 46	syl2anc	$$⊢\phi \to 0_Y\in \left(I\left(U\right)\underset{\dot{}}{\oplus }I\left(V\right)\right)$$
48	28 47	eqeltrrd	$$⊢\phi \to {\mathrm{I}\upharpoonright }_{{\mathrm{Base}}_K}\in \left(I\left(U\right)\underset{\dot{}}{\oplus }I\left(V\right)\right)$$
49		eleq1a	$$⊢{\mathrm{I}\upharpoonright }_{{\mathrm{Base}}_K}\in \left(I\left(U\right)\underset{\dot{}}{\oplus }I\left(V\right)\right)\to \left(F={\mathrm{I}\upharpoonright }_{{\mathrm{Base}}_K}\to F\in \left(I\left(U\right)\underset{\dot{}}{\oplus }I\left(V\right)\right)\right)$$
50	48 49	syl	$$⊢\phi \to \left(F={\mathrm{I}\upharpoonright }_{{\mathrm{Base}}_K}\to F\in \left(I\left(U\right)\underset{\dot{}}{\oplus }I\left(V\right)\right)\right)$$
51	25 50	sylbird	$$⊢\phi \to \left(F\left(P\right)=P\to F\in \left(I\left(U\right)\underset{\dot{}}{\oplus }I\left(V\right)\right)\right)$$
52	51	imp	$$⊢\left(\phi \wedge F\left(P\right)=P\right)\to F\in \left(I\left(U\right)\underset{\dot{}}{\oplus }I\left(V\right)\right)$$
53	14	adantr	$$⊢\left(\phi \wedge F\left(P\right)\ne P\right)\to \left(K\in \mathrm{HL}\wedge W\in H\right)$$
54	15	adantr	$$⊢\left(\phi \wedge F\left(P\right)\ne P\right)\to \left(U\in A\wedge U\underset{\dot{}}{\le }W\right)$$
55	16	adantr	$$⊢\left(\phi \wedge F\left(P\right)\ne P\right)\to \left(V\in A\wedge V\underset{\dot{}}{\le }W\right)$$
56	17	adantr	$$⊢\left(\phi \wedge F\left(P\right)\ne P\right)\to \left(P\in A\wedge \neg P\underset{\dot{}}{\le }W\right)$$
57	18	anim1i	$$⊢\left(\phi \wedge F\left(P\right)\ne P\right)\to \left(F\in T\wedge F\left(P\right)\ne P\right)$$
58	19	adantr	$$⊢\left(\phi \wedge F\left(P\right)\ne P\right)\to R\left(F\right)\underset{\dot{}}{\le }\left(U\underset{\dot{}}{\vee }V\right)$$
59	20	adantr	$$⊢\left(\phi \wedge F\left(P\right)\ne P\right)\to U\ne V$$
60	21	adantr	$$⊢\left(\phi \wedge F\left(P\right)\ne P\right)\to R\left(F\right)\ne U$$
61	22	adantr	$$⊢\left(\phi \wedge F\left(P\right)\ne P\right)\to R\left(F\right)\ne V$$
62	1 2 3 4 5 6 7 8 9 10 11 12 13 53 54 55 56 57 58 59 60 61	dia2dimlem6	$$⊢\left(\phi \wedge F\left(P\right)\ne P\right)\to F\in \left(I\left(U\right)\underset{\dot{}}{\oplus }I\left(V\right)\right)$$
63	52 62	pm2.61dane	$$⊢\phi \to F\in \left(I\left(U\right)\underset{\dot{}}{\oplus }I\left(V\right)\right)$$