Metamath Proof Explorer

Theorem lkrpssN

Description: Proper subset relation between kernels. (Contributed by NM, 16-Feb-2015) (New usage is discouraged.)

Ref Expression
Hypotheses lkrpss.f ⊢ 𝐹 = ( LFnl ‘ 𝑊 )
lkrpss.k ⊢ 𝐾 = ( LKer ‘ 𝑊 )
lkrpss.d ⊢ 𝐷 = ( LDual ‘ 𝑊 )
lkrpss.o ⊢ 0 = ( 0g ‘ 𝐷 )
lkrpss.w ⊢ ( 𝜑 → 𝑊 ∈ LVec )
lkrpss.g ⊢ ( 𝜑 → 𝐺 ∈ 𝐹 )
lkrpss.h ⊢ ( 𝜑 → 𝐻 ∈ 𝐹 )
Assertion lkrpssN ( 𝜑 → ( ( 𝐾 ‘ 𝐺 ) ⊊ ( 𝐾 ‘ 𝐻 ) ↔ ( 𝐺 ≠ 0 ∧ 𝐻 = 0 ) ) )

Proof

Step Hyp Ref Expression
1 lkrpss.f ⊢ 𝐹 = ( LFnl ‘ 𝑊 )
2 lkrpss.k ⊢ 𝐾 = ( LKer ‘ 𝑊 )
3 lkrpss.d ⊢ 𝐷 = ( LDual ‘ 𝑊 )
4 lkrpss.o ⊢ 0 = ( 0g ‘ 𝐷 )
5 lkrpss.w ⊢ ( 𝜑 → 𝑊 ∈ LVec )
6 lkrpss.g ⊢ ( 𝜑 → 𝐺 ∈ 𝐹 )
7 lkrpss.h ⊢ ( 𝜑 → 𝐻 ∈ 𝐹 )
8 df-pss ⊢ ( ( 𝐾 ‘ 𝐺 ) ⊊ ( 𝐾 ‘ 𝐻 ) ↔ ( ( 𝐾 ‘ 𝐺 ) ⊆ ( 𝐾 ‘ 𝐻 ) ∧ ( 𝐾 ‘ 𝐺 ) ≠ ( 𝐾 ‘ 𝐻 ) ) )
9 simpr ⊢ ( ( 𝜑 ∧ ( 𝐾 ‘ 𝐺 ) ⊊ ( 𝐾 ‘ 𝐻 ) ) → ( 𝐾 ‘ 𝐺 ) ⊊ ( 𝐾 ‘ 𝐻 ) )
10 eqid ⊢ ( Base ‘ 𝑊 ) = ( Base ‘ 𝑊 )
11 lveclmod ⊢ ( 𝑊 ∈ LVec → 𝑊 ∈ LMod )
12 5 11 syl ⊢ ( 𝜑 → 𝑊 ∈ LMod )
13 10 1 2 12 7 lkrssv ⊢ ( 𝜑 → ( 𝐾 ‘ 𝐻 ) ⊆ ( Base ‘ 𝑊 ) )
14 13 adantr ⊢ ( ( 𝜑 ∧ ( 𝐾 ‘ 𝐺 ) ⊊ ( 𝐾 ‘ 𝐻 ) ) → ( 𝐾 ‘ 𝐻 ) ⊆ ( Base ‘ 𝑊 ) )
15 9 14 psssstrd ⊢ ( ( 𝜑 ∧ ( 𝐾 ‘ 𝐺 ) ⊊ ( 𝐾 ‘ 𝐻 ) ) → ( 𝐾 ‘ 𝐺 ) ⊊ ( Base ‘ 𝑊 ) )
16 15 pssned ⊢ ( ( 𝜑 ∧ ( 𝐾 ‘ 𝐺 ) ⊊ ( 𝐾 ‘ 𝐻 ) ) → ( 𝐾 ‘ 𝐺 ) ≠ ( Base ‘ 𝑊 ) )
17 8 16 sylan2br ⊢ ( ( 𝜑 ∧ ( ( 𝐾 ‘ 𝐺 ) ⊆ ( 𝐾 ‘ 𝐻 ) ∧ ( 𝐾 ‘ 𝐺 ) ≠ ( 𝐾 ‘ 𝐻 ) ) ) → ( 𝐾 ‘ 𝐺 ) ≠ ( Base ‘ 𝑊 ) )
18 simplr ⊢ ( ( ( 𝜑 ∧ ( 𝐾 ‘ 𝐺 ) ⊆ ( 𝐾 ‘ 𝐻 ) ) ∧ ( 𝐾 ‘ 𝐻 ) ∈ ( LSHyp ‘ 𝑊 ) ) → ( 𝐾 ‘ 𝐺 ) ⊆ ( 𝐾 ‘ 𝐻 ) )
19 eqid ⊢ ( LSHyp ‘ 𝑊 ) = ( LSHyp ‘ 𝑊 )
20 5 ad2antrr ⊢ ( ( ( 𝜑 ∧ ( 𝐾 ‘ 𝐺 ) ⊆ ( 𝐾 ‘ 𝐻 ) ) ∧ ( 𝐾 ‘ 𝐻 ) ∈ ( LSHyp ‘ 𝑊 ) ) → 𝑊 ∈ LVec )
21 simpr ⊢ ( ( ( ( 𝜑 ∧ ( 𝐾 ‘ 𝐺 ) ⊆ ( 𝐾 ‘ 𝐻 ) ) ∧ ( 𝐾 ‘ 𝐻 ) ∈ ( LSHyp ‘ 𝑊 ) ) ∧ ( 𝐾 ‘ 𝐺 ) ∈ ( LSHyp ‘ 𝑊 ) ) → ( 𝐾 ‘ 𝐺 ) ∈ ( LSHyp ‘ 𝑊 ) )
22 simplr ⊢ ( ( ( ( 𝜑 ∧ ( 𝐾 ‘ 𝐺 ) ⊆ ( 𝐾 ‘ 𝐻 ) ) ∧ ( 𝐾 ‘ 𝐻 ) ∈ ( LSHyp ‘ 𝑊 ) ) ∧ ( 𝐾 ‘ 𝐺 ) = ( Base ‘ 𝑊 ) ) → ( 𝐾 ‘ 𝐻 ) ∈ ( LSHyp ‘ 𝑊 ) )
23 13 ad3antrrr ⊢ ( ( ( ( 𝜑 ∧ ( 𝐾 ‘ 𝐺 ) ⊆ ( 𝐾 ‘ 𝐻 ) ) ∧ ( 𝐾 ‘ 𝐻 ) ∈ ( LSHyp ‘ 𝑊 ) ) ∧ ( 𝐾 ‘ 𝐺 ) = ( Base ‘ 𝑊 ) ) → ( 𝐾 ‘ 𝐻 ) ⊆ ( Base ‘ 𝑊 ) )
24 simpr ⊢ ( ( ( ( 𝜑 ∧ ( 𝐾 ‘ 𝐺 ) ⊆ ( 𝐾 ‘ 𝐻 ) ) ∧ ( 𝐾 ‘ 𝐻 ) ∈ ( LSHyp ‘ 𝑊 ) ) ∧ ( 𝐾 ‘ 𝐺 ) = ( Base ‘ 𝑊 ) ) → ( 𝐾 ‘ 𝐺 ) = ( Base ‘ 𝑊 ) )
25 simpllr ⊢ ( ( ( ( 𝜑 ∧ ( 𝐾 ‘ 𝐺 ) ⊆ ( 𝐾 ‘ 𝐻 ) ) ∧ ( 𝐾 ‘ 𝐻 ) ∈ ( LSHyp ‘ 𝑊 ) ) ∧ ( 𝐾 ‘ 𝐺 ) = ( Base ‘ 𝑊 ) ) → ( 𝐾 ‘ 𝐺 ) ⊆ ( 𝐾 ‘ 𝐻 ) )
26 24 25 eqsstrrd ⊢ ( ( ( ( 𝜑 ∧ ( 𝐾 ‘ 𝐺 ) ⊆ ( 𝐾 ‘ 𝐻 ) ) ∧ ( 𝐾 ‘ 𝐻 ) ∈ ( LSHyp ‘ 𝑊 ) ) ∧ ( 𝐾 ‘ 𝐺 ) = ( Base ‘ 𝑊 ) ) → ( Base ‘ 𝑊 ) ⊆ ( 𝐾 ‘ 𝐻 ) )
27 23 26 eqssd ⊢ ( ( ( ( 𝜑 ∧ ( 𝐾 ‘ 𝐺 ) ⊆ ( 𝐾 ‘ 𝐻 ) ) ∧ ( 𝐾 ‘ 𝐻 ) ∈ ( LSHyp ‘ 𝑊 ) ) ∧ ( 𝐾 ‘ 𝐺 ) = ( Base ‘ 𝑊 ) ) → ( 𝐾 ‘ 𝐻 ) = ( Base ‘ 𝑊 ) )
28 10 19 1 2 5 7 lkrshp4 ⊢ ( 𝜑 → ( ( 𝐾 ‘ 𝐻 ) ≠ ( Base ‘ 𝑊 ) ↔ ( 𝐾 ‘ 𝐻 ) ∈ ( LSHyp ‘ 𝑊 ) ) )
29 28 ad3antrrr ⊢ ( ( ( ( 𝜑 ∧ ( 𝐾 ‘ 𝐺 ) ⊆ ( 𝐾 ‘ 𝐻 ) ) ∧ ( 𝐾 ‘ 𝐻 ) ∈ ( LSHyp ‘ 𝑊 ) ) ∧ ( 𝐾 ‘ 𝐺 ) = ( Base ‘ 𝑊 ) ) → ( ( 𝐾 ‘ 𝐻 ) ≠ ( Base ‘ 𝑊 ) ↔ ( 𝐾 ‘ 𝐻 ) ∈ ( LSHyp ‘ 𝑊 ) ) )
30 29 necon1bbid ⊢ ( ( ( ( 𝜑 ∧ ( 𝐾 ‘ 𝐺 ) ⊆ ( 𝐾 ‘ 𝐻 ) ) ∧ ( 𝐾 ‘ 𝐻 ) ∈ ( LSHyp ‘ 𝑊 ) ) ∧ ( 𝐾 ‘ 𝐺 ) = ( Base ‘ 𝑊 ) ) → ( ¬ ( 𝐾 ‘ 𝐻 ) ∈ ( LSHyp ‘ 𝑊 ) ↔ ( 𝐾 ‘ 𝐻 ) = ( Base ‘ 𝑊 ) ) )
31 27 30 mpbird ⊢ ( ( ( ( 𝜑 ∧ ( 𝐾 ‘ 𝐺 ) ⊆ ( 𝐾 ‘ 𝐻 ) ) ∧ ( 𝐾 ‘ 𝐻 ) ∈ ( LSHyp ‘ 𝑊 ) ) ∧ ( 𝐾 ‘ 𝐺 ) = ( Base ‘ 𝑊 ) ) → ¬ ( 𝐾 ‘ 𝐻 ) ∈ ( LSHyp ‘ 𝑊 ) )
32 22 31 pm2.21dd ⊢ ( ( ( ( 𝜑 ∧ ( 𝐾 ‘ 𝐺 ) ⊆ ( 𝐾 ‘ 𝐻 ) ) ∧ ( 𝐾 ‘ 𝐻 ) ∈ ( LSHyp ‘ 𝑊 ) ) ∧ ( 𝐾 ‘ 𝐺 ) = ( Base ‘ 𝑊 ) ) → ( 𝐾 ‘ 𝐺 ) ∈ ( LSHyp ‘ 𝑊 ) )
33 10 19 1 2 5 6 lkrshpor ⊢ ( 𝜑 → ( ( 𝐾 ‘ 𝐺 ) ∈ ( LSHyp ‘ 𝑊 ) ∨ ( 𝐾 ‘ 𝐺 ) = ( Base ‘ 𝑊 ) ) )
34 33 ad2antrr ⊢ ( ( ( 𝜑 ∧ ( 𝐾 ‘ 𝐺 ) ⊆ ( 𝐾 ‘ 𝐻 ) ) ∧ ( 𝐾 ‘ 𝐻 ) ∈ ( LSHyp ‘ 𝑊 ) ) → ( ( 𝐾 ‘ 𝐺 ) ∈ ( LSHyp ‘ 𝑊 ) ∨ ( 𝐾 ‘ 𝐺 ) = ( Base ‘ 𝑊 ) ) )
35 21 32 34 mpjaodan ⊢ ( ( ( 𝜑 ∧ ( 𝐾 ‘ 𝐺 ) ⊆ ( 𝐾 ‘ 𝐻 ) ) ∧ ( 𝐾 ‘ 𝐻 ) ∈ ( LSHyp ‘ 𝑊 ) ) → ( 𝐾 ‘ 𝐺 ) ∈ ( LSHyp ‘ 𝑊 ) )
36 simpr ⊢ ( ( ( 𝜑 ∧ ( 𝐾 ‘ 𝐺 ) ⊆ ( 𝐾 ‘ 𝐻 ) ) ∧ ( 𝐾 ‘ 𝐻 ) ∈ ( LSHyp ‘ 𝑊 ) ) → ( 𝐾 ‘ 𝐻 ) ∈ ( LSHyp ‘ 𝑊 ) )
37 19 20 35 36 lshpcmp ⊢ ( ( ( 𝜑 ∧ ( 𝐾 ‘ 𝐺 ) ⊆ ( 𝐾 ‘ 𝐻 ) ) ∧ ( 𝐾 ‘ 𝐻 ) ∈ ( LSHyp ‘ 𝑊 ) ) → ( ( 𝐾 ‘ 𝐺 ) ⊆ ( 𝐾 ‘ 𝐻 ) ↔ ( 𝐾 ‘ 𝐺 ) = ( 𝐾 ‘ 𝐻 ) ) )
38 18 37 mpbid ⊢ ( ( ( 𝜑 ∧ ( 𝐾 ‘ 𝐺 ) ⊆ ( 𝐾 ‘ 𝐻 ) ) ∧ ( 𝐾 ‘ 𝐻 ) ∈ ( LSHyp ‘ 𝑊 ) ) → ( 𝐾 ‘ 𝐺 ) = ( 𝐾 ‘ 𝐻 ) )
39 38 ex ⊢ ( ( 𝜑 ∧ ( 𝐾 ‘ 𝐺 ) ⊆ ( 𝐾 ‘ 𝐻 ) ) → ( ( 𝐾 ‘ 𝐻 ) ∈ ( LSHyp ‘ 𝑊 ) → ( 𝐾 ‘ 𝐺 ) = ( 𝐾 ‘ 𝐻 ) ) )
40 39 necon3ad ⊢ ( ( 𝜑 ∧ ( 𝐾 ‘ 𝐺 ) ⊆ ( 𝐾 ‘ 𝐻 ) ) → ( ( 𝐾 ‘ 𝐺 ) ≠ ( 𝐾 ‘ 𝐻 ) → ¬ ( 𝐾 ‘ 𝐻 ) ∈ ( LSHyp ‘ 𝑊 ) ) )
41 40 impr ⊢ ( ( 𝜑 ∧ ( ( 𝐾 ‘ 𝐺 ) ⊆ ( 𝐾 ‘ 𝐻 ) ∧ ( 𝐾 ‘ 𝐺 ) ≠ ( 𝐾 ‘ 𝐻 ) ) ) → ¬ ( 𝐾 ‘ 𝐻 ) ∈ ( LSHyp ‘ 𝑊 ) )
42 28 necon1bbid ⊢ ( 𝜑 → ( ¬ ( 𝐾 ‘ 𝐻 ) ∈ ( LSHyp ‘ 𝑊 ) ↔ ( 𝐾 ‘ 𝐻 ) = ( Base ‘ 𝑊 ) ) )
43 42 adantr ⊢ ( ( 𝜑 ∧ ( ( 𝐾 ‘ 𝐺 ) ⊆ ( 𝐾 ‘ 𝐻 ) ∧ ( 𝐾 ‘ 𝐺 ) ≠ ( 𝐾 ‘ 𝐻 ) ) ) → ( ¬ ( 𝐾 ‘ 𝐻 ) ∈ ( LSHyp ‘ 𝑊 ) ↔ ( 𝐾 ‘ 𝐻 ) = ( Base ‘ 𝑊 ) ) )
44 41 43 mpbid ⊢ ( ( 𝜑 ∧ ( ( 𝐾 ‘ 𝐺 ) ⊆ ( 𝐾 ‘ 𝐻 ) ∧ ( 𝐾 ‘ 𝐺 ) ≠ ( 𝐾 ‘ 𝐻 ) ) ) → ( 𝐾 ‘ 𝐻 ) = ( Base ‘ 𝑊 ) )
45 17 44 jca ⊢ ( ( 𝜑 ∧ ( ( 𝐾 ‘ 𝐺 ) ⊆ ( 𝐾 ‘ 𝐻 ) ∧ ( 𝐾 ‘ 𝐺 ) ≠ ( 𝐾 ‘ 𝐻 ) ) ) → ( ( 𝐾 ‘ 𝐺 ) ≠ ( Base ‘ 𝑊 ) ∧ ( 𝐾 ‘ 𝐻 ) = ( Base ‘ 𝑊 ) ) )
46 10 1 2 12 6 lkrssv ⊢ ( 𝜑 → ( 𝐾 ‘ 𝐺 ) ⊆ ( Base ‘ 𝑊 ) )
47 46 adantr ⊢ ( ( 𝜑 ∧ ( ( 𝐾 ‘ 𝐺 ) ≠ ( Base ‘ 𝑊 ) ∧ ( 𝐾 ‘ 𝐻 ) = ( Base ‘ 𝑊 ) ) ) → ( 𝐾 ‘ 𝐺 ) ⊆ ( Base ‘ 𝑊 ) )
48 simprr ⊢ ( ( 𝜑 ∧ ( ( 𝐾 ‘ 𝐺 ) ≠ ( Base ‘ 𝑊 ) ∧ ( 𝐾 ‘ 𝐻 ) = ( Base ‘ 𝑊 ) ) ) → ( 𝐾 ‘ 𝐻 ) = ( Base ‘ 𝑊 ) )
49 48 eqcomd ⊢ ( ( 𝜑 ∧ ( ( 𝐾 ‘ 𝐺 ) ≠ ( Base ‘ 𝑊 ) ∧ ( 𝐾 ‘ 𝐻 ) = ( Base ‘ 𝑊 ) ) ) → ( Base ‘ 𝑊 ) = ( 𝐾 ‘ 𝐻 ) )
50 47 49 sseqtrd ⊢ ( ( 𝜑 ∧ ( ( 𝐾 ‘ 𝐺 ) ≠ ( Base ‘ 𝑊 ) ∧ ( 𝐾 ‘ 𝐻 ) = ( Base ‘ 𝑊 ) ) ) → ( 𝐾 ‘ 𝐺 ) ⊆ ( 𝐾 ‘ 𝐻 ) )
51 simprl ⊢ ( ( 𝜑 ∧ ( ( 𝐾 ‘ 𝐺 ) ≠ ( Base ‘ 𝑊 ) ∧ ( 𝐾 ‘ 𝐻 ) = ( Base ‘ 𝑊 ) ) ) → ( 𝐾 ‘ 𝐺 ) ≠ ( Base ‘ 𝑊 ) )
52 51 49 neeqtrd ⊢ ( ( 𝜑 ∧ ( ( 𝐾 ‘ 𝐺 ) ≠ ( Base ‘ 𝑊 ) ∧ ( 𝐾 ‘ 𝐻 ) = ( Base ‘ 𝑊 ) ) ) → ( 𝐾 ‘ 𝐺 ) ≠ ( 𝐾 ‘ 𝐻 ) )
53 50 52 jca ⊢ ( ( 𝜑 ∧ ( ( 𝐾 ‘ 𝐺 ) ≠ ( Base ‘ 𝑊 ) ∧ ( 𝐾 ‘ 𝐻 ) = ( Base ‘ 𝑊 ) ) ) → ( ( 𝐾 ‘ 𝐺 ) ⊆ ( 𝐾 ‘ 𝐻 ) ∧ ( 𝐾 ‘ 𝐺 ) ≠ ( 𝐾 ‘ 𝐻 ) ) )
54 45 53 impbida ⊢ ( 𝜑 → ( ( ( 𝐾 ‘ 𝐺 ) ⊆ ( 𝐾 ‘ 𝐻 ) ∧ ( 𝐾 ‘ 𝐺 ) ≠ ( 𝐾 ‘ 𝐻 ) ) ↔ ( ( 𝐾 ‘ 𝐺 ) ≠ ( Base ‘ 𝑊 ) ∧ ( 𝐾 ‘ 𝐻 ) = ( Base ‘ 𝑊 ) ) ) )
55 8 54 syl5bb ⊢ ( 𝜑 → ( ( 𝐾 ‘ 𝐺 ) ⊊ ( 𝐾 ‘ 𝐻 ) ↔ ( ( 𝐾 ‘ 𝐺 ) ≠ ( Base ‘ 𝑊 ) ∧ ( 𝐾 ‘ 𝐻 ) = ( Base ‘ 𝑊 ) ) ) )
56 10 1 2 3 4 12 6 lkr0f2 ⊢ ( 𝜑 → ( ( 𝐾 ‘ 𝐺 ) = ( Base ‘ 𝑊 ) ↔ 𝐺 = 0 ) )
57 56 necon3bid ⊢ ( 𝜑 → ( ( 𝐾 ‘ 𝐺 ) ≠ ( Base ‘ 𝑊 ) ↔ 𝐺 ≠ 0 ) )
58 10 1 2 3 4 12 7 lkr0f2 ⊢ ( 𝜑 → ( ( 𝐾 ‘ 𝐻 ) = ( Base ‘ 𝑊 ) ↔ 𝐻 = 0 ) )
59 57 58 anbi12d ⊢ ( 𝜑 → ( ( ( 𝐾 ‘ 𝐺 ) ≠ ( Base ‘ 𝑊 ) ∧ ( 𝐾 ‘ 𝐻 ) = ( Base ‘ 𝑊 ) ) ↔ ( 𝐺 ≠ 0 ∧ 𝐻 = 0 ) ) )
60 55 59 bitrd ⊢ ( 𝜑 → ( ( 𝐾 ‘ 𝐺 ) ⊊ ( 𝐾 ‘ 𝐻 ) ↔ ( 𝐺 ≠ 0 ∧ 𝐻 = 0 ) ) )