Theorem 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 ‘ 𝐾 )
	dia2dimlem5.j	⊢ ∨ = ( join ‘ 𝐾 )
	dia2dimlem5.m	⊢ ∧ = ( meet ‘ 𝐾 )
	dia2dimlem5.a	⊢ 𝐴 = ( Atoms ‘ 𝐾 )
	dia2dimlem5.h	⊢ 𝐻 = ( LHyp ‘ 𝐾 )
	dia2dimlem5.t	⊢ 𝑇 = ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 )
	dia2dimlem5.r	⊢ 𝑅 = ( ( trL ‘ 𝐾 ) ‘ 𝑊 )
	dia2dimlem5.y	⊢ 𝑌 = ( ( DVecA ‘ 𝐾 ) ‘ 𝑊 )
	dia2dimlem5.s	⊢ 𝑆 = ( LSubSp ‘ 𝑌 )
	dia2dimlem5.pl	⊢ ⊕ = ( LSSum ‘ 𝑌 )
	dia2dimlem5.n	⊢ 𝑁 = ( LSpan ‘ 𝑌 )
	dia2dimlem5.i	⊢ 𝐼 = ( ( DIsoA ‘ 𝐾 ) ‘ 𝑊 )
	dia2dimlem5.q	⊢ 𝑄 = ( ( 𝑃 ∨ 𝑈 ) ∧ ( ( 𝐹 ‘ 𝑃 ) ∨ 𝑉 ) )
	dia2dimlem5.k	⊢ ( 𝜑 → ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) )
	dia2dimlem5.u	⊢ ( 𝜑 → ( 𝑈 ∈ 𝐴 ∧ 𝑈 ≤ 𝑊 ) )
	dia2dimlem5.v	⊢ ( 𝜑 → ( 𝑉 ∈ 𝐴 ∧ 𝑉 ≤ 𝑊 ) )
	dia2dimlem5.p	⊢ ( 𝜑 → ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) )
	dia2dimlem5.f	⊢ ( 𝜑 → ( 𝐹 ∈ 𝑇 ∧ ( 𝐹 ‘ 𝑃 ) ≠ 𝑃 ) )
	dia2dimlem5.rf	⊢ ( 𝜑 → ( 𝑅 ‘ 𝐹 ) ≤ ( 𝑈 ∨ 𝑉 ) )
	dia2dimlem5.uv	⊢ ( 𝜑 → 𝑈 ≠ 𝑉 )
	dia2dimlem5.ru	⊢ ( 𝜑 → ( 𝑅 ‘ 𝐹 ) ≠ 𝑈 )
	dia2dimlem5.rv	⊢ ( 𝜑 → ( 𝑅 ‘ 𝐹 ) ≠ 𝑉 )
	dia2dimlem5.g	⊢ ( 𝜑 → 𝐺 ∈ 𝑇 )
	dia2dimlem5.gv	⊢ ( 𝜑 → ( 𝐺 ‘ 𝑃 ) = 𝑄 )
	dia2dimlem5.d	⊢ ( 𝜑 → 𝐷 ∈ 𝑇 )
	dia2dimlem5.dv	⊢ ( 𝜑 → ( 𝐷 ‘ 𝑄 ) = ( 𝐹 ‘ 𝑃 ) )
Assertion	dia2dimlem5	⊢ ( 𝜑 → 𝐹 ∈ ( ( 𝐼 ‘ 𝑈 ) ⊕ ( 𝐼 ‘ 𝑉 ) ) )

Proof

