This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 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 ⊢ ( 𝜑 → 𝐹 ∈ ( ( 𝐼 ‘ 𝑈 ) ⊕ ( 𝐼 ‘ 𝑉 ) ) )