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