Metamath Proof Explorer

Theorem dihprrnlem2

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

Ref Expression
Hypotheses dihprrn.h ⊢ 𝐻 = ( LHyp ‘ 𝐾 )
dihprrn.u ⊢ 𝑈 = ( ( DVecH ‘ 𝐾 ) ‘ 𝑊 )
dihprrn.v ⊢ 𝑉 = ( Base ‘ 𝑈 )
dihprrn.n ⊢ 𝑁 = ( LSpan ‘ 𝑈 )
dihprrn.i ⊢ 𝐼 = ( ( DIsoH ‘ 𝐾 ) ‘ 𝑊 )
dihprrn.k ⊢ ( 𝜑 → ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) )
dihprrn.x ⊢ ( 𝜑 → 𝑋 ∈ 𝑉 )
dihprrn.y ⊢ ( 𝜑 → 𝑌 ∈ 𝑉 )
dihprrnlem2.o ⊢ 0 = ( 0g ‘ 𝑈 )
dihprrnlem2.xz ⊢ ( 𝜑 → 𝑋 ≠ 0 )
dihprrnlem2.yz ⊢ ( 𝜑 → 𝑌 ≠ 0 )
Assertion dihprrnlem2 ( 𝜑 → ( 𝑁 ‘ { 𝑋 , 𝑌 } ) ∈ ran 𝐼 )

Proof

