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 φ K HL W H
dihprrn.x φ X V
dihprrn.y φ Y V
dihprrnlem1.l ˙ = K
dihprrnlem1.o 0 ˙ = 0 U
dihprrnlem1.nz φ Y 0 ˙
dihprrnlem1.x φ I -1 N X ˙ W
dihprrnlem1.y φ ¬ I -1 N Y ˙ W
Assertion dihprrnlem1N φ N X Y 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 φ K HL W H
7 dihprrn.x φ X V
8 dihprrn.y φ Y V
9 dihprrnlem1.l ˙ = K
10 dihprrnlem1.o 0 ˙ = 0 U
11 dihprrnlem1.nz φ Y 0 ˙
12 dihprrnlem1.x φ I -1 N X ˙ W
13 dihprrnlem1.y φ ¬ I -1 N Y ˙ W
14 df-pr X Y = X Y
15 14 fveq2i N X Y = N X 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 HL W H X V N X ran I
21 6 7 20 syl2anc φ N X ran I
22 16 1 5 dihcnvcl K HL W H N X ran I I -1 N X Base K
23 6 21 22 syl2anc φ I -1 N X Base K
24 23 12 jca φ I -1 N X Base K I -1 N X ˙ W
25 18 1 2 3 10 4 5 dihlspsnat K HL W H Y V Y 0 ˙ I -1 N Y Atoms K
26 6 8 11 25 syl3anc φ I -1 N Y Atoms K
27 26 13 jca φ I -1 N Y Atoms K ¬ I -1 N Y ˙ W
28 16 9 1 17 18 2 19 5 6 24 27 dihjatc φ I I -1 N X join K I -1 N Y = I I -1 N X LSSum U I I -1 N Y
29 1 5 dihcnvid2 K HL W H N X ran I I I -1 N X = N X
30 6 21 29 syl2anc φ I I -1 N X = N X
31 1 2 3 4 5 dihlsprn K HL W H Y V N Y ran I
32 6 8 31 syl2anc φ N Y ran I
33 1 5 dihcnvid2 K HL W H N Y ran I I I -1 N Y = N Y
34 6 32 33 syl2anc φ I I -1 N Y = N Y
35 30 34 oveq12d φ I I -1 N X LSSum U I I -1 N Y = N X LSSum U N Y
36 1 2 6 dvhlmod φ U LMod
37 7 snssd φ X V
38 8 snssd φ Y V
39 3 4 19 lsmsp2 U LMod X V Y V N X LSSum U N Y = N X Y
40 36 37 38 39 syl3anc φ N X LSSum U N Y = N X Y
41 28 35 40 3eqtrrd φ N X Y = I I -1 N X join K I -1 N Y
42 15 41 syl5eq φ N X Y = I I -1 N X join K I -1 N Y
43 6 simpld φ K HL
44 43 hllatd φ K Lat
45 16 1 5 dihcnvcl K HL W H N Y ran I I -1 N Y Base K
46 6 32 45 syl2anc φ I -1 N Y Base K
47 16 17 latjcl K Lat I -1 N X Base K I -1 N Y Base K I -1 N X join K I -1 N Y Base K
48 44 23 46 47 syl3anc φ I -1 N X join K I -1 N Y Base K
49 16 1 5 dihcl K HL W H I -1 N X join K I -1 N Y Base K I I -1 N X join K I -1 N Y ran I
50 6 48 49 syl2anc φ I I -1 N X join K I -1 N Y ran I
51 42 50 eqeltrd φ N X Y ran I