Metamath Proof Explorer

Theorem dicvscacl

Description: Membership in value of the partial isomorphism C is closed under scalar product. (Contributed by NM, 16-Feb-2014) (Revised by Mario Carneiro, 24-Jun-2014)

Ref Expression
Hypotheses dicvscacl.l 
|- .<_ = ( le ` K )
dicvscacl.a 
|- A = ( Atoms ` K )
dicvscacl.h 
|- H = ( LHyp ` K )
dicvscacl.e 
|- E = ( ( TEndo ` K ) ` W )
dicvscacl.u 
|- U = ( ( DVecH ` K ) ` W )
dicvscacl.i 
|- I = ( ( DIsoC ` K ) ` W )
dicvscacl.s 
|- .x. = ( .s ` U )
Assertion dicvscacl 
|- ( ( ( K e. HL /\ W e. H ) /\ ( Q e. A /\ -. Q .<_ W ) /\ ( X e. E /\ Y e. ( I ` Q ) ) ) -> ( X .x. Y ) e. ( I ` Q ) )

Proof

Step Hyp Ref Expression
1 dicvscacl.l 
 |-  .<_ = ( le ` K )
2 dicvscacl.a 
 |-  A = ( Atoms ` K )
3 dicvscacl.h 
 |-  H = ( LHyp ` K )
4 dicvscacl.e 
 |-  E = ( ( TEndo ` K ) ` W )
5 dicvscacl.u 
 |-  U = ( ( DVecH ` K ) ` W )
6 dicvscacl.i 
 |-  I = ( ( DIsoC ` K ) ` W )
7 dicvscacl.s 
 |-  .x. = ( .s ` U )
8 simp1 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( Q e. A /\ -. Q .<_ W ) /\ ( X e. E /\ Y e. ( I ` Q ) ) ) -> ( K e. HL /\ W e. H ) )
9 simp3l 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( Q e. A /\ -. Q .<_ W ) /\ ( X e. E /\ Y e. ( I ` Q ) ) ) -> X e. E )
10 eqid 
 |-  ( Base ` U ) = ( Base ` U )
11 1 2 3 6 5 10 dicssdvh 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( Q e. A /\ -. Q .<_ W ) ) -> ( I ` Q ) C_ ( Base ` U ) )
12 eqid 
 |-  ( ( LTrn ` K ) ` W ) = ( ( LTrn ` K ) ` W )
13 3 12 4 5 10 dvhvbase 
 |-  ( ( K e. HL /\ W e. H ) -> ( Base ` U ) = ( ( ( LTrn ` K ) ` W ) X. E ) )
14 13 eqcomd 
 |-  ( ( K e. HL /\ W e. H ) -> ( ( ( LTrn ` K ) ` W ) X. E ) = ( Base ` U ) )
