Metamath Proof Explorer

Theorem lcfl8

Description: Property of a functional with a closed kernel. (Contributed by NM, 17-Jan-2015)

Ref Expression
Hypotheses lcfl8.h ⊢ 𝐻 = ( LHyp ‘ 𝐾 )
lcfl8.o ⊢ ⊥ = ( ( ocH ‘ 𝐾 ) ‘ 𝑊 )
lcfl8.u ⊢ 𝑈 = ( ( DVecH ‘ 𝐾 ) ‘ 𝑊 )
lcfl8.v ⊢ 𝑉 = ( Base ‘ 𝑈 )
lcfl8.f ⊢ 𝐹 = ( LFnl ‘ 𝑈 )
lcfl8.l ⊢ 𝐿 = ( LKer ‘ 𝑈 )
lcfl8.c ⊢ 𝐶 = { 𝑓 ∈ 𝐹 ∣ ( ⊥ ‘ ( ⊥ ‘ ( 𝐿 ‘ 𝑓 ) ) ) = ( 𝐿 ‘ 𝑓 ) }
lcfl8.k ⊢ ( 𝜑 → ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) )
lcfl8.g ⊢ ( 𝜑 → 𝐺 ∈ 𝐹 )
Assertion lcfl8 ( 𝜑 → ( 𝐺 ∈ 𝐶 ↔ ∃ 𝑥 ∈ 𝑉 ( 𝐿 ‘ 𝐺 ) = ( ⊥ ‘ { 𝑥 } ) ) )

Proof

