Metamath Proof Explorer

Theorem dialss

Description: The value of partial isomorphism A is a subspace of partial vector space A. Part of Lemma M of Crawley p. 120 line 26. (Contributed by NM, 17-Jan-2014) (Revised by Mario Carneiro, 23-Jun-2014)

Ref Expression
Hypotheses dialss.b 
|- B = ( Base ` K )
dialss.l 
|- .<_ = ( le ` K )
dialss.h 
|- H = ( LHyp ` K )
dialss.u 
|- U = ( ( DVecA ` K ) ` W )
dialss.i 
|- I = ( ( DIsoA ` K ) ` W )
dialss.s 
|- S = ( LSubSp ` U )
Assertion dialss 
|- ( ( ( K e. HL /\ W e. H ) /\ ( X e. B /\ X .<_ W ) ) -> ( I ` X ) e. S )

Proof

Step Hyp Ref Expression
1 dialss.b 
 |-  B = ( Base ` K )
2 dialss.l 
 |-  .<_ = ( le ` K )
3 dialss.h 
 |-  H = ( LHyp ` K )
4 dialss.u 
 |-  U = ( ( DVecA ` K ) ` W )
5 dialss.i 
 |-  I = ( ( DIsoA ` K ) ` W )
6 dialss.s 
 |-  S = ( LSubSp ` U )
7 eqidd 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( X e. B /\ X .<_ W ) ) -> ( Scalar ` U ) = ( Scalar ` U ) )
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 dvabase 
 |-  ( ( K e. HL /\ W e. H ) -> ( Base ` ( Scalar ` U ) ) = ( ( TEndo ` K ) ` W ) )
12 11 eqcomd 
 |-  ( ( K e. HL /\ W e. H ) -> ( ( TEndo ` K ) ` W ) = ( Base ` ( Scalar ` U ) ) )
13 12 adantr 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( X e. B /\ X .<_ W ) ) -> ( ( TEndo ` K ) ` W ) = ( Base ` ( Scalar ` U ) ) )
14 eqid 
 |-  ( ( LTrn ` K ) ` W ) = ( ( LTrn ` K ) ` W )
15 eqid 
 |-  ( Base ` U ) = ( Base ` U )
16 3 14 4 15 dvavbase 
 |-  ( ( K e. HL /\ W e. H ) -> ( Base ` U ) = ( ( LTrn ` K ) ` W ) )
17 16 eqcomd 
 |-  ( ( K e. HL /\ W e. H ) -> ( ( LTrn ` K ) ` W ) = ( Base ` U ) )
18 17 adantr 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( X e. B /\ X .<_ W ) ) -> ( ( LTrn ` K ) ` W ) = ( Base ` U ) )
19 eqidd 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( X e. B /\ X .<_ W ) ) -> ( +g ` U ) = ( +g ` U ) )
20 eqidd 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( X e. B /\ X .<_ W ) ) -> ( .s ` U ) = ( .s ` U ) )
21 6 a1i 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( X e. B /\ X .<_ W ) ) -> S = ( LSubSp ` U ) )
22 1 2 3 14 5 diass 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( X e. B /\ X .<_ W ) ) -> ( I ` X ) C_ ( ( LTrn ` K ) ` W ) )
23 1 2 3 5 dian0 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( X e. B /\ X .<_ W ) ) -> ( I ` X ) =/= (/) )
24 simpll 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ ( X e. B /\ X .<_ W ) ) /\ ( x e. ( ( TEndo ` K ) ` W ) /\ a e. ( I ` X ) /\ b e. ( I ` X ) ) ) -> ( K e. HL /\ W e. H ) )
25 simpr1 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ ( X e. B /\ X .<_ W ) ) /\ ( x e. ( ( TEndo ` K ) ` W ) /\ a e. ( I ` X ) /\ b e. ( I ` X ) ) ) -> x e. ( ( TEndo ` K ) ` W ) )
26 simplr 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ ( X e. B /\ X .<_ W ) ) /\ ( x e. ( ( TEndo ` K ) ` W ) /\ a e. ( I ` X ) /\ b e. ( I ` X ) ) ) -> ( X e. B /\ X .<_ W ) )
27 simpr2 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ ( X e. B /\ X .<_ W ) ) /\ ( x e. ( ( TEndo ` K ) ` W ) /\ a e. ( I ` X ) /\ b e. ( I ` X ) ) ) -> a e. ( I ` X ) )
28 1 2 3 14 5 diael 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( X e. B /\ X .<_ W ) /\ a e. ( I ` X ) ) -> a e. ( ( LTrn ` K ) ` W ) )
29 24 26 27 28 syl3anc 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ ( X e. B /\ X .<_ W ) ) /\ ( x e. ( ( TEndo ` K ) ` W ) /\ a e. ( I ` X ) /\ b e. ( I ` X ) ) ) -> a e. ( ( LTrn ` K ) ` W ) )
30 eqid 
 |-  ( .s ` U ) = ( .s ` U )
31 3 14 8 4 30 dvavsca 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( x e. ( ( TEndo ` K ) ` W ) /\ a e. ( ( LTrn ` K ) ` W ) ) ) -> ( x ( .s ` U ) a ) = ( x ` a ) )
32 24 25 29 31 syl12anc 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ ( X e. B /\ X .<_ W ) ) /\ ( x e. ( ( TEndo ` K ) ` W ) /\ a e. ( I ` X ) /\ b e. ( I ` X ) ) ) -> ( x ( .s ` U ) a ) = ( x ` a ) )
33 32 oveq1d 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ ( X e. B /\ X .<_ W ) ) /\ ( x e. ( ( TEndo ` K ) ` W ) /\ a e. ( I ` X ) /\ b e. ( I ` X ) ) ) -> ( ( x ( .s ` U ) a ) ( +g ` U ) b ) = ( ( x ` a ) ( +g ` U ) b ) )
34 3 14 8 tendocl 
 |-  ( ( ( K e. HL /\ W e. H ) /\ x e. ( ( TEndo ` K ) ` W ) /\ a e. ( ( LTrn ` K ) ` W ) ) -> ( x ` a ) e. ( ( LTrn ` K ) ` W ) )
