Metamath Proof Explorer

Theorem dicvaddcl

Description: Membership in value of the partial isomorphism C is closed under vector sum. (Contributed by NM, 16-Feb-2014)

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

Proof

Step Hyp Ref Expression
1 dicvaddcl.l 
 |-  .<_ = ( le ` K )
2 dicvaddcl.a 
 |-  A = ( Atoms ` K )
3 dicvaddcl.h 
 |-  H = ( LHyp ` K )
4 dicvaddcl.u 
 |-  U = ( ( DVecH ` K ) ` W )
5 dicvaddcl.i 
 |-  I = ( ( DIsoC ` K ) ` W )
6 dicvaddcl.p 
 |-  .+ = ( +g ` U )
7 simp1 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( Q e. A /\ -. Q .<_ W ) /\ ( X e. ( I ` Q ) /\ Y e. ( I ` Q ) ) ) -> ( K e. HL /\ W e. H ) )
8 eqid 
 |-  ( Base ` U ) = ( Base ` U )
9 1 2 3 5 4 8 dicssdvh 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( Q e. A /\ -. Q .<_ W ) ) -> ( I ` Q ) C_ ( Base ` U ) )
10 eqid 
 |-  ( ( LTrn ` K ) ` W ) = ( ( LTrn ` K ) ` W )
11 eqid 
 |-  ( ( TEndo ` K ) ` W ) = ( ( TEndo ` K ) ` W )
12 3 10 11 4 8 dvhvbase 
 |-  ( ( K e. HL /\ W e. H ) -> ( Base ` U ) = ( ( ( LTrn ` K ) ` W ) X. ( ( TEndo ` K ) ` W ) ) )
13 12 eqcomd 
 |-  ( ( K e. HL /\ W e. H ) -> ( ( ( LTrn ` K ) ` W ) X. ( ( TEndo ` K ) ` W ) ) = ( Base ` U ) )
