Metamath Proof Explorer

Theorem dihprrnlem2

Description: Lemma for dihprrn . (Contributed by NM, 29-Sep-2014)

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 )
dihprrnlem2.o 
|- .0. = ( 0g ` U )
dihprrnlem2.xz 
|- ( ph -> X =/= .0. )
dihprrnlem2.yz 
|- ( ph -> Y =/= .0. )
Assertion dihprrnlem2 
|- ( 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 dihprrnlem2.o 
 |-  .0. = ( 0g ` U )
10 dihprrnlem2.xz 
 |-  ( ph -> X =/= .0. )
11 dihprrnlem2.yz 
 |-  ( ph -> Y =/= .0. )
12 df-pr 
 |-  { X , Y } = ( { X } u. { Y } )
13 12 fveq2i 
 |-  ( N ` { X , Y } ) = ( N ` ( { X } u. { Y } ) )
14 eqid 
 |-  ( join ` K ) = ( join ` K )
15 eqid 
 |-  ( Atoms ` K ) = ( Atoms ` K )
16 eqid 
 |-  ( LSSum ` U ) = ( LSSum ` U )
17 15 1 2 3 9 4 5 dihlspsnat 
 |-  ( ( ( K e. HL /\ W e. H ) /\ X e. V /\ X =/= .0. ) -> ( `' I ` ( N ` { X } ) ) e. ( Atoms ` K ) )
18 6 7 10 17 syl3anc 
 |-  ( ph -> ( `' I ` ( N ` { X } ) ) e. ( Atoms ` K ) )
19 15 1 2 3 9 4 5 dihlspsnat 
 |-  ( ( ( K e. HL /\ W e. H ) /\ Y e. V /\ Y =/= .0. ) -> ( `' I ` ( N ` { Y } ) ) e. ( Atoms ` K ) )
20 6 8 11 19 syl3anc 
 |-  ( ph -> ( `' I ` ( N ` { Y } ) ) e. ( Atoms ` K ) )
21 1 14 15 2 16 5 6 18 20 dihjat 
 |-  ( ph -> ( I ` ( ( `' I ` ( N ` { X } ) ) ( join ` K ) ( `' I ` ( N ` { Y } ) ) ) ) = ( ( I ` ( `' I ` ( N ` { X } ) ) ) ( LSSum ` U ) ( I ` ( `' I ` ( N ` { Y } ) ) ) ) )
22 1 2 3 4 5 dihlsprn 
 |-  ( ( ( K e. HL /\ W e. H ) /\ X e. V ) -> ( N ` { X } ) e. ran I )
23 6 7 22 syl2anc 
 |-  ( ph -> ( N ` { X } ) e. ran I )
24 1 5 dihcnvid2 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( N ` { X } ) e. ran I ) -> ( I ` ( `' I ` ( N ` { X } ) ) ) = ( N ` { X } ) )
25 6 23 24 syl2anc 
 |-  ( ph -> ( I ` ( `' I ` ( N ` { X } ) ) ) = ( N ` { X } ) )
26 1 2 3 4 5 dihlsprn 
 |-  ( ( ( K e. HL /\ W e. H ) /\ Y e. V ) -> ( N ` { Y } ) e. ran I )
27 6 8 26 syl2anc 
 |-  ( ph -> ( N ` { Y } ) e. ran I )
28 1 5 dihcnvid2 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( N ` { Y } ) e. ran I ) -> ( I ` ( `' I ` ( N ` { Y } ) ) ) = ( N ` { Y } ) )
29 6 27 28 syl2anc 
 |-  ( ph -> ( I ` ( `' I ` ( N ` { Y } ) ) ) = ( N ` { Y } ) )
30 25 29 oveq12d 
 |-  ( ph -> ( ( I ` ( `' I ` ( N ` { X } ) ) ) ( LSSum ` U ) ( I ` ( `' I ` ( N ` { Y } ) ) ) ) = ( ( N ` { X } ) ( LSSum ` U ) ( N ` { Y } ) ) )
31 1 2 6 dvhlmod 
 |-  ( ph -> U e. LMod )
32 7 snssd 
 |-  ( ph -> { X } C_ V )
33 8 snssd 
 |-  ( ph -> { Y } C_ V )
34 3 4 16 lsmsp2 
 |-  ( ( U e. LMod /\ { X } C_ V /\ { Y } C_ V ) -> ( ( N ` { X } ) ( LSSum ` U ) ( N ` { Y } ) ) = ( N ` ( { X } u. { Y } ) ) )
35 31 32 33 34 syl3anc 
 |-  ( ph -> ( ( N ` { X } ) ( LSSum ` U ) ( N ` { Y } ) ) = ( N ` ( { X } u. { Y } ) ) )
36 21 30 35 3eqtrrd 
 |-  ( ph -> ( N ` ( { X } u. { Y } ) ) = ( I ` ( ( `' I ` ( N ` { X } ) ) ( join ` K ) ( `' I ` ( N ` { Y } ) ) ) ) )
37 13 36 eqtrid 
 |-  ( ph -> ( N ` { X , Y } ) = ( I ` ( ( `' I ` ( N ` { X } ) ) ( join ` K ) ( `' I ` ( N ` { Y } ) ) ) ) )
38 6 simpld 
 |-  ( ph -> K e. HL )
39 38 hllatd 
 |-  ( ph -> K e. Lat )
40 eqid 
 |-  ( Base ` K ) = ( Base ` K )
41 40 1 5 dihcnvcl 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( N ` { X } ) e. ran I ) -> ( `' I ` ( N ` { X } ) ) e. ( Base ` K ) )
42 6 23 41 syl2anc 
 |-  ( ph -> ( `' I ` ( N ` { X } ) ) e. ( Base ` K ) )
43 40 1 5 dihcnvcl 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( N ` { Y } ) e. ran I ) -> ( `' I ` ( N ` { Y } ) ) e. ( Base ` K ) )
44 6 27 43 syl2anc 
 |-  ( ph -> ( `' I ` ( N ` { Y } ) ) e. ( Base ` K ) )
45 40 14 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 ) )
46 39 42 44 45 syl3anc 
 |-  ( ph -> ( ( `' I ` ( N ` { X } ) ) ( join ` K ) ( `' I ` ( N ` { Y } ) ) ) e. ( Base ` K ) )
47 40 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 )
48 6 46 47 syl2anc 
 |-  ( ph -> ( I ` ( ( `' I ` ( N ` { X } ) ) ( join ` K ) ( `' I ` ( N ` { Y } ) ) ) ) e. ran I )
49 37 48 eqeltrd 
 |-  ( ph -> ( N ` { X , Y } ) e. ran I )