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