Metamath Proof Explorer

Theorem dochkr1OLDN

Description: A nonzero functional has a value of 1 at some argument belonging to the orthocomplement of its kernel (when its kernel is a closed hyperplane). Tighter version of lfl1 . (Contributed by NM, 2-Jan-2015) (New usage is discouraged.)

Ref Expression
Hypotheses dochkr1OLD.h ⊢ 𝐻 = ( LHyp ‘ 𝐾 )
dochkr1OLD.o ⊢ ⊥ = ( ( ocH ‘ 𝐾 ) ‘ 𝑊 )
dochkr1OLD.u ⊢ 𝑈 = ( ( DVecH ‘ 𝐾 ) ‘ 𝑊 )
dochkr1OLD.v ⊢ 𝑉 = ( Base ‘ 𝑈 )
dochkr1OLD.r ⊢ 𝑅 = ( Scalar ‘ 𝑈 )
dochkr1OLD.z ⊢ 0 = ( 0g ‘ 𝑅 )
dochkr1OLD.i ⊢ 1 = ( 1r ‘ 𝑅 )
dochkr1OLD.f ⊢ 𝐹 = ( LFnl ‘ 𝑈 )
dochkr1OLD.l ⊢ 𝐿 = ( LKer ‘ 𝑈 )
dochkr1OLD.k ⊢ ( 𝜑 → ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) )
dochkr1OLD.g ⊢ ( 𝜑 → 𝐺 ∈ 𝐹 )
dochkr1OLD.n ⊢ ( 𝜑 → ( ⊥ ‘ ( ⊥ ‘ ( 𝐿 ‘ 𝐺 ) ) ) ≠ 𝑉 )
Assertion dochkr1OLDN ( 𝜑 → ∃ 𝑥 ∈ ( ⊥ ‘ ( 𝐿 ‘ 𝐺 ) ) ( 𝐺 ‘ 𝑥 ) = 1 )

Proof

