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 eqtrid ⊢ φ → 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