Metamath Proof Explorer

Theorem dvalveclem

Description: Lemma for dvalvec . (Contributed by NM, 11-Oct-2013) (Proof shortened by Mario Carneiro, 22-Jun-2014)

Ref Expression
Hypotheses dvalvec.h 
|- H = ( LHyp ` K )
dvalvec.v 
|- U = ( ( DVecA ` K ) ` W )
dvalveclem.t 
|- T = ( ( LTrn ` K ) ` W )
dvalveclem.a 
|- .+ = ( +g ` U )
dvalveclem.e 
|- E = ( ( TEndo ` K ) ` W )
dvalveclem.d 
|- D = ( Scalar ` U )
dvalveclem.b 
|- B = ( Base ` K )
dvalveclem.p 
|- .+^ = ( +g ` D )
dvalveclem.m 
|- .X. = ( .r ` D )
dvalveclem.s 
|- .x. = ( .s ` U )
Assertion dvalveclem 
|- ( ( K e. HL /\ W e. H ) -> U e. LVec )

Proof

Step Hyp Ref Expression
1 dvalvec.h 
 |-  H = ( LHyp ` K )
2 dvalvec.v 
 |-  U = ( ( DVecA ` K ) ` W )
3 dvalveclem.t 
 |-  T = ( ( LTrn ` K ) ` W )
4 dvalveclem.a 
 |-  .+ = ( +g ` U )
5 dvalveclem.e 
 |-  E = ( ( TEndo ` K ) ` W )
6 dvalveclem.d 
 |-  D = ( Scalar ` U )
7 dvalveclem.b 
 |-  B = ( Base ` K )
8 dvalveclem.p 
 |-  .+^ = ( +g ` D )
9 dvalveclem.m 
 |-  .X. = ( .r ` D )
10 dvalveclem.s 
 |-  .x. = ( .s ` U )
11 eqid 
 |-  ( Base ` U ) = ( Base ` U )
12 1 3 2 11 dvavbase 
 |-  ( ( K e. HL /\ W e. H ) -> ( Base ` U ) = T )
13 12 eqcomd 
 |-  ( ( K e. HL /\ W e. H ) -> T = ( Base ` U ) )
14 4 a1i 
 |-  ( ( K e. HL /\ W e. H ) -> .+ = ( +g ` U ) )
15 6 a1i 
 |-  ( ( K e. HL /\ W e. H ) -> D = ( Scalar ` U ) )
16 10 a1i 
 |-  ( ( K e. HL /\ W e. H ) -> .x. = ( .s ` U ) )
17 eqid 
 |-  ( Base ` D ) = ( Base ` D )
18 1 5 2 6 17 dvabase 
 |-  ( ( K e. HL /\ W e. H ) -> ( Base ` D ) = E )
19 18 eqcomd 
 |-  ( ( K e. HL /\ W e. H ) -> E = ( Base ` D ) )
20 8 a1i 
 |-  ( ( K e. HL /\ W e. H ) -> .+^ = ( +g ` D ) )
21 9 a1i 
 |-  ( ( K e. HL /\ W e. H ) -> .X. = ( .r ` D ) )
22 1 3 5 tendoidcl 
 |-  ( ( K e. HL /\ W e. H ) -> ( _I |` T ) e. E )
23 22 19 eleqtrd 
 |-  ( ( K e. HL /\ W e. H ) -> ( _I |` T ) e. ( Base ` D ) )
24 eqid 
 |-  ( f e. T |-> ( _I |` B ) ) = ( f e. T |-> ( _I |` B ) )
25 7 1 3 5 24 tendo1ne0 
 |-  ( ( K e. HL /\ W e. H ) -> ( _I |` T ) =/= ( f e. T |-> ( _I |` B ) ) )
26 eqid 
 |-  ( ( EDRing ` K ) ` W ) = ( ( EDRing ` K ) ` W )
27 1 26 2 6 dvasca 
 |-  ( ( K e. HL /\ W e. H ) -> D = ( ( EDRing ` K ) ` W ) )
28 27 fveq2d 
 |-  ( ( K e. HL /\ W e. H ) -> ( 0g ` D ) = ( 0g ` ( ( EDRing ` K ) ` W ) ) )
29 eqid 
 |-  ( 0g ` ( ( EDRing ` K ) ` W ) ) = ( 0g ` ( ( EDRing ` K ) ` W ) )
30 7 1 3 26 24 29 erng0g 
 |-  ( ( K e. HL /\ W e. H ) -> ( 0g ` ( ( EDRing ` K ) ` W ) ) = ( f e. T |-> ( _I |` B ) ) )
31 28 30 eqtrd 
 |-  ( ( K e. HL /\ W e. H ) -> ( 0g ` D ) = ( f e. T |-> ( _I |` B ) ) )
32 25 31 neeqtrrd 
 |-  ( ( K e. HL /\ W e. H ) -> ( _I |` T ) =/= ( 0g ` D ) )
33 22 22 jca 
 |-  ( ( K e. HL /\ W e. H ) -> ( ( _I |` T ) e. E /\ ( _I |` T ) e. E ) )
34 1 3 5 2 6 9 dvamulr 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( ( _I |` T ) e. E /\ ( _I |` T ) e. E ) ) -> ( ( _I |` T ) .X. ( _I |` T ) ) = ( ( _I |` T ) o. ( _I |` T ) ) )
35 33 34 mpdan 
 |-  ( ( K e. HL /\ W e. H ) -> ( ( _I |` T ) .X. ( _I |` T ) ) = ( ( _I |` T ) o. ( _I |` T ) ) )