Step Hyp Ref Expression
1 dochkr1OLD.h ⊢ 𝐻 = ( LHyp ‘ 𝐾 )
2 dochkr1OLD.o ⊢ ⊥ = ( ( ocH ‘ 𝐾 ) ‘ 𝑊 )
3 dochkr1OLD.u ⊢ 𝑈 = ( ( DVecH ‘ 𝐾 ) ‘ 𝑊 )
4 dochkr1OLD.v ⊢ 𝑉 = ( Base ‘ 𝑈 )
5 dochkr1OLD.r ⊢ 𝑅 = ( Scalar ‘ 𝑈 )
6 dochkr1OLD.z ⊢ 0 = ( 0g ‘ 𝑅 )
7 dochkr1OLD.i ⊢ 1 = ( 1r ‘ 𝑅 )
8 dochkr1OLD.f ⊢ 𝐹 = ( LFnl ‘ 𝑈 )
9 dochkr1OLD.l ⊢ 𝐿 = ( LKer ‘ 𝑈 )
10 dochkr1OLD.k ⊢ ( 𝜑 → ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) )
11 dochkr1OLD.g ⊢ ( 𝜑 → 𝐺 ∈ 𝐹 )
12 dochkr1OLD.n ⊢ ( 𝜑 → ( ⊥ ‘ ( ⊥ ‘ ( 𝐿 ‘ 𝐺 ) ) ) ≠ 𝑉 )
13 eqid ⊢ ( 0g ‘ 𝑈 ) = ( 0g ‘ 𝑈 )
14 eqid ⊢ ( LSAtoms ‘ 𝑈 ) = ( LSAtoms ‘ 𝑈 )
15 1 3 10 dvhlmod ⊢ ( 𝜑 → 𝑈 ∈ LMod )
16 1 2 3 4 14 8 9 10 11 dochkrsat2 ⊢ ( 𝜑 → ( ( ⊥ ‘ ( ⊥ ‘ ( 𝐿 ‘ 𝐺 ) ) ) ≠ 𝑉 ↔ ( ⊥ ‘ ( 𝐿 ‘ 𝐺 ) ) ∈ ( LSAtoms ‘ 𝑈 ) ) )
17 12 16 mpbid ⊢ ( 𝜑 → ( ⊥ ‘ ( 𝐿 ‘ 𝐺 ) ) ∈ ( LSAtoms ‘ 𝑈 ) )
18 13 14 15 17 lsateln0 ⊢ ( 𝜑 → ∃ 𝑧 ∈ ( ⊥ ‘ ( 𝐿 ‘ 𝐺 ) ) 𝑧 ≠ ( 0g ‘ 𝑈 ) )
19 10 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑧 ∈ ( ⊥ ‘ ( 𝐿 ‘ 𝐺 ) ) ) ∧ 𝑧 ≠ ( 0g ‘ 𝑈 ) ) → ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) )
20 11 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑧 ∈ ( ⊥ ‘ ( 𝐿 ‘ 𝐺 ) ) ) ∧ 𝑧 ≠ ( 0g ‘ 𝑈 ) ) → 𝐺 ∈ 𝐹 )
21 eldifsn ⊢ ( 𝑧 ∈ ( ( ⊥ ‘ ( 𝐿 ‘ 𝐺 ) ) ∖ { ( 0g ‘ 𝑈 ) } ) ↔ ( 𝑧 ∈ ( ⊥ ‘ ( 𝐿 ‘ 𝐺 ) ) ∧ 𝑧 ≠ ( 0g ‘ 𝑈 ) ) )
22 21 biimpri ⊢ ( ( 𝑧 ∈ ( ⊥ ‘ ( 𝐿 ‘ 𝐺 ) ) ∧ 𝑧 ≠ ( 0g ‘ 𝑈 ) ) → 𝑧 ∈ ( ( ⊥ ‘ ( 𝐿 ‘ 𝐺 ) ) ∖ { ( 0g ‘ 𝑈 ) } ) )
23 22 adantll ⊢ ( ( ( 𝜑 ∧ 𝑧 ∈ ( ⊥ ‘ ( 𝐿 ‘ 𝐺 ) ) ) ∧ 𝑧 ≠ ( 0g ‘ 𝑈 ) ) → 𝑧 ∈ ( ( ⊥ ‘ ( 𝐿 ‘ 𝐺 ) ) ∖ { ( 0g ‘ 𝑈 ) } ) )
24 1 2 3 4 5 6 13 8 9 19 20 23 dochfln0 ⊢ ( ( ( 𝜑 ∧ 𝑧 ∈ ( ⊥ ‘ ( 𝐿 ‘ 𝐺 ) ) ) ∧ 𝑧 ≠ ( 0g ‘ 𝑈 ) ) → ( 𝐺 ‘ 𝑧 ) ≠ 0 )
25 24 ex ⊢ ( ( 𝜑 ∧ 𝑧 ∈ ( ⊥ ‘ ( 𝐿 ‘ 𝐺 ) ) ) → ( 𝑧 ≠ ( 0g ‘ 𝑈 ) → ( 𝐺 ‘ 𝑧 ) ≠ 0 ) )
26 25 reximdva ⊢ ( 𝜑 → ( ∃ 𝑧 ∈ ( ⊥ ‘ ( 𝐿 ‘ 𝐺 ) ) 𝑧 ≠ ( 0g ‘ 𝑈 ) → ∃ 𝑧 ∈ ( ⊥ ‘ ( 𝐿 ‘ 𝐺 ) ) ( 𝐺 ‘ 𝑧 ) ≠ 0 ) )
27 18 26 mpd ⊢ ( 𝜑 → ∃ 𝑧 ∈ ( ⊥ ‘ ( 𝐿 ‘ 𝐺 ) ) ( 𝐺 ‘ 𝑧 ) ≠ 0 )
28 4 8 9 15 11 lkrssv ⊢ ( 𝜑 → ( 𝐿 ‘ 𝐺 ) ⊆ 𝑉 )
29 eqid ⊢ ( LSubSp ‘ 𝑈 ) = ( LSubSp ‘ 𝑈 )
30 1 3 4 29 2 dochlss ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝐿 ‘ 𝐺 ) ⊆ 𝑉 ) → ( ⊥ ‘ ( 𝐿 ‘ 𝐺 ) ) ∈ ( LSubSp ‘ 𝑈 ) )
31 10 28 30 syl2anc ⊢ ( 𝜑 → ( ⊥ ‘ ( 𝐿 ‘ 𝐺 ) ) ∈ ( LSubSp ‘ 𝑈 ) )
32 15 31 jca ⊢ ( 𝜑 → ( 𝑈 ∈ LMod ∧ ( ⊥ ‘ ( 𝐿 ‘ 𝐺 ) ) ∈ ( LSubSp ‘ 𝑈 ) ) )
33 32 3ad2ant1 ⊢ ( ( 𝜑 ∧ 𝑧 ∈ ( ⊥ ‘ ( 𝐿 ‘ 𝐺 ) ) ∧ ( 𝐺 ‘ 𝑧 ) ≠ 0 ) → ( 𝑈 ∈ LMod ∧ ( ⊥ ‘ ( 𝐿 ‘ 𝐺 ) ) ∈ ( LSubSp ‘ 𝑈 ) ) )
34 1 3 10 dvhlvec ⊢ ( 𝜑 → 𝑈 ∈ LVec )
35 34 3ad2ant1 ⊢ ( ( 𝜑 ∧ 𝑧 ∈ ( ⊥ ‘ ( 𝐿 ‘ 𝐺 ) ) ∧ ( 𝐺 ‘ 𝑧 ) ≠ 0 ) → 𝑈 ∈ LVec )
36 5 lvecdrng ⊢ ( 𝑈 ∈ LVec → 𝑅 ∈ DivRing )
37 35 36 syl ⊢ ( ( 𝜑 ∧ 𝑧 ∈ ( ⊥ ‘ ( 𝐿 ‘ 𝐺 ) ) ∧ ( 𝐺 ‘ 𝑧 ) ≠ 0 ) → 𝑅 ∈ DivRing )
38 15 3ad2ant1 ⊢ ( ( 𝜑 ∧ 𝑧 ∈ ( ⊥ ‘ ( 𝐿 ‘ 𝐺 ) ) ∧ ( 𝐺 ‘ 𝑧 ) ≠ 0 ) → 𝑈 ∈ LMod )
39 11 3ad2ant1 ⊢ ( ( 𝜑 ∧ 𝑧 ∈ ( ⊥ ‘ ( 𝐿 ‘ 𝐺 ) ) ∧ ( 𝐺 ‘ 𝑧 ) ≠ 0 ) → 𝐺 ∈ 𝐹 )
40 1 3 4 2 dochssv ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝐿 ‘ 𝐺 ) ⊆ 𝑉 ) → ( ⊥ ‘ ( 𝐿 ‘ 𝐺 ) ) ⊆ 𝑉 )
41 10 28 40 syl2anc ⊢ ( 𝜑 → ( ⊥ ‘ ( 𝐿 ‘ 𝐺 ) ) ⊆ 𝑉 )
42 41 sselda ⊢ ( ( 𝜑 ∧ 𝑧 ∈ ( ⊥ ‘ ( 𝐿 ‘ 𝐺 ) ) ) → 𝑧 ∈ 𝑉 )
43 42 3adant3 ⊢ ( ( 𝜑 ∧ 𝑧 ∈ ( ⊥ ‘ ( 𝐿 ‘ 𝐺 ) ) ∧ ( 𝐺 ‘ 𝑧 ) ≠ 0 ) → 𝑧 ∈ 𝑉 )
44 eqid ⊢ ( Base ‘ 𝑅 ) = ( Base ‘ 𝑅 )
45 5 44 4 8 lflcl ⊢ ( ( 𝑈 ∈ LMod ∧ 𝐺 ∈ 𝐹 ∧ 𝑧 ∈ 𝑉 ) → ( 𝐺 ‘ 𝑧 ) ∈ ( Base ‘ 𝑅 ) )
46 38 39 43 45 syl3anc ⊢ ( ( 𝜑 ∧ 𝑧 ∈ ( ⊥ ‘ ( 𝐿 ‘ 𝐺 ) ) ∧ ( 𝐺 ‘ 𝑧 ) ≠ 0 ) → ( 𝐺 ‘ 𝑧 ) ∈ ( Base ‘ 𝑅 ) )
47 simp3 ⊢ ( ( 𝜑 ∧ 𝑧 ∈ ( ⊥ ‘ ( 𝐿 ‘ 𝐺 ) ) ∧ ( 𝐺 ‘ 𝑧 ) ≠ 0 ) → ( 𝐺 ‘ 𝑧 ) ≠ 0 )
48 eqid ⊢ ( invr ‘ 𝑅 ) = ( invr ‘ 𝑅 )
49 44 6 48 drnginvrcl ⊢ ( ( 𝑅 ∈ DivRing ∧ ( 𝐺 ‘ 𝑧 ) ∈ ( Base ‘ 𝑅 ) ∧ ( 𝐺 ‘ 𝑧 ) ≠ 0 ) → ( ( invr ‘ 𝑅 ) ‘ ( 𝐺 ‘ 𝑧 ) ) ∈ ( Base ‘ 𝑅 ) )
50 37 46 47 49 syl3anc ⊢ ( ( 𝜑 ∧ 𝑧 ∈ ( ⊥ ‘ ( 𝐿 ‘ 𝐺 ) ) ∧ ( 𝐺 ‘ 𝑧 ) ≠ 0 ) → ( ( invr ‘ 𝑅 ) ‘ ( 𝐺 ‘ 𝑧 ) ) ∈ ( Base ‘ 𝑅 ) )
51 simp2 ⊢ ( ( 𝜑 ∧ 𝑧 ∈ ( ⊥ ‘ ( 𝐿 ‘ 𝐺 ) ) ∧ ( 𝐺 ‘ 𝑧 ) ≠ 0 ) → 𝑧 ∈ ( ⊥ ‘ ( 𝐿 ‘ 𝐺 ) ) )
52 eqid ⊢ ( ·𝑠 ‘ 𝑈 ) = ( ·𝑠 ‘ 𝑈 )
53 5 52 44 29 lssvscl ⊢ ( ( ( 𝑈 ∈ LMod ∧ ( ⊥ ‘ ( 𝐿 ‘ 𝐺 ) ) ∈ ( LSubSp ‘ 𝑈 ) ) ∧ ( ( ( invr ‘ 𝑅 ) ‘ ( 𝐺 ‘ 𝑧 ) ) ∈ ( Base ‘ 𝑅 ) ∧ 𝑧 ∈ ( ⊥ ‘ ( 𝐿 ‘ 𝐺 ) ) ) ) → ( ( ( invr ‘ 𝑅 ) ‘ ( 𝐺 ‘ 𝑧 ) ) ( ·𝑠 ‘ 𝑈 ) 𝑧 ) ∈ ( ⊥ ‘ ( 𝐿 ‘ 𝐺 ) ) )
54 33 50 51 53 syl12anc ⊢ ( ( 𝜑 ∧ 𝑧 ∈ ( ⊥ ‘ ( 𝐿 ‘ 𝐺 ) ) ∧ ( 𝐺 ‘ 𝑧 ) ≠ 0 ) → ( ( ( invr ‘ 𝑅 ) ‘ ( 𝐺 ‘ 𝑧 ) ) ( ·𝑠 ‘ 𝑈 ) 𝑧 ) ∈ ( ⊥ ‘ ( 𝐿 ‘ 𝐺 ) ) )
55 eqid ⊢ ( .r ‘ 𝑅 ) = ( .r ‘ 𝑅 )
56 5 44 55 4 52 8 lflmul ⊢ ( ( 𝑈 ∈ LMod ∧ 𝐺 ∈ 𝐹 ∧ ( ( ( invr ‘ 𝑅 ) ‘ ( 𝐺 ‘ 𝑧 ) ) ∈ ( Base ‘ 𝑅 ) ∧ 𝑧 ∈ 𝑉 ) ) → ( 𝐺 ‘ ( ( ( invr ‘ 𝑅 ) ‘ ( 𝐺 ‘ 𝑧 ) ) ( ·𝑠 ‘ 𝑈 ) 𝑧 ) ) = ( ( ( invr ‘ 𝑅 ) ‘ ( 𝐺 ‘ 𝑧 ) ) ( .r ‘ 𝑅 ) ( 𝐺 ‘ 𝑧 ) ) )
57 38 39 50 43 56 syl112anc ⊢ ( ( 𝜑 ∧ 𝑧 ∈ ( ⊥ ‘ ( 𝐿 ‘ 𝐺 ) ) ∧ ( 𝐺 ‘ 𝑧 ) ≠ 0 ) → ( 𝐺 ‘ ( ( ( invr ‘ 𝑅 ) ‘ ( 𝐺 ‘ 𝑧 ) ) ( ·𝑠 ‘ 𝑈 ) 𝑧 ) ) = ( ( ( invr ‘ 𝑅 ) ‘ ( 𝐺 ‘ 𝑧 ) ) ( .r ‘ 𝑅 ) ( 𝐺 ‘ 𝑧 ) ) )
58 44 6 55 7 48 drnginvrl ⊢ ( ( 𝑅 ∈ DivRing ∧ ( 𝐺 ‘ 𝑧 ) ∈ ( Base ‘ 𝑅 ) ∧ ( 𝐺 ‘ 𝑧 ) ≠ 0 ) → ( ( ( invr ‘ 𝑅 ) ‘ ( 𝐺 ‘ 𝑧 ) ) ( .r ‘ 𝑅 ) ( 𝐺 ‘ 𝑧 ) ) = 1 )
59 37 46 47 58 syl3anc ⊢ ( ( 𝜑 ∧ 𝑧 ∈ ( ⊥ ‘ ( 𝐿 ‘ 𝐺 ) ) ∧ ( 𝐺 ‘ 𝑧 ) ≠ 0 ) → ( ( ( invr ‘ 𝑅 ) ‘ ( 𝐺 ‘ 𝑧 ) ) ( .r ‘ 𝑅 ) ( 𝐺 ‘ 𝑧 ) ) = 1 )
60 57 59 eqtrd ⊢ ( ( 𝜑 ∧ 𝑧 ∈ ( ⊥ ‘ ( 𝐿 ‘ 𝐺 ) ) ∧ ( 𝐺 ‘ 𝑧 ) ≠ 0 ) → ( 𝐺 ‘ ( ( ( invr ‘ 𝑅 ) ‘ ( 𝐺 ‘ 𝑧 ) ) ( ·𝑠 ‘ 𝑈 ) 𝑧 ) ) = 1 )
61 fveqeq2 ⊢ ( 𝑥 = ( ( ( invr ‘ 𝑅 ) ‘ ( 𝐺 ‘ 𝑧 ) ) ( ·𝑠 ‘ 𝑈 ) 𝑧 ) → ( ( 𝐺 ‘ 𝑥 ) = 1 ↔ ( 𝐺 ‘ ( ( ( invr ‘ 𝑅 ) ‘ ( 𝐺 ‘ 𝑧 ) ) ( ·𝑠 ‘ 𝑈 ) 𝑧 ) ) = 1 ) )
62 61 rspcev ⊢ ( ( ( ( ( invr ‘ 𝑅 ) ‘ ( 𝐺 ‘ 𝑧 ) ) ( ·𝑠 ‘ 𝑈 ) 𝑧 ) ∈ ( ⊥ ‘ ( 𝐿 ‘ 𝐺 ) ) ∧ ( 𝐺 ‘ ( ( ( invr ‘ 𝑅 ) ‘ ( 𝐺 ‘ 𝑧 ) ) ( ·𝑠 ‘ 𝑈 ) 𝑧 ) ) = 1 ) → ∃ 𝑥 ∈ ( ⊥ ‘ ( 𝐿 ‘ 𝐺 ) ) ( 𝐺 ‘ 𝑥 ) = 1 )
63 54 60 62 syl2anc ⊢ ( ( 𝜑 ∧ 𝑧 ∈ ( ⊥ ‘ ( 𝐿 ‘ 𝐺 ) ) ∧ ( 𝐺 ‘ 𝑧 ) ≠ 0 ) → ∃ 𝑥 ∈ ( ⊥ ‘ ( 𝐿 ‘ 𝐺 ) ) ( 𝐺 ‘ 𝑥 ) = 1 )
64 63 rexlimdv3a ⊢ ( 𝜑 → ( ∃ 𝑧 ∈ ( ⊥ ‘ ( 𝐿 ‘ 𝐺 ) ) ( 𝐺 ‘ 𝑧 ) ≠ 0 → ∃ 𝑥 ∈ ( ⊥ ‘ ( 𝐿 ‘ 𝐺 ) ) ( 𝐺 ‘ 𝑥 ) = 1 ) )
65 27 64 mpd ⊢ ( 𝜑 → ∃ 𝑥 ∈ ( ⊥ ‘ ( 𝐿 ‘ 𝐺 ) ) ( 𝐺 ‘ 𝑥 ) = 1 )