Metamath Proof Explorer


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 lspsnel5 ( 𝜑 → ( 𝐷 ∈ ( 𝐼𝑉 ) ↔ ( 𝑁 ‘ { 𝐷 } ) ⊆ ( 𝐼𝑉 ) ) )
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 lspsnel5 ( 𝜑 → ( 𝐺 ∈ ( 𝐼𝑈 ) ↔ ( 𝑁 ‘ { 𝐺 } ) ⊆ ( 𝐼𝑈 ) ) )
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 ( 𝜑𝐹 ∈ ( ( 𝐼𝑈 ) ( 𝐼𝑉 ) ) )