35 24 25 29 34 syl3anc 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ ( X e. B /\ X .<_ W ) ) /\ ( x e. ( ( TEndo ` K ) ` W ) /\ a e. ( I ` X ) /\ b e. ( I ` X ) ) ) -> ( x ` a ) e. ( ( LTrn ` K ) ` W ) )
36 simpr3 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ ( X e. B /\ X .<_ W ) ) /\ ( x e. ( ( TEndo ` K ) ` W ) /\ a e. ( I ` X ) /\ b e. ( I ` X ) ) ) -> b e. ( I ` X ) )
37 1 2 3 14 5 diael 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( X e. B /\ X .<_ W ) /\ b e. ( I ` X ) ) -> b e. ( ( LTrn ` K ) ` W ) )
38 24 26 36 37 syl3anc 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ ( X e. B /\ X .<_ W ) ) /\ ( x e. ( ( TEndo ` K ) ` W ) /\ a e. ( I ` X ) /\ b e. ( I ` X ) ) ) -> b e. ( ( LTrn ` K ) ` W ) )
39 eqid 
 |-  ( +g ` U ) = ( +g ` U )
40 3 14 4 39 dvavadd 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( ( x ` a ) e. ( ( LTrn ` K ) ` W ) /\ b e. ( ( LTrn ` K ) ` W ) ) ) -> ( ( x ` a ) ( +g ` U ) b ) = ( ( x ` a ) o. b ) )
41 24 35 38 40 syl12anc 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ ( X e. B /\ X .<_ W ) ) /\ ( x e. ( ( TEndo ` K ) ` W ) /\ a e. ( I ` X ) /\ b e. ( I ` X ) ) ) -> ( ( x ` a ) ( +g ` U ) b ) = ( ( x ` a ) o. b ) )
42 33 41 eqtrd 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ ( X e. B /\ X .<_ W ) ) /\ ( x e. ( ( TEndo ` K ) ` W ) /\ a e. ( I ` X ) /\ b e. ( I ` X ) ) ) -> ( ( x ( .s ` U ) a ) ( +g ` U ) b ) = ( ( x ` a ) o. b ) )
43 3 14 ltrnco 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( x ` a ) e. ( ( LTrn ` K ) ` W ) /\ b e. ( ( LTrn ` K ) ` W ) ) -> ( ( x ` a ) o. b ) e. ( ( LTrn ` K ) ` W ) )
44 24 35 38 43 syl3anc 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ ( X e. B /\ X .<_ W ) ) /\ ( x e. ( ( TEndo ` K ) ` W ) /\ a e. ( I ` X ) /\ b e. ( I ` X ) ) ) -> ( ( x ` a ) o. b ) e. ( ( LTrn ` K ) ` W ) )
45 hllat 
 |-  ( K e. HL -> K e. Lat )
46 45 ad3antrrr 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ ( X e. B /\ X .<_ W ) ) /\ ( x e. ( ( TEndo ` K ) ` W ) /\ a e. ( I ` X ) /\ b e. ( I ` X ) ) ) -> K e. Lat )
47 eqid 
 |-  ( ( trL ` K ) ` W ) = ( ( trL ` K ) ` W )
48 1 3 14 47 trlcl 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( ( x ` a ) o. b ) e. ( ( LTrn ` K ) ` W ) ) -> ( ( ( trL ` K ) ` W ) ` ( ( x ` a ) o. b ) ) e. B )
49 24 44 48 syl2anc 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ ( X e. B /\ X .<_ W ) ) /\ ( x e. ( ( TEndo ` K ) ` W ) /\ a e. ( I ` X ) /\ b e. ( I ` X ) ) ) -> ( ( ( trL ` K ) ` W ) ` ( ( x ` a ) o. b ) ) e. B )
50 1 3 14 47 trlcl 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( x ` a ) e. ( ( LTrn ` K ) ` W ) ) -> ( ( ( trL ` K ) ` W ) ` ( x ` a ) ) e. B )
51 24 35 50 syl2anc 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ ( X e. B /\ X .<_ W ) ) /\ ( x e. ( ( TEndo ` K ) ` W ) /\ a e. ( I ` X ) /\ b e. ( I ` X ) ) ) -> ( ( ( trL ` K ) ` W ) ` ( x ` a ) ) e. B )
52 1 3 14 47 trlcl 
 |-  ( ( ( K e. HL /\ W e. H ) /\ b e. ( ( LTrn ` K ) ` W ) ) -> ( ( ( trL ` K ) ` W ) ` b ) e. B )
53 24 38 52 syl2anc 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ ( X e. B /\ X .<_ W ) ) /\ ( x e. ( ( TEndo ` K ) ` W ) /\ a e. ( I ` X ) /\ b e. ( I ` X ) ) ) -> ( ( ( trL ` K ) ` W ) ` b ) e. B )
54 eqid 
 |-  ( join ` K ) = ( join ` K )
