Metamath Proof Explorer

Theorem lcfl6

Description: Property of a functional with a closed kernel. Note that ( LG ) = V means the functional is zero by lkr0f . (Contributed by NM, 3-Jan-2015)

Ref Expression
Hypotheses lcfl6.h ⊢ H = LHyp ⁡ K
lcfl6.o ⊢ ⊥ ˙ = ocH ⁡ K ⁡ W
lcfl6.u ⊢ U = DVecH ⁡ K ⁡ W
lcfl6.v ⊢ V = Base U
lcfl6.a ⊢ + ˙ = + U
lcfl6.t ⊢ · ˙ = ⋅ U
lcfl6.s ⊢ S = Scalar ⁡ U
lcfl6.r ⊢ R = Base S
lcfl6.z ⊢ 0 ˙ = 0 U
lcfl6.f ⊢ F = LFnl ⁡ U
lcfl6.l ⊢ L = LKer ⁡ U
lcfl6.c ⊢ C = f ∈ F | ⊥ ˙ ⁡ ⊥ ˙ ⁡ L ⁡ f = L ⁡ f
lcfl6.k ⊢ φ → K ∈ HL ∧ W ∈ H
lcfl6.g ⊢ φ → G ∈ F
Assertion lcfl6 ⊢ φ → G ∈ C ↔ L ⁡ G = V ∨ ∃ x ∈ V ∖ 0 ˙ G = v ∈ V ⟼ ι k ∈ R | ∃ w ∈ ⊥ ˙ ⁡ x v = w + ˙ k · ˙ x

Proof

