Metamath Proof Explorer

Theorem dihprrnlem1N

Description: Lemma for dihprrn , showing one of 4 cases. (Contributed by NM, 30-Aug-2014) (New usage is discouraged.)

Ref Expression
Hypotheses dihprrn.h 
|- H = ( LHyp ` K )
dihprrn.u 
|- U = ( ( DVecH ` K ) ` W )
dihprrn.v 
|- V = ( Base ` U )
dihprrn.n 
|- N = ( LSpan ` U )
dihprrn.i 
|- I = ( ( DIsoH ` K ) ` W )
dihprrn.k 
|- ( ph -> ( K e. HL /\ W e. H ) )
dihprrn.x 
|- ( ph -> X e. V )
dihprrn.y 
|- ( ph -> Y e. V )
dihprrnlem1.l 
|- .<_ = ( le ` K )
dihprrnlem1.o 
|- .0. = ( 0g ` U )
dihprrnlem1.nz 
|- ( ph -> Y =/= .0. )
dihprrnlem1.x 
|- ( ph -> ( `' I ` ( N ` { X } ) ) .<_ W )
dihprrnlem1.y 
|- ( ph -> -. ( `' I ` ( N ` { Y } ) ) .<_ W )
Assertion dihprrnlem1N 
|- ( ph -> ( N ` { X , Y } ) e. ran I )

Proof

Step Hyp Ref Expression
1 dihprrn.h 
 |-  H = ( LHyp ` K )
2 dihprrn.u 
 |-  U = ( ( DVecH ` K ) ` W )
3 dihprrn.v 
 |-  V = ( Base ` U )
4 dihprrn.n 
 |-  N = ( LSpan ` U )
5 dihprrn.i 
 |-  I = ( ( DIsoH ` K ) ` W )
6 dihprrn.k 
 |-  ( ph -> ( K e. HL /\ W e. H ) )
7 dihprrn.x 
 |-  ( ph -> X e. V )
8 dihprrn.y 
 |-  ( ph -> Y e. V )
9 dihprrnlem1.l 
 |-  .<_ = ( le ` K )
