Metamath Proof Explorer

Theorem dihjat1lem

Description: Subspace sum of a closed subspace and an atom. ( pmapjat1 analog.) TODO: merge into dihjat1 ? (Contributed by NM, 18-Aug-2014)

Ref Expression
Hypotheses dihjat1.h 
|- H = ( LHyp ` K )
dihjat1.u 
|- U = ( ( DVecH ` K ) ` W )
dihjat1.v 
|- V = ( Base ` U )
dihjat1.p 
|- .(+) = ( LSSum ` U )
dihjat1.n 
|- N = ( LSpan ` U )
dihjat1.i 
|- I = ( ( DIsoH ` K ) ` W )
dihjat1.j 
|- .\/ = ( ( joinH ` K ) ` W )
dihjat1.k 
|- ( ph -> ( K e. HL /\ W e. H ) )
dihjat1.x 
|- ( ph -> X e. ran I )
dihjat1.o 
|- .0. = ( 0g ` U )
dihjat1lem.q 
|- ( ph -> T e. ( V \ { .0. } ) )
Assertion dihjat1lem 
|- ( ph -> ( X .\/ ( N ` { T } ) ) = ( X .(+) ( N ` { T } ) ) )

Proof

Step Hyp Ref Expression
1 dihjat1.h 
 |-  H = ( LHyp ` K )
2 dihjat1.u 
 |-  U = ( ( DVecH ` K ) ` W )
3 dihjat1.v 
 |-  V = ( Base ` U )
4 dihjat1.p 
 |-  .(+) = ( LSSum ` U )
5 dihjat1.n 
 |-  N = ( LSpan ` U )
6 dihjat1.i 
 |-  I = ( ( DIsoH ` K ) ` W )
7 dihjat1.j 
 |-  .\/ = ( ( joinH ` K ) ` W )
8 dihjat1.k 
 |-  ( ph -> ( K e. HL /\ W e. H ) )
9 dihjat1.x 
 |-  ( ph -> X e. ran I )
10 dihjat1.o 
 |-  .0. = ( 0g ` U )
11 dihjat1lem.q 
 |-  ( ph -> T e. ( V \ { .0. } ) )
12 simpr 
 |-  ( ( ph /\ X = { .0. } ) -> X = { .0. } )
13 12 oveq1d 
 |-  ( ( ph /\ X = { .0. } ) -> ( X .\/ ( N ` { T } ) ) = ( { .0. } .\/ ( N ` { T } ) ) )
14 12 oveq1d 
 |-  ( ( ph /\ X = { .0. } ) -> ( X .(+) ( N ` { T } ) ) = ( { .0. } .(+) ( N ` { T } ) ) )
15 eldifi 
 |-  ( T e. ( V \ { .0. } ) -> T e. V )
16 11 15 syl 
 |-  ( ph -> T e. V )
17 1 2 3 5 6 dihlsprn 
 |-  ( ( ( K e. HL /\ W e. H ) /\ T e. V ) -> ( N ` { T } ) e. ran I )
18 8 16 17 syl2anc 
 |-  ( ph -> ( N ` { T } ) e. ran I )
19 1 2 10 6 7 8 18 djh02 
 |-  ( ph -> ( { .0. } .\/ ( N ` { T } ) ) = ( N ` { T } ) )
20 1 2 8 dvhlmod 
 |-  ( ph -> U e. LMod )
21 eqid 
 |-  ( LSubSp ` U ) = ( LSubSp ` U )
22 3 21 5 lspsncl 
 |-  ( ( U e. LMod /\ T e. V ) -> ( N ` { T } ) e. ( LSubSp ` U ) )
23 20 16 22 syl2anc 
 |-  ( ph -> ( N ` { T } ) e. ( LSubSp ` U ) )
24 21 lsssubg 
 |-  ( ( U e. LMod /\ ( N ` { T } ) e. ( LSubSp ` U ) ) -> ( N ` { T } ) e. ( SubGrp ` U ) )
25 20 23 24 syl2anc 
 |-  ( ph -> ( N ` { T } ) e. ( SubGrp ` U ) )
26 10 4 lsm02 
 |-  ( ( N ` { T } ) e. ( SubGrp ` U ) -> ( { .0. } .(+) ( N ` { T } ) ) = ( N ` { T } ) )
27 25 26 syl 
 |-  ( ph -> ( { .0. } .(+) ( N ` { T } ) ) = ( N ` { T } ) )
28 19 27 eqtr4d 
 |-  ( ph -> ( { .0. } .\/ ( N ` { T } ) ) = ( { .0. } .(+) ( N ` { T } ) ) )
29 28 adantr 
 |-  ( ( ph /\ X = { .0. } ) -> ( { .0. } .\/ ( N ` { T } ) ) = ( { .0. } .(+) ( N ` { T } ) ) )
30 14 29 eqtr4d 
 |-  ( ( ph /\ X = { .0. } ) -> ( X .(+) ( N ` { T } ) ) = ( { .0. } .\/ ( N ` { T } ) ) )
31 13 30 eqtr4d 
 |-  ( ( ph /\ X = { .0. } ) -> ( X .\/ ( N ` { T } ) ) = ( X .(+) ( N ` { T } ) ) )
32 20 adantr 
 |-  ( ( ph /\ X =/= { .0. } ) -> U e. LMod )
33 1 2 6 3 dihrnss 
 |-  ( ( ( K e. HL /\ W e. H ) /\ X e. ran I ) -> X C_ V )
34 8 9 33 syl2anc 
 |-  ( ph -> X C_ V )
35 3 21 lssss 
 |-  ( ( N ` { T } ) e. ( LSubSp ` U ) -> ( N ` { T } ) C_ V )
36 23 35 syl 
 |-  ( ph -> ( N ` { T } ) C_ V )
37 1 6 2 3 7 djhcl 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( X C_ V /\ ( N ` { T } ) C_ V ) ) -> ( X .\/ ( N ` { T } ) ) e. ran I )
38 8 34 36 37 syl12anc 
 |-  ( ph -> ( X .\/ ( N ` { T } ) ) e. ran I )
39 1 2 6 3 dihrnss 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( X .\/ ( N ` { T } ) ) e. ran I ) -> ( X .\/ ( N ` { T } ) ) C_ V )
40 8 38 39 syl2anc 
 |-  ( ph -> ( X .\/ ( N ` { T } ) ) C_ V )
41 40 adantr 
 |-  ( ( ph /\ X =/= { .0. } ) -> ( X .\/ ( N ` { T } ) ) C_ V )
42 1 2 6 21 dihrnlss 
 |-  ( ( ( K e. HL /\ W e. H ) /\ X e. ran I ) -> X e. ( LSubSp ` U ) )
43 8 9 42 syl2anc 
 |-  ( ph -> X e. ( LSubSp ` U ) )
44 21 4 lsmcl 
 |-  ( ( U e. LMod /\ X e. ( LSubSp ` U ) /\ ( N ` { T } ) e. ( LSubSp ` U ) ) -> ( X .(+) ( N ` { T } ) ) e. ( LSubSp ` U ) )
45 20 43 23 44 syl3anc 
 |-  ( ph -> ( X .(+) ( N ` { T } ) ) e. ( LSubSp ` U ) )
46 45 adantr 
 |-  ( ( ph /\ X =/= { .0. } ) -> ( X .(+) ( N ` { T } ) ) e. ( LSubSp ` U ) )
47 simplr 
 |-  ( ( ( ph /\ X =/= { .0. } ) /\ x e. ( V \ { .0. } ) ) -> X =/= { .0. } )
48 8 ad2antrr 
 |-  ( ( ( ph /\ X =/= { .0. } ) /\ x e. ( V \ { .0. } ) ) -> ( K e. HL /\ W e. H ) )
49 9 ad2antrr 
 |-  ( ( ( ph /\ X =/= { .0. } ) /\ x e. ( V \ { .0. } ) ) -> X e. ran I )
50 simpr 
 |-  ( ( ( ph /\ X =/= { .0. } ) /\ x e. ( V \ { .0. } ) ) -> x e. ( V \ { .0. } ) )
51 11 ad2antrr 
 |-  ( ( ( ph /\ X =/= { .0. } ) /\ x e. ( V \ { .0. } ) ) -> T e. ( V \ { .0. } ) )
52 1 2 3 10 5 6 7 48 49 50 51 djhcvat42 
 |-  ( ( ( ph /\ X =/= { .0. } ) /\ x e. ( V \ { .0. } ) ) -> ( ( X =/= { .0. } /\ ( N ` { x } ) C_ ( X .\/ ( N ` { T } ) ) ) -> E. y e. ( V \ { .0. } ) ( ( N ` { y } ) C_ X /\ ( N ` { x } ) C_ ( ( N ` { y } ) .\/ ( N ` { T } ) ) ) ) )
53 47 52 mpand 
 |-  ( ( ( ph /\ X =/= { .0. } ) /\ x e. ( V \ { .0. } ) ) -> ( ( N ` { x } ) C_ ( X .\/ ( N ` { T } ) ) -> E. y e. ( V \ { .0. } ) ( ( N ` { y } ) C_ X /\ ( N ` { x } ) C_ ( ( N ` { y } ) .\/ ( N ` { T } ) ) ) ) )
54 simprrl 
 |-  ( ( ( ( ph /\ X =/= { .0. } ) /\ x e. ( V \ { .0. } ) ) /\ ( y e. ( V \ { .0. } ) /\ ( ( N ` { y } ) C_ X /\ ( N ` { x } ) C_ ( ( N ` { y } ) .\/ ( N ` { T } ) ) ) ) ) -> ( N ` { y } ) C_ X )
55 20 ad3antrrr 
 |-  ( ( ( ( ph /\ X =/= { .0. } ) /\ x e. ( V \ { .0. } ) ) /\ ( y e. ( V \ { .0. } ) /\ ( ( N ` { y } ) C_ X /\ ( N ` { x } ) C_ ( ( N ` { y } ) .\/ ( N ` { T } ) ) ) ) ) -> U e. LMod )
56 43 ad3antrrr 
 |-  ( ( ( ( ph /\ X =/= { .0. } ) /\ x e. ( V \ { .0. } ) ) /\ ( y e. ( V \ { .0. } ) /\ ( ( N ` { y } ) C_ X /\ ( N ` { x } ) C_ ( ( N ` { y } ) .\/ ( N ` { T } ) ) ) ) ) -> X e. ( LSubSp ` U ) )
57 eldifi 
 |-  ( y e. ( V \ { .0. } ) -> y e. V )
58 57 ad2antrl 
 |-  ( ( ( ( ph /\ X =/= { .0. } ) /\ x e. ( V \ { .0. } ) ) /\ ( y e. ( V \ { .0. } ) /\ ( ( N ` { y } ) C_ X /\ ( N ` { x } ) C_ ( ( N ` { y } ) .\/ ( N ` { T } ) ) ) ) ) -> y e. V )
59 3 21 5 55 56 58 ellspsn5b 
 |-  ( ( ( ( ph /\ X =/= { .0. } ) /\ x e. ( V \ { .0. } ) ) /\ ( y e. ( V \ { .0. } ) /\ ( ( N ` { y } ) C_ X /\ ( N ` { x } ) C_ ( ( N ` { y } ) .\/ ( N ` { T } ) ) ) ) ) -> ( y e. X <-> ( N ` { y } ) C_ X ) )
60 54 59 mpbird 
 |-  ( ( ( ( ph /\ X =/= { .0. } ) /\ x e. ( V \ { .0. } ) ) /\ ( y e. ( V \ { .0. } ) /\ ( ( N ` { y } ) C_ X /\ ( N ` { x } ) C_ ( ( N ` { y } ) .\/ ( N ` { T } ) ) ) ) ) -> y e. X )
61 16 ad3antrrr 
 |-  ( ( ( ( ph /\ X =/= { .0. } ) /\ x e. ( V \ { .0. } ) ) /\ ( y e. ( V \ { .0. } ) /\ ( ( N ` { y } ) C_ X /\ ( N ` { x } ) C_ ( ( N ` { y } ) .\/ ( N ` { T } ) ) ) ) ) -> T e. V )
62 3 5 lspsnid 
 |-  ( ( U e. LMod /\ T e. V ) -> T e. ( N ` { T } ) )
63 55 61 62 syl2anc 
 |-  ( ( ( ( ph /\ X =/= { .0. } ) /\ x e. ( V \ { .0. } ) ) /\ ( y e. ( V \ { .0. } ) /\ ( ( N ` { y } ) C_ X /\ ( N ` { x } ) C_ ( ( N ` { y } ) .\/ ( N ` { T } ) ) ) ) ) -> T e. ( N ` { T } ) )
64 simprrr 
 |-  ( ( ( ( ph /\ X =/= { .0. } ) /\ x e. ( V \ { .0. } ) ) /\ ( y e. ( V \ { .0. } ) /\ ( ( N ` { y } ) C_ X /\ ( N ` { x } ) C_ ( ( N ` { y } ) .\/ ( N ` { T } ) ) ) ) ) -> ( N ` { x } ) C_ ( ( N ` { y } ) .\/ ( N ` { T } ) ) )
65 sneq 
 |-  ( z = T -> { z } = { T } )
66 65 fveq2d 
 |-  ( z = T -> ( N ` { z } ) = ( N ` { T } ) )
67 66 oveq2d 
 |-  ( z = T -> ( ( N ` { y } ) .\/ ( N ` { z } ) ) = ( ( N ` { y } ) .\/ ( N ` { T } ) ) )
68 67 sseq2d 
 |-  ( z = T -> ( ( N ` { x } ) C_ ( ( N ` { y } ) .\/ ( N ` { z } ) ) <-> ( N ` { x } ) C_ ( ( N ` { y } ) .\/ ( N ` { T } ) ) ) )
69 68 rspcev 
 |-  ( ( T e. ( N ` { T } ) /\ ( N ` { x } ) C_ ( ( N ` { y } ) .\/ ( N ` { T } ) ) ) -> E. z e. ( N ` { T } ) ( N ` { x } ) C_ ( ( N ` { y } ) .\/ ( N ` { z } ) ) )
70 63 64 69 syl2anc 
 |-  ( ( ( ( ph /\ X =/= { .0. } ) /\ x e. ( V \ { .0. } ) ) /\ ( y e. ( V \ { .0. } ) /\ ( ( N ` { y } ) C_ X /\ ( N ` { x } ) C_ ( ( N ` { y } ) .\/ ( N ` { T } ) ) ) ) ) -> E. z e. ( N ` { T } ) ( N ` { x } ) C_ ( ( N ` { y } ) .\/ ( N ` { z } ) ) )
71 60 70 jca 
 |-  ( ( ( ( ph /\ X =/= { .0. } ) /\ x e. ( V \ { .0. } ) ) /\ ( y e. ( V \ { .0. } ) /\ ( ( N ` { y } ) C_ X /\ ( N ` { x } ) C_ ( ( N ` { y } ) .\/ ( N ` { T } ) ) ) ) ) -> ( y e. X /\ E. z e. ( N ` { T } ) ( N ` { x } ) C_ ( ( N ` { y } ) .\/ ( N ` { z } ) ) ) )
72 71 ex 
 |-  ( ( ( ph /\ X =/= { .0. } ) /\ x e. ( V \ { .0. } ) ) -> ( ( y e. ( V \ { .0. } ) /\ ( ( N ` { y } ) C_ X /\ ( N ` { x } ) C_ ( ( N ` { y } ) .\/ ( N ` { T } ) ) ) ) -> ( y e. X /\ E. z e. ( N ` { T } ) ( N ` { x } ) C_ ( ( N ` { y } ) .\/ ( N ` { z } ) ) ) ) )
73 72 reximdv2 
 |-  ( ( ( ph /\ X =/= { .0. } ) /\ x e. ( V \ { .0. } ) ) -> ( E. y e. ( V \ { .0. } ) ( ( N ` { y } ) C_ X /\ ( N ` { x } ) C_ ( ( N ` { y } ) .\/ ( N ` { T } ) ) ) -> E. y e. X E. z e. ( N ` { T } ) ( N ` { x } ) C_ ( ( N ` { y } ) .\/ ( N ` { z } ) ) ) )
74 53 73 syld 
 |-  ( ( ( ph /\ X =/= { .0. } ) /\ x e. ( V \ { .0. } ) ) -> ( ( N ` { x } ) C_ ( X .\/ ( N ` { T } ) ) -> E. y e. X E. z e. ( N ` { T } ) ( N ` { x } ) C_ ( ( N ` { y } ) .\/ ( N ` { z } ) ) ) )
75 74 anim2d 
 |-  ( ( ( ph /\ X =/= { .0. } ) /\ x e. ( V \ { .0. } ) ) -> ( ( x e. V /\ ( N ` { x } ) C_ ( X .\/ ( N ` { T } ) ) ) -> ( x e. V /\ E. y e. X E. z e. ( N ` { T } ) ( N ` { x } ) C_ ( ( N ` { y } ) .\/ ( N ` { z } ) ) ) ) )
76 1 2 6 21 dihrnlss 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( X .\/ ( N ` { T } ) ) e. ran I ) -> ( X .\/ ( N ` { T } ) ) e. ( LSubSp ` U ) )
77 8 38 76 syl2anc 
 |-  ( ph -> ( X .\/ ( N ` { T } ) ) e. ( LSubSp ` U ) )
78 3 21 5 20 77 ellspsn6 
 |-  ( ph -> ( x e. ( X .\/ ( N ` { T } ) ) <-> ( x e. V /\ ( N ` { x } ) C_ ( X .\/ ( N ` { T } ) ) ) ) )
