Metamath Proof Explorer

Theorem lcfl8b

Description: Property of a nonzero functional with a closed kernel. (Contributed by NM, 4-Feb-2015)

Ref Expression
Hypotheses lcfl8b.h ⊢ 𝐻 = ( LHyp ‘ 𝐾 )
lcfl8b.o ⊢ ⊥ = ( ( ocH ‘ 𝐾 ) ‘ 𝑊 )
lcfl8b.u ⊢ 𝑈 = ( ( DVecH ‘ 𝐾 ) ‘ 𝑊 )
lcfl8b.v ⊢ 𝑉 = ( Base ‘ 𝑈 )
lcfl8b.n ⊢ 𝑁 = ( LSpan ‘ 𝑈 )
lcfl8b.z ⊢ 0 = ( 0g ‘ 𝑈 )
lcfl8b.f ⊢ 𝐹 = ( LFnl ‘ 𝑈 )
lcfl8b.l ⊢ 𝐿 = ( LKer ‘ 𝑈 )
lcfl8b.d ⊢ 𝐷 = ( LDual ‘ 𝑈 )
lcfl8b.y ⊢ 𝑌 = ( 0g ‘ 𝐷 )
lcfl8b.c ⊢ 𝐶 = { 𝑓 ∈ 𝐹 ∣ ( ⊥ ‘ ( ⊥ ‘ ( 𝐿 ‘ 𝑓 ) ) ) = ( 𝐿 ‘ 𝑓 ) }
lcfl8b.k ⊢ ( 𝜑 → ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) )
lcfl8b.g ⊢ ( 𝜑 → 𝐺 ∈ ( 𝐶 ∖ { 𝑌 } ) )
Assertion lcfl8b ( 𝜑 → ∃ 𝑥 ∈ ( 𝑉 ∖ { 0 } ) ( ⊥ ‘ ( 𝐿 ‘ 𝐺 ) ) = ( 𝑁 ‘ { 𝑥 } ) )

Proof