Step Hyp Ref Expression
1 lcfl6.h ⊢ H = LHyp ⁡ K
2 lcfl6.o ⊢ ⊥ ˙ = ocH ⁡ K ⁡ W
3 lcfl6.u ⊢ U = DVecH ⁡ K ⁡ W
4 lcfl6.v ⊢ V = Base U
5 lcfl6.a ⊢ + ˙ = + U
6 lcfl6.t ⊢ · ˙ = ⋅ U
7 lcfl6.s ⊢ S = Scalar ⁡ U
8 lcfl6.r ⊢ R = Base S
9 lcfl6.z ⊢ 0 ˙ = 0 U
10 lcfl6.f ⊢ F = LFnl ⁡ U
11 lcfl6.l ⊢ L = LKer ⁡ U
12 lcfl6.c ⊢ C = f ∈ F | ⊥ ˙ ⁡ ⊥ ˙ ⁡ L ⁡ f = L ⁡ f
13 lcfl6.k ⊢ φ → K ∈ HL ∧ W ∈ H
14 lcfl6.g ⊢ φ → G ∈ F
15 df-ne ⊢ L ⁡ G ≠ V ↔ ¬ L ⁡ G = V
16 eqid ⊢ 1 S = 1 S
17 13 ad2antrr ⊢ φ ∧ G ∈ C ∧ L ⁡ G ≠ V → K ∈ HL ∧ W ∈ H
18 14 ad2antrr ⊢ φ ∧ G ∈ C ∧ L ⁡ G ≠ V → G ∈ F
19 1 2 3 4 10 11 12 13 14 lcfl2 ⊢ φ → G ∈ C ↔ ⊥ ˙ ⁡ ⊥ ˙ ⁡ L ⁡ G ≠ V ∨ L ⁡ G = V
20 19 biimpa ⊢ φ ∧ G ∈ C → ⊥ ˙ ⁡ ⊥ ˙ ⁡ L ⁡ G ≠ V ∨ L ⁡ G = V
21 20 orcomd ⊢ φ ∧ G ∈ C → L ⁡ G = V ∨ ⊥ ˙ ⁡ ⊥ ˙ ⁡ L ⁡ G ≠ V
22 21 ord ⊢ φ ∧ G ∈ C → ¬ L ⁡ G = V → ⊥ ˙ ⁡ ⊥ ˙ ⁡ L ⁡ G ≠ V
23 15 22 syl5bi ⊢ φ ∧ G ∈ C → L ⁡ G ≠ V → ⊥ ˙ ⁡ ⊥ ˙ ⁡ L ⁡ G ≠ V
24 23 imp ⊢ φ ∧ G ∈ C ∧ L ⁡ G ≠ V → ⊥ ˙ ⁡ ⊥ ˙ ⁡ L ⁡ G ≠ V
25 1 2 3 4 7 9 16 10 11 17 18 24 dochkr1 ⊢ φ ∧ G ∈ C ∧ L ⁡ G ≠ V → ∃ x ∈ ⊥ ˙ ⁡ L ⁡ G ∖ 0 ˙ G ⁡ x = 1 S
26 1 3 13 dvhlmod ⊢ φ → U ∈ LMod
27 4 10 11 26 14 lkrssv ⊢ φ → L ⁡ G ⊆ V
28 1 3 4 2 dochssv ⊢ K ∈ HL ∧ W ∈ H ∧ L ⁡ G ⊆ V → ⊥ ˙ ⁡ L ⁡ G ⊆ V
29 13 27 28 syl2anc ⊢ φ → ⊥ ˙ ⁡ L ⁡ G ⊆ V
30 29 ssdifd ⊢ φ → ⊥ ˙ ⁡ L ⁡ G ∖ 0 ˙ ⊆ V ∖ 0 ˙
31 30 ad3antrrr ⊢ φ ∧ G ∈ C ∧ L ⁡ G ≠ V ∧ x ∈ ⊥ ˙ ⁡ L ⁡ G ∖ 0 ˙ ∧ G ⁡ x = 1 S → ⊥ ˙ ⁡ L ⁡ G ∖ 0 ˙ ⊆ V ∖ 0 ˙
32 simprl ⊢ φ ∧ G ∈ C ∧ L ⁡ G ≠ V ∧ x ∈ ⊥ ˙ ⁡ L ⁡ G ∖ 0 ˙ ∧ G ⁡ x = 1 S → x ∈ ⊥ ˙ ⁡ L ⁡ G ∖ 0 ˙
33 31 32 sseldd ⊢ φ ∧ G ∈ C ∧ L ⁡ G ≠ V ∧ x ∈ ⊥ ˙ ⁡ L ⁡ G ∖ 0 ˙ ∧ G ⁡ x = 1 S → x ∈ V ∖ 0 ˙
34 13 ad3antrrr ⊢ φ ∧ G ∈ C ∧ L ⁡ G ≠ V ∧ x ∈ ⊥ ˙ ⁡ L ⁡ G ∖ 0 ˙ ∧ G ⁡ x = 1 S → K ∈ HL ∧ W ∈ H
35 14 ad3antrrr ⊢ φ ∧ G ∈ C ∧ L ⁡ G ≠ V ∧ x ∈ ⊥ ˙ ⁡ L ⁡ G ∖ 0 ˙ ∧ G ⁡ x = 1 S → G ∈ F
36 simprr ⊢ φ ∧ G ∈ C ∧ L ⁡ G ≠ V ∧ x ∈ ⊥ ˙ ⁡ L ⁡ G ∖ 0 ˙ ∧ G ⁡ x = 1 S → G ⁡ x = 1 S
37 1 2 3 4 5 6 7 16 8 9 10 11 34 35 32 36 lcfl6lem ⊢ φ ∧ G ∈ C ∧ L ⁡ G ≠ V ∧ x ∈ ⊥ ˙ ⁡ L ⁡ G ∖ 0 ˙ ∧ G ⁡ x = 1 S → G = v ∈ V ⟼ ι k ∈ R | ∃ w ∈ ⊥ ˙ ⁡ x v = w + ˙ k · ˙ x
38 25 33 37 reximssdv ⊢ φ ∧ G ∈ C ∧ L ⁡ G ≠ V → ∃ x ∈ V ∖ 0 ˙ G = v ∈ V ⟼ ι k ∈ R | ∃ w ∈ ⊥ ˙ ⁡ x v = w + ˙ k · ˙ x
39 38 ex ⊢ φ ∧ G ∈ C → L ⁡ G ≠ V → ∃ x ∈ V ∖ 0 ˙ G = v ∈ V ⟼ ι k ∈ R | ∃ w ∈ ⊥ ˙ ⁡ x v = w + ˙ k · ˙ x
40 15 39 syl5bir ⊢ φ ∧ G ∈ C → ¬ L ⁡ G = V → ∃ x ∈ V ∖ 0 ˙ G = v ∈ V ⟼ ι k ∈ R | ∃ w ∈ ⊥ ˙ ⁡ x v = w + ˙ k · ˙ x
41 40 orrd ⊢ φ ∧ G ∈ C → L ⁡ G = V ∨ ∃ x ∈ V ∖ 0 ˙ G = v ∈ V ⟼ ι k ∈ R | ∃ w ∈ ⊥ ˙ ⁡ x v = w + ˙ k · ˙ x
42 41 ex ⊢ φ → G ∈ C → L ⁡ G = V ∨ ∃ x ∈ V ∖ 0 ˙ G = v ∈ V ⟼ ι k ∈ R | ∃ w ∈ ⊥ ˙ ⁡ x v = w + ˙ k · ˙ x
43 olc ⊢ L ⁡ G = V → ⊥ ˙ ⁡ ⊥ ˙ ⁡ L ⁡ G ≠ V ∨ L ⁡ G = V
44 43 19 syl5ibr ⊢ φ → L ⁡ G = V → G ∈ C
45 13 adantr ⊢ φ ∧ x ∈ V ∖ 0 ˙ → K ∈ HL ∧ W ∈ H
46 eldifi ⊢ x ∈ V ∖ 0 ˙ → x ∈ V
47 46 adantl ⊢ φ ∧ x ∈ V ∖ 0 ˙ → x ∈ V
48 47 snssd ⊢ φ ∧ x ∈ V ∖ 0 ˙ → x ⊆ V
49 eqid ⊢ DIsoH ⁡ K ⁡ W = DIsoH ⁡ K ⁡ W
50 1 49 3 4 2 dochcl ⊢ K ∈ HL ∧ W ∈ H ∧ x ⊆ V → ⊥ ˙ ⁡ x ∈ ran ⁡ DIsoH ⁡ K ⁡ W
51 45 48 50 syl2anc ⊢ φ ∧ x ∈ V ∖ 0 ˙ → ⊥ ˙ ⁡ x ∈ ran ⁡ DIsoH ⁡ K ⁡ W
52 1 49 2 dochoc ⊢ K ∈ HL ∧ W ∈ H ∧ ⊥ ˙ ⁡ x ∈ ran ⁡ DIsoH ⁡ K ⁡ W → ⊥ ˙ ⁡ ⊥ ˙ ⁡ ⊥ ˙ ⁡ x = ⊥ ˙ ⁡ x
53 45 51 52 syl2anc ⊢ φ ∧ x ∈ V ∖ 0 ˙ → ⊥ ˙ ⁡ ⊥ ˙ ⁡ ⊥ ˙ ⁡ x = ⊥ ˙ ⁡ x
54 53 3adant3 ⊢ φ ∧ x ∈ V ∖ 0 ˙ ∧ G = v ∈ V ⟼ ι k ∈ R | ∃ w ∈ ⊥ ˙ ⁡ x v = w + ˙ k · ˙ x → ⊥ ˙ ⁡ ⊥ ˙ ⁡ ⊥ ˙ ⁡ x = ⊥ ˙ ⁡ x
55 simp3 ⊢ φ ∧ x ∈ V ∖ 0 ˙ ∧ G = v ∈ V ⟼ ι k ∈ R | ∃ w ∈ ⊥ ˙ ⁡ x v = w + ˙ k · ˙ x → G = v ∈ V ⟼ ι k ∈ R | ∃ w ∈ ⊥ ˙ ⁡ x v = w + ˙ k · ˙ x
56 55 fveq2d ⊢ φ ∧ x ∈ V ∖ 0 ˙ ∧ G = v ∈ V ⟼ ι k ∈ R | ∃ w ∈ ⊥ ˙ ⁡ x v = w + ˙ k · ˙ x → L ⁡ G = L ⁡ v ∈ V ⟼ ι k ∈ R | ∃ w ∈ ⊥ ˙ ⁡ x v = w + ˙ k · ˙ x
57 eqid ⊢ v ∈ V ⟼ ι k ∈ R | ∃ w ∈ ⊥ ˙ ⁡ x v = w + ˙ k · ˙ x = v ∈ V ⟼ ι k ∈ R | ∃ w ∈ ⊥ ˙ ⁡ x v = w + ˙ k · ˙ x
58 simpr ⊢ φ ∧ x ∈ V ∖ 0 ˙ → x ∈ V ∖ 0 ˙
59 1 2 3 4 9 5 6 11 7 8 57 45 58 dochsnkr2 ⊢ φ ∧ x ∈ V ∖ 0 ˙ → L ⁡ v ∈ V ⟼ ι k ∈ R | ∃ w ∈ ⊥ ˙ ⁡ x v = w + ˙ k · ˙ x = ⊥ ˙ ⁡ x
60 59 3adant3 ⊢ φ ∧ x ∈ V ∖ 0 ˙ ∧ G = v ∈ V ⟼ ι k ∈ R | ∃ w ∈ ⊥ ˙ ⁡ x v = w + ˙ k · ˙ x → L ⁡ v ∈ V ⟼ ι k ∈ R | ∃ w ∈ ⊥ ˙ ⁡ x v = w + ˙ k · ˙ x = ⊥ ˙ ⁡ x
61 56 60 eqtrd ⊢ φ ∧ x ∈ V ∖ 0 ˙ ∧ G = v ∈ V ⟼ ι k ∈ R | ∃ w ∈ ⊥ ˙ ⁡ x v = w + ˙ k · ˙ x → L ⁡ G = ⊥ ˙ ⁡ x
62 61 fveq2d ⊢ φ ∧ x ∈ V ∖ 0 ˙ ∧ G = v ∈ V ⟼ ι k ∈ R | ∃ w ∈ ⊥ ˙ ⁡ x v = w + ˙ k · ˙ x → ⊥ ˙ ⁡ L ⁡ G = ⊥ ˙ ⁡ ⊥ ˙ ⁡ x
63 62 fveq2d ⊢ φ ∧ x ∈ V ∖ 0 ˙ ∧ G = v ∈ V ⟼ ι k ∈ R | ∃ w ∈ ⊥ ˙ ⁡ x v = w + ˙ k · ˙ x → ⊥ ˙ ⁡ ⊥ ˙ ⁡ L ⁡ G = ⊥ ˙ ⁡ ⊥ ˙ ⁡ ⊥ ˙ ⁡ x
64 54 63 61 3eqtr4d ⊢ φ ∧ x ∈ V ∖ 0 ˙ ∧ G = v ∈ V ⟼ ι k ∈ R | ∃ w ∈ ⊥ ˙ ⁡ x v = w + ˙ k · ˙ x → ⊥ ˙ ⁡ ⊥ ˙ ⁡ L ⁡ G = L ⁡ G
65 14 3ad2ant1 ⊢ φ ∧ x ∈ V ∖ 0 ˙ ∧ G = v ∈ V ⟼ ι k ∈ R | ∃ w ∈ ⊥ ˙ ⁡ x v = w + ˙ k · ˙ x → G ∈ F
66 12 65 lcfl1 ⊢ φ ∧ x ∈ V ∖ 0 ˙ ∧ G = v ∈ V ⟼ ι k ∈ R | ∃ w ∈ ⊥ ˙ ⁡ x v = w + ˙ k · ˙ x → G ∈ C ↔ ⊥ ˙ ⁡ ⊥ ˙ ⁡ L ⁡ G = L ⁡ G
67 64 66 mpbird ⊢ φ ∧ x ∈ V ∖ 0 ˙ ∧ G = v ∈ V ⟼ ι k ∈ R | ∃ w ∈ ⊥ ˙ ⁡ x v = w + ˙ k · ˙ x → G ∈ C
68 67 rexlimdv3a ⊢ φ → ∃ x ∈ V ∖ 0 ˙ G = v ∈ V ⟼ ι k ∈ R | ∃ w ∈ ⊥ ˙ ⁡ x v = w + ˙ k · ˙ x → G ∈ C
69 44 68 jaod ⊢ φ → L ⁡ G = V ∨ ∃ x ∈ V ∖ 0 ˙ G = v ∈ V ⟼ ι k ∈ R | ∃ w ∈ ⊥ ˙ ⁡ x v = w + ˙ k · ˙ x → G ∈ C
70 42 69 impbid ⊢ φ → G ∈ C ↔ L ⁡ G = V ∨ ∃ x ∈ V ∖ 0 ˙ G = v ∈ V ⟼ ι k ∈ R | ∃ w ∈ ⊥ ˙ ⁡ x v = w + ˙ k · ˙ x