36 f1oi 
 |-  ( _I |` T ) : T -1-1-onto-> T
37 f1of 
 |-  ( ( _I |` T ) : T -1-1-onto-> T -> ( _I |` T ) : T --> T )
38 fcoi2 
 |-  ( ( _I |` T ) : T --> T -> ( ( _I |` T ) o. ( _I |` T ) ) = ( _I |` T ) )
39 36 37 38 mp2b 
 |-  ( ( _I |` T ) o. ( _I |` T ) ) = ( _I |` T )
40 35 39 eqtrdi 
 |-  ( ( K e. HL /\ W e. H ) -> ( ( _I |` T ) .X. ( _I |` T ) ) = ( _I |` T ) )
41 23 32 40 3jca 
 |-  ( ( K e. HL /\ W e. H ) -> ( ( _I |` T ) e. ( Base ` D ) /\ ( _I |` T ) =/= ( 0g ` D ) /\ ( ( _I |` T ) .X. ( _I |` T ) ) = ( _I |` T ) ) )
42 1 26 erngdv 
 |-  ( ( K e. HL /\ W e. H ) -> ( ( EDRing ` K ) ` W ) e. DivRing )
43 27 42 eqeltrd 
 |-  ( ( K e. HL /\ W e. H ) -> D e. DivRing )
44 eqid 
 |-  ( 0g ` D ) = ( 0g ` D )
45 eqid 
 |-  ( 1r ` D ) = ( 1r ` D )
46 17 9 44 45 drngid2 
 |-  ( D e. DivRing -> ( ( ( _I |` T ) e. ( Base ` D ) /\ ( _I |` T ) =/= ( 0g ` D ) /\ ( ( _I |` T ) .X. ( _I |` T ) ) = ( _I |` T ) ) <-> ( 1r ` D ) = ( _I |` T ) ) )
47 43 46 syl 
 |-  ( ( K e. HL /\ W e. H ) -> ( ( ( _I |` T ) e. ( Base ` D ) /\ ( _I |` T ) =/= ( 0g ` D ) /\ ( ( _I |` T ) .X. ( _I |` T ) ) = ( _I |` T ) ) <-> ( 1r ` D ) = ( _I |` T ) ) )
48 41 47 mpbid 
 |-  ( ( K e. HL /\ W e. H ) -> ( 1r ` D ) = ( _I |` T ) )
49 48 eqcomd 
 |-  ( ( K e. HL /\ W e. H ) -> ( _I |` T ) = ( 1r ` D ) )
50 drngring 
 |-  ( D e. DivRing -> D e. Ring )
51 43 50 syl 
 |-  ( ( K e. HL /\ W e. H ) -> D e. Ring )
52 1 2 dvaabl 
 |-  ( ( K e. HL /\ W e. H ) -> U e. Abel )
53 ablgrp 
 |-  ( U e. Abel -> U e. Grp )
54 52 53 syl 
 |-  ( ( K e. HL /\ W e. H ) -> U e. Grp )
55 1 3 5 2 10 dvavsca 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( s e. E /\ t e. T ) ) -> ( s .x. t ) = ( s ` t ) )
56 55 3impb 
 |-  ( ( ( K e. HL /\ W e. H ) /\ s e. E /\ t e. T ) -> ( s .x. t ) = ( s ` t ) )
