dia2dimlem5

Description: Lemma for dia2dim . The sum of vectors G and D belongs to the sum of the subspaces generated by them. Thus, F = ( G o. D ) belongs to the subspace sum. Part of proof of Lemma M in Crawley p. 121 line 5. (Contributed by NM, 8-Sep-2014)

	Ref	Expression
Hypotheses	dia2dimlem5.l	\|- .<_ = ( le ` K )
	dia2dimlem5.j	\|- .\/ = ( join ` K )
	dia2dimlem5.m	\|- ./\ = ( meet ` K )
	dia2dimlem5.a	\|- A = ( Atoms ` K )
	dia2dimlem5.h	\|- H = ( LHyp ` K )
	dia2dimlem5.t	\|- T = ( ( LTrn ` K ) ` W )
	dia2dimlem5.r	\|- R = ( ( trL ` K ) ` W )
	dia2dimlem5.y	\|- Y = ( ( DVecA ` K ) ` W )
	dia2dimlem5.s	\|- S = ( LSubSp ` Y )
	dia2dimlem5.pl	\|- .(+) = ( LSSum ` Y )
	dia2dimlem5.n	\|- N = ( LSpan ` Y )
	dia2dimlem5.i	\|- I = ( ( DIsoA ` K ) ` W )
	dia2dimlem5.q	\|- Q = ( ( P .\/ U ) ./\ ( ( F ` P ) .\/ V ) )
	dia2dimlem5.k	\|- ( ph -> ( K e. HL /\ W e. H ) )
	dia2dimlem5.u	\|- ( ph -> ( U e. A /\ U .<_ W ) )
	dia2dimlem5.v	\|- ( ph -> ( V e. A /\ V .<_ W ) )
	dia2dimlem5.p	\|- ( ph -> ( P e. A /\ -. P .<_ W ) )
	dia2dimlem5.f	\|- ( ph -> ( F e. T /\ ( F ` P ) =/= P ) )
	dia2dimlem5.rf	\|- ( ph -> ( R ` F ) .<_ ( U .\/ V ) )
	dia2dimlem5.uv	\|- ( ph -> U =/= V )
	dia2dimlem5.ru	\|- ( ph -> ( R ` F ) =/= U )
	dia2dimlem5.rv	\|- ( ph -> ( R ` F ) =/= V )
	dia2dimlem5.g	\|- ( ph -> G e. T )
	dia2dimlem5.gv	\|- ( ph -> ( G ` P ) = Q )
	dia2dimlem5.d	\|- ( ph -> D e. T )
	dia2dimlem5.dv	\|- ( ph -> ( D ` Q ) = ( F ` P ) )
Assertion	dia2dimlem5	\|- ( ph -> F e. ( ( I ` U ) .(+) ( I ` V ) ) )

Proof

Step	Hyp	Ref	Expression
1		dia2dimlem5.l	\|- .<_ = ( le ` K )
2		dia2dimlem5.j	\|- .\/ = ( join ` K )
3		dia2dimlem5.m	\|- ./\ = ( meet ` K )
4		dia2dimlem5.a	\|- A = ( Atoms ` K )
5		dia2dimlem5.h	\|- H = ( LHyp ` K )
6		dia2dimlem5.t	\|- T = ( ( LTrn ` K ) ` W )
7		dia2dimlem5.r	\|- R = ( ( trL ` K ) ` W )
8		dia2dimlem5.y	\|- Y = ( ( DVecA ` K ) ` W )
9		dia2dimlem5.s	\|- S = ( LSubSp ` Y )
10		dia2dimlem5.pl	\|- .(+) = ( LSSum ` Y )
11		dia2dimlem5.n	\|- N = ( LSpan ` Y )
12		dia2dimlem5.i	\|- I = ( ( DIsoA ` K ) ` W )
13		dia2dimlem5.q	\|- Q = ( ( P .\/ U ) ./\ ( ( F ` P ) .\/ V ) )
14		dia2dimlem5.k	\|- ( ph -> ( K e. HL /\ W e. H ) )
15		dia2dimlem5.u	\|- ( ph -> ( U e. A /\ U .<_ W ) )
16		dia2dimlem5.v	\|- ( ph -> ( V e. A /\ V .<_ W ) )
17		dia2dimlem5.p	\|- ( ph -> ( P e. A /\ -. P .<_ W ) )
18		dia2dimlem5.f	\|- ( ph -> ( F e. T /\ ( F ` P ) =/= P ) )
19		dia2dimlem5.rf	\|- ( ph -> ( R ` F ) .<_ ( U .\/ V ) )
20		dia2dimlem5.uv	\|- ( ph -> U =/= V )
21		dia2dimlem5.ru	\|- ( ph -> ( R ` F ) =/= U )
22		dia2dimlem5.rv	\|- ( ph -> ( R ` F ) =/= V )
23		dia2dimlem5.g	\|- ( ph -> G e. T )
24		dia2dimlem5.gv	\|- ( ph -> ( G ` P ) = Q )
25		dia2dimlem5.d	\|- ( ph -> D e. T )
26		dia2dimlem5.dv	\|- ( ph -> ( D ` Q ) = ( F ` P ) )
27		eqid	\|- ( +g ` Y ) = ( +g ` Y )
28	5 6 8 27	dvavadd	\|- ( ( ( K e. HL /\ W e. H ) /\ ( D e. T /\ G e. T ) ) -> ( D ( +g ` Y ) G ) = ( D o. G ) )
29	14 25 23 28	syl12anc	\|- ( ph -> ( D ( +g ` Y ) G ) = ( D o. G ) )
30	18	simpld	\|- ( ph -> F e. T )
31	1 4 5 6 14 17 30 23 24 25 26	dia2dimlem4	\|- ( ph -> ( D o. G ) = F )
32	29 31	eqtr2d	\|- ( ph -> F = ( D ( +g ` Y ) G ) )
33	5 8	dvalvec	\|- ( ( K e. HL /\ W e. H ) -> Y e. LVec )
34		lveclmod	\|- ( Y e. LVec -> Y e. LMod )
35	14 33 34	3syl	\|- ( ph -> Y e. LMod )
36	9	lsssssubg	\|- ( Y e. LMod -> S C_ ( SubGrp ` Y ) )
37	35 36	syl	\|- ( ph -> S C_ ( SubGrp ` Y ) )
38	16	simpld	\|- ( ph -> V e. A )
39		eqid	\|- ( Base ` K ) = ( Base ` K )
40	39 4	atbase	\|- ( V e. A -> V e. ( Base ` K ) )
41	38 40	syl	\|- ( ph -> V e. ( Base ` K ) )
42	16	simprd	\|- ( ph -> V .<_ W )
43	39 1 5 8 12 9	dialss	\|- ( ( ( K e. HL /\ W e. H ) /\ ( V e. ( Base ` K ) /\ V .<_ W ) ) -> ( I ` V ) e. S )
44	14 41 42 43	syl12anc	\|- ( ph -> ( I ` V ) e. S )
45	37 44	sseldd	\|- ( ph -> ( I ` V ) e. ( SubGrp ` Y ) )
46	15	simpld	\|- ( ph -> U e. A )
47	39 4	atbase	\|- ( U e. A -> U e. ( Base ` K ) )
48	46 47	syl	\|- ( ph -> U e. ( Base ` K ) )
49	15	simprd	\|- ( ph -> U .<_ W )
50	39 1 5 8 12 9	dialss	\|- ( ( ( K e. HL /\ W e. H ) /\ ( U e. ( Base ` K ) /\ U .<_ W ) ) -> ( I ` U ) e. S )
51	14 48 49 50	syl12anc	\|- ( ph -> ( I ` U ) e. S )
52	37 51	sseldd	\|- ( ph -> ( I ` U ) e. ( SubGrp ` Y ) )
53	5 6 7 8 12 11	dia1dim2	\|- ( ( ( K e. HL /\ W e. H ) /\ D e. T ) -> ( I ` ( R ` D ) ) = ( N ` { D } ) )
54	14 25 53	syl2anc	\|- ( ph -> ( I ` ( R ` D ) ) = ( N ` { D } ) )
55	1 2 3 4 5 6 7 13 14 15 16 17 18 19 20 21 22 25 26	dia2dimlem3	\|- ( ph -> ( R ` D ) = V )
56	55	fveq2d	\|- ( ph -> ( I ` ( R ` D ) ) = ( I ` V ) )
57		eqss	\|- ( ( I ` ( R ` D ) ) = ( I ` V ) <-> ( ( I ` ( R ` D ) ) C_ ( I ` V ) /\ ( I ` V ) C_ ( I ` ( R ` D ) ) ) )
58	56 57	sylib	\|- ( ph -> ( ( I ` ( R ` D ) ) C_ ( I ` V ) /\ ( I ` V ) C_ ( I ` ( R ` D ) ) ) )
59	58	simpld	\|- ( ph -> ( I ` ( R ` D ) ) C_ ( I ` V ) )
60	54 59	eqsstrrd	\|- ( ph -> ( N ` { D } ) C_ ( I ` V ) )
61		eqid	\|- ( Base ` Y ) = ( Base ` Y )
62	5 6 8 61	dvavbase	\|- ( ( K e. HL /\ W e. H ) -> ( Base ` Y ) = T )
63	14 62	syl	\|- ( ph -> ( Base ` Y ) = T )
64	25 63	eleqtrrd	\|- ( ph -> D e. ( Base ` Y ) )
65	61 9 11 35 44 64	ellspsn5b	\|- ( ph -> ( D e. ( I ` V ) <-> ( N ` { D } ) C_ ( I ` V ) ) )
66	60 65	mpbird	\|- ( ph -> D e. ( I ` V ) )
67	5 6 7 8 12 11	dia1dim2	\|- ( ( ( K e. HL /\ W e. H ) /\ G e. T ) -> ( I ` ( R ` G ) ) = ( N ` { G } ) )
68	14 23 67	syl2anc	\|- ( ph -> ( I ` ( R ` G ) ) = ( N ` { G } ) )
69	1 2 3 4 5 6 7 13 14 15 16 17 18 19 22 23 24	dia2dimlem2	\|- ( ph -> ( R ` G ) = U )
70	69	fveq2d	\|- ( ph -> ( I ` ( R ` G ) ) = ( I ` U ) )
71		eqss	\|- ( ( I ` ( R ` G ) ) = ( I ` U ) <-> ( ( I ` ( R ` G ) ) C_ ( I ` U ) /\ ( I ` U ) C_ ( I ` ( R ` G ) ) ) )
72	70 71	sylib	\|- ( ph -> ( ( I ` ( R ` G ) ) C_ ( I ` U ) /\ ( I ` U ) C_ ( I ` ( R ` G ) ) ) )
73	72	simpld	\|- ( ph -> ( I ` ( R ` G ) ) C_ ( I ` U ) )
74	68 73	eqsstrrd	\|- ( ph -> ( N ` { G } ) C_ ( I ` U ) )
75	23 63	eleqtrrd	\|- ( ph -> G e. ( Base ` Y ) )
76	61 9 11 35 51 75	ellspsn5b	\|- ( ph -> ( G e. ( I ` U ) <-> ( N ` { G } ) C_ ( I ` U ) ) )
77	74 76	mpbird	\|- ( ph -> G e. ( I ` U ) )
78	27 10	lsmelvali	\|- ( ( ( ( I ` V ) e. ( SubGrp ` Y ) /\ ( I ` U ) e. ( SubGrp ` Y ) ) /\ ( D e. ( I ` V ) /\ G e. ( I ` U ) ) ) -> ( D ( +g ` Y ) G ) e. ( ( I ` V ) .(+) ( I ` U ) ) )
79	45 52 66 77 78	syl22anc	\|- ( ph -> ( D ( +g ` Y ) G ) e. ( ( I ` V ) .(+) ( I ` U ) ) )
80	32 79	eqeltrd	\|- ( ph -> F e. ( ( I ` V ) .(+) ( I ` U ) ) )
81		lmodabl	\|- ( Y e. LMod -> Y e. Abel )
82	35 81	syl	\|- ( ph -> Y e. Abel )
83	10	lsmcom	\|- ( ( Y e. Abel /\ ( I ` V ) e. ( SubGrp ` Y ) /\ ( I ` U ) e. ( SubGrp ` Y ) ) -> ( ( I ` V ) .(+) ( I ` U ) ) = ( ( I ` U ) .(+) ( I ` V ) ) )
84	82 45 52 83	syl3anc	\|- ( ph -> ( ( I ` V ) .(+) ( I ` U ) ) = ( ( I ` U ) .(+) ( I ` V ) ) )
85	80 84	eleqtrd	\|- ( ph -> F e. ( ( I ` U ) .(+) ( I ` V ) ) )

Metamath Proof Explorer

Theorem dia2dimlem5

Proof