10 dihprrnlem1.o 
 |-  .0. = ( 0g ` U )
11 dihprrnlem1.nz 
 |-  ( ph -> Y =/= .0. )
12 dihprrnlem1.x 
 |-  ( ph -> ( `' I ` ( N ` { X } ) ) .<_ W )
13 dihprrnlem1.y 
 |-  ( ph -> -. ( `' I ` ( N ` { Y } ) ) .<_ W )
14 df-pr 
 |-  { X , Y } = ( { X } u. { Y } )
15 14 fveq2i 
 |-  ( N ` { X , Y } ) = ( N ` ( { X } u. { Y } ) )
16 eqid 
 |-  ( Base ` K ) = ( Base ` K )
17 eqid 
 |-  ( join ` K ) = ( join ` K )
18 eqid 
 |-  ( Atoms ` K ) = ( Atoms ` K )
19 eqid 
 |-  ( LSSum ` U ) = ( LSSum ` U )
20 1 2 3 4 5 dihlsprn 
 |-  ( ( ( K e. HL /\ W e. H ) /\ X e. V ) -> ( N ` { X } ) e. ran I )
21 6 7 20 syl2anc 
 |-  ( ph -> ( N ` { X } ) e. ran I )
22 16 1 5 dihcnvcl 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( N ` { X } ) e. ran I ) -> ( `' I ` ( N ` { X } ) ) e. ( Base ` K ) )
23 6 21 22 syl2anc 
 |-  ( ph -> ( `' I ` ( N ` { X } ) ) e. ( Base ` K ) )
24 23 12 jca 
 |-  ( ph -> ( ( `' I ` ( N ` { X } ) ) e. ( Base ` K ) /\ ( `' I ` ( N ` { X } ) ) .<_ W ) )
25 18 1 2 3 10 4 5 dihlspsnat 
 |-  ( ( ( K e. HL /\ W e. H ) /\ Y e. V /\ Y =/= .0. ) -> ( `' I ` ( N ` { Y } ) ) e. ( Atoms ` K ) )
26 6 8 11 25 syl3anc 
 |-  ( ph -> ( `' I ` ( N ` { Y } ) ) e. ( Atoms ` K ) )
27 26 13 jca 
 |-  ( ph -> ( ( `' I ` ( N ` { Y } ) ) e. ( Atoms ` K ) /\ -. ( `' I ` ( N ` { Y } ) ) .<_ W ) )
28 16 9 1 17 18 2 19 5 6 24 27 dihjatc 
 |-  ( ph -> ( I ` ( ( `' I ` ( N ` { X } ) ) ( join ` K ) ( `' I ` ( N ` { Y } ) ) ) ) = ( ( I ` ( `' I ` ( N ` { X } ) ) ) ( LSSum ` U ) ( I ` ( `' I ` ( N ` { Y } ) ) ) ) )
29 1 5 dihcnvid2 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( N ` { X } ) e. ran I ) -> ( I ` ( `' I ` ( N ` { X } ) ) ) = ( N ` { X } ) )
30 6 21 29 syl2anc 
 |-  ( ph -> ( I ` ( `' I ` ( N ` { X } ) ) ) = ( N ` { X } ) )
31 1 2 3 4 5 dihlsprn 
 |-  ( ( ( K e. HL /\ W e. H ) /\ Y e. V ) -> ( N ` { Y } ) e. ran I )
32 6 8 31 syl2anc 
 |-  ( ph -> ( N ` { Y } ) e. ran I )
33 1 5 dihcnvid2 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( N ` { Y } ) e. ran I ) -> ( I ` ( `' I ` ( N ` { Y } ) ) ) = ( N ` { Y } ) )
34 6 32 33 syl2anc 
 |-  ( ph -> ( I ` ( `' I ` ( N ` { Y } ) ) ) = ( N ` { Y } ) )
35 30 34 oveq12d 
 |-  ( ph -> ( ( I ` ( `' I ` ( N ` { X } ) ) ) ( LSSum ` U ) ( I ` ( `' I ` ( N ` { Y } ) ) ) ) = ( ( N ` { X } ) ( LSSum ` U ) ( N ` { Y } ) ) )
36 1 2 6 dvhlmod 
 |-  ( ph -> U e. LMod )
37 7 snssd 
 |-  ( ph -> { X } C_ V )
38 8 snssd 
 |-  ( ph -> { Y } C_ V )
39 3 4 19 lsmsp2 
 |-  ( ( U e. LMod /\ { X } C_ V /\ { Y } C_ V ) -> ( ( N ` { X } ) ( LSSum ` U ) ( N ` { Y } ) ) = ( N ` ( { X } u. { Y } ) ) )
40 36 37 38 39 syl3anc 
 |-  ( ph -> ( ( N ` { X } ) ( LSSum ` U ) ( N ` { Y } ) ) = ( N ` ( { X } u. { Y } ) ) )
41 28 35 40 3eqtrrd 
 |-  ( ph -> ( N ` ( { X } u. { Y } ) ) = ( I ` ( ( `' I ` ( N ` { X } ) ) ( join ` K ) ( `' I ` ( N ` { Y } ) ) ) ) )
42 15 41 syl5eq 
 |-  ( ph -> ( N ` { X , Y } ) = ( I ` ( ( `' I ` ( N ` { X } ) ) ( join ` K ) ( `' I ` ( N ` { Y } ) ) ) ) )
43 6 simpld 
 |-  ( ph -> K e. HL )
44 43 hllatd 
 |-  ( ph -> K e. Lat )
45 16 1 5 dihcnvcl 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( N ` { Y } ) e. ran I ) -> ( `' I ` ( N ` { Y } ) ) e. ( Base ` K ) )
46 6 32 45 syl2anc 
 |-  ( ph -> ( `' I ` ( N ` { Y } ) ) e. ( Base ` K ) )
47 16 17 latjcl 
 |-  ( ( K e. Lat /\ ( `' I ` ( N ` { X } ) ) e. ( Base ` K ) /\ ( `' I ` ( N ` { Y } ) ) e. ( Base ` K ) ) -> ( ( `' I ` ( N ` { X } ) ) ( join ` K ) ( `' I ` ( N ` { Y } ) ) ) e. ( Base ` K ) )
48 44 23 46 47 syl3anc 
 |-  ( ph -> ( ( `' I ` ( N ` { X } ) ) ( join ` K ) ( `' I ` ( N ` { Y } ) ) ) e. ( Base ` K ) )
49 16 1 5 dihcl 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( ( `' I ` ( N ` { X } ) ) ( join ` K ) ( `' I ` ( N ` { Y } ) ) ) e. ( Base ` K ) ) -> ( I ` ( ( `' I ` ( N ` { X } ) ) ( join ` K ) ( `' I ` ( N ` { Y } ) ) ) ) e. ran I )
50 6 48 49 syl2anc 
 |-  ( ph -> ( I ` ( ( `' I ` ( N ` { X } ) ) ( join ` K ) ( `' I ` ( N ` { Y } ) ) ) ) e. ran I )
51 42 50 eqeltrd 
 |-  ( ph -> ( N ` { X , Y } ) e. ran I )