Step Hyp Ref Expression
1 lcfl8.h ⊢ 𝐻 = ( LHyp ‘ 𝐾 )
2 lcfl8.o ⊢ ⊥ = ( ( ocH ‘ 𝐾 ) ‘ 𝑊 )
3 lcfl8.u ⊢ 𝑈 = ( ( DVecH ‘ 𝐾 ) ‘ 𝑊 )
4 lcfl8.v ⊢ 𝑉 = ( Base ‘ 𝑈 )
5 lcfl8.f ⊢ 𝐹 = ( LFnl ‘ 𝑈 )
6 lcfl8.l ⊢ 𝐿 = ( LKer ‘ 𝑈 )
7 lcfl8.c ⊢ 𝐶 = { 𝑓 ∈ 𝐹 ∣ ( ⊥ ‘ ( ⊥ ‘ ( 𝐿 ‘ 𝑓 ) ) ) = ( 𝐿 ‘ 𝑓 ) }
8 lcfl8.k ⊢ ( 𝜑 → ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) )
9 lcfl8.g ⊢ ( 𝜑 → 𝐺 ∈ 𝐹 )
10 1 3 8 dvhlmod ⊢ ( 𝜑 → 𝑈 ∈ LMod )
11 10 adantr ⊢ ( ( 𝜑 ∧ 𝐺 ∈ 𝐶 ) → 𝑈 ∈ LMod )
12 eqid ⊢ ( LSpan ‘ 𝑈 ) = ( LSpan ‘ 𝑈 )
13 eqid ⊢ ( LSAtoms ‘ 𝑈 ) = ( LSAtoms ‘ 𝑈 )
14 4 12 13 islsati ⊢ ( ( 𝑈 ∈ LMod ∧ ( ⊥ ‘ ( 𝐿 ‘ 𝐺 ) ) ∈ ( LSAtoms ‘ 𝑈 ) ) → ∃ 𝑥 ∈ 𝑉 ( ⊥ ‘ ( 𝐿 ‘ 𝐺 ) ) = ( ( LSpan ‘ 𝑈 ) ‘ { 𝑥 } ) )
15 11 14 sylan ⊢ ( ( ( 𝜑 ∧ 𝐺 ∈ 𝐶 ) ∧ ( ⊥ ‘ ( 𝐿 ‘ 𝐺 ) ) ∈ ( LSAtoms ‘ 𝑈 ) ) → ∃ 𝑥 ∈ 𝑉 ( ⊥ ‘ ( 𝐿 ‘ 𝐺 ) ) = ( ( LSpan ‘ 𝑈 ) ‘ { 𝑥 } ) )
16 simpr ⊢ ( ( ( ( ( 𝜑 ∧ 𝐺 ∈ 𝐶 ) ∧ ( ⊥ ‘ ( 𝐿 ‘ 𝐺 ) ) ∈ ( LSAtoms ‘ 𝑈 ) ) ∧ 𝑥 ∈ 𝑉 ) ∧ ( ⊥ ‘ ( 𝐿 ‘ 𝐺 ) ) = ( ( LSpan ‘ 𝑈 ) ‘ { 𝑥 } ) ) → ( ⊥ ‘ ( 𝐿 ‘ 𝐺 ) ) = ( ( LSpan ‘ 𝑈 ) ‘ { 𝑥 } ) )
17 16 fveq2d ⊢ ( ( ( ( ( 𝜑 ∧ 𝐺 ∈ 𝐶 ) ∧ ( ⊥ ‘ ( 𝐿 ‘ 𝐺 ) ) ∈ ( LSAtoms ‘ 𝑈 ) ) ∧ 𝑥 ∈ 𝑉 ) ∧ ( ⊥ ‘ ( 𝐿 ‘ 𝐺 ) ) = ( ( LSpan ‘ 𝑈 ) ‘ { 𝑥 } ) ) → ( ⊥ ‘ ( ⊥ ‘ ( 𝐿 ‘ 𝐺 ) ) ) = ( ⊥ ‘ ( ( LSpan ‘ 𝑈 ) ‘ { 𝑥 } ) ) )
18 simp-4r ⊢ ( ( ( ( ( 𝜑 ∧ 𝐺 ∈ 𝐶 ) ∧ ( ⊥ ‘ ( 𝐿 ‘ 𝐺 ) ) ∈ ( LSAtoms ‘ 𝑈 ) ) ∧ 𝑥 ∈ 𝑉 ) ∧ ( ⊥ ‘ ( 𝐿 ‘ 𝐺 ) ) = ( ( LSpan ‘ 𝑈 ) ‘ { 𝑥 } ) ) → 𝐺 ∈ 𝐶 )
19 9 ad4antr ⊢ ( ( ( ( ( 𝜑 ∧ 𝐺 ∈ 𝐶 ) ∧ ( ⊥ ‘ ( 𝐿 ‘ 𝐺 ) ) ∈ ( LSAtoms ‘ 𝑈 ) ) ∧ 𝑥 ∈ 𝑉 ) ∧ ( ⊥ ‘ ( 𝐿 ‘ 𝐺 ) ) = ( ( LSpan ‘ 𝑈 ) ‘ { 𝑥 } ) ) → 𝐺 ∈ 𝐹 )
20 7 19 lcfl1 ⊢ ( ( ( ( ( 𝜑 ∧ 𝐺 ∈ 𝐶 ) ∧ ( ⊥ ‘ ( 𝐿 ‘ 𝐺 ) ) ∈ ( LSAtoms ‘ 𝑈 ) ) ∧ 𝑥 ∈ 𝑉 ) ∧ ( ⊥ ‘ ( 𝐿 ‘ 𝐺 ) ) = ( ( LSpan ‘ 𝑈 ) ‘ { 𝑥 } ) ) → ( 𝐺 ∈ 𝐶 ↔ ( ⊥ ‘ ( ⊥ ‘ ( 𝐿 ‘ 𝐺 ) ) ) = ( 𝐿 ‘ 𝐺 ) ) )
21 18 20 mpbid ⊢ ( ( ( ( ( 𝜑 ∧ 𝐺 ∈ 𝐶 ) ∧ ( ⊥ ‘ ( 𝐿 ‘ 𝐺 ) ) ∈ ( LSAtoms ‘ 𝑈 ) ) ∧ 𝑥 ∈ 𝑉 ) ∧ ( ⊥ ‘ ( 𝐿 ‘ 𝐺 ) ) = ( ( LSpan ‘ 𝑈 ) ‘ { 𝑥 } ) ) → ( ⊥ ‘ ( ⊥ ‘ ( 𝐿 ‘ 𝐺 ) ) ) = ( 𝐿 ‘ 𝐺 ) )
22 8 ad4antr ⊢ ( ( ( ( ( 𝜑 ∧ 𝐺 ∈ 𝐶 ) ∧ ( ⊥ ‘ ( 𝐿 ‘ 𝐺 ) ) ∈ ( LSAtoms ‘ 𝑈 ) ) ∧ 𝑥 ∈ 𝑉 ) ∧ ( ⊥ ‘ ( 𝐿 ‘ 𝐺 ) ) = ( ( LSpan ‘ 𝑈 ) ‘ { 𝑥 } ) ) → ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) )
23 simplr ⊢ ( ( ( ( ( 𝜑 ∧ 𝐺 ∈ 𝐶 ) ∧ ( ⊥ ‘ ( 𝐿 ‘ 𝐺 ) ) ∈ ( LSAtoms ‘ 𝑈 ) ) ∧ 𝑥 ∈ 𝑉 ) ∧ ( ⊥ ‘ ( 𝐿 ‘ 𝐺 ) ) = ( ( LSpan ‘ 𝑈 ) ‘ { 𝑥 } ) ) → 𝑥 ∈ 𝑉 )
24 23 snssd ⊢ ( ( ( ( ( 𝜑 ∧ 𝐺 ∈ 𝐶 ) ∧ ( ⊥ ‘ ( 𝐿 ‘ 𝐺 ) ) ∈ ( LSAtoms ‘ 𝑈 ) ) ∧ 𝑥 ∈ 𝑉 ) ∧ ( ⊥ ‘ ( 𝐿 ‘ 𝐺 ) ) = ( ( LSpan ‘ 𝑈 ) ‘ { 𝑥 } ) ) → { 𝑥 } ⊆ 𝑉 )
25 1 3 2 4 12 22 24 dochocsp ⊢ ( ( ( ( ( 𝜑 ∧ 𝐺 ∈ 𝐶 ) ∧ ( ⊥ ‘ ( 𝐿 ‘ 𝐺 ) ) ∈ ( LSAtoms ‘ 𝑈 ) ) ∧ 𝑥 ∈ 𝑉 ) ∧ ( ⊥ ‘ ( 𝐿 ‘ 𝐺 ) ) = ( ( LSpan ‘ 𝑈 ) ‘ { 𝑥 } ) ) → ( ⊥ ‘ ( ( LSpan ‘ 𝑈 ) ‘ { 𝑥 } ) ) = ( ⊥ ‘ { 𝑥 } ) )
26 17 21 25 3eqtr3d ⊢ ( ( ( ( ( 𝜑 ∧ 𝐺 ∈ 𝐶 ) ∧ ( ⊥ ‘ ( 𝐿 ‘ 𝐺 ) ) ∈ ( LSAtoms ‘ 𝑈 ) ) ∧ 𝑥 ∈ 𝑉 ) ∧ ( ⊥ ‘ ( 𝐿 ‘ 𝐺 ) ) = ( ( LSpan ‘ 𝑈 ) ‘ { 𝑥 } ) ) → ( 𝐿 ‘ 𝐺 ) = ( ⊥ ‘ { 𝑥 } ) )
27 26 ex ⊢ ( ( ( ( 𝜑 ∧ 𝐺 ∈ 𝐶 ) ∧ ( ⊥ ‘ ( 𝐿 ‘ 𝐺 ) ) ∈ ( LSAtoms ‘ 𝑈 ) ) ∧ 𝑥 ∈ 𝑉 ) → ( ( ⊥ ‘ ( 𝐿 ‘ 𝐺 ) ) = ( ( LSpan ‘ 𝑈 ) ‘ { 𝑥 } ) → ( 𝐿 ‘ 𝐺 ) = ( ⊥ ‘ { 𝑥 } ) ) )
28 27 reximdva ⊢ ( ( ( 𝜑 ∧ 𝐺 ∈ 𝐶 ) ∧ ( ⊥ ‘ ( 𝐿 ‘ 𝐺 ) ) ∈ ( LSAtoms ‘ 𝑈 ) ) → ( ∃ 𝑥 ∈ 𝑉 ( ⊥ ‘ ( 𝐿 ‘ 𝐺 ) ) = ( ( LSpan ‘ 𝑈 ) ‘ { 𝑥 } ) → ∃ 𝑥 ∈ 𝑉 ( 𝐿 ‘ 𝐺 ) = ( ⊥ ‘ { 𝑥 } ) ) )
29 15 28 mpd ⊢ ( ( ( 𝜑 ∧ 𝐺 ∈ 𝐶 ) ∧ ( ⊥ ‘ ( 𝐿 ‘ 𝐺 ) ) ∈ ( LSAtoms ‘ 𝑈 ) ) → ∃ 𝑥 ∈ 𝑉 ( 𝐿 ‘ 𝐺 ) = ( ⊥ ‘ { 𝑥 } ) )
30 11 adantr ⊢ ( ( ( 𝜑 ∧ 𝐺 ∈ 𝐶 ) ∧ ( 𝐿 ‘ 𝐺 ) = 𝑉 ) → 𝑈 ∈ LMod )
31 eqid ⊢ ( 0g ‘ 𝑈 ) = ( 0g ‘ 𝑈 )
32 4 31 lmod0vcl ⊢ ( 𝑈 ∈ LMod → ( 0g ‘ 𝑈 ) ∈ 𝑉 )
33 30 32 syl ⊢ ( ( ( 𝜑 ∧ 𝐺 ∈ 𝐶 ) ∧ ( 𝐿 ‘ 𝐺 ) = 𝑉 ) → ( 0g ‘ 𝑈 ) ∈ 𝑉 )
34 simpr ⊢ ( ( ( 𝜑 ∧ 𝐺 ∈ 𝐶 ) ∧ ( 𝐿 ‘ 𝐺 ) = 𝑉 ) → ( 𝐿 ‘ 𝐺 ) = 𝑉 )
35 8 adantr ⊢ ( ( 𝜑 ∧ 𝐺 ∈ 𝐶 ) → ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) )
36 35 adantr ⊢ ( ( ( 𝜑 ∧ 𝐺 ∈ 𝐶 ) ∧ ( 𝐿 ‘ 𝐺 ) = 𝑉 ) → ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) )
37 1 3 2 4 31 doch0 ⊢ ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) → ( ⊥ ‘ { ( 0g ‘ 𝑈 ) } ) = 𝑉 )
38 36 37 syl ⊢ ( ( ( 𝜑 ∧ 𝐺 ∈ 𝐶 ) ∧ ( 𝐿 ‘ 𝐺 ) = 𝑉 ) → ( ⊥ ‘ { ( 0g ‘ 𝑈 ) } ) = 𝑉 )
39 34 38 eqtr4d ⊢ ( ( ( 𝜑 ∧ 𝐺 ∈ 𝐶 ) ∧ ( 𝐿 ‘ 𝐺 ) = 𝑉 ) → ( 𝐿 ‘ 𝐺 ) = ( ⊥ ‘ { ( 0g ‘ 𝑈 ) } ) )
40 sneq ⊢ ( 𝑥 = ( 0g ‘ 𝑈 ) → { 𝑥 } = { ( 0g ‘ 𝑈 ) } )
41 40 fveq2d ⊢ ( 𝑥 = ( 0g ‘ 𝑈 ) → ( ⊥ ‘ { 𝑥 } ) = ( ⊥ ‘ { ( 0g ‘ 𝑈 ) } ) )
42 41 rspceeqv ⊢ ( ( ( 0g ‘ 𝑈 ) ∈ 𝑉 ∧ ( 𝐿 ‘ 𝐺 ) = ( ⊥ ‘ { ( 0g ‘ 𝑈 ) } ) ) → ∃ 𝑥 ∈ 𝑉 ( 𝐿 ‘ 𝐺 ) = ( ⊥ ‘ { 𝑥 } ) )
43 33 39 42 syl2anc ⊢ ( ( ( 𝜑 ∧ 𝐺 ∈ 𝐶 ) ∧ ( 𝐿 ‘ 𝐺 ) = 𝑉 ) → ∃ 𝑥 ∈ 𝑉 ( 𝐿 ‘ 𝐺 ) = ( ⊥ ‘ { 𝑥 } ) )
44 1 2 3 4 13 5 6 7 8 9 lcfl3 ⊢ ( 𝜑 → ( 𝐺 ∈ 𝐶 ↔ ( ( ⊥ ‘ ( 𝐿 ‘ 𝐺 ) ) ∈ ( LSAtoms ‘ 𝑈 ) ∨ ( 𝐿 ‘ 𝐺 ) = 𝑉 ) ) )
45 44 biimpa ⊢ ( ( 𝜑 ∧ 𝐺 ∈ 𝐶 ) → ( ( ⊥ ‘ ( 𝐿 ‘ 𝐺 ) ) ∈ ( LSAtoms ‘ 𝑈 ) ∨ ( 𝐿 ‘ 𝐺 ) = 𝑉 ) )
46 29 43 45 mpjaodan ⊢ ( ( 𝜑 ∧ 𝐺 ∈ 𝐶 ) → ∃ 𝑥 ∈ 𝑉 ( 𝐿 ‘ 𝐺 ) = ( ⊥ ‘ { 𝑥 } ) )
47 46 ex ⊢ ( 𝜑 → ( 𝐺 ∈ 𝐶 → ∃ 𝑥 ∈ 𝑉 ( 𝐿 ‘ 𝐺 ) = ( ⊥ ‘ { 𝑥 } ) ) )
48 8 3ad2ant1 ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑉 ∧ ( 𝐿 ‘ 𝐺 ) = ( ⊥ ‘ { 𝑥 } ) ) → ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) )
49 simp2 ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑉 ∧ ( 𝐿 ‘ 𝐺 ) = ( ⊥ ‘ { 𝑥 } ) ) → 𝑥 ∈ 𝑉 )
50 49 snssd ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑉 ∧ ( 𝐿 ‘ 𝐺 ) = ( ⊥ ‘ { 𝑥 } ) ) → { 𝑥 } ⊆ 𝑉 )
51 eqid ⊢ ( ( DIsoH ‘ 𝐾 ) ‘ 𝑊 ) = ( ( DIsoH ‘ 𝐾 ) ‘ 𝑊 )
52 1 51 3 4 2 dochcl ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ { 𝑥 } ⊆ 𝑉 ) → ( ⊥ ‘ { 𝑥 } ) ∈ ran ( ( DIsoH ‘ 𝐾 ) ‘ 𝑊 ) )
53 48 50 52 syl2anc ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑉 ∧ ( 𝐿 ‘ 𝐺 ) = ( ⊥ ‘ { 𝑥 } ) ) → ( ⊥ ‘ { 𝑥 } ) ∈ ran ( ( DIsoH ‘ 𝐾 ) ‘ 𝑊 ) )
54 1 51 2 dochoc ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( ⊥ ‘ { 𝑥 } ) ∈ ran ( ( DIsoH ‘ 𝐾 ) ‘ 𝑊 ) ) → ( ⊥ ‘ ( ⊥ ‘ ( ⊥ ‘ { 𝑥 } ) ) ) = ( ⊥ ‘ { 𝑥 } ) )
55 48 53 54 syl2anc ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑉 ∧ ( 𝐿 ‘ 𝐺 ) = ( ⊥ ‘ { 𝑥 } ) ) → ( ⊥ ‘ ( ⊥ ‘ ( ⊥ ‘ { 𝑥 } ) ) ) = ( ⊥ ‘ { 𝑥 } ) )
56 simp3 ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑉 ∧ ( 𝐿 ‘ 𝐺 ) = ( ⊥ ‘ { 𝑥 } ) ) → ( 𝐿 ‘ 𝐺 ) = ( ⊥ ‘ { 𝑥 } ) )
57 56 fveq2d ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑉 ∧ ( 𝐿 ‘ 𝐺 ) = ( ⊥ ‘ { 𝑥 } ) ) → ( ⊥ ‘ ( 𝐿 ‘ 𝐺 ) ) = ( ⊥ ‘ ( ⊥ ‘ { 𝑥 } ) ) )
58 57 fveq2d ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑉 ∧ ( 𝐿 ‘ 𝐺 ) = ( ⊥ ‘ { 𝑥 } ) ) → ( ⊥ ‘ ( ⊥ ‘ ( 𝐿 ‘ 𝐺 ) ) ) = ( ⊥ ‘ ( ⊥ ‘ ( ⊥ ‘ { 𝑥 } ) ) ) )
59 55 58 56 3eqtr4d ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑉 ∧ ( 𝐿 ‘ 𝐺 ) = ( ⊥ ‘ { 𝑥 } ) ) → ( ⊥ ‘ ( ⊥ ‘ ( 𝐿 ‘ 𝐺 ) ) ) = ( 𝐿 ‘ 𝐺 ) )
60 59 rexlimdv3a ⊢ ( 𝜑 → ( ∃ 𝑥 ∈ 𝑉 ( 𝐿 ‘ 𝐺 ) = ( ⊥ ‘ { 𝑥 } ) → ( ⊥ ‘ ( ⊥ ‘ ( 𝐿 ‘ 𝐺 ) ) ) = ( 𝐿 ‘ 𝐺 ) ) )
61 7 9 lcfl1 ⊢ ( 𝜑 → ( 𝐺 ∈ 𝐶 ↔ ( ⊥ ‘ ( ⊥ ‘ ( 𝐿 ‘ 𝐺 ) ) ) = ( 𝐿 ‘ 𝐺 ) ) )
62 60 61 sylibrd ⊢ ( 𝜑 → ( ∃ 𝑥 ∈ 𝑉 ( 𝐿 ‘ 𝐺 ) = ( ⊥ ‘ { 𝑥 } ) → 𝐺 ∈ 𝐶 ) )
63 47 62 impbid ⊢ ( 𝜑 → ( 𝐺 ∈ 𝐶 ↔ ∃ 𝑥 ∈ 𝑉 ( 𝐿 ‘ 𝐺 ) = ( ⊥ ‘ { 𝑥 } ) ) )