Metamath Proof Explorer

Theorem lclkrlem2c

Description: Lemma for lclkr . (Contributed by NM, 16-Jan-2015)

Ref Expression
Hypotheses lclkrlem2a.h ⊢ 𝐻 = ( LHyp ‘ 𝐾 )
lclkrlem2a.o ⊢ ⊥ = ( ( ocH ‘ 𝐾 ) ‘ 𝑊 )
lclkrlem2a.u ⊢ 𝑈 = ( ( DVecH ‘ 𝐾 ) ‘ 𝑊 )
lclkrlem2a.v ⊢ 𝑉 = ( Base ‘ 𝑈 )
lclkrlem2a.z ⊢ 0 = ( 0g ‘ 𝑈 )
lclkrlem2a.p ⊢ ⊕ = ( LSSum ‘ 𝑈 )
lclkrlem2a.n ⊢ 𝑁 = ( LSpan ‘ 𝑈 )
lclkrlem2a.a ⊢ 𝐴 = ( LSAtoms ‘ 𝑈 )
lclkrlem2a.k ⊢ ( 𝜑 → ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) )
lclkrlem2a.b ⊢ ( 𝜑 → 𝐵 ∈ ( 𝑉 ∖ { 0 } ) )
lclkrlem2a.x ⊢ ( 𝜑 → 𝑋 ∈ ( 𝑉 ∖ { 0 } ) )
lclkrlem2a.y ⊢ ( 𝜑 → 𝑌 ∈ ( 𝑉 ∖ { 0 } ) )
lclkrlem2a.e ⊢ ( 𝜑 → ( ⊥ ‘ { 𝑋 } ) ≠ ( ⊥ ‘ { 𝑌 } ) )
lclkrlem2b.da ⊢ ( 𝜑 → ( ¬ 𝑋 ∈ ( ⊥ ‘ { 𝐵 } ) ∨ ¬ 𝑌 ∈ ( ⊥ ‘ { 𝐵 } ) ) )
lclkrlem2c.j ⊢ 𝐽 = ( LSHyp ‘ 𝑈 )
Assertion lclkrlem2c ( 𝜑 → ( ( ( ⊥ ‘ { 𝑋 } ) ∩ ( ⊥ ‘ { 𝑌 } ) ) ⊕ ( 𝑁 ‘ { 𝐵 } ) ) ∈ 𝐽 )

Proof