79 78 ad2antrr 
 |-  ( ( ( ph /\ X =/= { .0. } ) /\ x e. ( V \ { .0. } ) ) -> ( x e. ( X .\/ ( N ` { T } ) ) <-> ( x e. V /\ ( N ` { x } ) C_ ( X .\/ ( N ` { T } ) ) ) ) )
80 3 21 4 5 20 43 23 lsmelval2 
 |-  ( ph -> ( x e. ( X .(+) ( N ` { T } ) ) <-> ( x e. V /\ E. y e. X E. z e. ( N ` { T } ) ( N ` { x } ) C_ ( ( N ` { y } ) .(+) ( N ` { z } ) ) ) ) )
81 8 ad2antrr 
 |-  ( ( ( ph /\ y e. X ) /\ z e. ( N ` { T } ) ) -> ( K e. HL /\ W e. H ) )
82 43 ad2antrr 
 |-  ( ( ( ph /\ y e. X ) /\ z e. ( N ` { T } ) ) -> X e. ( LSubSp ` U ) )
83 simplr 
 |-  ( ( ( ph /\ y e. X ) /\ z e. ( N ` { T } ) ) -> y e. X )
84 3 21 lssel 
 |-  ( ( X e. ( LSubSp ` U ) /\ y e. X ) -> y e. V )
85 82 83 84 syl2anc 
 |-  ( ( ( ph /\ y e. X ) /\ z e. ( N ` { T } ) ) -> y e. V )
