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 ) )