57 1 3 5 tendocl 
 |-  ( ( ( K e. HL /\ W e. H ) /\ s e. E /\ t e. T ) -> ( s ` t ) e. T )
58 56 57 eqeltrd 
 |-  ( ( ( K e. HL /\ W e. H ) /\ s e. E /\ t e. T ) -> ( s .x. t ) e. T )
59 1 3 5 tendospdi1 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( s e. E /\ t e. T /\ f e. T ) ) -> ( s ` ( t o. f ) ) = ( ( s ` t ) o. ( s ` f ) ) )
60 simpr1 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( s e. E /\ t e. T /\ f e. T ) ) -> s e. E )
61 1 3 ltrnco 
 |-  ( ( ( K e. HL /\ W e. H ) /\ t e. T /\ f e. T ) -> ( t o. f ) e. T )
62 61 3adant3r1 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( s e. E /\ t e. T /\ f e. T ) ) -> ( t o. f ) e. T )
63 60 62 jca 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( s e. E /\ t e. T /\ f e. T ) ) -> ( s e. E /\ ( t o. f ) e. T ) )
64 1 3 5 2 10 dvavsca 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( s e. E /\ ( t o. f ) e. T ) ) -> ( s .x. ( t o. f ) ) = ( s ` ( t o. f ) ) )
65 63 64 syldan 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( s e. E /\ t e. T /\ f e. T ) ) -> ( s .x. ( t o. f ) ) = ( s ` ( t o. f ) ) )
66 57 3adant3r3 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( s e. E /\ t e. T /\ f e. T ) ) -> ( s ` t ) e. T )
67 1 3 5 tendocl 
 |-  ( ( ( K e. HL /\ W e. H ) /\ s e. E /\ f e. T ) -> ( s ` f ) e. T )