86 23 ad2antrr 
 |-  ( ( ( ph /\ y e. X ) /\ z e. ( N ` { T } ) ) -> ( N ` { T } ) e. ( LSubSp ` U ) )
87 simpr 
 |-  ( ( ( ph /\ y e. X ) /\ z e. ( N ` { T } ) ) -> z e. ( N ` { T } ) )
88 3 21 lssel 
 |-  ( ( ( N ` { T } ) e. ( LSubSp ` U ) /\ z e. ( N ` { T } ) ) -> z e. V )
89 86 87 88 syl2anc 
 |-  ( ( ( ph /\ y e. X ) /\ z e. ( N ` { T } ) ) -> z e. V )
90 1 2 3 4 5 6 7 81 85 89 djhlsmat 
 |-  ( ( ( ph /\ y e. X ) /\ z e. ( N ` { T } ) ) -> ( ( N ` { y } ) .(+) ( N ` { z } ) ) = ( ( N ` { y } ) .\/ ( N ` { z } ) ) )
91 90 sseq2d 
 |-  ( ( ( ph /\ y e. X ) /\ z e. ( N ` { T } ) ) -> ( ( N ` { x } ) C_ ( ( N ` { y } ) .(+) ( N ` { z } ) ) <-> ( N ` { x } ) C_ ( ( N ` { y } ) .\/ ( N ` { z } ) ) ) )
92 91 rexbidva 
 |-  ( ( ph /\ y e. X ) -> ( E. z e. ( N ` { T } ) ( N ` { x } ) C_ ( ( N ` { y } ) .(+) ( N ` { z } ) ) <-> E. z e. ( N ` { T } ) ( N ` { x } ) C_ ( ( N ` { y } ) .\/ ( N ` { z } ) ) ) )
93 92 rexbidva 
 |-  ( ph -> ( E. y e. X E. z e. ( N ` { T } ) ( N ` { x } ) C_ ( ( N ` { y } ) .(+) ( N ` { z } ) ) <-> E. y e. X E. z e. ( N ` { T } ) ( N ` { x } ) C_ ( ( N ` { y } ) .\/ ( N ` { z } ) ) ) )
94 93 anbi2d 
 |-  ( ph -> ( ( x e. V /\ E. y e. X E. z e. ( N ` { T } ) ( N ` { x } ) C_ ( ( N ` { y } ) .(+) ( N ` { z } ) ) ) <-> ( x e. V /\ E. y e. X E. z e. ( N ` { T } ) ( N ` { x } ) C_ ( ( N ` { y } ) .\/ ( N ` { z } ) ) ) ) )
95 80 94 bitrd 
 |-  ( ph -> ( x e. ( X .(+) ( N ` { T } ) ) <-> ( x e. V /\ E. y e. X E. z e. ( N ` { T } ) ( N ` { x } ) C_ ( ( N ` { y } ) .\/ ( N ` { z } ) ) ) ) )
