Metamath Proof Explorer

Theorem lcfrlem23

Description: Lemma for lcfr . TODO: this proof was built from other proof pieces that may change N{ X , Y } into subspace sum and back unnecessarily, or similar things. (Contributed by NM, 1-Mar-2015)

Ref Expression
Hypotheses lcfrlem17.h 
|- H = ( LHyp ` K )
lcfrlem17.o 
|- ._|_ = ( ( ocH ` K ) ` W )
lcfrlem17.u 
|- U = ( ( DVecH ` K ) ` W )
lcfrlem17.v 
|- V = ( Base ` U )
lcfrlem17.p 
|- .+ = ( +g ` U )
lcfrlem17.z 
|- .0. = ( 0g ` U )
lcfrlem17.n 
|- N = ( LSpan ` U )
lcfrlem17.a 
|- A = ( LSAtoms ` U )
lcfrlem17.k 
|- ( ph -> ( K e. HL /\ W e. H ) )
lcfrlem17.x 
|- ( ph -> X e. ( V \ { .0. } ) )
lcfrlem17.y 
|- ( ph -> Y e. ( V \ { .0. } ) )
lcfrlem17.ne 
|- ( ph -> ( N ` { X } ) =/= ( N ` { Y } ) )
lcfrlem22.b 
|- B = ( ( N ` { X , Y } ) i^i ( ._|_ ` { ( X .+ Y ) } ) )
lcfrlem23.s 
|- .(+) = ( LSSum ` U )
Assertion lcfrlem23 
|- ( ph -> ( ( ._|_ ` { X , Y } ) .(+) B ) = ( ._|_ ` { ( X .+ Y ) } ) )

Proof

Step Hyp Ref Expression
1 lcfrlem17.h 
 |-  H = ( LHyp ` K )