68 67 3adant3r2 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( s e. E /\ t e. T /\ f e. T ) ) -> ( s ` f ) e. T )
69 66 68 jca 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( s e. E /\ t e. T /\ f e. T ) ) -> ( ( s ` t ) e. T /\ ( s ` f ) e. T ) )
70 1 3 2 4 dvavadd 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( ( s ` t ) e. T /\ ( s ` f ) e. T ) ) -> ( ( s ` t ) .+ ( s ` f ) ) = ( ( s ` t ) o. ( s ` f ) ) )
71 69 70 syldan 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( s e. E /\ t e. T /\ f e. T ) ) -> ( ( s ` t ) .+ ( s ` f ) ) = ( ( s ` t ) o. ( s ` f ) ) )
72 59 65 71 3eqtr4d 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( s e. E /\ t e. T /\ f e. T ) ) -> ( s .x. ( t o. f ) ) = ( ( s ` t ) .+ ( s ` f ) ) )
73 1 3 2 4 dvavadd 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( t e. T /\ f e. T ) ) -> ( t .+ f ) = ( t o. f ) )
74 73 3adantr1 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( s e. E /\ t e. T /\ f e. T ) ) -> ( t .+ f ) = ( t o. f ) )
75 74 oveq2d 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( s e. E /\ t e. T /\ f e. T ) ) -> ( s .x. ( t .+ f ) ) = ( s .x. ( t o. f ) ) )
76 55 3adantr3 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( s e. E /\ t e. T /\ f e. T ) ) -> ( s .x. t ) = ( s ` t ) )
77 1 3 5 2 10 dvavsca 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( s e. E /\ f e. T ) ) -> ( s .x. f ) = ( s ` f ) )
78 77 3adantr2 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( s e. E /\ t e. T /\ f e. T ) ) -> ( s .x. f ) = ( s ` f ) )
79 76 78 oveq12d 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( s e. E /\ t e. T /\ f e. T ) ) -> ( ( s .x. t ) .+ ( s .x. f ) ) = ( ( s ` t ) .+ ( s ` f ) ) )
80 72 75 79 3eqtr4d 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( s e. E /\ t e. T /\ f e. T ) ) -> ( s .x. ( t .+ f ) ) = ( ( s .x. t ) .+ ( s .x. f ) ) )
81 1 3 5 2 6 8 dvaplusgv 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( s e. E /\ t e. E /\ f e. T ) ) -> ( ( s .+^ t ) ` f ) = ( ( s ` f ) o. ( t ` f ) ) )
82 1 3 5 2 6 8 dvafplusg 
 |-  ( ( K e. HL /\ W e. H ) -> .+^ = ( a e. E , b e. E |-> ( f e. T |-> ( ( a ` f ) o. ( b ` f ) ) ) ) )
83 82 3ad2ant1 
 |-  ( ( ( K e. HL /\ W e. H ) /\ s e. E /\ t e. E ) -> .+^ = ( a e. E , b e. E |-> ( f e. T |-> ( ( a ` f ) o. ( b ` f ) ) ) ) )
84 83 oveqd 
 |-  ( ( ( K e. HL /\ W e. H ) /\ s e. E /\ t e. E ) -> ( s .+^ t ) = ( s ( a e. E , b e. E |-> ( f e. T |-> ( ( a ` f ) o. ( b ` f ) ) ) ) t ) )
85 eqid 
 |-  ( a e. E , b e. E |-> ( f e. T |-> ( ( a ` f ) o. ( b ` f ) ) ) ) = ( a e. E , b e. E |-> ( f e. T |-> ( ( a ` f ) o. ( b ` f ) ) ) )
86 1 3 5 85 tendoplcl 
 |-  ( ( ( K e. HL /\ W e. H ) /\ s e. E /\ t e. E ) -> ( s ( a e. E , b e. E |-> ( f e. T |-> ( ( a ` f ) o. ( b ` f ) ) ) ) t ) e. E )
87 84 86 eqeltrd 
 |-  ( ( ( K e. HL /\ W e. H ) /\ s e. E /\ t e. E ) -> ( s .+^ t ) e. E )
88 87 3adant3r3 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( s e. E /\ t e. E /\ f e. T ) ) -> ( s .+^ t ) e. E )
89 simpr3 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( s e. E /\ t e. E /\ f e. T ) ) -> f e. T )
90 88 89 jca 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( s e. E /\ t e. E /\ f e. T ) ) -> ( ( s .+^ t ) e. E /\ f e. T ) )
91 1 3 5 2 10 dvavsca 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( ( s .+^ t ) e. E /\ f e. T ) ) -> ( ( s .+^ t ) .x. f ) = ( ( s .+^ t ) ` f ) )
92 90 91 syldan 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( s e. E /\ t e. E /\ f e. T ) ) -> ( ( s .+^ t ) .x. f ) = ( ( s .+^ t ) ` f ) )
93 77 3adantr2 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( s e. E /\ t e. E /\ f e. T ) ) -> ( s .x. f ) = ( s ` f ) )
94 1 3 5 2 10 dvavsca 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( t e. E /\ f e. T ) ) -> ( t .x. f ) = ( t ` f ) )
95 94 3adantr1 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( s e. E /\ t e. E /\ f e. T ) ) -> ( t .x. f ) = ( t ` f ) )
96 93 95 oveq12d 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( s e. E /\ t e. E /\ f e. T ) ) -> ( ( s .x. f ) .+ ( t .x. f ) ) = ( ( s ` f ) .+ ( t ` f ) ) )
97 67 3adant3r2 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( s e. E /\ t e. E /\ f e. T ) ) -> ( s ` f ) e. T )
98 1 3 5 tendospcl 
 |-  ( ( ( K e. HL /\ W e. H ) /\ t e. E /\ f e. T ) -> ( t ` f ) e. T )
99 98 3adant3r1 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( s e. E /\ t e. E /\ f e. T ) ) -> ( t ` f ) e. T )
100 97 99 jca 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( s e. E /\ t e. E /\ f e. T ) ) -> ( ( s ` f ) e. T /\ ( t ` f ) e. T ) )
101 1 3 2 4 dvavadd 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( ( s ` f ) e. T /\ ( t ` f ) e. T ) ) -> ( ( s ` f ) .+ ( t ` f ) ) = ( ( s ` f ) o. ( t ` f ) ) )
102 100 101 syldan 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( s e. E /\ t e. E /\ f e. T ) ) -> ( ( s ` f ) .+ ( t ` f ) ) = ( ( s ` f ) o. ( t ` f ) ) )
103 96 102 eqtrd 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( s e. E /\ t e. E /\ f e. T ) ) -> ( ( s .x. f ) .+ ( t .x. f ) ) = ( ( s ` f ) o. ( t ` f ) ) )
104 81 92 103 3eqtr4d 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( s e. E /\ t e. E /\ f e. T ) ) -> ( ( s .+^ t ) .x. f ) = ( ( s .x. f ) .+ ( t .x. f ) ) )
105 1 3 5 tendospass 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( s e. E /\ t e. E /\ f e. T ) ) -> ( ( s o. t ) ` f ) = ( s ` ( t ` f ) ) )
106 1 5 tendococl 
 |-  ( ( ( K e. HL /\ W e. H ) /\ s e. E /\ t e. E ) -> ( s o. t ) e. E )