Step	Hyp	Ref	Expression
1		dia2dimlem5.l	⊢ ≤ = ( le ‘ 𝐾 )
2		dia2dimlem5.j	⊢ ∨ = ( join ‘ 𝐾 )
3		dia2dimlem5.m	⊢ ∧ = ( meet ‘ 𝐾 )
4		dia2dimlem5.a	⊢ 𝐴 = ( Atoms ‘ 𝐾 )
5		dia2dimlem5.h	⊢ 𝐻 = ( LHyp ‘ 𝐾 )
6		dia2dimlem5.t	⊢ 𝑇 = ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 )
7		dia2dimlem5.r	⊢ 𝑅 = ( ( trL ‘ 𝐾 ) ‘ 𝑊 )
8		dia2dimlem5.y	⊢ 𝑌 = ( ( DVecA ‘ 𝐾 ) ‘ 𝑊 )
9		dia2dimlem5.s	⊢ 𝑆 = ( LSubSp ‘ 𝑌 )
10		dia2dimlem5.pl	⊢ ⊕ = ( LSSum ‘ 𝑌 )
11		dia2dimlem5.n	⊢ 𝑁 = ( LSpan ‘ 𝑌 )
12		dia2dimlem5.i	⊢ 𝐼 = ( ( DIsoA ‘ 𝐾 ) ‘ 𝑊 )
13		dia2dimlem5.q	⊢ 𝑄 = ( ( 𝑃 ∨ 𝑈 ) ∧ ( ( 𝐹 ‘ 𝑃 ) ∨ 𝑉 ) )
14		dia2dimlem5.k	⊢ ( 𝜑 → ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) )
15		dia2dimlem5.u	⊢ ( 𝜑 → ( 𝑈 ∈ 𝐴 ∧ 𝑈 ≤ 𝑊 ) )
16		dia2dimlem5.v	⊢ ( 𝜑 → ( 𝑉 ∈ 𝐴 ∧ 𝑉 ≤ 𝑊 ) )
17		dia2dimlem5.p	⊢ ( 𝜑 → ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) )
18		dia2dimlem5.f	⊢ ( 𝜑 → ( 𝐹 ∈ 𝑇 ∧ ( 𝐹 ‘ 𝑃 ) ≠ 𝑃 ) )
19		dia2dimlem5.rf	⊢ ( 𝜑 → ( 𝑅 ‘ 𝐹 ) ≤ ( 𝑈 ∨ 𝑉 ) )
20		dia2dimlem5.uv	⊢ ( 𝜑 → 𝑈 ≠ 𝑉 )
21		dia2dimlem5.ru	⊢ ( 𝜑 → ( 𝑅 ‘ 𝐹 ) ≠ 𝑈 )
22		dia2dimlem5.rv	⊢ ( 𝜑 → ( 𝑅 ‘ 𝐹 ) ≠ 𝑉 )
23		dia2dimlem5.g	⊢ ( 𝜑 → 𝐺 ∈ 𝑇 )
24		dia2dimlem5.gv	⊢ ( 𝜑 → ( 𝐺 ‘ 𝑃 ) = 𝑄 )
25		dia2dimlem5.d	⊢ ( 𝜑 → 𝐷 ∈ 𝑇 )
26		dia2dimlem5.dv	⊢ ( 𝜑 → ( 𝐷 ‘ 𝑄 ) = ( 𝐹 ‘ 𝑃 ) )
27		eqid	⊢ ( +g ‘ 𝑌 ) = ( +g ‘ 𝑌 )
28	5 6 8 27	dvavadd	⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝐷 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇 ) ) → ( 𝐷 ( +g ‘ 𝑌 ) 𝐺 ) = ( 𝐷 ∘ 𝐺 ) )
29	14 25 23 28	syl12anc	⊢ ( 𝜑 → ( 𝐷 ( +g ‘ 𝑌 ) 𝐺 ) = ( 𝐷 ∘ 𝐺 ) )
30	18	simpld	⊢ ( 𝜑 → 𝐹 ∈ 𝑇 )
31	1 4 5 6 14 17 30 23 24 25 26	dia2dimlem4	⊢ ( 𝜑 → ( 𝐷 ∘ 𝐺 ) = 𝐹 )
32	29 31	eqtr2d	⊢ ( 𝜑 → 𝐹 = ( 𝐷 ( +g ‘ 𝑌 ) 𝐺 ) )
33	5 8	dvalvec	⊢ ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) → 𝑌 ∈ LVec )
34		lveclmod	⊢ ( 𝑌 ∈ LVec → 𝑌 ∈ LMod )
35	14 33 34	3syl	⊢ ( 𝜑 → 𝑌 ∈ LMod )
36	9	lsssssubg	⊢ ( 𝑌 ∈ LMod → 𝑆 ⊆ ( SubGrp ‘ 𝑌 ) )
37	35 36	syl	⊢ ( 𝜑 → 𝑆 ⊆ ( SubGrp ‘ 𝑌 ) )
38	16	simpld	⊢ ( 𝜑 → 𝑉 ∈ 𝐴 )
39		eqid	⊢ ( Base ‘ 𝐾 ) = ( Base ‘ 𝐾 )
40	39 4	atbase	⊢ ( 𝑉 ∈ 𝐴 → 𝑉 ∈ ( Base ‘ 𝐾 ) )
41	38 40	syl	⊢ ( 𝜑 → 𝑉 ∈ ( Base ‘ 𝐾 ) )
42	16	simprd	⊢ ( 𝜑 → 𝑉 ≤ 𝑊 )
43	39 1 5 8 12 9	dialss	⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑉 ∈ ( Base ‘ 𝐾 ) ∧ 𝑉 ≤ 𝑊 ) ) → ( 𝐼 ‘ 𝑉 ) ∈ 𝑆 )
44	14 41 42 43	syl12anc	⊢ ( 𝜑 → ( 𝐼 ‘ 𝑉 ) ∈ 𝑆 )
45	37 44	sseldd	⊢ ( 𝜑 → ( 𝐼 ‘ 𝑉 ) ∈ ( SubGrp ‘ 𝑌 ) )
46	15	simpld	⊢ ( 𝜑 → 𝑈 ∈ 𝐴 )
47	39 4	atbase	⊢ ( 𝑈 ∈ 𝐴 → 𝑈 ∈ ( Base ‘ 𝐾 ) )
48	46 47	syl	⊢ ( 𝜑 → 𝑈 ∈ ( Base ‘ 𝐾 ) )
49	15	simprd	⊢ ( 𝜑 → 𝑈 ≤ 𝑊 )
50	39 1 5 8 12 9	dialss	⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑈 ∈ ( Base ‘ 𝐾 ) ∧ 𝑈 ≤ 𝑊 ) ) → ( 𝐼 ‘ 𝑈 ) ∈ 𝑆 )
51	14 48 49 50	syl12anc	⊢ ( 𝜑 → ( 𝐼 ‘ 𝑈 ) ∈ 𝑆 )
52	37 51	sseldd	⊢ ( 𝜑 → ( 𝐼 ‘ 𝑈 ) ∈ ( SubGrp ‘ 𝑌 ) )
53	5 6 7 8 12 11	dia1dim2	⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝐷 ∈ 𝑇 ) → ( 𝐼 ‘ ( 𝑅 ‘ 𝐷 ) ) = ( 𝑁 ‘ { 𝐷 } ) )
54	14 25 53	syl2anc	⊢ ( 𝜑 → ( 𝐼 ‘ ( 𝑅 ‘ 𝐷 ) ) = ( 𝑁 ‘ { 𝐷 } ) )
55	1 2 3 4 5 6 7 13 14 15 16 17 18 19 20 21 22 25 26	dia2dimlem3	⊢ ( 𝜑 → ( 𝑅 ‘ 𝐷 ) = 𝑉 )
56	55	fveq2d	⊢ ( 𝜑 → ( 𝐼 ‘ ( 𝑅 ‘ 𝐷 ) ) = ( 𝐼 ‘ 𝑉 ) )
57		eqss	⊢ ( ( 𝐼 ‘ ( 𝑅 ‘ 𝐷 ) ) = ( 𝐼 ‘ 𝑉 ) ↔ ( ( 𝐼 ‘ ( 𝑅 ‘ 𝐷 ) ) ⊆ ( 𝐼 ‘ 𝑉 ) ∧ ( 𝐼 ‘ 𝑉 ) ⊆ ( 𝐼 ‘ ( 𝑅 ‘ 𝐷 ) ) ) )
58	56 57	sylib	⊢ ( 𝜑 → ( ( 𝐼 ‘ ( 𝑅 ‘ 𝐷 ) ) ⊆ ( 𝐼 ‘ 𝑉 ) ∧ ( 𝐼 ‘ 𝑉 ) ⊆ ( 𝐼 ‘ ( 𝑅 ‘ 𝐷 ) ) ) )
59	58	simpld	⊢ ( 𝜑 → ( 𝐼 ‘ ( 𝑅 ‘ 𝐷 ) ) ⊆ ( 𝐼 ‘ 𝑉 ) )
60	54 59	eqsstrrd	⊢ ( 𝜑 → ( 𝑁 ‘ { 𝐷 } ) ⊆ ( 𝐼 ‘ 𝑉 ) )
61		eqid	⊢ ( Base ‘ 𝑌 ) = ( Base ‘ 𝑌 )
62	5 6 8 61	dvavbase	⊢ ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) → ( Base ‘ 𝑌 ) = 𝑇 )
63	14 62	syl	⊢ ( 𝜑 → ( Base ‘ 𝑌 ) = 𝑇 )
64	25 63	eleqtrrd	⊢ ( 𝜑 → 𝐷 ∈ ( Base ‘ 𝑌 ) )
65	61 9 11 35 44 64	ellspsn5b	⊢ ( 𝜑 → ( 𝐷 ∈ ( 𝐼 ‘ 𝑉 ) ↔ ( 𝑁 ‘ { 𝐷 } ) ⊆ ( 𝐼 ‘ 𝑉 ) ) )
66	60 65	mpbird	⊢ ( 𝜑 → 𝐷 ∈ ( 𝐼 ‘ 𝑉 ) )
67	5 6 7 8 12 11	dia1dim2	⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝐺 ∈ 𝑇 ) → ( 𝐼 ‘ ( 𝑅 ‘ 𝐺 ) ) = ( 𝑁 ‘ { 𝐺 } ) )
68	14 23 67	syl2anc	⊢ ( 𝜑 → ( 𝐼 ‘ ( 𝑅 ‘ 𝐺 ) ) = ( 𝑁 ‘ { 𝐺 } ) )
69	1 2 3 4 5 6 7 13 14 15 16 17 18 19 22 23 24	dia2dimlem2	⊢ ( 𝜑 → ( 𝑅 ‘ 𝐺 ) = 𝑈 )
70	69	fveq2d	⊢ ( 𝜑 → ( 𝐼 ‘ ( 𝑅 ‘ 𝐺 ) ) = ( 𝐼 ‘ 𝑈 ) )
71		eqss	⊢ ( ( 𝐼 ‘ ( 𝑅 ‘ 𝐺 ) ) = ( 𝐼 ‘ 𝑈 ) ↔ ( ( 𝐼 ‘ ( 𝑅 ‘ 𝐺 ) ) ⊆ ( 𝐼 ‘ 𝑈 ) ∧ ( 𝐼 ‘ 𝑈 ) ⊆ ( 𝐼 ‘ ( 𝑅 ‘ 𝐺 ) ) ) )
72	70 71	sylib	⊢ ( 𝜑 → ( ( 𝐼 ‘ ( 𝑅 ‘ 𝐺 ) ) ⊆ ( 𝐼 ‘ 𝑈 ) ∧ ( 𝐼 ‘ 𝑈 ) ⊆ ( 𝐼 ‘ ( 𝑅 ‘ 𝐺 ) ) ) )
73	72	simpld	⊢ ( 𝜑 → ( 𝐼 ‘ ( 𝑅 ‘ 𝐺 ) ) ⊆ ( 𝐼 ‘ 𝑈 ) )
74	68 73	eqsstrrd	⊢ ( 𝜑 → ( 𝑁 ‘ { 𝐺 } ) ⊆ ( 𝐼 ‘ 𝑈 ) )
75	23 63	eleqtrrd	⊢ ( 𝜑 → 𝐺 ∈ ( Base ‘ 𝑌 ) )
76	61 9 11 35 51 75	ellspsn5b	⊢ ( 𝜑 → ( 𝐺 ∈ ( 𝐼 ‘ 𝑈 ) ↔ ( 𝑁 ‘ { 𝐺 } ) ⊆ ( 𝐼 ‘ 𝑈 ) ) )
77	74 76	mpbird	⊢ ( 𝜑 → 𝐺 ∈ ( 𝐼 ‘ 𝑈 ) )
78	27 10	lsmelvali	⊢ ( ( ( ( 𝐼 ‘ 𝑉 ) ∈ ( SubGrp ‘ 𝑌 ) ∧ ( 𝐼 ‘ 𝑈 ) ∈ ( SubGrp ‘ 𝑌 ) ) ∧ ( 𝐷 ∈ ( 𝐼 ‘ 𝑉 ) ∧ 𝐺 ∈ ( 𝐼 ‘ 𝑈 ) ) ) → ( 𝐷 ( +g ‘ 𝑌 ) 𝐺 ) ∈ ( ( 𝐼 ‘ 𝑉 ) ⊕ ( 𝐼 ‘ 𝑈 ) ) )
79	45 52 66 77 78	syl22anc	⊢ ( 𝜑 → ( 𝐷 ( +g ‘ 𝑌 ) 𝐺 ) ∈ ( ( 𝐼 ‘ 𝑉 ) ⊕ ( 𝐼 ‘ 𝑈 ) ) )
80	32 79	eqeltrd	⊢ ( 𝜑 → 𝐹 ∈ ( ( 𝐼 ‘ 𝑉 ) ⊕ ( 𝐼 ‘ 𝑈 ) ) )
81		lmodabl	⊢ ( 𝑌 ∈ LMod → 𝑌 ∈ Abel )
82	35 81	syl	⊢ ( 𝜑 → 𝑌 ∈ Abel )
83	10	lsmcom	⊢ ( ( 𝑌 ∈ Abel ∧ ( 𝐼 ‘ 𝑉 ) ∈ ( SubGrp ‘ 𝑌 ) ∧ ( 𝐼 ‘ 𝑈 ) ∈ ( SubGrp ‘ 𝑌 ) ) → ( ( 𝐼 ‘ 𝑉 ) ⊕ ( 𝐼 ‘ 𝑈 ) ) = ( ( 𝐼 ‘ 𝑈 ) ⊕ ( 𝐼 ‘ 𝑉 ) ) )
84	82 45 52 83	syl3anc	⊢ ( 𝜑 → ( ( 𝐼 ‘ 𝑉 ) ⊕ ( 𝐼 ‘ 𝑈 ) ) = ( ( 𝐼 ‘ 𝑈 ) ⊕ ( 𝐼 ‘ 𝑉 ) ) )
85	80 84	eleqtrd	⊢ ( 𝜑 → 𝐹 ∈ ( ( 𝐼 ‘ 𝑈 ) ⊕ ( 𝐼 ‘ 𝑉 ) ) )