Step Hyp Ref Expression
1 lclkrlem2a.h ⊢ 𝐻 = ( LHyp ‘ 𝐾 )
2 lclkrlem2a.o ⊢ ⊥ = ( ( ocH ‘ 𝐾 ) ‘ 𝑊 )
3 lclkrlem2a.u ⊢ 𝑈 = ( ( DVecH ‘ 𝐾 ) ‘ 𝑊 )
4 lclkrlem2a.v ⊢ 𝑉 = ( Base ‘ 𝑈 )
5 lclkrlem2a.z ⊢ 0 = ( 0g ‘ 𝑈 )
6 lclkrlem2a.p ⊢ ⊕ = ( LSSum ‘ 𝑈 )
7 lclkrlem2a.n ⊢ 𝑁 = ( LSpan ‘ 𝑈 )
8 lclkrlem2a.a ⊢ 𝐴 = ( LSAtoms ‘ 𝑈 )
9 lclkrlem2a.k ⊢ ( 𝜑 → ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) )
10 lclkrlem2a.b ⊢ ( 𝜑 → 𝐵 ∈ ( 𝑉 ∖ { 0 } ) )
11 lclkrlem2a.x ⊢ ( 𝜑 → 𝑋 ∈ ( 𝑉 ∖ { 0 } ) )
12 lclkrlem2a.y ⊢ ( 𝜑 → 𝑌 ∈ ( 𝑉 ∖ { 0 } ) )
13 lclkrlem2a.e ⊢ ( 𝜑 → ( ⊥ ‘ { 𝑋 } ) ≠ ( ⊥ ‘ { 𝑌 } ) )
14 lclkrlem2b.da ⊢ ( 𝜑 → ( ¬ 𝑋 ∈ ( ⊥ ‘ { 𝐵 } ) ∨ ¬ 𝑌 ∈ ( ⊥ ‘ { 𝐵 } ) ) )
15 lclkrlem2c.j ⊢ 𝐽 = ( LSHyp ‘ 𝑈 )
16 eqid ⊢ ( ( DIsoH ‘ 𝐾 ) ‘ 𝑊 ) = ( ( DIsoH ‘ 𝐾 ) ‘ 𝑊 )
17 eqid ⊢ ( ( joinH ‘ 𝐾 ) ‘ 𝑊 ) = ( ( joinH ‘ 𝐾 ) ‘ 𝑊 )
18 11 eldifad ⊢ ( 𝜑 → 𝑋 ∈ 𝑉 )
19 1 3 4 7 16 dihlsprn ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝑋 ∈ 𝑉 ) → ( 𝑁 ‘ { 𝑋 } ) ∈ ran ( ( DIsoH ‘ 𝐾 ) ‘ 𝑊 ) )
20 9 18 19 syl2anc ⊢ ( 𝜑 → ( 𝑁 ‘ { 𝑋 } ) ∈ ran ( ( DIsoH ‘ 𝐾 ) ‘ 𝑊 ) )
21 1 3 9 dvhlmod ⊢ ( 𝜑 → 𝑈 ∈ LMod )
22 4 7 5 8 21 12 lsatlspsn ⊢ ( 𝜑 → ( 𝑁 ‘ { 𝑌 } ) ∈ 𝐴 )
23 1 16 3 6 8 9 20 22 dihsmatrn ⊢ ( 𝜑 → ( ( 𝑁 ‘ { 𝑋 } ) ⊕ ( 𝑁 ‘ { 𝑌 } ) ) ∈ ran ( ( DIsoH ‘ 𝐾 ) ‘ 𝑊 ) )
24 10 eldifad ⊢ ( 𝜑 → 𝐵 ∈ 𝑉 )
25 24 snssd ⊢ ( 𝜑 → { 𝐵 } ⊆ 𝑉 )
26 1 16 3 4 2 dochcl ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ { 𝐵 } ⊆ 𝑉 ) → ( ⊥ ‘ { 𝐵 } ) ∈ ran ( ( DIsoH ‘ 𝐾 ) ‘ 𝑊 ) )
27 9 25 26 syl2anc ⊢ ( 𝜑 → ( ⊥ ‘ { 𝐵 } ) ∈ ran ( ( DIsoH ‘ 𝐾 ) ‘ 𝑊 ) )
28 1 16 3 4 2 17 9 23 27 dochdmm1 ⊢ ( 𝜑 → ( ⊥ ‘ ( ( ( 𝑁 ‘ { 𝑋 } ) ⊕ ( 𝑁 ‘ { 𝑌 } ) ) ∩ ( ⊥ ‘ { 𝐵 } ) ) ) = ( ( ⊥ ‘ ( ( 𝑁 ‘ { 𝑋 } ) ⊕ ( 𝑁 ‘ { 𝑌 } ) ) ) ( ( joinH ‘ 𝐾 ) ‘ 𝑊 ) ( ⊥ ‘ ( ⊥ ‘ { 𝐵 } ) ) ) )
29 12 eldifad ⊢ ( 𝜑 → 𝑌 ∈ 𝑉 )
30 4 7 6 21 18 29 lsmpr ⊢ ( 𝜑 → ( 𝑁 ‘ { 𝑋 , 𝑌 } ) = ( ( 𝑁 ‘ { 𝑋 } ) ⊕ ( 𝑁 ‘ { 𝑌 } ) ) )
31 df-pr ⊢ { 𝑋 , 𝑌 } = ( { 𝑋 } ∪ { 𝑌 } )
32 31 fveq2i ⊢ ( 𝑁 ‘ { 𝑋 , 𝑌 } ) = ( 𝑁 ‘ ( { 𝑋 } ∪ { 𝑌 } ) )
33 30 32 eqtr3di ⊢ ( 𝜑 → ( ( 𝑁 ‘ { 𝑋 } ) ⊕ ( 𝑁 ‘ { 𝑌 } ) ) = ( 𝑁 ‘ ( { 𝑋 } ∪ { 𝑌 } ) ) )
34 33 fveq2d ⊢ ( 𝜑 → ( ⊥ ‘ ( ( 𝑁 ‘ { 𝑋 } ) ⊕ ( 𝑁 ‘ { 𝑌 } ) ) ) = ( ⊥ ‘ ( 𝑁 ‘ ( { 𝑋 } ∪ { 𝑌 } ) ) ) )
35 18 snssd ⊢ ( 𝜑 → { 𝑋 } ⊆ 𝑉 )
36 29 snssd ⊢ ( 𝜑 → { 𝑌 } ⊆ 𝑉 )
37 35 36 unssd ⊢ ( 𝜑 → ( { 𝑋 } ∪ { 𝑌 } ) ⊆ 𝑉 )
38 1 3 2 4 7 9 37 dochocsp ⊢ ( 𝜑 → ( ⊥ ‘ ( 𝑁 ‘ ( { 𝑋 } ∪ { 𝑌 } ) ) ) = ( ⊥ ‘ ( { 𝑋 } ∪ { 𝑌 } ) ) )
39 1 3 4 2 dochdmj1 ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ { 𝑋 } ⊆ 𝑉 ∧ { 𝑌 } ⊆ 𝑉 ) → ( ⊥ ‘ ( { 𝑋 } ∪ { 𝑌 } ) ) = ( ( ⊥ ‘ { 𝑋 } ) ∩ ( ⊥ ‘ { 𝑌 } ) ) )
40 9 35 36 39 syl3anc ⊢ ( 𝜑 → ( ⊥ ‘ ( { 𝑋 } ∪ { 𝑌 } ) ) = ( ( ⊥ ‘ { 𝑋 } ) ∩ ( ⊥ ‘ { 𝑌 } ) ) )
41 34 38 40 3eqtrd ⊢ ( 𝜑 → ( ⊥ ‘ ( ( 𝑁 ‘ { 𝑋 } ) ⊕ ( 𝑁 ‘ { 𝑌 } ) ) ) = ( ( ⊥ ‘ { 𝑋 } ) ∩ ( ⊥ ‘ { 𝑌 } ) ) )
42 1 3 2 4 7 9 24 dochocsn ⊢ ( 𝜑 → ( ⊥ ‘ ( ⊥ ‘ { 𝐵 } ) ) = ( 𝑁 ‘ { 𝐵 } ) )
43 41 42 oveq12d ⊢ ( 𝜑 → ( ( ⊥ ‘ ( ( 𝑁 ‘ { 𝑋 } ) ⊕ ( 𝑁 ‘ { 𝑌 } ) ) ) ( ( joinH ‘ 𝐾 ) ‘ 𝑊 ) ( ⊥ ‘ ( ⊥ ‘ { 𝐵 } ) ) ) = ( ( ( ⊥ ‘ { 𝑋 } ) ∩ ( ⊥ ‘ { 𝑌 } ) ) ( ( joinH ‘ 𝐾 ) ‘ 𝑊 ) ( 𝑁 ‘ { 𝐵 } ) ) )
44 1 16 3 4 2 dochcl ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ { 𝑋 } ⊆ 𝑉 ) → ( ⊥ ‘ { 𝑋 } ) ∈ ran ( ( DIsoH ‘ 𝐾 ) ‘ 𝑊 ) )
45 9 35 44 syl2anc ⊢ ( 𝜑 → ( ⊥ ‘ { 𝑋 } ) ∈ ran ( ( DIsoH ‘ 𝐾 ) ‘ 𝑊 ) )
46 1 16 3 4 2 dochcl ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ { 𝑌 } ⊆ 𝑉 ) → ( ⊥ ‘ { 𝑌 } ) ∈ ran ( ( DIsoH ‘ 𝐾 ) ‘ 𝑊 ) )
47 9 36 46 syl2anc ⊢ ( 𝜑 → ( ⊥ ‘ { 𝑌 } ) ∈ ran ( ( DIsoH ‘ 𝐾 ) ‘ 𝑊 ) )
48 1 16 dihmeetcl ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( ( ⊥ ‘ { 𝑋 } ) ∈ ran ( ( DIsoH ‘ 𝐾 ) ‘ 𝑊 ) ∧ ( ⊥ ‘ { 𝑌 } ) ∈ ran ( ( DIsoH ‘ 𝐾 ) ‘ 𝑊 ) ) ) → ( ( ⊥ ‘ { 𝑋 } ) ∩ ( ⊥ ‘ { 𝑌 } ) ) ∈ ran ( ( DIsoH ‘ 𝐾 ) ‘ 𝑊 ) )
49 9 45 47 48 syl12anc ⊢ ( 𝜑 → ( ( ⊥ ‘ { 𝑋 } ) ∩ ( ⊥ ‘ { 𝑌 } ) ) ∈ ran ( ( DIsoH ‘ 𝐾 ) ‘ 𝑊 ) )
50 1 3 4 6 7 16 17 9 49 24 dihjat1 ⊢ ( 𝜑 → ( ( ( ⊥ ‘ { 𝑋 } ) ∩ ( ⊥ ‘ { 𝑌 } ) ) ( ( joinH ‘ 𝐾 ) ‘ 𝑊 ) ( 𝑁 ‘ { 𝐵 } ) ) = ( ( ( ⊥ ‘ { 𝑋 } ) ∩ ( ⊥ ‘ { 𝑌 } ) ) ⊕ ( 𝑁 ‘ { 𝐵 } ) ) )
51 28 43 50 3eqtrrd ⊢ ( 𝜑 → ( ( ( ⊥ ‘ { 𝑋 } ) ∩ ( ⊥ ‘ { 𝑌 } ) ) ⊕ ( 𝑁 ‘ { 𝐵 } ) ) = ( ⊥ ‘ ( ( ( 𝑁 ‘ { 𝑋 } ) ⊕ ( 𝑁 ‘ { 𝑌 } ) ) ∩ ( ⊥ ‘ { 𝐵 } ) ) ) )
52 1 2 3 4 5 6 7 8 9 10 11 12 13 14 lclkrlem2b ⊢ ( 𝜑 → ( ( ( 𝑁 ‘ { 𝑋 } ) ⊕ ( 𝑁 ‘ { 𝑌 } ) ) ∩ ( ⊥ ‘ { 𝐵 } ) ) ∈ 𝐴 )
53 1 3 2 8 15 9 52 dochsatshp ⊢ ( 𝜑 → ( ⊥ ‘ ( ( ( 𝑁 ‘ { 𝑋 } ) ⊕ ( 𝑁 ‘ { 𝑌 } ) ) ∩ ( ⊥ ‘ { 𝐵 } ) ) ) ∈ 𝐽 )
54 51 53 eqeltrd ⊢ ( 𝜑 → ( ( ( ⊥ ‘ { 𝑋 } ) ∩ ( ⊥ ‘ { 𝑌 } ) ) ⊕ ( 𝑁 ‘ { 𝐵 } ) ) ∈ 𝐽 )