55 1 54 latjcl 
 |-  ( ( K e. Lat /\ ( ( ( trL ` K ) ` W ) ` ( x ` a ) ) e. B /\ ( ( ( trL ` K ) ` W ) ` b ) e. B ) -> ( ( ( ( trL ` K ) ` W ) ` ( x ` a ) ) ( join ` K ) ( ( ( trL ` K ) ` W ) ` b ) ) e. B )
56 46 51 53 55 syl3anc 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ ( X e. B /\ X .<_ W ) ) /\ ( x e. ( ( TEndo ` K ) ` W ) /\ a e. ( I ` X ) /\ b e. ( I ` X ) ) ) -> ( ( ( ( trL ` K ) ` W ) ` ( x ` a ) ) ( join ` K ) ( ( ( trL ` K ) ` W ) ` b ) ) e. B )
57 simplrl 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ ( X e. B /\ X .<_ W ) ) /\ ( x e. ( ( TEndo ` K ) ` W ) /\ a e. ( I ` X ) /\ b e. ( I ` X ) ) ) -> X e. B )
58 2 54 3 14 47 trlco 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( x ` a ) e. ( ( LTrn ` K ) ` W ) /\ b e. ( ( LTrn ` K ) ` W ) ) -> ( ( ( trL ` K ) ` W ) ` ( ( x ` a ) o. b ) ) .<_ ( ( ( ( trL ` K ) ` W ) ` ( x ` a ) ) ( join ` K ) ( ( ( trL ` K ) ` W ) ` b ) ) )
59 24 35 38 58 syl3anc 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ ( X e. B /\ X .<_ W ) ) /\ ( x e. ( ( TEndo ` K ) ` W ) /\ a e. ( I ` X ) /\ b e. ( I ` X ) ) ) -> ( ( ( trL ` K ) ` W ) ` ( ( x ` a ) o. b ) ) .<_ ( ( ( ( trL ` K ) ` W ) ` ( x ` a ) ) ( join ` K ) ( ( ( trL ` K ) ` W ) ` b ) ) )
60 1 3 14 47 trlcl 
 |-  ( ( ( K e. HL /\ W e. H ) /\ a e. ( ( LTrn ` K ) ` W ) ) -> ( ( ( trL ` K ) ` W ) ` a ) e. B )
61 24 29 60 syl2anc 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ ( X e. B /\ X .<_ W ) ) /\ ( x e. ( ( TEndo ` K ) ` W ) /\ a e. ( I ` X ) /\ b e. ( I ` X ) ) ) -> ( ( ( trL ` K ) ` W ) ` a ) e. B )
62 2 3 14 47 8 tendotp 
 |-  ( ( ( K e. HL /\ W e. H ) /\ x e. ( ( TEndo ` K ) ` W ) /\ a e. ( ( LTrn ` K ) ` W ) ) -> ( ( ( trL ` K ) ` W ) ` ( x ` a ) ) .<_ ( ( ( trL ` K ) ` W ) ` a ) )
63 24 25 29 62 syl3anc 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ ( X e. B /\ X .<_ W ) ) /\ ( x e. ( ( TEndo ` K ) ` W ) /\ a e. ( I ` X ) /\ b e. ( I ` X ) ) ) -> ( ( ( trL ` K ) ` W ) ` ( x ` a ) ) .<_ ( ( ( trL ` K ) ` W ) ` a ) )
64 1 2 3 14 47 5 diatrl 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( X e. B /\ X .<_ W ) /\ a e. ( I ` X ) ) -> ( ( ( trL ` K ) ` W ) ` a ) .<_ X )
65 24 26 27 64 syl3anc 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ ( X e. B /\ X .<_ W ) ) /\ ( x e. ( ( TEndo ` K ) ` W ) /\ a e. ( I ` X ) /\ b e. ( I ` X ) ) ) -> ( ( ( trL ` K ) ` W ) ` a ) .<_ X )
66 1 2 46 51 61 57 63 65 lattrd 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ ( X e. B /\ X .<_ W ) ) /\ ( x e. ( ( TEndo ` K ) ` W ) /\ a e. ( I ` X ) /\ b e. ( I ` X ) ) ) -> ( ( ( trL ` K ) ` W ) ` ( x ` a ) ) .<_ X )
67 1 2 3 14 47 5 diatrl 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( X e. B /\ X .<_ W ) /\ b e. ( I ` X ) ) -> ( ( ( trL ` K ) ` W ) ` b ) .<_ X )
68 24 26 36 67 syl3anc 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ ( X e. B /\ X .<_ W ) ) /\ ( x e. ( ( TEndo ` K ) ` W ) /\ a e. ( I ` X ) /\ b e. ( I ` X ) ) ) -> ( ( ( trL ` K ) ` W ) ` b ) .<_ X )
69 1 2 54 latjle12 
 |-  ( ( K e. Lat /\ ( ( ( ( trL ` K ) ` W ) ` ( x ` a ) ) e. B /\ ( ( ( trL ` K ) ` W ) ` b ) e. B /\ X e. B ) ) -> ( ( ( ( ( trL ` K ) ` W ) ` ( x ` a ) ) .<_ X /\ ( ( ( trL ` K ) ` W ) ` b ) .<_ X ) <-> ( ( ( ( trL ` K ) ` W ) ` ( x ` a ) ) ( join ` K ) ( ( ( trL ` K ) ` W ) ` b ) ) .<_ X ) )
