Metamath Proof Explorer

Theorem lclkrlem2v

Description: Lemma for lclkr . When the hypotheses of lclkrlem2u and lclkrlem2u are negated, the functional sum must be zero, so the kernel is the vector space. We make use of the law of excluded middle, dochexmid , which requires the orthomodular law dihoml4 (Lemma 3.3 of Holland95 p. 214). (Contributed by NM, 16-Jan-2015)

Ref Expression
Hypotheses lclkrlem2m.v ⊢ 𝑉 = ( Base ‘ 𝑈 )
lclkrlem2m.t ⊢ · = ( ·𝑠 ‘ 𝑈 )
lclkrlem2m.s ⊢ 𝑆 = ( Scalar ‘ 𝑈 )
lclkrlem2m.q ⊢ × = ( .r ‘ 𝑆 )
lclkrlem2m.z ⊢ 0 = ( 0g ‘ 𝑆 )
lclkrlem2m.i ⊢ 𝐼 = ( invr ‘ 𝑆 )
lclkrlem2m.m ⊢ − = ( -g ‘ 𝑈 )
lclkrlem2m.f ⊢ 𝐹 = ( LFnl ‘ 𝑈 )
lclkrlem2m.d ⊢ 𝐷 = ( LDual ‘ 𝑈 )
lclkrlem2m.p ⊢ + = ( +g ‘ 𝐷 )
lclkrlem2m.x ⊢ ( 𝜑 → 𝑋 ∈ 𝑉 )
lclkrlem2m.y ⊢ ( 𝜑 → 𝑌 ∈ 𝑉 )
lclkrlem2m.e ⊢ ( 𝜑 → 𝐸 ∈ 𝐹 )
lclkrlem2m.g ⊢ ( 𝜑 → 𝐺 ∈ 𝐹 )
lclkrlem2n.n ⊢ 𝑁 = ( LSpan ‘ 𝑈 )
lclkrlem2n.l ⊢ 𝐿 = ( LKer ‘ 𝑈 )
lclkrlem2o.h ⊢ 𝐻 = ( LHyp ‘ 𝐾 )
lclkrlem2o.o ⊢ ⊥ = ( ( ocH ‘ 𝐾 ) ‘ 𝑊 )
lclkrlem2o.u ⊢ 𝑈 = ( ( DVecH ‘ 𝐾 ) ‘ 𝑊 )
lclkrlem2o.a ⊢ ⊕ = ( LSSum ‘ 𝑈 )
lclkrlem2o.k ⊢ ( 𝜑 → ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) )
lclkrlem2q.le ⊢ ( 𝜑 → ( 𝐿 ‘ 𝐸 ) = ( ⊥ ‘ { 𝑋 } ) )
lclkrlem2q.lg ⊢ ( 𝜑 → ( 𝐿 ‘ 𝐺 ) = ( ⊥ ‘ { 𝑌 } ) )
lclkrlem2v.j ⊢ ( 𝜑 → ( ( 𝐸 + 𝐺 ) ‘ 𝑋 ) = 0 )
lclkrlem2v.k ⊢ ( 𝜑 → ( ( 𝐸 + 𝐺 ) ‘ 𝑌 ) = 0 )
Assertion lclkrlem2v ( 𝜑 → ( 𝐿 ‘ ( 𝐸 + 𝐺 ) ) = 𝑉 )

Proof