Step Hyp Ref Expression
1 dihprrn.h ⊢ 𝐻 = ( LHyp ‘ 𝐾 )
2 dihprrn.u ⊢ 𝑈 = ( ( DVecH ‘ 𝐾 ) ‘ 𝑊 )
3 dihprrn.v ⊢ 𝑉 = ( Base ‘ 𝑈 )
4 dihprrn.n ⊢ 𝑁 = ( LSpan ‘ 𝑈 )
5 dihprrn.i ⊢ 𝐼 = ( ( DIsoH ‘ 𝐾 ) ‘ 𝑊 )
6 dihprrn.k ⊢ ( 𝜑 → ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) )
7 dihprrn.x ⊢ ( 𝜑 → 𝑋 ∈ 𝑉 )
8 dihprrn.y ⊢ ( 𝜑 → 𝑌 ∈ 𝑉 )
9 dihprrnlem2.o ⊢ 0 = ( 0g ‘ 𝑈 )
10 dihprrnlem2.xz ⊢ ( 𝜑 → 𝑋 ≠ 0 )
11 dihprrnlem2.yz ⊢ ( 𝜑 → 𝑌 ≠ 0 )
12 df-pr ⊢ { 𝑋 , 𝑌 } = ( { 𝑋 } ∪ { 𝑌 } )
13 12 fveq2i ⊢ ( 𝑁 ‘ { 𝑋 , 𝑌 } ) = ( 𝑁 ‘ ( { 𝑋 } ∪ { 𝑌 } ) )
14 eqid ⊢ ( join ‘ 𝐾 ) = ( join ‘ 𝐾 )
15 eqid ⊢ ( Atoms ‘ 𝐾 ) = ( Atoms ‘ 𝐾 )
16 eqid ⊢ ( LSSum ‘ 𝑈 ) = ( LSSum ‘ 𝑈 )
17 15 1 2 3 9 4 5 dihlspsnat ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝑋 ∈ 𝑉 ∧ 𝑋 ≠ 0 ) → ( ◡ 𝐼 ‘ ( 𝑁 ‘ { 𝑋 } ) ) ∈ ( Atoms ‘ 𝐾 ) )
18 6 7 10 17 syl3anc ⊢ ( 𝜑 → ( ◡ 𝐼 ‘ ( 𝑁 ‘ { 𝑋 } ) ) ∈ ( Atoms ‘ 𝐾 ) )
19 15 1 2 3 9 4 5 dihlspsnat ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝑌 ∈ 𝑉 ∧ 𝑌 ≠ 0 ) → ( ◡ 𝐼 ‘ ( 𝑁 ‘ { 𝑌 } ) ) ∈ ( Atoms ‘ 𝐾 ) )
20 6 8 11 19 syl3anc ⊢ ( 𝜑 → ( ◡ 𝐼 ‘ ( 𝑁 ‘ { 𝑌 } ) ) ∈ ( Atoms ‘ 𝐾 ) )
21 1 14 15 2 16 5 6 18 20 dihjat ⊢ ( 𝜑 → ( 𝐼 ‘ ( ( ◡ 𝐼 ‘ ( 𝑁 ‘ { 𝑋 } ) ) ( join ‘ 𝐾 ) ( ◡ 𝐼 ‘ ( 𝑁 ‘ { 𝑌 } ) ) ) ) = ( ( 𝐼 ‘ ( ◡ 𝐼 ‘ ( 𝑁 ‘ { 𝑋 } ) ) ) ( LSSum ‘ 𝑈 ) ( 𝐼 ‘ ( ◡ 𝐼 ‘ ( 𝑁 ‘ { 𝑌 } ) ) ) ) )
22 1 2 3 4 5 dihlsprn ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝑋 ∈ 𝑉 ) → ( 𝑁 ‘ { 𝑋 } ) ∈ ran 𝐼 )
23 6 7 22 syl2anc ⊢ ( 𝜑 → ( 𝑁 ‘ { 𝑋 } ) ∈ ran 𝐼 )
24 1 5 dihcnvid2 ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑁 ‘ { 𝑋 } ) ∈ ran 𝐼 ) → ( 𝐼 ‘ ( ◡ 𝐼 ‘ ( 𝑁 ‘ { 𝑋 } ) ) ) = ( 𝑁 ‘ { 𝑋 } ) )
25 6 23 24 syl2anc ⊢ ( 𝜑 → ( 𝐼 ‘ ( ◡ 𝐼 ‘ ( 𝑁 ‘ { 𝑋 } ) ) ) = ( 𝑁 ‘ { 𝑋 } ) )
26 1 2 3 4 5 dihlsprn ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝑌 ∈ 𝑉 ) → ( 𝑁 ‘ { 𝑌 } ) ∈ ran 𝐼 )
27 6 8 26 syl2anc ⊢ ( 𝜑 → ( 𝑁 ‘ { 𝑌 } ) ∈ ran 𝐼 )
28 1 5 dihcnvid2 ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑁 ‘ { 𝑌 } ) ∈ ran 𝐼 ) → ( 𝐼 ‘ ( ◡ 𝐼 ‘ ( 𝑁 ‘ { 𝑌 } ) ) ) = ( 𝑁 ‘ { 𝑌 } ) )
29 6 27 28 syl2anc ⊢ ( 𝜑 → ( 𝐼 ‘ ( ◡ 𝐼 ‘ ( 𝑁 ‘ { 𝑌 } ) ) ) = ( 𝑁 ‘ { 𝑌 } ) )
30 25 29 oveq12d ⊢ ( 𝜑 → ( ( 𝐼 ‘ ( ◡ 𝐼 ‘ ( 𝑁 ‘ { 𝑋 } ) ) ) ( LSSum ‘ 𝑈 ) ( 𝐼 ‘ ( ◡ 𝐼 ‘ ( 𝑁 ‘ { 𝑌 } ) ) ) ) = ( ( 𝑁 ‘ { 𝑋 } ) ( LSSum ‘ 𝑈 ) ( 𝑁 ‘ { 𝑌 } ) ) )
31 1 2 6 dvhlmod ⊢ ( 𝜑 → 𝑈 ∈ LMod )
32 7 snssd ⊢ ( 𝜑 → { 𝑋 } ⊆ 𝑉 )
33 8 snssd ⊢ ( 𝜑 → { 𝑌 } ⊆ 𝑉 )
34 3 4 16 lsmsp2 ⊢ ( ( 𝑈 ∈ LMod ∧ { 𝑋 } ⊆ 𝑉 ∧ { 𝑌 } ⊆ 𝑉 ) → ( ( 𝑁 ‘ { 𝑋 } ) ( LSSum ‘ 𝑈 ) ( 𝑁 ‘ { 𝑌 } ) ) = ( 𝑁 ‘ ( { 𝑋 } ∪ { 𝑌 } ) ) )
35 31 32 33 34 syl3anc ⊢ ( 𝜑 → ( ( 𝑁 ‘ { 𝑋 } ) ( LSSum ‘ 𝑈 ) ( 𝑁 ‘ { 𝑌 } ) ) = ( 𝑁 ‘ ( { 𝑋 } ∪ { 𝑌 } ) ) )
36 21 30 35 3eqtrrd ⊢ ( 𝜑 → ( 𝑁 ‘ ( { 𝑋 } ∪ { 𝑌 } ) ) = ( 𝐼 ‘ ( ( ◡ 𝐼 ‘ ( 𝑁 ‘ { 𝑋 } ) ) ( join ‘ 𝐾 ) ( ◡ 𝐼 ‘ ( 𝑁 ‘ { 𝑌 } ) ) ) ) )
37 13 36 syl5eq ⊢ ( 𝜑 → ( 𝑁 ‘ { 𝑋 , 𝑌 } ) = ( 𝐼 ‘ ( ( ◡ 𝐼 ‘ ( 𝑁 ‘ { 𝑋 } ) ) ( join ‘ 𝐾 ) ( ◡ 𝐼 ‘ ( 𝑁 ‘ { 𝑌 } ) ) ) ) )
38 6 simpld ⊢ ( 𝜑 → 𝐾 ∈ HL )
39 38 hllatd ⊢ ( 𝜑 → 𝐾 ∈ Lat )
40 eqid ⊢ ( Base ‘ 𝐾 ) = ( Base ‘ 𝐾 )
41 40 1 5 dihcnvcl ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑁 ‘ { 𝑋 } ) ∈ ran 𝐼 ) → ( ◡ 𝐼 ‘ ( 𝑁 ‘ { 𝑋 } ) ) ∈ ( Base ‘ 𝐾 ) )
42 6 23 41 syl2anc ⊢ ( 𝜑 → ( ◡ 𝐼 ‘ ( 𝑁 ‘ { 𝑋 } ) ) ∈ ( Base ‘ 𝐾 ) )
43 40 1 5 dihcnvcl ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑁 ‘ { 𝑌 } ) ∈ ran 𝐼 ) → ( ◡ 𝐼 ‘ ( 𝑁 ‘ { 𝑌 } ) ) ∈ ( Base ‘ 𝐾 ) )
44 6 27 43 syl2anc ⊢ ( 𝜑 → ( ◡ 𝐼 ‘ ( 𝑁 ‘ { 𝑌 } ) ) ∈ ( Base ‘ 𝐾 ) )
45 40 14 latjcl ⊢ ( ( 𝐾 ∈ Lat ∧ ( ◡ 𝐼 ‘ ( 𝑁 ‘ { 𝑋 } ) ) ∈ ( Base ‘ 𝐾 ) ∧ ( ◡ 𝐼 ‘ ( 𝑁 ‘ { 𝑌 } ) ) ∈ ( Base ‘ 𝐾 ) ) → ( ( ◡ 𝐼 ‘ ( 𝑁 ‘ { 𝑋 } ) ) ( join ‘ 𝐾 ) ( ◡ 𝐼 ‘ ( 𝑁 ‘ { 𝑌 } ) ) ) ∈ ( Base ‘ 𝐾 ) )
46 39 42 44 45 syl3anc ⊢ ( 𝜑 → ( ( ◡ 𝐼 ‘ ( 𝑁 ‘ { 𝑋 } ) ) ( join ‘ 𝐾 ) ( ◡ 𝐼 ‘ ( 𝑁 ‘ { 𝑌 } ) ) ) ∈ ( Base ‘ 𝐾 ) )
47 40 1 5 dihcl ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( ( ◡ 𝐼 ‘ ( 𝑁 ‘ { 𝑋 } ) ) ( join ‘ 𝐾 ) ( ◡ 𝐼 ‘ ( 𝑁 ‘ { 𝑌 } ) ) ) ∈ ( Base ‘ 𝐾 ) ) → ( 𝐼 ‘ ( ( ◡ 𝐼 ‘ ( 𝑁 ‘ { 𝑋 } ) ) ( join ‘ 𝐾 ) ( ◡ 𝐼 ‘ ( 𝑁 ‘ { 𝑌 } ) ) ) ) ∈ ran 𝐼 )
48 6 46 47 syl2anc ⊢ ( 𝜑 → ( 𝐼 ‘ ( ( ◡ 𝐼 ‘ ( 𝑁 ‘ { 𝑋 } ) ) ( join ‘ 𝐾 ) ( ◡ 𝐼 ‘ ( 𝑁 ‘ { 𝑌 } ) ) ) ) ∈ ran 𝐼 )
49 37 48 eqeltrd ⊢ ( 𝜑 → ( 𝑁 ‘ { 𝑋 , 𝑌 } ) ∈ ran 𝐼 )