Step | Hyp | Ref
| Expression |
1 | | ssrab2 3687 |
. . . 4
⊢ {𝑓 ∈ 𝐹 ∣ (( ⊥ ‘( ⊥
‘(𝐿‘𝑓))) = (𝐿‘𝑓) ∧ ( ⊥ ‘(𝐿‘𝑓)) ⊆ 𝑅)} ⊆ 𝐹 |
2 | 1 | a1i 11 |
. . 3
⊢ (𝜑 → {𝑓 ∈ 𝐹 ∣ (( ⊥ ‘( ⊥
‘(𝐿‘𝑓))) = (𝐿‘𝑓) ∧ ( ⊥ ‘(𝐿‘𝑓)) ⊆ 𝑅)} ⊆ 𝐹) |
3 | | lclkrs.c |
. . . 4
⊢ 𝐶 = {𝑓 ∈ 𝐹 ∣ (( ⊥ ‘( ⊥
‘(𝐿‘𝑓))) = (𝐿‘𝑓) ∧ ( ⊥ ‘(𝐿‘𝑓)) ⊆ 𝑅)} |
4 | 3 | a1i 11 |
. . 3
⊢ (𝜑 → 𝐶 = {𝑓 ∈ 𝐹 ∣ (( ⊥ ‘( ⊥
‘(𝐿‘𝑓))) = (𝐿‘𝑓) ∧ ( ⊥ ‘(𝐿‘𝑓)) ⊆ 𝑅)}) |
5 | | lclkrs.f |
. . . 4
⊢ 𝐹 = (LFnl‘𝑈) |
6 | | lclkrs.d |
. . . 4
⊢ 𝐷 = (LDual‘𝑈) |
7 | | eqid 2622 |
. . . 4
⊢
(Base‘𝐷) =
(Base‘𝐷) |
8 | | lclkrs.h |
. . . . 5
⊢ 𝐻 = (LHyp‘𝐾) |
9 | | lclkrs.u |
. . . . 5
⊢ 𝑈 = ((DVecH‘𝐾)‘𝑊) |
10 | | lclkrs.k |
. . . . 5
⊢ (𝜑 → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻)) |
11 | 8, 9, 10 | dvhlmod 36399 |
. . . 4
⊢ (𝜑 → 𝑈 ∈ LMod) |
12 | 5, 6, 7, 11 | ldualvbase 34413 |
. . 3
⊢ (𝜑 → (Base‘𝐷) = 𝐹) |
13 | 2, 4, 12 | 3sstr4d 3648 |
. 2
⊢ (𝜑 → 𝐶 ⊆ (Base‘𝐷)) |
14 | | eqid 2622 |
. . . . . 6
⊢
(Scalar‘𝑈) =
(Scalar‘𝑈) |
15 | | eqid 2622 |
. . . . . 6
⊢
(0g‘(Scalar‘𝑈)) =
(0g‘(Scalar‘𝑈)) |
16 | | eqid 2622 |
. . . . . 6
⊢
(Base‘𝑈) =
(Base‘𝑈) |
17 | 14, 15, 16, 5 | lfl0f 34356 |
. . . . 5
⊢ (𝑈 ∈ LMod →
((Base‘𝑈) ×
{(0g‘(Scalar‘𝑈))}) ∈ 𝐹) |
18 | 11, 17 | syl 17 |
. . . 4
⊢ (𝜑 → ((Base‘𝑈) ×
{(0g‘(Scalar‘𝑈))}) ∈ 𝐹) |
19 | | lclkrs.o |
. . . . . 6
⊢ ⊥ =
((ocH‘𝐾)‘𝑊) |
20 | 8, 9, 19, 16, 10 | dochoc1 36650 |
. . . . 5
⊢ (𝜑 → ( ⊥ ‘( ⊥
‘(Base‘𝑈))) =
(Base‘𝑈)) |
21 | | eqidd 2623 |
. . . . . . . 8
⊢ (𝜑 → ((Base‘𝑈) ×
{(0g‘(Scalar‘𝑈))}) = ((Base‘𝑈) ×
{(0g‘(Scalar‘𝑈))})) |
22 | | lclkrs.l |
. . . . . . . . . 10
⊢ 𝐿 = (LKer‘𝑈) |
23 | 14, 15, 16, 5, 22 | lkr0f 34381 |
. . . . . . . . 9
⊢ ((𝑈 ∈ LMod ∧
((Base‘𝑈) ×
{(0g‘(Scalar‘𝑈))}) ∈ 𝐹) → ((𝐿‘((Base‘𝑈) ×
{(0g‘(Scalar‘𝑈))})) = (Base‘𝑈) ↔ ((Base‘𝑈) ×
{(0g‘(Scalar‘𝑈))}) = ((Base‘𝑈) ×
{(0g‘(Scalar‘𝑈))}))) |
24 | 11, 18, 23 | syl2anc 693 |
. . . . . . . 8
⊢ (𝜑 → ((𝐿‘((Base‘𝑈) ×
{(0g‘(Scalar‘𝑈))})) = (Base‘𝑈) ↔ ((Base‘𝑈) ×
{(0g‘(Scalar‘𝑈))}) = ((Base‘𝑈) ×
{(0g‘(Scalar‘𝑈))}))) |
25 | 21, 24 | mpbird 247 |
. . . . . . 7
⊢ (𝜑 → (𝐿‘((Base‘𝑈) ×
{(0g‘(Scalar‘𝑈))})) = (Base‘𝑈)) |
26 | 25 | fveq2d 6195 |
. . . . . 6
⊢ (𝜑 → ( ⊥ ‘(𝐿‘((Base‘𝑈) ×
{(0g‘(Scalar‘𝑈))}))) = ( ⊥
‘(Base‘𝑈))) |
27 | 26 | fveq2d 6195 |
. . . . 5
⊢ (𝜑 → ( ⊥ ‘( ⊥
‘(𝐿‘((Base‘𝑈) ×
{(0g‘(Scalar‘𝑈))})))) = ( ⊥ ‘( ⊥
‘(Base‘𝑈)))) |
28 | 20, 27, 25 | 3eqtr4d 2666 |
. . . 4
⊢ (𝜑 → ( ⊥ ‘( ⊥
‘(𝐿‘((Base‘𝑈) ×
{(0g‘(Scalar‘𝑈))})))) = (𝐿‘((Base‘𝑈) ×
{(0g‘(Scalar‘𝑈))}))) |
29 | | eqid 2622 |
. . . . . . . 8
⊢
(0g‘𝑈) = (0g‘𝑈) |
30 | 8, 9, 19, 16, 29 | doch1 36648 |
. . . . . . 7
⊢ ((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) → ( ⊥
‘(Base‘𝑈)) =
{(0g‘𝑈)}) |
31 | 10, 30 | syl 17 |
. . . . . 6
⊢ (𝜑 → ( ⊥
‘(Base‘𝑈)) =
{(0g‘𝑈)}) |
32 | 26, 31 | eqtrd 2656 |
. . . . 5
⊢ (𝜑 → ( ⊥ ‘(𝐿‘((Base‘𝑈) ×
{(0g‘(Scalar‘𝑈))}))) = {(0g‘𝑈)}) |
33 | | lclkrs.r |
. . . . . 6
⊢ (𝜑 → 𝑅 ∈ 𝑆) |
34 | | lclkrs.s |
. . . . . . 7
⊢ 𝑆 = (LSubSp‘𝑈) |
35 | 29, 34 | lss0ss 18949 |
. . . . . 6
⊢ ((𝑈 ∈ LMod ∧ 𝑅 ∈ 𝑆) → {(0g‘𝑈)} ⊆ 𝑅) |
36 | 11, 33, 35 | syl2anc 693 |
. . . . 5
⊢ (𝜑 →
{(0g‘𝑈)}
⊆ 𝑅) |
37 | 32, 36 | eqsstrd 3639 |
. . . 4
⊢ (𝜑 → ( ⊥ ‘(𝐿‘((Base‘𝑈) ×
{(0g‘(Scalar‘𝑈))}))) ⊆ 𝑅) |
38 | 3 | lcfls1lem 36823 |
. . . 4
⊢
(((Base‘𝑈)
× {(0g‘(Scalar‘𝑈))}) ∈ 𝐶 ↔ (((Base‘𝑈) ×
{(0g‘(Scalar‘𝑈))}) ∈ 𝐹 ∧ ( ⊥ ‘( ⊥
‘(𝐿‘((Base‘𝑈) ×
{(0g‘(Scalar‘𝑈))})))) = (𝐿‘((Base‘𝑈) ×
{(0g‘(Scalar‘𝑈))})) ∧ ( ⊥ ‘(𝐿‘((Base‘𝑈) ×
{(0g‘(Scalar‘𝑈))}))) ⊆ 𝑅)) |
39 | 18, 28, 37, 38 | syl3anbrc 1246 |
. . 3
⊢ (𝜑 → ((Base‘𝑈) ×
{(0g‘(Scalar‘𝑈))}) ∈ 𝐶) |
40 | | ne0i 3921 |
. . 3
⊢
(((Base‘𝑈)
× {(0g‘(Scalar‘𝑈))}) ∈ 𝐶 → 𝐶 ≠ ∅) |
41 | 39, 40 | syl 17 |
. 2
⊢ (𝜑 → 𝐶 ≠ ∅) |
42 | | eqid 2622 |
. . . 4
⊢
(Base‘(Scalar‘𝑈)) = (Base‘(Scalar‘𝑈)) |
43 | | eqid 2622 |
. . . 4
⊢ (
·𝑠 ‘𝐷) = ( ·𝑠
‘𝐷) |
44 | 10 | adantr 481 |
. . . 4
⊢ ((𝜑 ∧ (𝑥 ∈ (Base‘(Scalar‘𝐷)) ∧ 𝑎 ∈ 𝐶 ∧ 𝑏 ∈ 𝐶)) → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻)) |
45 | 33 | adantr 481 |
. . . 4
⊢ ((𝜑 ∧ (𝑥 ∈ (Base‘(Scalar‘𝐷)) ∧ 𝑎 ∈ 𝐶 ∧ 𝑏 ∈ 𝐶)) → 𝑅 ∈ 𝑆) |
46 | | simpr3 1069 |
. . . 4
⊢ ((𝜑 ∧ (𝑥 ∈ (Base‘(Scalar‘𝐷)) ∧ 𝑎 ∈ 𝐶 ∧ 𝑏 ∈ 𝐶)) → 𝑏 ∈ 𝐶) |
47 | | eqid 2622 |
. . . 4
⊢
(+g‘𝐷) = (+g‘𝐷) |
48 | | simpr2 1068 |
. . . . 5
⊢ ((𝜑 ∧ (𝑥 ∈ (Base‘(Scalar‘𝐷)) ∧ 𝑎 ∈ 𝐶 ∧ 𝑏 ∈ 𝐶)) → 𝑎 ∈ 𝐶) |
49 | | simpr1 1067 |
. . . . . 6
⊢ ((𝜑 ∧ (𝑥 ∈ (Base‘(Scalar‘𝐷)) ∧ 𝑎 ∈ 𝐶 ∧ 𝑏 ∈ 𝐶)) → 𝑥 ∈ (Base‘(Scalar‘𝐷))) |
50 | | eqid 2622 |
. . . . . . . 8
⊢
(Scalar‘𝐷) =
(Scalar‘𝐷) |
51 | | eqid 2622 |
. . . . . . . 8
⊢
(Base‘(Scalar‘𝐷)) = (Base‘(Scalar‘𝐷)) |
52 | 14, 42, 6, 50, 51, 11 | ldualsbase 34420 |
. . . . . . 7
⊢ (𝜑 →
(Base‘(Scalar‘𝐷)) = (Base‘(Scalar‘𝑈))) |
53 | 52 | adantr 481 |
. . . . . 6
⊢ ((𝜑 ∧ (𝑥 ∈ (Base‘(Scalar‘𝐷)) ∧ 𝑎 ∈ 𝐶 ∧ 𝑏 ∈ 𝐶)) → (Base‘(Scalar‘𝐷)) =
(Base‘(Scalar‘𝑈))) |
54 | 49, 53 | eleqtrd 2703 |
. . . . 5
⊢ ((𝜑 ∧ (𝑥 ∈ (Base‘(Scalar‘𝐷)) ∧ 𝑎 ∈ 𝐶 ∧ 𝑏 ∈ 𝐶)) → 𝑥 ∈ (Base‘(Scalar‘𝑈))) |
55 | 8, 19, 9, 34, 5, 22, 6, 14, 42, 43, 3, 44, 45, 48, 54 | lclkrslem1 36826 |
. . . 4
⊢ ((𝜑 ∧ (𝑥 ∈ (Base‘(Scalar‘𝐷)) ∧ 𝑎 ∈ 𝐶 ∧ 𝑏 ∈ 𝐶)) → (𝑥( ·𝑠
‘𝐷)𝑎) ∈ 𝐶) |
56 | 8, 19, 9, 34, 5, 22, 6, 14, 42, 43, 3, 44, 45, 46, 47, 55 | lclkrslem2 36827 |
. . 3
⊢ ((𝜑 ∧ (𝑥 ∈ (Base‘(Scalar‘𝐷)) ∧ 𝑎 ∈ 𝐶 ∧ 𝑏 ∈ 𝐶)) → ((𝑥( ·𝑠
‘𝐷)𝑎)(+g‘𝐷)𝑏) ∈ 𝐶) |
57 | 56 | ralrimivvva 2972 |
. 2
⊢ (𝜑 → ∀𝑥 ∈ (Base‘(Scalar‘𝐷))∀𝑎 ∈ 𝐶 ∀𝑏 ∈ 𝐶 ((𝑥( ·𝑠
‘𝐷)𝑎)(+g‘𝐷)𝑏) ∈ 𝐶) |
58 | | lclkrs.t |
. . 3
⊢ 𝑇 = (LSubSp‘𝐷) |
59 | 50, 51, 7, 47, 43, 58 | islss 18935 |
. 2
⊢ (𝐶 ∈ 𝑇 ↔ (𝐶 ⊆ (Base‘𝐷) ∧ 𝐶 ≠ ∅ ∧ ∀𝑥 ∈
(Base‘(Scalar‘𝐷))∀𝑎 ∈ 𝐶 ∀𝑏 ∈ 𝐶 ((𝑥( ·𝑠
‘𝐷)𝑎)(+g‘𝐷)𝑏) ∈ 𝐶)) |
60 | 13, 41, 57, 59 | syl3anbrc 1246 |
1
⊢ (𝜑 → 𝐶 ∈ 𝑇) |