107 106 3adant3r3 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( s e. E /\ t e. E /\ f e. T ) ) -> ( s o. t ) e. E )
108 107 89 jca 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( s e. E /\ t e. E /\ f e. T ) ) -> ( ( s o. t ) e. E /\ f e. T ) )
109 1 3 5 2 10 dvavsca 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( ( s o. t ) e. E /\ f e. T ) ) -> ( ( s o. t ) .x. f ) = ( ( s o. t ) ` f ) )
110 108 109 syldan 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( s e. E /\ t e. E /\ f e. T ) ) -> ( ( s o. t ) .x. f ) = ( ( s o. t ) ` f ) )
111 simpr1 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( s e. E /\ t e. E /\ f e. T ) ) -> s e. E )
112 111 99 jca 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( s e. E /\ t e. E /\ f e. T ) ) -> ( s e. E /\ ( t ` f ) e. T ) )
113 1 3 5 2 10 dvavsca 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( s e. E /\ ( t ` f ) e. T ) ) -> ( s .x. ( t ` f ) ) = ( s ` ( t ` f ) ) )
114 112 113 syldan 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( s e. E /\ t e. E /\ f e. T ) ) -> ( s .x. ( t ` f ) ) = ( s ` ( t ` f ) ) )
115 105 110 114 3eqtr4d 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( s e. E /\ t e. E /\ f e. T ) ) -> ( ( s o. t ) .x. f ) = ( s .x. ( t ` f ) ) )
116 1 3 5 2 6 9 dvamulr 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( s e. E /\ t e. E ) ) -> ( s .X. t ) = ( s o. t ) )
117 116 3adantr3 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( s e. E /\ t e. E /\ f e. T ) ) -> ( s .X. t ) = ( s o. t ) )
118 117 oveq1d 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( s e. E /\ t e. E /\ f e. T ) ) -> ( ( s .X. t ) .x. f ) = ( ( s o. t ) .x. f ) )
119 95 oveq2d 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( s e. E /\ t e. E /\ f e. T ) ) -> ( s .x. ( t .x. f ) ) = ( s .x. ( t ` f ) ) )
120 115 118 119 3eqtr4d 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( s e. E /\ t e. E /\ f e. T ) ) -> ( ( s .X. t ) .x. f ) = ( s .x. ( t .x. f ) ) )
121 22 anim1i 
 |-  ( ( ( K e. HL /\ W e. H ) /\ s e. T ) -> ( ( _I |` T ) e. E /\ s e. T ) )
122 1 3 5 2 10 dvavsca 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( ( _I |` T ) e. E /\ s e. T ) ) -> ( ( _I |` T ) .x. s ) = ( ( _I |` T ) ` s ) )
123 121 122 syldan 
 |-  ( ( ( K e. HL /\ W e. H ) /\ s e. T ) -> ( ( _I |` T ) .x. s ) = ( ( _I |` T ) ` s ) )
124 fvresi 
 |-  ( s e. T -> ( ( _I |` T ) ` s ) = s )
125 124 adantl 
 |-  ( ( ( K e. HL /\ W e. H ) /\ s e. T ) -> ( ( _I |` T ) ` s ) = s )
126 123 125 eqtrd 
 |-  ( ( ( K e. HL /\ W e. H ) /\ s e. T ) -> ( ( _I |` T ) .x. s ) = s )
127 13 14 15 16 19 20 21 49 51 54 58 80 104 120 126 islmodd 
 |-  ( ( K e. HL /\ W e. H ) -> U e. LMod )
128 6 islvec 
 |-  ( U e. LVec <-> ( U e. LMod /\ D e. DivRing ) )
129 127 43 128 sylanbrc 
 |-  ( ( K e. HL /\ W e. H ) -> U e. LVec )