96 95 ad2antrr 
 |-  ( ( ( ph /\ X =/= { .0. } ) /\ x e. ( V \ { .0. } ) ) -> ( x e. ( X .(+) ( N ` { T } ) ) <-> ( x e. V /\ E. y e. X E. z e. ( N ` { T } ) ( N ` { x } ) C_ ( ( N ` { y } ) .\/ ( N ` { z } ) ) ) ) )
97 75 79 96 3imtr4d 
 |-  ( ( ( ph /\ X =/= { .0. } ) /\ x e. ( V \ { .0. } ) ) -> ( x e. ( X .\/ ( N ` { T } ) ) -> x e. ( X .(+) ( N ` { T } ) ) ) )
98 10 21 32 41 46 97 lssssr 
 |-  ( ( ph /\ X =/= { .0. } ) -> ( X .\/ ( N ` { T } ) ) C_ ( X .(+) ( N ` { T } ) ) )
99 1 2 3 4 7 8 34 36 djhsumss 
 |-  ( ph -> ( X .(+) ( N ` { T } ) ) C_ ( X .\/ ( N ` { T } ) ) )
100 99 adantr 
 |-  ( ( ph /\ X =/= { .0. } ) -> ( X .(+) ( N ` { T } ) ) C_ ( X .\/ ( N ` { T } ) ) )
101 98 100 eqssd 
 |-  ( ( ph /\ X =/= { .0. } ) -> ( X .\/ ( N ` { T } ) ) = ( X .(+) ( N ` { T } ) ) )
102 31 101 pm2.61dane 
 |-  ( ph -> ( X .\/ ( N ` { T } ) ) = ( X .(+) ( N ` { T } ) ) )