15 14 adantr 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( Q e. A /\ -. Q .<_ W ) ) -> ( ( ( LTrn ` K ) ` W ) X. E ) = ( Base ` U ) )
16 11 15 sseqtrrd 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( Q e. A /\ -. Q .<_ W ) ) -> ( I ` Q ) C_ ( ( ( LTrn ` K ) ` W ) X. E ) )
17 16 3adant3 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( Q e. A /\ -. Q .<_ W ) /\ ( X e. E /\ Y e. ( I ` Q ) ) ) -> ( I ` Q ) C_ ( ( ( LTrn ` K ) ` W ) X. E ) )
18 simp3r 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( Q e. A /\ -. Q .<_ W ) /\ ( X e. E /\ Y e. ( I ` Q ) ) ) -> Y e. ( I ` Q ) )
19 17 18 sseldd 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( Q e. A /\ -. Q .<_ W ) /\ ( X e. E /\ Y e. ( I ` Q ) ) ) -> Y e. ( ( ( LTrn ` K ) ` W ) X. E ) )
20 3 12 4 5 7 dvhvsca 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( X e. E /\ Y e. ( ( ( LTrn ` K ) ` W ) X. E ) ) ) -> ( X .x. Y ) = <. ( X ` ( 1st ` Y ) ) , ( X o. ( 2nd ` Y ) ) >. )
21 8 9 19 20 syl12anc 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( Q e. A /\ -. Q .<_ W ) /\ ( X e. E /\ Y e. ( I ` Q ) ) ) -> ( X .x. Y ) = <. ( X ` ( 1st ` Y ) ) , ( X o. ( 2nd ` Y ) ) >. )
22 fvi 
 |-  ( X e. E -> ( _I ` X ) = X )
23 9 22 syl 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( Q e. A /\ -. Q .<_ W ) /\ ( X e. E /\ Y e. ( I ` Q ) ) ) -> ( _I ` X ) = X )
24 23 coeq1d 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( Q e. A /\ -. Q .<_ W ) /\ ( X e. E /\ Y e. ( I ` Q ) ) ) -> ( ( _I ` X ) o. ( 2nd ` Y ) ) = ( X o. ( 2nd ` Y ) ) )
25 24 opeq2d 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( Q e. A /\ -. Q .<_ W ) /\ ( X e. E /\ Y e. ( I ` Q ) ) ) -> <. ( X ` ( 1st ` Y ) ) , ( ( _I ` X ) o. ( 2nd ` Y ) ) >. = <. ( X ` ( 1st ` Y ) ) , ( X o. ( 2nd ` Y ) ) >. )
26 21 25 eqtr4d 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( Q e. A /\ -. Q .<_ W ) /\ ( X e. E /\ Y e. ( I ` Q ) ) ) -> ( X .x. Y ) = <. ( X ` ( 1st ` Y ) ) , ( ( _I ` X ) o. ( 2nd ` Y ) ) >. )
27 eqid 
 |-  ( ( oc ` K ) ` W ) = ( ( oc ` K ) ` W )
28 1 2 3 27 12 6 dicelval1sta 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( Q e. A /\ -. Q .<_ W ) /\ Y e. ( I ` Q ) ) -> ( 1st ` Y ) = ( ( 2nd ` Y ) ` ( iota_ g e. ( ( LTrn ` K ) ` W ) ( g ` ( ( oc ` K ) ` W ) ) = Q ) ) )
29 28 3adant3l 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( Q e. A /\ -. Q .<_ W ) /\ ( X e. E /\ Y e. ( I ` Q ) ) ) -> ( 1st ` Y ) = ( ( 2nd ` Y ) ` ( iota_ g e. ( ( LTrn ` K ) ` W ) ( g ` ( ( oc ` K ) ` W ) ) = Q ) ) )
30 29 fveq2d 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( Q e. A /\ -. Q .<_ W ) /\ ( X e. E /\ Y e. ( I ` Q ) ) ) -> ( X ` ( 1st ` Y ) ) = ( X ` ( ( 2nd ` Y ) ` ( iota_ g e. ( ( LTrn ` K ) ` W ) ( g ` ( ( oc ` K ) ` W ) ) = Q ) ) ) )
31 1 2 3 4 6 dicelval2nd 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( Q e. A /\ -. Q .<_ W ) /\ Y e. ( I ` Q ) ) -> ( 2nd ` Y ) e. E )
32 31 3adant3l 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( Q e. A /\ -. Q .<_ W ) /\ ( X e. E /\ Y e. ( I ` Q ) ) ) -> ( 2nd ` Y ) e. E )
33 3 12 4 tendof 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( 2nd ` Y ) e. E ) -> ( 2nd ` Y ) : ( ( LTrn ` K ) ` W ) --> ( ( LTrn ` K ) ` W ) )
34 8 32 33 syl2anc 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( Q e. A /\ -. Q .<_ W ) /\ ( X e. E /\ Y e. ( I ` Q ) ) ) -> ( 2nd ` Y ) : ( ( LTrn ` K ) ` W ) --> ( ( LTrn ` K ) ` W ) )
35 eqid 
 |-  ( oc ` K ) = ( oc ` K )
36 1 35 2 3 lhpocnel 
 |-  ( ( K e. HL /\ W e. H ) -> ( ( ( oc ` K ) ` W ) e. A /\ -. ( ( oc ` K ) ` W ) .<_ W ) )
37 36 3ad2ant1 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( Q e. A /\ -. Q .<_ W ) /\ ( X e. E /\ Y e. ( I ` Q ) ) ) -> ( ( ( oc ` K ) ` W ) e. A /\ -. ( ( oc ` K ) ` W ) .<_ W ) )
38 simp2 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( Q e. A /\ -. Q .<_ W ) /\ ( X e. E /\ Y e. ( I ` Q ) ) ) -> ( Q e. A /\ -. Q .<_ W ) )
39 eqid 
 |-  ( iota_ g e. ( ( LTrn ` K ) ` W ) ( g ` ( ( oc ` K ) ` W ) ) = Q ) = ( iota_ g e. ( ( LTrn ` K ) ` W ) ( g ` ( ( oc ` K ) ` W ) ) = Q )
40 1 2 3 12 39 ltrniotacl 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( ( ( oc ` K ) ` W ) e. A /\ -. ( ( oc ` K ) ` W ) .<_ W ) /\ ( Q e. A /\ -. Q .<_ W ) ) -> ( iota_ g e. ( ( LTrn ` K ) ` W ) ( g ` ( ( oc ` K ) ` W ) ) = Q ) e. ( ( LTrn ` K ) ` W ) )
41 8 37 38 40 syl3anc 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( Q e. A /\ -. Q .<_ W ) /\ ( X e. E /\ Y e. ( I ` Q ) ) ) -> ( iota_ g e. ( ( LTrn ` K ) ` W ) ( g ` ( ( oc ` K ) ` W ) ) = Q ) e. ( ( LTrn ` K ) ` W ) )
42 fvco3 
 |-  ( ( ( 2nd ` Y ) : ( ( LTrn ` K ) ` W ) --> ( ( LTrn ` K ) ` W ) /\ ( iota_ g e. ( ( LTrn ` K ) ` W ) ( g ` ( ( oc ` K ) ` W ) ) = Q ) e. ( ( LTrn ` K ) ` W ) ) -> ( ( X o. ( 2nd ` Y ) ) ` ( iota_ g e. ( ( LTrn ` K ) ` W ) ( g ` ( ( oc ` K ) ` W ) ) = Q ) ) = ( X ` ( ( 2nd ` Y ) ` ( iota_ g e. ( ( LTrn ` K ) ` W ) ( g ` ( ( oc ` K ) ` W ) ) = Q ) ) ) )
43 34 41 42 syl2anc 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( Q e. A /\ -. Q .<_ W ) /\ ( X e. E /\ Y e. ( I ` Q ) ) ) -> ( ( X o. ( 2nd ` Y ) ) ` ( iota_ g e. ( ( LTrn ` K ) ` W ) ( g ` ( ( oc ` K ) ` W ) ) = Q ) ) = ( X ` ( ( 2nd ` Y ) ` ( iota_ g e. ( ( LTrn ` K ) ` W ) ( g ` ( ( oc ` K ) ` W ) ) = Q ) ) ) )
44 30 43 eqtr4d 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( Q e. A /\ -. Q .<_ W ) /\ ( X e. E /\ Y e. ( I ` Q ) ) ) -> ( X ` ( 1st ` Y ) ) = ( ( X o. ( 2nd ` Y ) ) ` ( iota_ g e. ( ( LTrn ` K ) ` W ) ( g ` ( ( oc ` K ) ` W ) ) = Q ) ) )
45 24 fveq1d 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( Q e. A /\ -. Q .<_ W ) /\ ( X e. E /\ Y e. ( I ` Q ) ) ) -> ( ( ( _I ` X ) o. ( 2nd ` Y ) ) ` ( iota_ g e. ( ( LTrn ` K ) ` W ) ( g ` ( ( oc ` K ) ` W ) ) = Q ) ) = ( ( X o. ( 2nd ` Y ) ) ` ( iota_ g e. ( ( LTrn ` K ) ` W ) ( g ` ( ( oc ` K ) ` W ) ) = Q ) ) )
46 44 45 eqtr4d 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( Q e. A /\ -. Q .<_ W ) /\ ( X e. E /\ Y e. ( I ` Q ) ) ) -> ( X ` ( 1st ` Y ) ) = ( ( ( _I ` X ) o. ( 2nd ` Y ) ) ` ( iota_ g e. ( ( LTrn ` K ) ` W ) ( g ` ( ( oc ` K ) ` W ) ) = Q ) ) )
47 3 4 tendococl 
 |-  ( ( ( K e. HL /\ W e. H ) /\ X e. E /\ ( 2nd ` Y ) e. E ) -> ( X o. ( 2nd ` Y ) ) e. E )
48 8 9 32 47 syl3anc 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( Q e. A /\ -. Q .<_ W ) /\ ( X e. E /\ Y e. ( I ` Q ) ) ) -> ( X o. ( 2nd ` Y ) ) e. E )
49 24 48 eqeltrd 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( Q e. A /\ -. Q .<_ W ) /\ ( X e. E /\ Y e. ( I ` Q ) ) ) -> ( ( _I ` X ) o. ( 2nd ` Y ) ) e. E )
50 fvex 
 |-  ( X ` ( 1st ` Y ) ) e. _V
51 fvex 
 |-  ( _I ` X ) e. _V
52 fvex 
 |-  ( 2nd ` Y ) e. _V
53 51 52 coex 
 |-  ( ( _I ` X ) o. ( 2nd ` Y ) ) e. _V
54 1 2 3 27 12 4 6 50 53 dicopelval 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( Q e. A /\ -. Q .<_ W ) ) -> ( <. ( X ` ( 1st ` Y ) ) , ( ( _I ` X ) o. ( 2nd ` Y ) ) >. e. ( I ` Q ) <-> ( ( X ` ( 1st ` Y ) ) = ( ( ( _I ` X ) o. ( 2nd ` Y ) ) ` ( iota_ g e. ( ( LTrn ` K ) ` W ) ( g ` ( ( oc ` K ) ` W ) ) = Q ) ) /\ ( ( _I ` X ) o. ( 2nd ` Y ) ) e. E ) ) )
55 54 3adant3 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( Q e. A /\ -. Q .<_ W ) /\ ( X e. E /\ Y e. ( I ` Q ) ) ) -> ( <. ( X ` ( 1st ` Y ) ) , ( ( _I ` X ) o. ( 2nd ` Y ) ) >. e. ( I ` Q ) <-> ( ( X ` ( 1st ` Y ) ) = ( ( ( _I ` X ) o. ( 2nd ` Y ) ) ` ( iota_ g e. ( ( LTrn ` K ) ` W ) ( g ` ( ( oc ` K ) ` W ) ) = Q ) ) /\ ( ( _I ` X ) o. ( 2nd ` Y ) ) e. E ) ) )
56 46 49 55 mpbir2and 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( Q e. A /\ -. Q .<_ W ) /\ ( X e. E /\ Y e. ( I ` Q ) ) ) -> <. ( X ` ( 1st ` Y ) ) , ( ( _I ` X ) o. ( 2nd ` Y ) ) >. e. ( I ` Q ) )
57 26 56 eqeltrd 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( Q e. A /\ -. Q .<_ W ) /\ ( X e. E /\ Y e. ( I ` Q ) ) ) -> ( X .x. Y ) e. ( I ` Q ) )