14 13 adantr 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( Q e. A /\ -. Q .<_ W ) ) -> ( ( ( LTrn ` K ) ` W ) X. ( ( TEndo ` K ) ` W ) ) = ( Base ` U ) )
15 9 14 sseqtrrd 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( Q e. A /\ -. Q .<_ W ) ) -> ( I ` Q ) C_ ( ( ( LTrn ` K ) ` W ) X. ( ( TEndo ` K ) ` W ) ) )
16 15 3adant3 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( Q e. A /\ -. Q .<_ W ) /\ ( X e. ( I ` Q ) /\ Y e. ( I ` Q ) ) ) -> ( I ` Q ) C_ ( ( ( LTrn ` K ) ` W ) X. ( ( TEndo ` K ) ` W ) ) )
17 simp3l 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( Q e. A /\ -. Q .<_ W ) /\ ( X e. ( I ` Q ) /\ Y e. ( I ` Q ) ) ) -> X e. ( I ` Q ) )
18 16 17 sseldd 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( Q e. A /\ -. Q .<_ W ) /\ ( X e. ( I ` Q ) /\ Y e. ( I ` Q ) ) ) -> X e. ( ( ( LTrn ` K ) ` W ) X. ( ( TEndo ` K ) ` W ) ) )
19 simp3r 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( Q e. A /\ -. Q .<_ W ) /\ ( X e. ( I ` Q ) /\ Y e. ( I ` Q ) ) ) -> Y e. ( I ` Q ) )
20 16 19 sseldd 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( Q e. A /\ -. Q .<_ W ) /\ ( X e. ( I ` Q ) /\ Y e. ( I ` Q ) ) ) -> Y e. ( ( ( LTrn ` K ) ` W ) X. ( ( TEndo ` K ) ` W ) ) )
21 eqid 
 |-  ( Scalar ` U ) = ( Scalar ` U )
22 eqid 
 |-  ( +g ` ( Scalar ` U ) ) = ( +g ` ( Scalar ` U ) )
23 3 10 11 4 21 6 22 dvhvadd 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( X e. ( ( ( LTrn ` K ) ` W ) X. ( ( TEndo ` K ) ` W ) ) /\ Y e. ( ( ( LTrn ` K ) ` W ) X. ( ( TEndo ` K ) ` W ) ) ) ) -> ( X .+ Y ) = <. ( ( 1st ` X ) o. ( 1st ` Y ) ) , ( ( 2nd ` X ) ( +g ` ( Scalar ` U ) ) ( 2nd ` Y ) ) >. )
24 7 18 20 23 syl12anc 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( Q e. A /\ -. Q .<_ W ) /\ ( X e. ( I ` Q ) /\ Y e. ( I ` Q ) ) ) -> ( X .+ Y ) = <. ( ( 1st ` X ) o. ( 1st ` Y ) ) , ( ( 2nd ` X ) ( +g ` ( Scalar ` U ) ) ( 2nd ` Y ) ) >. )
25 1 2 3 11 5 dicelval2nd 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( Q e. A /\ -. Q .<_ W ) /\ X e. ( I ` Q ) ) -> ( 2nd ` X ) e. ( ( TEndo ` K ) ` W ) )
26 25 3adant3r 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( Q e. A /\ -. Q .<_ W ) /\ ( X e. ( I ` Q ) /\ Y e. ( I ` Q ) ) ) -> ( 2nd ` X ) e. ( ( TEndo ` K ) ` W ) )
27 1 2 3 11 5 dicelval2nd 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( Q e. A /\ -. Q .<_ W ) /\ Y e. ( I ` Q ) ) -> ( 2nd ` Y ) e. ( ( TEndo ` K ) ` W ) )
28 27 3adant3l 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( Q e. A /\ -. Q .<_ W ) /\ ( X e. ( I ` Q ) /\ Y e. ( I ` Q ) ) ) -> ( 2nd ` Y ) e. ( ( TEndo ` K ) ` W ) )
29 eqid 
 |-  ( oc ` K ) = ( oc ` K )
30 1 29 2 3 lhpocnel 
 |-  ( ( K e. HL /\ W e. H ) -> ( ( ( oc ` K ) ` W ) e. A /\ -. ( ( oc ` K ) ` W ) .<_ W ) )
31 30 3ad2ant1 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( Q e. A /\ -. Q .<_ W ) /\ ( X e. ( I ` Q ) /\ Y e. ( I ` Q ) ) ) -> ( ( ( oc ` K ) ` W ) e. A /\ -. ( ( oc ` K ) ` W ) .<_ W ) )
32 simp2 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( Q e. A /\ -. Q .<_ W ) /\ ( X e. ( I ` Q ) /\ Y e. ( I ` Q ) ) ) -> ( Q e. A /\ -. Q .<_ W ) )
33 eqid 
 |-  ( iota_ g e. ( ( LTrn ` K ) ` W ) ( g ` ( ( oc ` K ) ` W ) ) = Q ) = ( iota_ g e. ( ( LTrn ` K ) ` W ) ( g ` ( ( oc ` K ) ` W ) ) = Q )
34 1 2 3 10 33 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 ) )
35 7 31 32 34 syl3anc 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( Q e. A /\ -. Q .<_ W ) /\ ( X e. ( I ` Q ) /\ Y e. ( I ` Q ) ) ) -> ( iota_ g e. ( ( LTrn ` K ) ` W ) ( g ` ( ( oc ` K ) ` W ) ) = Q ) e. ( ( LTrn ` K ) ` W ) )
36 eqid 
 |-  ( s e. ( ( TEndo ` K ) ` W ) , t e. ( ( TEndo ` K ) ` W ) |-> ( h e. ( ( LTrn ` K ) ` W ) |-> ( ( s ` h ) o. ( t ` h ) ) ) ) = ( s e. ( ( TEndo ` K ) ` W ) , t e. ( ( TEndo ` K ) ` W ) |-> ( h e. ( ( LTrn ` K ) ` W ) |-> ( ( s ` h ) o. ( t ` h ) ) ) )
37 10 36 tendospdi2 
 |-  ( ( ( 2nd ` X ) e. ( ( TEndo ` K ) ` W ) /\ ( 2nd ` Y ) e. ( ( TEndo ` K ) ` W ) /\ ( iota_ g e. ( ( LTrn ` K ) ` W ) ( g ` ( ( oc ` K ) ` W ) ) = Q ) e. ( ( LTrn ` K ) ` W ) ) -> ( ( ( 2nd ` X ) ( s e. ( ( TEndo ` K ) ` W ) , t e. ( ( TEndo ` K ) ` W ) |-> ( h e. ( ( LTrn ` K ) ` W ) |-> ( ( s ` h ) o. ( t ` h ) ) ) ) ( 2nd ` Y ) ) ` ( iota_ g e. ( ( LTrn ` K ) ` W ) ( g ` ( ( oc ` K ) ` W ) ) = Q ) ) = ( ( ( 2nd ` X ) ` ( iota_ g e. ( ( LTrn ` K ) ` W ) ( g ` ( ( oc ` K ) ` W ) ) = Q ) ) o. ( ( 2nd ` Y ) ` ( iota_ g e. ( ( LTrn ` K ) ` W ) ( g ` ( ( oc ` K ) ` W ) ) = Q ) ) ) )
38 26 28 35 37 syl3anc 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( Q e. A /\ -. Q .<_ W ) /\ ( X e. ( I ` Q ) /\ Y e. ( I ` Q ) ) ) -> ( ( ( 2nd ` X ) ( s e. ( ( TEndo ` K ) ` W ) , t e. ( ( TEndo ` K ) ` W ) |-> ( h e. ( ( LTrn ` K ) ` W ) |-> ( ( s ` h ) o. ( t ` h ) ) ) ) ( 2nd ` Y ) ) ` ( iota_ g e. ( ( LTrn ` K ) ` W ) ( g ` ( ( oc ` K ) ` W ) ) = Q ) ) = ( ( ( 2nd ` X ) ` ( iota_ g e. ( ( LTrn ` K ) ` W ) ( g ` ( ( oc ` K ) ` W ) ) = Q ) ) o. ( ( 2nd ` Y ) ` ( iota_ g e. ( ( LTrn ` K ) ` W ) ( g ` ( ( oc ` K ) ` W ) ) = Q ) ) ) )
39 3 10 11 4 21 36 22 dvhfplusr 
 |-  ( ( K e. HL /\ W e. H ) -> ( +g ` ( Scalar ` U ) ) = ( s e. ( ( TEndo ` K ) ` W ) , t e. ( ( TEndo ` K ) ` W ) |-> ( h e. ( ( LTrn ` K ) ` W ) |-> ( ( s ` h ) o. ( t ` h ) ) ) ) )
40 39 3ad2ant1 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( Q e. A /\ -. Q .<_ W ) /\ ( X e. ( I ` Q ) /\ Y e. ( I ` Q ) ) ) -> ( +g ` ( Scalar ` U ) ) = ( s e. ( ( TEndo ` K ) ` W ) , t e. ( ( TEndo ` K ) ` W ) |-> ( h e. ( ( LTrn ` K ) ` W ) |-> ( ( s ` h ) o. ( t ` h ) ) ) ) )
41 40 oveqd 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( Q e. A /\ -. Q .<_ W ) /\ ( X e. ( I ` Q ) /\ Y e. ( I ` Q ) ) ) -> ( ( 2nd ` X ) ( +g ` ( Scalar ` U ) ) ( 2nd ` Y ) ) = ( ( 2nd ` X ) ( s e. ( ( TEndo ` K ) ` W ) , t e. ( ( TEndo ` K ) ` W ) |-> ( h e. ( ( LTrn ` K ) ` W ) |-> ( ( s ` h ) o. ( t ` h ) ) ) ) ( 2nd ` Y ) ) )
42 41 fveq1d 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( Q e. A /\ -. Q .<_ W ) /\ ( X e. ( I ` Q ) /\ Y e. ( I ` Q ) ) ) -> ( ( ( 2nd ` X ) ( +g ` ( Scalar ` U ) ) ( 2nd ` Y ) ) ` ( iota_ g e. ( ( LTrn ` K ) ` W ) ( g ` ( ( oc ` K ) ` W ) ) = Q ) ) = ( ( ( 2nd ` X ) ( s e. ( ( TEndo ` K ) ` W ) , t e. ( ( TEndo ` K ) ` W ) |-> ( h e. ( ( LTrn ` K ) ` W ) |-> ( ( s ` h ) o. ( t ` h ) ) ) ) ( 2nd ` Y ) ) ` ( iota_ g e. ( ( LTrn ` K ) ` W ) ( g ` ( ( oc ` K ) ` W ) ) = Q ) ) )
43 eqid 
 |-  ( ( oc ` K ) ` W ) = ( ( oc ` K ) ` W )
44 1 2 3 43 10 5 dicelval1sta 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( Q e. A /\ -. Q .<_ W ) /\ X e. ( I ` Q ) ) -> ( 1st ` X ) = ( ( 2nd ` X ) ` ( iota_ g e. ( ( LTrn ` K ) ` W ) ( g ` ( ( oc ` K ) ` W ) ) = Q ) ) )
45 44 3adant3r 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( Q e. A /\ -. Q .<_ W ) /\ ( X e. ( I ` Q ) /\ Y e. ( I ` Q ) ) ) -> ( 1st ` X ) = ( ( 2nd ` X ) ` ( iota_ g e. ( ( LTrn ` K ) ` W ) ( g ` ( ( oc ` K ) ` W ) ) = Q ) ) )
46 1 2 3 43 10 5 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 ) ) )
47 46 3adant3l 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( Q e. A /\ -. Q .<_ W ) /\ ( X e. ( I ` Q ) /\ Y e. ( I ` Q ) ) ) -> ( 1st ` Y ) = ( ( 2nd ` Y ) ` ( iota_ g e. ( ( LTrn ` K ) ` W ) ( g ` ( ( oc ` K ) ` W ) ) = Q ) ) )
48 45 47 coeq12d 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( Q e. A /\ -. Q .<_ W ) /\ ( X e. ( I ` Q ) /\ Y e. ( I ` Q ) ) ) -> ( ( 1st ` X ) o. ( 1st ` Y ) ) = ( ( ( 2nd ` X ) ` ( iota_ g e. ( ( LTrn ` K ) ` W ) ( g ` ( ( oc ` K ) ` W ) ) = Q ) ) o. ( ( 2nd ` Y ) ` ( iota_ g e. ( ( LTrn ` K ) ` W ) ( g ` ( ( oc ` K ) ` W ) ) = Q ) ) ) )
49 38 42 48 3eqtr4rd 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( Q e. A /\ -. Q .<_ W ) /\ ( X e. ( I ` Q ) /\ Y e. ( I ` Q ) ) ) -> ( ( 1st ` X ) o. ( 1st ` Y ) ) = ( ( ( 2nd ` X ) ( +g ` ( Scalar ` U ) ) ( 2nd ` Y ) ) ` ( iota_ g e. ( ( LTrn ` K ) ` W ) ( g ` ( ( oc ` K ) ` W ) ) = Q ) ) )
50 3 10 11 36 tendoplcl 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( 2nd ` X ) e. ( ( TEndo ` K ) ` W ) /\ ( 2nd ` Y ) e. ( ( TEndo ` K ) ` W ) ) -> ( ( 2nd ` X ) ( s e. ( ( TEndo ` K ) ` W ) , t e. ( ( TEndo ` K ) ` W ) |-> ( h e. ( ( LTrn ` K ) ` W ) |-> ( ( s ` h ) o. ( t ` h ) ) ) ) ( 2nd ` Y ) ) e. ( ( TEndo ` K ) ` W ) )
51 7 26 28 50 syl3anc 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( Q e. A /\ -. Q .<_ W ) /\ ( X e. ( I ` Q ) /\ Y e. ( I ` Q ) ) ) -> ( ( 2nd ` X ) ( s e. ( ( TEndo ` K ) ` W ) , t e. ( ( TEndo ` K ) ` W ) |-> ( h e. ( ( LTrn ` K ) ` W ) |-> ( ( s ` h ) o. ( t ` h ) ) ) ) ( 2nd ` Y ) ) e. ( ( TEndo ` K ) ` W ) )
52 41 51 eqeltrd 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( Q e. A /\ -. Q .<_ W ) /\ ( X e. ( I ` Q ) /\ Y e. ( I ` Q ) ) ) -> ( ( 2nd ` X ) ( +g ` ( Scalar ` U ) ) ( 2nd ` Y ) ) e. ( ( TEndo ` K ) ` W ) )
53 fvex 
 |-  ( 1st ` X ) e. _V
54 fvex 
 |-  ( 1st ` Y ) e. _V
55 53 54 coex 
 |-  ( ( 1st ` X ) o. ( 1st ` Y ) ) e. _V
56 ovex 
 |-  ( ( 2nd ` X ) ( +g ` ( Scalar ` U ) ) ( 2nd ` Y ) ) e. _V
57 1 2 3 43 10 11 5 55 56 dicopelval 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( Q e. A /\ -. Q .<_ W ) ) -> ( <. ( ( 1st ` X ) o. ( 1st ` Y ) ) , ( ( 2nd ` X ) ( +g ` ( Scalar ` U ) ) ( 2nd ` Y ) ) >. e. ( I ` Q ) <-> ( ( ( 1st ` X ) o. ( 1st ` Y ) ) = ( ( ( 2nd ` X ) ( +g ` ( Scalar ` U ) ) ( 2nd ` Y ) ) ` ( iota_ g e. ( ( LTrn ` K ) ` W ) ( g ` ( ( oc ` K ) ` W ) ) = Q ) ) /\ ( ( 2nd ` X ) ( +g ` ( Scalar ` U ) ) ( 2nd ` Y ) ) e. ( ( TEndo ` K ) ` W ) ) ) )
58 57 3adant3 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( Q e. A /\ -. Q .<_ W ) /\ ( X e. ( I ` Q ) /\ Y e. ( I ` Q ) ) ) -> ( <. ( ( 1st ` X ) o. ( 1st ` Y ) ) , ( ( 2nd ` X ) ( +g ` ( Scalar ` U ) ) ( 2nd ` Y ) ) >. e. ( I ` Q ) <-> ( ( ( 1st ` X ) o. ( 1st ` Y ) ) = ( ( ( 2nd ` X ) ( +g ` ( Scalar ` U ) ) ( 2nd ` Y ) ) ` ( iota_ g e. ( ( LTrn ` K ) ` W ) ( g ` ( ( oc ` K ) ` W ) ) = Q ) ) /\ ( ( 2nd ` X ) ( +g ` ( Scalar ` U ) ) ( 2nd ` Y ) ) e. ( ( TEndo ` K ) ` W ) ) ) )
59 49 52 58 mpbir2and 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( Q e. A /\ -. Q .<_ W ) /\ ( X e. ( I ` Q ) /\ Y e. ( I ` Q ) ) ) -> <. ( ( 1st ` X ) o. ( 1st ` Y ) ) , ( ( 2nd ` X ) ( +g ` ( Scalar ` U ) ) ( 2nd ` Y ) ) >. e. ( I ` Q ) )
60 24 59 eqeltrd 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( Q e. A /\ -. Q .<_ W ) /\ ( X e. ( I ` Q ) /\ Y e. ( I ` Q ) ) ) -> ( X .+ Y ) e. ( I ` Q ) )