2 lcfrlem17.o 
 |-  ._|_ = ( ( ocH ` K ) ` W )
3 lcfrlem17.u 
 |-  U = ( ( DVecH ` K ) ` W )
4 lcfrlem17.v 
 |-  V = ( Base ` U )
5 lcfrlem17.p 
 |-  .+ = ( +g ` U )
6 lcfrlem17.z 
 |-  .0. = ( 0g ` U )
7 lcfrlem17.n 
 |-  N = ( LSpan ` U )
8 lcfrlem17.a 
 |-  A = ( LSAtoms ` U )
9 lcfrlem17.k 
 |-  ( ph -> ( K e. HL /\ W e. H ) )
10 lcfrlem17.x 
 |-  ( ph -> X e. ( V \ { .0. } ) )
11 lcfrlem17.y 
 |-  ( ph -> Y e. ( V \ { .0. } ) )
12 lcfrlem17.ne 
 |-  ( ph -> ( N ` { X } ) =/= ( N ` { Y } ) )
13 lcfrlem22.b 
 |-  B = ( ( N ` { X , Y } ) i^i ( ._|_ ` { ( X .+ Y ) } ) )
14 lcfrlem23.s 
 |-  .(+) = ( LSSum ` U )
15 13 fveq2i 
 |-  ( ._|_ ` B ) = ( ._|_ ` ( ( N ` { X , Y } ) i^i ( ._|_ ` { ( X .+ Y ) } ) ) )
16 eqid 
 |-  ( ( DIsoH ` K ) ` W ) = ( ( DIsoH ` K ) ` W )
17 eqid 
 |-  ( ( joinH ` K ) ` W ) = ( ( joinH ` K ) ` W )
18 10 eldifad 
 |-  ( ph -> X e. V )
19 11 eldifad 
 |-  ( ph -> Y e. V )
20 1 3 4 7 16 9 18 19 dihprrn 
 |-  ( ph -> ( N ` { X , Y } ) e. ran ( ( DIsoH ` K ) ` W ) )
21 1 3 9 dvhlmod 
 |-  ( ph -> U e. LMod )
22 4 5 lmodvacl 
 |-  ( ( U e. LMod /\ X e. V /\ Y e. V ) -> ( X .+ Y ) e. V )
23 21 18 19 22 syl3anc 
 |-  ( ph -> ( X .+ Y ) e. V )
24 23 snssd 
 |-  ( ph -> { ( X .+ Y ) } C_ V )
25 1 16 3 4 2 dochcl 
 |-  ( ( ( K e. HL /\ W e. H ) /\ { ( X .+ Y ) } C_ V ) -> ( ._|_ ` { ( X .+ Y ) } ) e. ran ( ( DIsoH ` K ) ` W ) )
26 9 24 25 syl2anc 
 |-  ( ph -> ( ._|_ ` { ( X .+ Y ) } ) e. ran ( ( DIsoH ` K ) ` W ) )
27 1 16 3 4 2 17 9 20 26 dochdmm1 
 |-  ( ph -> ( ._|_ ` ( ( N ` { X , Y } ) i^i ( ._|_ ` { ( X .+ Y ) } ) ) ) = ( ( ._|_ ` ( N ` { X , Y } ) ) ( ( joinH ` K ) ` W ) ( ._|_ ` ( ._|_ ` { ( X .+ Y ) } ) ) ) )
28 1 3 2 4 7 9 23 dochocsn 
 |-  ( ph -> ( ._|_ ` ( ._|_ ` { ( X .+ Y ) } ) ) = ( N ` { ( X .+ Y ) } ) )
29 28 oveq2d 
 |-  ( ph -> ( ( ._|_ ` ( N ` { X , Y } ) ) ( ( joinH ` K ) ` W ) ( ._|_ ` ( ._|_ ` { ( X .+ Y ) } ) ) ) = ( ( ._|_ ` ( N ` { X , Y } ) ) ( ( joinH ` K ) ` W ) ( N ` { ( X .+ Y ) } ) ) )
30 prssi 
 |-  ( ( X e. V /\ Y e. V ) -> { X , Y } C_ V )
31 18 19 30 syl2anc 
 |-  ( ph -> { X , Y } C_ V )
32 4 7 lspssv 
 |-  ( ( U e. LMod /\ { X , Y } C_ V ) -> ( N ` { X , Y } ) C_ V )
33 21 31 32 syl2anc 
 |-  ( ph -> ( N ` { X , Y } ) C_ V )
34 1 16 3 4 2 dochcl 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( N ` { X , Y } ) C_ V ) -> ( ._|_ ` ( N ` { X , Y } ) ) e. ran ( ( DIsoH ` K ) ` W ) )
35 9 33 34 syl2anc 
 |-  ( ph -> ( ._|_ ` ( N ` { X , Y } ) ) e. ran ( ( DIsoH ` K ) ` W ) )
36 1 3 4 14 7 16 17 9 35 23 dihjat1 
 |-  ( ph -> ( ( ._|_ ` ( N ` { X , Y } ) ) ( ( joinH ` K ) ` W ) ( N ` { ( X .+ Y ) } ) ) = ( ( ._|_ ` ( N ` { X , Y } ) ) .(+) ( N ` { ( X .+ Y ) } ) ) )
37 27 29 36 3eqtrd 
 |-  ( ph -> ( ._|_ ` ( ( N ` { X , Y } ) i^i ( ._|_ ` { ( X .+ Y ) } ) ) ) = ( ( ._|_ ` ( N ` { X , Y } ) ) .(+) ( N ` { ( X .+ Y ) } ) ) )
38 15 37 syl5eq 
 |-  ( ph -> ( ._|_ ` B ) = ( ( ._|_ ` ( N ` { X , Y } ) ) .(+) ( N ` { ( X .+ Y ) } ) ) )
39 38 ineq2d 
 |-  ( ph -> ( ( ( N ` { X } ) .(+) ( N ` { Y } ) ) i^i ( ._|_ ` B ) ) = ( ( ( N ` { X } ) .(+) ( N ` { Y } ) ) i^i ( ( ._|_ ` ( N ` { X , Y } ) ) .(+) ( N ` { ( X .+ Y ) } ) ) ) )
40 eqid 
 |-  ( LSubSp ` U ) = ( LSubSp ` U )
41 40 lsssssubg 
 |-  ( U e. LMod -> ( LSubSp ` U ) C_ ( SubGrp ` U ) )
42 21 41 syl 
 |-  ( ph -> ( LSubSp ` U ) C_ ( SubGrp ` U ) )
43 4 40 7 lspsncl 
 |-  ( ( U e. LMod /\ X e. V ) -> ( N ` { X } ) e. ( LSubSp ` U ) )
44 21 18 43 syl2anc 
 |-  ( ph -> ( N ` { X } ) e. ( LSubSp ` U ) )
45 4 40 7 lspsncl 
 |-  ( ( U e. LMod /\ Y e. V ) -> ( N ` { Y } ) e. ( LSubSp ` U ) )
46 21 19 45 syl2anc 
 |-  ( ph -> ( N ` { Y } ) e. ( LSubSp ` U ) )
47 40 14 lsmcl 
 |-  ( ( U e. LMod /\ ( N ` { X } ) e. ( LSubSp ` U ) /\ ( N ` { Y } ) e. ( LSubSp ` U ) ) -> ( ( N ` { X } ) .(+) ( N ` { Y } ) ) e. ( LSubSp ` U ) )
48 21 44 46 47 syl3anc 
 |-  ( ph -> ( ( N ` { X } ) .(+) ( N ` { Y } ) ) e. ( LSubSp ` U ) )
49 42 48 sseldd 
 |-  ( ph -> ( ( N ` { X } ) .(+) ( N ` { Y } ) ) e. ( SubGrp ` U ) )
50 1 3 4 40 2 dochlss 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( N ` { X , Y } ) C_ V ) -> ( ._|_ ` ( N ` { X , Y } ) ) e. ( LSubSp ` U ) )
51 9 33 50 syl2anc 
 |-  ( ph -> ( ._|_ ` ( N ` { X , Y } ) ) e. ( LSubSp ` U ) )
52 42 51 sseldd 
 |-  ( ph -> ( ._|_ ` ( N ` { X , Y } ) ) e. ( SubGrp ` U ) )
53 4 40 7 lspsncl 
 |-  ( ( U e. LMod /\ ( X .+ Y ) e. V ) -> ( N ` { ( X .+ Y ) } ) e. ( LSubSp ` U ) )
54 21 23 53 syl2anc 
 |-  ( ph -> ( N ` { ( X .+ Y ) } ) e. ( LSubSp ` U ) )
55 42 54 sseldd 
 |-  ( ph -> ( N ` { ( X .+ Y ) } ) e. ( SubGrp ` U ) )
56 4 5 7 14 lspsntri 
 |-  ( ( U e. LMod /\ X e. V /\ Y e. V ) -> ( N ` { ( X .+ Y ) } ) C_ ( ( N ` { X } ) .(+) ( N ` { Y } ) ) )
57 21 18 19 56 syl3anc 
 |-  ( ph -> ( N ` { ( X .+ Y ) } ) C_ ( ( N ` { X } ) .(+) ( N ` { Y } ) ) )
58 14 lsmmod2 
 |-  ( ( ( ( ( N ` { X } ) .(+) ( N ` { Y } ) ) e. ( SubGrp ` U ) /\ ( ._|_ ` ( N ` { X , Y } ) ) e. ( SubGrp ` U ) /\ ( N ` { ( X .+ Y ) } ) e. ( SubGrp ` U ) ) /\ ( N ` { ( X .+ Y ) } ) C_ ( ( N ` { X } ) .(+) ( N ` { Y } ) ) ) -> ( ( ( N ` { X } ) .(+) ( N ` { Y } ) ) i^i ( ( ._|_ ` ( N ` { X , Y } ) ) .(+) ( N ` { ( X .+ Y ) } ) ) ) = ( ( ( ( N ` { X } ) .(+) ( N ` { Y } ) ) i^i ( ._|_ ` ( N ` { X , Y } ) ) ) .(+) ( N ` { ( X .+ Y ) } ) ) )
59 49 52 55 57 58 syl31anc 
 |-  ( ph -> ( ( ( N ` { X } ) .(+) ( N ` { Y } ) ) i^i ( ( ._|_ ` ( N ` { X , Y } ) ) .(+) ( N ` { ( X .+ Y ) } ) ) ) = ( ( ( ( N ` { X } ) .(+) ( N ` { Y } ) ) i^i ( ._|_ ` ( N ` { X , Y } ) ) ) .(+) ( N ` { ( X .+ Y ) } ) ) )
60 4 7 14 21 18 19 lsmpr 
 |-  ( ph -> ( N ` { X , Y } ) = ( ( N ` { X } ) .(+) ( N ` { Y } ) ) )
61 60 ineq1d 
 |-  ( ph -> ( ( N ` { X , Y } ) i^i ( ._|_ ` ( N ` { X , Y } ) ) ) = ( ( ( N ` { X } ) .(+) ( N ` { Y } ) ) i^i ( ._|_ ` ( N ` { X , Y } ) ) ) )
62 4 40 7 21 18 19 lspprcl 
 |-  ( ph -> ( N ` { X , Y } ) e. ( LSubSp ` U ) )
63 1 3 40 6 2 dochnoncon 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( N ` { X , Y } ) e. ( LSubSp ` U ) ) -> ( ( N ` { X , Y } ) i^i ( ._|_ ` ( N ` { X , Y } ) ) ) = { .0. } )
64 9 62 63 syl2anc 
 |-  ( ph -> ( ( N ` { X , Y } ) i^i ( ._|_ ` ( N ` { X , Y } ) ) ) = { .0. } )
65 61 64 eqtr3d 
 |-  ( ph -> ( ( ( N ` { X } ) .(+) ( N ` { Y } ) ) i^i ( ._|_ ` ( N ` { X , Y } ) ) ) = { .0. } )
66 65 oveq1d 
 |-  ( ph -> ( ( ( ( N ` { X } ) .(+) ( N ` { Y } ) ) i^i ( ._|_ ` ( N ` { X , Y } ) ) ) .(+) ( N ` { ( X .+ Y ) } ) ) = ( { .0. } .(+) ( N ` { ( X .+ Y ) } ) ) )
67 6 14 lsm02 
 |-  ( ( N ` { ( X .+ Y ) } ) e. ( SubGrp ` U ) -> ( { .0. } .(+) ( N ` { ( X .+ Y ) } ) ) = ( N ` { ( X .+ Y ) } ) )
68 55 67 syl 
 |-  ( ph -> ( { .0. } .(+) ( N ` { ( X .+ Y ) } ) ) = ( N ` { ( X .+ Y ) } ) )
69 66 68 eqtrd 
 |-  ( ph -> ( ( ( ( N ` { X } ) .(+) ( N ` { Y } ) ) i^i ( ._|_ ` ( N ` { X , Y } ) ) ) .(+) ( N ` { ( X .+ Y ) } ) ) = ( N ` { ( X .+ Y ) } ) )
70 39 59 69 3eqtrd 
 |-  ( ph -> ( ( ( N ` { X } ) .(+) ( N ` { Y } ) ) i^i ( ._|_ ` B ) ) = ( N ` { ( X .+ Y ) } ) )
71 70 fveq2d 
 |-  ( ph -> ( ._|_ ` ( ( ( N ` { X } ) .(+) ( N ` { Y } ) ) i^i ( ._|_ ` B ) ) ) = ( ._|_ ` ( N ` { ( X .+ Y ) } ) ) )
72 1 3 4 14 7 16 9 18 19 dihsmsnrn 
 |-  ( ph -> ( ( N ` { X } ) .(+) ( N ` { Y } ) ) e. ran ( ( DIsoH ` K ) ` W ) )
73 1 2 3 4 5 6 7 8 9 10 11 12 13 lcfrlem22 
 |-  ( ph -> B e. A )
74 4 8 21 73 lsatssv 
 |-  ( ph -> B C_ V )
75 1 16 3 4 2 dochcl 
 |-  ( ( ( K e. HL /\ W e. H ) /\ B C_ V ) -> ( ._|_ ` B ) e. ran ( ( DIsoH ` K ) ` W ) )
76 9 74 75 syl2anc 
 |-  ( ph -> ( ._|_ ` B ) e. ran ( ( DIsoH ` K ) ` W ) )
77 1 16 3 4 2 17 9 72 76 dochdmm1 
 |-  ( ph -> ( ._|_ ` ( ( ( N ` { X } ) .(+) ( N ` { Y } ) ) i^i ( ._|_ ` B ) ) ) = ( ( ._|_ ` ( ( N ` { X } ) .(+) ( N ` { Y } ) ) ) ( ( joinH ` K ) ` W ) ( ._|_ ` ( ._|_ ` B ) ) ) )
78 60 fveq2d 
 |-  ( ph -> ( ._|_ ` ( N ` { X , Y } ) ) = ( ._|_ ` ( ( N ` { X } ) .(+) ( N ` { Y } ) ) ) )
79 1 3 2 4 7 9 31 dochocsp 
 |-  ( ph -> ( ._|_ ` ( N ` { X , Y } ) ) = ( ._|_ ` { X , Y } ) )
80 78 79 eqtr3d 
 |-  ( ph -> ( ._|_ ` ( ( N ` { X } ) .(+) ( N ` { Y } ) ) ) = ( ._|_ ` { X , Y } ) )
81 1 3 16 8 dih1dimat 
 |-  ( ( ( K e. HL /\ W e. H ) /\ B e. A ) -> B e. ran ( ( DIsoH ` K ) ` W ) )
82 9 73 81 syl2anc 
 |-  ( ph -> B e. ran ( ( DIsoH ` K ) ` W ) )
83 1 16 2 dochoc 
 |-  ( ( ( K e. HL /\ W e. H ) /\ B e. ran ( ( DIsoH ` K ) ` W ) ) -> ( ._|_ ` ( ._|_ ` B ) ) = B )
84 9 82 83 syl2anc 
 |-  ( ph -> ( ._|_ ` ( ._|_ ` B ) ) = B )
85 80 84 oveq12d 
 |-  ( ph -> ( ( ._|_ ` ( ( N ` { X } ) .(+) ( N ` { Y } ) ) ) ( ( joinH ` K ) ` W ) ( ._|_ ` ( ._|_ ` B ) ) ) = ( ( ._|_ ` { X , Y } ) ( ( joinH ` K ) ` W ) B ) )
86 1 16 3 4 2 dochcl 
 |-  ( ( ( K e. HL /\ W e. H ) /\ { X , Y } C_ V ) -> ( ._|_ ` { X , Y } ) e. ran ( ( DIsoH ` K ) ` W ) )
87 9 31 86 syl2anc 
 |-  ( ph -> ( ._|_ ` { X , Y } ) e. ran ( ( DIsoH ` K ) ` W ) )
88 1 16 17 3 14 8 9 87 73 dihjat2 
 |-  ( ph -> ( ( ._|_ ` { X , Y } ) ( ( joinH ` K ) ` W ) B ) = ( ( ._|_ ` { X , Y } ) .(+) B ) )
89 77 85 88 3eqtrd 
 |-  ( ph -> ( ._|_ ` ( ( ( N ` { X } ) .(+) ( N ` { Y } ) ) i^i ( ._|_ ` B ) ) ) = ( ( ._|_ ` { X , Y } ) .(+) B ) )
90 1 3 2 4 7 9 24 dochocsp 
 |-  ( ph -> ( ._|_ ` ( N ` { ( X .+ Y ) } ) ) = ( ._|_ ` { ( X .+ Y ) } ) )
91 71 89 90 3eqtr3d 
 |-  ( ph -> ( ( ._|_ ` { X , Y } ) .(+) B ) = ( ._|_ ` { ( X .+ Y ) } ) )