70 46 51 53 57 69 syl13anc 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ ( X e. B /\ X .<_ W ) ) /\ ( x e. ( ( TEndo ` K ) ` W ) /\ a e. ( I ` X ) /\ b e. ( I ` X ) ) ) -> ( ( ( ( ( trL ` K ) ` W ) ` ( x ` a ) ) .<_ X /\ ( ( ( trL ` K ) ` W ) ` b ) .<_ X ) <-> ( ( ( ( trL ` K ) ` W ) ` ( x ` a ) ) ( join ` K ) ( ( ( trL ` K ) ` W ) ` b ) ) .<_ X ) )
71 66 68 70 mpbi2and 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ ( X e. B /\ X .<_ W ) ) /\ ( x e. ( ( TEndo ` K ) ` W ) /\ a e. ( I ` X ) /\ b e. ( I ` X ) ) ) -> ( ( ( ( trL ` K ) ` W ) ` ( x ` a ) ) ( join ` K ) ( ( ( trL ` K ) ` W ) ` b ) ) .<_ X )
72 1 2 46 49 56 57 59 71 lattrd 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ ( X e. B /\ X .<_ W ) ) /\ ( x e. ( ( TEndo ` K ) ` W ) /\ a e. ( I ` X ) /\ b e. ( I ` X ) ) ) -> ( ( ( trL ` K ) ` W ) ` ( ( x ` a ) o. b ) ) .<_ X )
73 1 2 3 14 47 5 diaelval 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( X e. B /\ X .<_ W ) ) -> ( ( ( x ` a ) o. b ) e. ( I ` X ) <-> ( ( ( x ` a ) o. b ) e. ( ( LTrn ` K ) ` W ) /\ ( ( ( trL ` K ) ` W ) ` ( ( x ` a ) o. b ) ) .<_ X ) ) )
74 73 adantr 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ ( X e. B /\ X .<_ W ) ) /\ ( x e. ( ( TEndo ` K ) ` W ) /\ a e. ( I ` X ) /\ b e. ( I ` X ) ) ) -> ( ( ( x ` a ) o. b ) e. ( I ` X ) <-> ( ( ( x ` a ) o. b ) e. ( ( LTrn ` K ) ` W ) /\ ( ( ( trL ` K ) ` W ) ` ( ( x ` a ) o. b ) ) .<_ X ) ) )
75 44 72 74 mpbir2and 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ ( X e. B /\ X .<_ W ) ) /\ ( x e. ( ( TEndo ` K ) ` W ) /\ a e. ( I ` X ) /\ b e. ( I ` X ) ) ) -> ( ( x ` a ) o. b ) e. ( I ` X ) )
76 42 75 eqeltrd 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ ( X e. B /\ X .<_ W ) ) /\ ( x e. ( ( TEndo ` K ) ` W ) /\ a e. ( I ` X ) /\ b e. ( I ` X ) ) ) -> ( ( x ( .s ` U ) a ) ( +g ` U ) b ) e. ( I ` X ) )
77 7 13 18 19 20 21 22 23 76 islssd 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( X e. B /\ X .<_ W ) ) -> ( I ` X ) e. S )