# Metamath Proof Explorer

## Theorem diblss

Description: The value of partial isomorphism B is a subspace of partial vector space H. TODO: use dib* specific theorems instead of dia* ones to shorten proof? (Contributed by NM, 11-Feb-2014)

Ref Expression
Hypotheses diblss.b $⊢ B = Base K$
diblss.l
diblss.h $⊢ H = LHyp ⁡ K$
diblss.u $⊢ U = DVecH ⁡ K ⁡ W$
diblss.i $⊢ I = DIsoB ⁡ K ⁡ W$
diblss.s $⊢ S = LSubSp ⁡ U$
Assertion diblss

### Proof

Step Hyp Ref Expression
1 diblss.b $⊢ B = Base K$
2 diblss.l
3 diblss.h $⊢ H = LHyp ⁡ K$
4 diblss.u $⊢ U = DVecH ⁡ K ⁡ W$
5 diblss.i $⊢ I = DIsoB ⁡ K ⁡ W$
6 diblss.s $⊢ S = LSubSp ⁡ U$
7 eqidd
8 eqid $⊢ TEndo ⁡ K ⁡ W = TEndo ⁡ K ⁡ W$
9 eqid $⊢ Scalar ⁡ U = Scalar ⁡ U$
10 eqid $⊢ Base Scalar ⁡ U = Base Scalar ⁡ U$
11 3 8 4 9 10 dvhbase $⊢ K ∈ HL ∧ W ∈ H → Base Scalar ⁡ U = TEndo ⁡ K ⁡ W$
12 11 eqcomd $⊢ K ∈ HL ∧ W ∈ H → TEndo ⁡ K ⁡ W = Base Scalar ⁡ U$
14 eqid $⊢ LTrn ⁡ K ⁡ W = LTrn ⁡ K ⁡ W$
15 eqid $⊢ Base U = Base U$
16 3 14 8 4 15 dvhvbase $⊢ K ∈ HL ∧ W ∈ H → Base U = LTrn ⁡ K ⁡ W × TEndo ⁡ K ⁡ W$
17 16 eqcomd $⊢ K ∈ HL ∧ W ∈ H → LTrn ⁡ K ⁡ W × TEndo ⁡ K ⁡ W = Base U$
19 eqidd
20 eqidd
21 6 a1i
22 1 2 3 5 4 15 dibss
23 22 18 sseqtrrd
24 1 2 3 5 dibn0
25 fvex $⊢ x ⁡ 1 st ⁡ a ∈ V$
26 vex $⊢ x ∈ V$
27 fvex $⊢ 2 nd ⁡ a ∈ V$
28 26 27 coex $⊢ x ∘ 2 nd ⁡ a ∈ V$
29 25 28 op1st $⊢ 1 st ⁡ x ⁡ 1 st ⁡ a x ∘ 2 nd ⁡ a = x ⁡ 1 st ⁡ a$
30 29 coeq1i $⊢ 1 st ⁡ x ⁡ 1 st ⁡ a x ∘ 2 nd ⁡ a ∘ 1 st ⁡ b = x ⁡ 1 st ⁡ a ∘ 1 st ⁡ b$
31 simpll
32 simpr1
33 simplr
34 simpr2
35 1 2 3 14 5 dibelval1st1
36 31 33 34 35 syl3anc
37 3 14 8 tendocl $⊢ K ∈ HL ∧ W ∈ H ∧ x ∈ TEndo ⁡ K ⁡ W ∧ 1 st ⁡ a ∈ LTrn ⁡ K ⁡ W → x ⁡ 1 st ⁡ a ∈ LTrn ⁡ K ⁡ W$
38 31 32 36 37 syl3anc
39 simpr3
40 1 2 3 14 5 dibelval1st1
41 31 33 39 40 syl3anc
42 3 14 ltrnco $⊢ K ∈ HL ∧ W ∈ H ∧ x ⁡ 1 st ⁡ a ∈ LTrn ⁡ K ⁡ W ∧ 1 st ⁡ b ∈ LTrn ⁡ K ⁡ W → x ⁡ 1 st ⁡ a ∘ 1 st ⁡ b ∈ LTrn ⁡ K ⁡ W$
43 31 38 41 42 syl3anc
44 simplll
45 44 hllatd
46 eqid $⊢ trL ⁡ K ⁡ W = trL ⁡ K ⁡ W$
47 1 3 14 46 trlcl $⊢ K ∈ HL ∧ W ∈ H ∧ x ⁡ 1 st ⁡ a ∘ 1 st ⁡ b ∈ LTrn ⁡ K ⁡ W → trL ⁡ K ⁡ W ⁡ x ⁡ 1 st ⁡ a ∘ 1 st ⁡ b ∈ B$
48 31 43 47 syl2anc
49 1 3 14 46 trlcl $⊢ K ∈ HL ∧ W ∈ H ∧ x ⁡ 1 st ⁡ a ∈ LTrn ⁡ K ⁡ W → trL ⁡ K ⁡ W ⁡ x ⁡ 1 st ⁡ a ∈ B$
50 31 38 49 syl2anc
51 1 3 14 46 trlcl $⊢ K ∈ HL ∧ W ∈ H ∧ 1 st ⁡ b ∈ LTrn ⁡ K ⁡ W → trL ⁡ K ⁡ W ⁡ 1 st ⁡ b ∈ B$
52 31 41 51 syl2anc
53 eqid $⊢ join ⁡ K = join ⁡ K$
54 1 53 latjcl $⊢ K ∈ Lat ∧ trL ⁡ K ⁡ W ⁡ x ⁡ 1 st ⁡ a ∈ B ∧ trL ⁡ K ⁡ W ⁡ 1 st ⁡ b ∈ B → trL ⁡ K ⁡ W ⁡ x ⁡ 1 st ⁡ a join ⁡ K trL ⁡ K ⁡ W ⁡ 1 st ⁡ b ∈ B$
55 45 50 52 54 syl3anc
56 simplrl
57 2 53 3 14 46 trlco
58 31 38 41 57 syl3anc
59 1 3 14 46 trlcl $⊢ K ∈ HL ∧ W ∈ H ∧ 1 st ⁡ a ∈ LTrn ⁡ K ⁡ W → trL ⁡ K ⁡ W ⁡ 1 st ⁡ a ∈ B$
60 31 36 59 syl2anc
61 2 3 14 46 8 tendotp
62 31 32 36 61 syl3anc
63 eqid $⊢ DIsoA ⁡ K ⁡ W = DIsoA ⁡ K ⁡ W$
64 1 2 3 63 5 dibelval1st
65 31 33 34 64 syl3anc
66 1 2 3 14 46 63 diatrl
67 31 33 65 66 syl3anc
68 1 2 45 50 60 56 62 67 lattrd
69 1 2 3 63 5 dibelval1st
70 31 33 39 69 syl3anc
71 1 2 3 14 46 63 diatrl
72 31 33 70 71 syl3anc
73 1 2 53 latjle12
74 45 50 52 56 73 syl13anc
75 68 72 74 mpbi2and
76 1 2 45 48 55 56 58 75 lattrd
77 1 2 3 14 46 63 diaelval
79 43 76 78 mpbir2and
80 30 79 eqeltrid
81 eqid $⊢ s ∈ TEndo ⁡ K ⁡ W , t ∈ TEndo ⁡ K ⁡ W ⟼ h ∈ LTrn ⁡ K ⁡ W ⟼ s ⁡ h ∘ t ⁡ h = s ∈ TEndo ⁡ K ⁡ W , t ∈ TEndo ⁡ K ⁡ W ⟼ h ∈ LTrn ⁡ K ⁡ W ⟼ s ⁡ h ∘ t ⁡ h$
82 eqid $⊢ + Scalar ⁡ U = + Scalar ⁡ U$
83 3 14 8 4 9 81 82 dvhfplusr $⊢ K ∈ HL ∧ W ∈ H → + Scalar ⁡ U = s ∈ TEndo ⁡ K ⁡ W , t ∈ TEndo ⁡ K ⁡ W ⟼ h ∈ LTrn ⁡ K ⁡ W ⟼ s ⁡ h ∘ t ⁡ h$
85 25 28 op2nd $⊢ 2 nd ⁡ x ⁡ 1 st ⁡ a x ∘ 2 nd ⁡ a = x ∘ 2 nd ⁡ a$
86 eqid $⊢ h ∈ LTrn ⁡ K ⁡ W ⟼ I ↾ B = h ∈ LTrn ⁡ K ⁡ W ⟼ I ↾ B$
87 1 2 3 14 86 5 dibelval2nd
88 31 33 34 87 syl3anc
89 88 coeq2d
90 1 3 14 8 86 tendo0mulr $⊢ K ∈ HL ∧ W ∈ H ∧ x ∈ TEndo ⁡ K ⁡ W → x ∘ h ∈ LTrn ⁡ K ⁡ W ⟼ I ↾ B = h ∈ LTrn ⁡ K ⁡ W ⟼ I ↾ B$
91 31 32 90 syl2anc
92 89 91 eqtrd
93 85 92 syl5eq
94 1 2 3 14 86 5 dibelval2nd
95 31 33 39 94 syl3anc
96 84 93 95 oveq123d
97 simpllr
98 1 3 14 8 86 tendo0cl $⊢ K ∈ HL ∧ W ∈ H → h ∈ LTrn ⁡ K ⁡ W ⟼ I ↾ B ∈ TEndo ⁡ K ⁡ W$
100 1 3 14 8 86 81 tendo0pl $⊢ K ∈ HL ∧ W ∈ H ∧ h ∈ LTrn ⁡ K ⁡ W ⟼ I ↾ B ∈ TEndo ⁡ K ⁡ W → h ∈ LTrn ⁡ K ⁡ W ⟼ I ↾ B s ∈ TEndo ⁡ K ⁡ W , t ∈ TEndo ⁡ K ⁡ W ⟼ h ∈ LTrn ⁡ K ⁡ W ⟼ s ⁡ h ∘ t ⁡ h h ∈ LTrn ⁡ K ⁡ W ⟼ I ↾ B = h ∈ LTrn ⁡ K ⁡ W ⟼ I ↾ B$
101 44 97 99 100 syl21anc
102 96 101 eqtrd
103 ovex $⊢ 2 nd ⁡ x ⁡ 1 st ⁡ a x ∘ 2 nd ⁡ a + Scalar ⁡ U 2 nd ⁡ b ∈ V$
104 103 elsn $⊢ 2 nd ⁡ x ⁡ 1 st ⁡ a x ∘ 2 nd ⁡ a + Scalar ⁡ U 2 nd ⁡ b ∈ h ∈ LTrn ⁡ K ⁡ W ⟼ I ↾ B ↔ 2 nd ⁡ x ⁡ 1 st ⁡ a x ∘ 2 nd ⁡ a + Scalar ⁡ U 2 nd ⁡ b = h ∈ LTrn ⁡ K ⁡ W ⟼ I ↾ B$
105 102 104 sylibr
106 opelxpi $⊢ 1 st ⁡ x ⁡ 1 st ⁡ a x ∘ 2 nd ⁡ a ∘ 1 st ⁡ b ∈ DIsoA ⁡ K ⁡ W ⁡ X ∧ 2 nd ⁡ x ⁡ 1 st ⁡ a x ∘ 2 nd ⁡ a + Scalar ⁡ U 2 nd ⁡ b ∈ h ∈ LTrn ⁡ K ⁡ W ⟼ I ↾ B → 1 st ⁡ x ⁡ 1 st ⁡ a x ∘ 2 nd ⁡ a ∘ 1 st ⁡ b 2 nd ⁡ x ⁡ 1 st ⁡ a x ∘ 2 nd ⁡ a + Scalar ⁡ U 2 nd ⁡ b ∈ DIsoA ⁡ K ⁡ W ⁡ X × h ∈ LTrn ⁡ K ⁡ W ⟼ I ↾ B$
107 80 105 106 syl2anc
109 108 34 sseldd
110 eqid $⊢ ⋅ U = ⋅ U$
111 3 14 8 4 110 dvhvsca $⊢ K ∈ HL ∧ W ∈ H ∧ x ∈ TEndo ⁡ K ⁡ W ∧ a ∈ LTrn ⁡ K ⁡ W × TEndo ⁡ K ⁡ W → x ⋅ U a = x ⁡ 1 st ⁡ a x ∘ 2 nd ⁡ a$
112 31 32 109 111 syl12anc
113 112 oveq1d
114 88 99 eqeltrd
115 3 8 tendococl $⊢ K ∈ HL ∧ W ∈ H ∧ x ∈ TEndo ⁡ K ⁡ W ∧ 2 nd ⁡ a ∈ TEndo ⁡ K ⁡ W → x ∘ 2 nd ⁡ a ∈ TEndo ⁡ K ⁡ W$
116 31 32 114 115 syl3anc
117 opelxpi $⊢ x ⁡ 1 st ⁡ a ∈ LTrn ⁡ K ⁡ W ∧ x ∘ 2 nd ⁡ a ∈ TEndo ⁡ K ⁡ W → x ⁡ 1 st ⁡ a x ∘ 2 nd ⁡ a ∈ LTrn ⁡ K ⁡ W × TEndo ⁡ K ⁡ W$
118 38 116 117 syl2anc
119 108 39 sseldd
120 eqid $⊢ + U = + U$
121 3 14 8 4 9 120 82 dvhvadd $⊢ K ∈ HL ∧ W ∈ H ∧ x ⁡ 1 st ⁡ a x ∘ 2 nd ⁡ a ∈ LTrn ⁡ K ⁡ W × TEndo ⁡ K ⁡ W ∧ b ∈ LTrn ⁡ K ⁡ W × TEndo ⁡ K ⁡ W → x ⁡ 1 st ⁡ a x ∘ 2 nd ⁡ a + U b = 1 st ⁡ x ⁡ 1 st ⁡ a x ∘ 2 nd ⁡ a ∘ 1 st ⁡ b 2 nd ⁡ x ⁡ 1 st ⁡ a x ∘ 2 nd ⁡ a + Scalar ⁡ U 2 nd ⁡ b$
122 31 118 119 121 syl12anc
123 113 122 eqtrd
124 1 2 3 14 86 63 5 dibval2