Step Hyp Ref Expression
1 lcfl8b.h ⊢ 𝐻 = ( LHyp ‘ 𝐾 )
2 lcfl8b.o ⊢ ⊥ = ( ( ocH ‘ 𝐾 ) ‘ 𝑊 )
3 lcfl8b.u ⊢ 𝑈 = ( ( DVecH ‘ 𝐾 ) ‘ 𝑊 )
4 lcfl8b.v ⊢ 𝑉 = ( Base ‘ 𝑈 )
5 lcfl8b.n ⊢ 𝑁 = ( LSpan ‘ 𝑈 )
6 lcfl8b.z ⊢ 0 = ( 0g ‘ 𝑈 )
7 lcfl8b.f ⊢ 𝐹 = ( LFnl ‘ 𝑈 )
8 lcfl8b.l ⊢ 𝐿 = ( LKer ‘ 𝑈 )
9 lcfl8b.d ⊢ 𝐷 = ( LDual ‘ 𝑈 )
10 lcfl8b.y ⊢ 𝑌 = ( 0g ‘ 𝐷 )
11 lcfl8b.c ⊢ 𝐶 = { 𝑓 ∈ 𝐹 ∣ ( ⊥ ‘ ( ⊥ ‘ ( 𝐿 ‘ 𝑓 ) ) ) = ( 𝐿 ‘ 𝑓 ) }
12 lcfl8b.k ⊢ ( 𝜑 → ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) )
13 lcfl8b.g ⊢ ( 𝜑 → 𝐺 ∈ ( 𝐶 ∖ { 𝑌 } ) )
14 13 eldifad ⊢ ( 𝜑 → 𝐺 ∈ 𝐶 )
15 11 lcfl1lem ⊢ ( 𝐺 ∈ 𝐶 ↔ ( 𝐺 ∈ 𝐹 ∧ ( ⊥ ‘ ( ⊥ ‘ ( 𝐿 ‘ 𝐺 ) ) ) = ( 𝐿 ‘ 𝐺 ) ) )
16 15 simplbi ⊢ ( 𝐺 ∈ 𝐶 → 𝐺 ∈ 𝐹 )
17 14 16 syl ⊢ ( 𝜑 → 𝐺 ∈ 𝐹 )
18 1 2 3 4 7 8 11 12 17 lcfl8 ⊢ ( 𝜑 → ( 𝐺 ∈ 𝐶 ↔ ∃ 𝑥 ∈ 𝑉 ( 𝐿 ‘ 𝐺 ) = ( ⊥ ‘ { 𝑥 } ) ) )
19 14 18 mpbid ⊢ ( 𝜑 → ∃ 𝑥 ∈ 𝑉 ( 𝐿 ‘ 𝐺 ) = ( ⊥ ‘ { 𝑥 } ) )
20 fveq2 ⊢ ( ( 𝐿 ‘ 𝐺 ) = ( ⊥ ‘ { 𝑥 } ) → ( ⊥ ‘ ( 𝐿 ‘ 𝐺 ) ) = ( ⊥ ‘ ( ⊥ ‘ { 𝑥 } ) ) )
21 20 adantl ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ 𝑉 ) ∧ ( 𝐿 ‘ 𝐺 ) = ( ⊥ ‘ { 𝑥 } ) ) → ( ⊥ ‘ ( 𝐿 ‘ 𝐺 ) ) = ( ⊥ ‘ ( ⊥ ‘ { 𝑥 } ) ) )
22 12 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ 𝑉 ) ∧ ( 𝐿 ‘ 𝐺 ) = ( ⊥ ‘ { 𝑥 } ) ) → ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) )
23 simplr ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ 𝑉 ) ∧ ( 𝐿 ‘ 𝐺 ) = ( ⊥ ‘ { 𝑥 } ) ) → 𝑥 ∈ 𝑉 )
24 1 3 2 4 5 22 23 dochocsn ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ 𝑉 ) ∧ ( 𝐿 ‘ 𝐺 ) = ( ⊥ ‘ { 𝑥 } ) ) → ( ⊥ ‘ ( ⊥ ‘ { 𝑥 } ) ) = ( 𝑁 ‘ { 𝑥 } ) )
25 21 24 eqtrd ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ 𝑉 ) ∧ ( 𝐿 ‘ 𝐺 ) = ( ⊥ ‘ { 𝑥 } ) ) → ( ⊥ ‘ ( 𝐿 ‘ 𝐺 ) ) = ( 𝑁 ‘ { 𝑥 } ) )
26 14 15 sylib ⊢ ( 𝜑 → ( 𝐺 ∈ 𝐹 ∧ ( ⊥ ‘ ( ⊥ ‘ ( 𝐿 ‘ 𝐺 ) ) ) = ( 𝐿 ‘ 𝐺 ) ) )
27 26 simprd ⊢ ( 𝜑 → ( ⊥ ‘ ( ⊥ ‘ ( 𝐿 ‘ 𝐺 ) ) ) = ( 𝐿 ‘ 𝐺 ) )
28 eldifsni ⊢ ( 𝐺 ∈ ( 𝐶 ∖ { 𝑌 } ) → 𝐺 ≠ 𝑌 )
29 13 28 syl ⊢ ( 𝜑 → 𝐺 ≠ 𝑌 )
30 1 3 12 dvhlmod ⊢ ( 𝜑 → 𝑈 ∈ LMod )
31 4 7 8 9 10 30 17 lkr0f2 ⊢ ( 𝜑 → ( ( 𝐿 ‘ 𝐺 ) = 𝑉 ↔ 𝐺 = 𝑌 ) )
32 31 necon3bid ⊢ ( 𝜑 → ( ( 𝐿 ‘ 𝐺 ) ≠ 𝑉 ↔ 𝐺 ≠ 𝑌 ) )
33 29 32 mpbird ⊢ ( 𝜑 → ( 𝐿 ‘ 𝐺 ) ≠ 𝑉 )
34 27 33 eqnetrd ⊢ ( 𝜑 → ( ⊥ ‘ ( ⊥ ‘ ( 𝐿 ‘ 𝐺 ) ) ) ≠ 𝑉 )
35 34 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ 𝑉 ) ∧ ( 𝐿 ‘ 𝐺 ) = ( ⊥ ‘ { 𝑥 } ) ) → ( ⊥ ‘ ( ⊥ ‘ ( 𝐿 ‘ 𝐺 ) ) ) ≠ 𝑉 )
36 eqid ⊢ ( LSAtoms ‘ 𝑈 ) = ( LSAtoms ‘ 𝑈 )
37 17 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ 𝑉 ) ∧ ( 𝐿 ‘ 𝐺 ) = ( ⊥ ‘ { 𝑥 } ) ) → 𝐺 ∈ 𝐹 )
38 1 2 3 4 36 7 8 22 37 dochkrsat2 ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ 𝑉 ) ∧ ( 𝐿 ‘ 𝐺 ) = ( ⊥ ‘ { 𝑥 } ) ) → ( ( ⊥ ‘ ( ⊥ ‘ ( 𝐿 ‘ 𝐺 ) ) ) ≠ 𝑉 ↔ ( ⊥ ‘ ( 𝐿 ‘ 𝐺 ) ) ∈ ( LSAtoms ‘ 𝑈 ) ) )
39 35 38 mpbid ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ 𝑉 ) ∧ ( 𝐿 ‘ 𝐺 ) = ( ⊥ ‘ { 𝑥 } ) ) → ( ⊥ ‘ ( 𝐿 ‘ 𝐺 ) ) ∈ ( LSAtoms ‘ 𝑈 ) )
40 25 39 eqeltrrd ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ 𝑉 ) ∧ ( 𝐿 ‘ 𝐺 ) = ( ⊥ ‘ { 𝑥 } ) ) → ( 𝑁 ‘ { 𝑥 } ) ∈ ( LSAtoms ‘ 𝑈 ) )
41 30 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ 𝑉 ) ∧ ( 𝐿 ‘ 𝐺 ) = ( ⊥ ‘ { 𝑥 } ) ) → 𝑈 ∈ LMod )
42 4 5 6 36 41 23 lsatspn0 ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ 𝑉 ) ∧ ( 𝐿 ‘ 𝐺 ) = ( ⊥ ‘ { 𝑥 } ) ) → ( ( 𝑁 ‘ { 𝑥 } ) ∈ ( LSAtoms ‘ 𝑈 ) ↔ 𝑥 ≠ 0 ) )
43 40 42 mpbid ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ 𝑉 ) ∧ ( 𝐿 ‘ 𝐺 ) = ( ⊥ ‘ { 𝑥 } ) ) → 𝑥 ≠ 0 )
44 43 25 jca ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ 𝑉 ) ∧ ( 𝐿 ‘ 𝐺 ) = ( ⊥ ‘ { 𝑥 } ) ) → ( 𝑥 ≠ 0 ∧ ( ⊥ ‘ ( 𝐿 ‘ 𝐺 ) ) = ( 𝑁 ‘ { 𝑥 } ) ) )
45 44 ex ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑉 ) → ( ( 𝐿 ‘ 𝐺 ) = ( ⊥ ‘ { 𝑥 } ) → ( 𝑥 ≠ 0 ∧ ( ⊥ ‘ ( 𝐿 ‘ 𝐺 ) ) = ( 𝑁 ‘ { 𝑥 } ) ) ) )
46 45 reximdva ⊢ ( 𝜑 → ( ∃ 𝑥 ∈ 𝑉 ( 𝐿 ‘ 𝐺 ) = ( ⊥ ‘ { 𝑥 } ) → ∃ 𝑥 ∈ 𝑉 ( 𝑥 ≠ 0 ∧ ( ⊥ ‘ ( 𝐿 ‘ 𝐺 ) ) = ( 𝑁 ‘ { 𝑥 } ) ) ) )
47 19 46 mpd ⊢ ( 𝜑 → ∃ 𝑥 ∈ 𝑉 ( 𝑥 ≠ 0 ∧ ( ⊥ ‘ ( 𝐿 ‘ 𝐺 ) ) = ( 𝑁 ‘ { 𝑥 } ) ) )
48 rexdifsn ⊢ ( ∃ 𝑥 ∈ ( 𝑉 ∖ { 0 } ) ( ⊥ ‘ ( 𝐿 ‘ 𝐺 ) ) = ( 𝑁 ‘ { 𝑥 } ) ↔ ∃ 𝑥 ∈ 𝑉 ( 𝑥 ≠ 0 ∧ ( ⊥ ‘ ( 𝐿 ‘ 𝐺 ) ) = ( 𝑁 ‘ { 𝑥 } ) ) )
49 47 48 sylibr ⊢ ( 𝜑 → ∃ 𝑥 ∈ ( 𝑉 ∖ { 0 } ) ( ⊥ ‘ ( 𝐿 ‘ 𝐺 ) ) = ( 𝑁 ‘ { 𝑥 } ) )