Step Hyp Ref Expression
1 lclkrlem2m.v ⊢ 𝑉 = ( Base ‘ 𝑈 )
2 lclkrlem2m.t ⊢ · = ( ·𝑠 ‘ 𝑈 )
3 lclkrlem2m.s ⊢ 𝑆 = ( Scalar ‘ 𝑈 )
4 lclkrlem2m.q ⊢ × = ( .r ‘ 𝑆 )
5 lclkrlem2m.z ⊢ 0 = ( 0g ‘ 𝑆 )
6 lclkrlem2m.i ⊢ 𝐼 = ( invr ‘ 𝑆 )
7 lclkrlem2m.m ⊢ − = ( -g ‘ 𝑈 )
8 lclkrlem2m.f ⊢ 𝐹 = ( LFnl ‘ 𝑈 )
9 lclkrlem2m.d ⊢ 𝐷 = ( LDual ‘ 𝑈 )
10 lclkrlem2m.p ⊢ + = ( +g ‘ 𝐷 )
11 lclkrlem2m.x ⊢ ( 𝜑 → 𝑋 ∈ 𝑉 )
12 lclkrlem2m.y ⊢ ( 𝜑 → 𝑌 ∈ 𝑉 )
13 lclkrlem2m.e ⊢ ( 𝜑 → 𝐸 ∈ 𝐹 )
14 lclkrlem2m.g ⊢ ( 𝜑 → 𝐺 ∈ 𝐹 )
15 lclkrlem2n.n ⊢ 𝑁 = ( LSpan ‘ 𝑈 )
16 lclkrlem2n.l ⊢ 𝐿 = ( LKer ‘ 𝑈 )
17 lclkrlem2o.h ⊢ 𝐻 = ( LHyp ‘ 𝐾 )
18 lclkrlem2o.o ⊢ ⊥ = ( ( ocH ‘ 𝐾 ) ‘ 𝑊 )
19 lclkrlem2o.u ⊢ 𝑈 = ( ( DVecH ‘ 𝐾 ) ‘ 𝑊 )
20 lclkrlem2o.a ⊢ ⊕ = ( LSSum ‘ 𝑈 )
21 lclkrlem2o.k ⊢ ( 𝜑 → ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) )
22 lclkrlem2q.le ⊢ ( 𝜑 → ( 𝐿 ‘ 𝐸 ) = ( ⊥ ‘ { 𝑋 } ) )
23 lclkrlem2q.lg ⊢ ( 𝜑 → ( 𝐿 ‘ 𝐺 ) = ( ⊥ ‘ { 𝑌 } ) )
24 lclkrlem2v.j ⊢ ( 𝜑 → ( ( 𝐸 + 𝐺 ) ‘ 𝑋 ) = 0 )
25 lclkrlem2v.k ⊢ ( 𝜑 → ( ( 𝐸 + 𝐺 ) ‘ 𝑌 ) = 0 )
26 17 19 21 dvhlmod ⊢ ( 𝜑 → 𝑈 ∈ LMod )
27 8 9 10 26 13 14 ldualvaddcl ⊢ ( 𝜑 → ( 𝐸 + 𝐺 ) ∈ 𝐹 )
28 1 8 16 26 27 lkrssv ⊢ ( 𝜑 → ( 𝐿 ‘ ( 𝐸 + 𝐺 ) ) ⊆ 𝑉 )
29 eqid ⊢ ( LSubSp ‘ 𝑈 ) = ( LSubSp ‘ 𝑈 )
30 1 29 15 26 11 12 lspprcl ⊢ ( 𝜑 → ( 𝑁 ‘ { 𝑋 , 𝑌 } ) ∈ ( LSubSp ‘ 𝑈 ) )
31 eqid ⊢ ( ( DIsoH ‘ 𝐾 ) ‘ 𝑊 ) = ( ( DIsoH ‘ 𝐾 ) ‘ 𝑊 )
32 17 19 1 15 31 21 11 12 dihprrn ⊢ ( 𝜑 → ( 𝑁 ‘ { 𝑋 , 𝑌 } ) ∈ ran ( ( DIsoH ‘ 𝐾 ) ‘ 𝑊 ) )
33 1 29 lssss ⊢ ( ( 𝑁 ‘ { 𝑋 , 𝑌 } ) ∈ ( LSubSp ‘ 𝑈 ) → ( 𝑁 ‘ { 𝑋 , 𝑌 } ) ⊆ 𝑉 )
34 30 33 syl ⊢ ( 𝜑 → ( 𝑁 ‘ { 𝑋 , 𝑌 } ) ⊆ 𝑉 )
35 17 31 19 1 18 21 34 dochoccl ⊢ ( 𝜑 → ( ( 𝑁 ‘ { 𝑋 , 𝑌 } ) ∈ ran ( ( DIsoH ‘ 𝐾 ) ‘ 𝑊 ) ↔ ( ⊥ ‘ ( ⊥ ‘ ( 𝑁 ‘ { 𝑋 , 𝑌 } ) ) ) = ( 𝑁 ‘ { 𝑋 , 𝑌 } ) ) )
36 32 35 mpbid ⊢ ( 𝜑 → ( ⊥ ‘ ( ⊥ ‘ ( 𝑁 ‘ { 𝑋 , 𝑌 } ) ) ) = ( 𝑁 ‘ { 𝑋 , 𝑌 } ) )
37 17 18 19 1 29 20 21 30 36 dochexmid ⊢ ( 𝜑 → ( ( 𝑁 ‘ { 𝑋 , 𝑌 } ) ⊕ ( ⊥ ‘ ( 𝑁 ‘ { 𝑋 , 𝑌 } ) ) ) = 𝑉 )
38 17 19 21 dvhlvec ⊢ ( 𝜑 → 𝑈 ∈ LVec )
39 1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 38 24 25 lclkrlem2n ⊢ ( 𝜑 → ( 𝑁 ‘ { 𝑋 , 𝑌 } ) ⊆ ( 𝐿 ‘ ( 𝐸 + 𝐺 ) ) )
40 11 snssd ⊢ ( 𝜑 → { 𝑋 } ⊆ 𝑉 )
41 12 snssd ⊢ ( 𝜑 → { 𝑌 } ⊆ 𝑉 )
42 17 19 1 18 dochdmj1 ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ { 𝑋 } ⊆ 𝑉 ∧ { 𝑌 } ⊆ 𝑉 ) → ( ⊥ ‘ ( { 𝑋 } ∪ { 𝑌 } ) ) = ( ( ⊥ ‘ { 𝑋 } ) ∩ ( ⊥ ‘ { 𝑌 } ) ) )
43 21 40 41 42 syl3anc ⊢ ( 𝜑 → ( ⊥ ‘ ( { 𝑋 } ∪ { 𝑌 } ) ) = ( ( ⊥ ‘ { 𝑋 } ) ∩ ( ⊥ ‘ { 𝑌 } ) ) )
44 df-pr ⊢ { 𝑋 , 𝑌 } = ( { 𝑋 } ∪ { 𝑌 } )
45 44 fveq2i ⊢ ( 𝑁 ‘ { 𝑋 , 𝑌 } ) = ( 𝑁 ‘ ( { 𝑋 } ∪ { 𝑌 } ) )
46 45 fveq2i ⊢ ( ⊥ ‘ ( 𝑁 ‘ { 𝑋 , 𝑌 } ) ) = ( ⊥ ‘ ( 𝑁 ‘ ( { 𝑋 } ∪ { 𝑌 } ) ) )
47 40 41 unssd ⊢ ( 𝜑 → ( { 𝑋 } ∪ { 𝑌 } ) ⊆ 𝑉 )
48 17 19 18 1 15 21 47 dochocsp ⊢ ( 𝜑 → ( ⊥ ‘ ( 𝑁 ‘ ( { 𝑋 } ∪ { 𝑌 } ) ) ) = ( ⊥ ‘ ( { 𝑋 } ∪ { 𝑌 } ) ) )
49 46 48 syl5eq ⊢ ( 𝜑 → ( ⊥ ‘ ( 𝑁 ‘ { 𝑋 , 𝑌 } ) ) = ( ⊥ ‘ ( { 𝑋 } ∪ { 𝑌 } ) ) )
50 22 23 ineq12d ⊢ ( 𝜑 → ( ( 𝐿 ‘ 𝐸 ) ∩ ( 𝐿 ‘ 𝐺 ) ) = ( ( ⊥ ‘ { 𝑋 } ) ∩ ( ⊥ ‘ { 𝑌 } ) ) )
51 43 49 50 3eqtr4d ⊢ ( 𝜑 → ( ⊥ ‘ ( 𝑁 ‘ { 𝑋 , 𝑌 } ) ) = ( ( 𝐿 ‘ 𝐸 ) ∩ ( 𝐿 ‘ 𝐺 ) ) )
52 8 16 9 10 26 13 14 lkrin ⊢ ( 𝜑 → ( ( 𝐿 ‘ 𝐸 ) ∩ ( 𝐿 ‘ 𝐺 ) ) ⊆ ( 𝐿 ‘ ( 𝐸 + 𝐺 ) ) )
53 51 52 eqsstrd ⊢ ( 𝜑 → ( ⊥ ‘ ( 𝑁 ‘ { 𝑋 , 𝑌 } ) ) ⊆ ( 𝐿 ‘ ( 𝐸 + 𝐺 ) ) )
54 29 lsssssubg ⊢ ( 𝑈 ∈ LMod → ( LSubSp ‘ 𝑈 ) ⊆ ( SubGrp ‘ 𝑈 ) )
55 26 54 syl ⊢ ( 𝜑 → ( LSubSp ‘ 𝑈 ) ⊆ ( SubGrp ‘ 𝑈 ) )
56 55 30 sseldd ⊢ ( 𝜑 → ( 𝑁 ‘ { 𝑋 , 𝑌 } ) ∈ ( SubGrp ‘ 𝑈 ) )
57 17 19 1 29 18 dochlss ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑁 ‘ { 𝑋 , 𝑌 } ) ⊆ 𝑉 ) → ( ⊥ ‘ ( 𝑁 ‘ { 𝑋 , 𝑌 } ) ) ∈ ( LSubSp ‘ 𝑈 ) )
58 21 34 57 syl2anc ⊢ ( 𝜑 → ( ⊥ ‘ ( 𝑁 ‘ { 𝑋 , 𝑌 } ) ) ∈ ( LSubSp ‘ 𝑈 ) )
59 55 58 sseldd ⊢ ( 𝜑 → ( ⊥ ‘ ( 𝑁 ‘ { 𝑋 , 𝑌 } ) ) ∈ ( SubGrp ‘ 𝑈 ) )
60 8 16 29 lkrlss ⊢ ( ( 𝑈 ∈ LMod ∧ ( 𝐸 + 𝐺 ) ∈ 𝐹 ) → ( 𝐿 ‘ ( 𝐸 + 𝐺 ) ) ∈ ( LSubSp ‘ 𝑈 ) )
61 26 27 60 syl2anc ⊢ ( 𝜑 → ( 𝐿 ‘ ( 𝐸 + 𝐺 ) ) ∈ ( LSubSp ‘ 𝑈 ) )
62 55 61 sseldd ⊢ ( 𝜑 → ( 𝐿 ‘ ( 𝐸 + 𝐺 ) ) ∈ ( SubGrp ‘ 𝑈 ) )
63 20 lsmlub ⊢ ( ( ( 𝑁 ‘ { 𝑋 , 𝑌 } ) ∈ ( SubGrp ‘ 𝑈 ) ∧ ( ⊥ ‘ ( 𝑁 ‘ { 𝑋 , 𝑌 } ) ) ∈ ( SubGrp ‘ 𝑈 ) ∧ ( 𝐿 ‘ ( 𝐸 + 𝐺 ) ) ∈ ( SubGrp ‘ 𝑈 ) ) → ( ( ( 𝑁 ‘ { 𝑋 , 𝑌 } ) ⊆ ( 𝐿 ‘ ( 𝐸 + 𝐺 ) ) ∧ ( ⊥ ‘ ( 𝑁 ‘ { 𝑋 , 𝑌 } ) ) ⊆ ( 𝐿 ‘ ( 𝐸 + 𝐺 ) ) ) ↔ ( ( 𝑁 ‘ { 𝑋 , 𝑌 } ) ⊕ ( ⊥ ‘ ( 𝑁 ‘ { 𝑋 , 𝑌 } ) ) ) ⊆ ( 𝐿 ‘ ( 𝐸 + 𝐺 ) ) ) )
64 56 59 62 63 syl3anc ⊢ ( 𝜑 → ( ( ( 𝑁 ‘ { 𝑋 , 𝑌 } ) ⊆ ( 𝐿 ‘ ( 𝐸 + 𝐺 ) ) ∧ ( ⊥ ‘ ( 𝑁 ‘ { 𝑋 , 𝑌 } ) ) ⊆ ( 𝐿 ‘ ( 𝐸 + 𝐺 ) ) ) ↔ ( ( 𝑁 ‘ { 𝑋 , 𝑌 } ) ⊕ ( ⊥ ‘ ( 𝑁 ‘ { 𝑋 , 𝑌 } ) ) ) ⊆ ( 𝐿 ‘ ( 𝐸 + 𝐺 ) ) ) )
65 39 53 64 mpbi2and ⊢ ( 𝜑 → ( ( 𝑁 ‘ { 𝑋 , 𝑌 } ) ⊕ ( ⊥ ‘ ( 𝑁 ‘ { 𝑋 , 𝑌 } ) ) ) ⊆ ( 𝐿 ‘ ( 𝐸 + 𝐺 ) ) )
66 37 65 eqsstrrd ⊢ ( 𝜑 → 𝑉 ⊆ ( 𝐿 ‘ ( 𝐸 + 𝐺 ) ) )
67 28 66 eqssd ⊢ ( 𝜑 → ( 𝐿 ‘ ( 𝐸 + 𝐺 ) ) = 𝑉 )