Step | Hyp | Ref
| Expression |
1 | | lcfr.q |
. . . 4
⊢ 𝑄 = ∪ 𝑔 ∈ 𝑅 ( ⊥ ‘(𝐿‘𝑔)) |
2 | | fveq2 6191 |
. . . . . 6
⊢ (𝑔 = ℎ → (𝐿‘𝑔) = (𝐿‘ℎ)) |
3 | 2 | fveq2d 6195 |
. . . . 5
⊢ (𝑔 = ℎ → ( ⊥ ‘(𝐿‘𝑔)) = ( ⊥ ‘(𝐿‘ℎ))) |
4 | 3 | cbviunv 4559 |
. . . 4
⊢ ∪ 𝑔 ∈ 𝑅 ( ⊥ ‘(𝐿‘𝑔)) = ∪
ℎ ∈ 𝑅 ( ⊥ ‘(𝐿‘ℎ)) |
5 | 1, 4 | eqtri 2644 |
. . 3
⊢ 𝑄 = ∪ ℎ
∈ 𝑅 ( ⊥
‘(𝐿‘ℎ)) |
6 | | lcfr.k |
. . . . . . 7
⊢ (𝜑 → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻)) |
7 | 6 | adantr 481 |
. . . . . 6
⊢ ((𝜑 ∧ ℎ ∈ 𝑅) → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻)) |
8 | | eqid 2622 |
. . . . . . 7
⊢
(Base‘𝑈) =
(Base‘𝑈) |
9 | | lcfr.f |
. . . . . . 7
⊢ 𝐹 = (LFnl‘𝑈) |
10 | | lcfr.l |
. . . . . . 7
⊢ 𝐿 = (LKer‘𝑈) |
11 | | lcfr.h |
. . . . . . . . 9
⊢ 𝐻 = (LHyp‘𝐾) |
12 | | lcfr.u |
. . . . . . . . 9
⊢ 𝑈 = ((DVecH‘𝐾)‘𝑊) |
13 | 11, 12, 6 | dvhlmod 36399 |
. . . . . . . 8
⊢ (𝜑 → 𝑈 ∈ LMod) |
14 | 13 | adantr 481 |
. . . . . . 7
⊢ ((𝜑 ∧ ℎ ∈ 𝑅) → 𝑈 ∈ LMod) |
15 | | lcfr.r |
. . . . . . . . . 10
⊢ (𝜑 → 𝑅 ∈ 𝑇) |
16 | | eqid 2622 |
. . . . . . . . . . 11
⊢
(Base‘𝐷) =
(Base‘𝐷) |
17 | | lcfr.t |
. . . . . . . . . . 11
⊢ 𝑇 = (LSubSp‘𝐷) |
18 | 16, 17 | lssss 18937 |
. . . . . . . . . 10
⊢ (𝑅 ∈ 𝑇 → 𝑅 ⊆ (Base‘𝐷)) |
19 | 15, 18 | syl 17 |
. . . . . . . . 9
⊢ (𝜑 → 𝑅 ⊆ (Base‘𝐷)) |
20 | | lcfr.d |
. . . . . . . . . 10
⊢ 𝐷 = (LDual‘𝑈) |
21 | 9, 20, 16, 13 | ldualvbase 34413 |
. . . . . . . . 9
⊢ (𝜑 → (Base‘𝐷) = 𝐹) |
22 | 19, 21 | sseqtrd 3641 |
. . . . . . . 8
⊢ (𝜑 → 𝑅 ⊆ 𝐹) |
23 | 22 | sselda 3603 |
. . . . . . 7
⊢ ((𝜑 ∧ ℎ ∈ 𝑅) → ℎ ∈ 𝐹) |
24 | 8, 9, 10, 14, 23 | lkrssv 34383 |
. . . . . 6
⊢ ((𝜑 ∧ ℎ ∈ 𝑅) → (𝐿‘ℎ) ⊆ (Base‘𝑈)) |
25 | | lcfr.o |
. . . . . . 7
⊢ ⊥ =
((ocH‘𝐾)‘𝑊) |
26 | 11, 12, 8, 25 | dochssv 36644 |
. . . . . 6
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝐿‘ℎ) ⊆ (Base‘𝑈)) → ( ⊥ ‘(𝐿‘ℎ)) ⊆ (Base‘𝑈)) |
27 | 7, 24, 26 | syl2anc 693 |
. . . . 5
⊢ ((𝜑 ∧ ℎ ∈ 𝑅) → ( ⊥ ‘(𝐿‘ℎ)) ⊆ (Base‘𝑈)) |
28 | 27 | ralrimiva 2966 |
. . . 4
⊢ (𝜑 → ∀ℎ ∈ 𝑅 ( ⊥ ‘(𝐿‘ℎ)) ⊆ (Base‘𝑈)) |
29 | | iunss 4561 |
. . . 4
⊢ (∪ ℎ
∈ 𝑅 ( ⊥
‘(𝐿‘ℎ)) ⊆ (Base‘𝑈) ↔ ∀ℎ ∈ 𝑅 ( ⊥ ‘(𝐿‘ℎ)) ⊆ (Base‘𝑈)) |
30 | 28, 29 | sylibr 224 |
. . 3
⊢ (𝜑 → ∪ ℎ
∈ 𝑅 ( ⊥
‘(𝐿‘ℎ)) ⊆ (Base‘𝑈)) |
31 | 5, 30 | syl5eqss 3649 |
. 2
⊢ (𝜑 → 𝑄 ⊆ (Base‘𝑈)) |
32 | 5 | a1i 11 |
. . 3
⊢ (𝜑 → 𝑄 = ∪ ℎ ∈ 𝑅 ( ⊥ ‘(𝐿‘ℎ))) |
33 | 20, 13 | lduallmod 34440 |
. . . . . . 7
⊢ (𝜑 → 𝐷 ∈ LMod) |
34 | | eqid 2622 |
. . . . . . . 8
⊢
(0g‘𝐷) = (0g‘𝐷) |
35 | 34, 17 | lss0cl 18947 |
. . . . . . 7
⊢ ((𝐷 ∈ LMod ∧ 𝑅 ∈ 𝑇) → (0g‘𝐷) ∈ 𝑅) |
36 | 33, 15, 35 | syl2anc 693 |
. . . . . 6
⊢ (𝜑 → (0g‘𝐷) ∈ 𝑅) |
37 | 9, 20, 34, 13 | ldual0vcl 34438 |
. . . . . . . . 9
⊢ (𝜑 → (0g‘𝐷) ∈ 𝐹) |
38 | 8, 9, 10, 13, 37 | lkrssv 34383 |
. . . . . . . 8
⊢ (𝜑 → (𝐿‘(0g‘𝐷)) ⊆ (Base‘𝑈)) |
39 | | lcfr.s |
. . . . . . . . 9
⊢ 𝑆 = (LSubSp‘𝑈) |
40 | 11, 12, 8, 39, 25 | dochlss 36643 |
. . . . . . . 8
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝐿‘(0g‘𝐷)) ⊆ (Base‘𝑈)) → ( ⊥ ‘(𝐿‘(0g‘𝐷))) ∈ 𝑆) |
41 | 6, 38, 40 | syl2anc 693 |
. . . . . . 7
⊢ (𝜑 → ( ⊥ ‘(𝐿‘(0g‘𝐷))) ∈ 𝑆) |
42 | | eqid 2622 |
. . . . . . . 8
⊢
(0g‘𝑈) = (0g‘𝑈) |
43 | 42, 39 | lss0cl 18947 |
. . . . . . 7
⊢ ((𝑈 ∈ LMod ∧ ( ⊥
‘(𝐿‘(0g‘𝐷))) ∈ 𝑆) → (0g‘𝑈) ∈ ( ⊥ ‘(𝐿‘(0g‘𝐷)))) |
44 | 13, 41, 43 | syl2anc 693 |
. . . . . 6
⊢ (𝜑 → (0g‘𝑈) ∈ ( ⊥ ‘(𝐿‘(0g‘𝐷)))) |
45 | | fveq2 6191 |
. . . . . . . . 9
⊢ (ℎ = (0g‘𝐷) → (𝐿‘ℎ) = (𝐿‘(0g‘𝐷))) |
46 | 45 | fveq2d 6195 |
. . . . . . . 8
⊢ (ℎ = (0g‘𝐷) → ( ⊥ ‘(𝐿‘ℎ)) = ( ⊥ ‘(𝐿‘(0g‘𝐷)))) |
47 | 46 | eleq2d 2687 |
. . . . . . 7
⊢ (ℎ = (0g‘𝐷) →
((0g‘𝑈)
∈ ( ⊥ ‘(𝐿‘ℎ)) ↔ (0g‘𝑈) ∈ ( ⊥ ‘(𝐿‘(0g‘𝐷))))) |
48 | 47 | rspcev 3309 |
. . . . . 6
⊢
(((0g‘𝐷) ∈ 𝑅 ∧ (0g‘𝑈) ∈ ( ⊥ ‘(𝐿‘(0g‘𝐷)))) → ∃ℎ ∈ 𝑅 (0g‘𝑈) ∈ ( ⊥ ‘(𝐿‘ℎ))) |
49 | 36, 44, 48 | syl2anc 693 |
. . . . 5
⊢ (𝜑 → ∃ℎ ∈ 𝑅 (0g‘𝑈) ∈ ( ⊥ ‘(𝐿‘ℎ))) |
50 | | eliun 4524 |
. . . . 5
⊢
((0g‘𝑈) ∈ ∪
ℎ ∈ 𝑅 ( ⊥ ‘(𝐿‘ℎ)) ↔ ∃ℎ ∈ 𝑅 (0g‘𝑈) ∈ ( ⊥ ‘(𝐿‘ℎ))) |
51 | 49, 50 | sylibr 224 |
. . . 4
⊢ (𝜑 → (0g‘𝑈) ∈ ∪ ℎ
∈ 𝑅 ( ⊥
‘(𝐿‘ℎ))) |
52 | | ne0i 3921 |
. . . 4
⊢
((0g‘𝑈) ∈ ∪
ℎ ∈ 𝑅 ( ⊥ ‘(𝐿‘ℎ)) → ∪
ℎ ∈ 𝑅 ( ⊥ ‘(𝐿‘ℎ)) ≠ ∅) |
53 | 51, 52 | syl 17 |
. . 3
⊢ (𝜑 → ∪ ℎ
∈ 𝑅 ( ⊥
‘(𝐿‘ℎ)) ≠ ∅) |
54 | 32, 53 | eqnetrd 2861 |
. 2
⊢ (𝜑 → 𝑄 ≠ ∅) |
55 | | eqid 2622 |
. . . 4
⊢
(+g‘𝑈) = (+g‘𝑈) |
56 | | lcfr.c |
. . . . 5
⊢ 𝐶 = {𝑓 ∈ 𝐹 ∣ ( ⊥ ‘( ⊥
‘(𝐿‘𝑓))) = (𝐿‘𝑓)} |
57 | | rabeq 3192 |
. . . . . 6
⊢ (𝐹 = (LFnl‘𝑈) → {𝑓 ∈ 𝐹 ∣ ( ⊥ ‘( ⊥
‘(𝐿‘𝑓))) = (𝐿‘𝑓)} = {𝑓 ∈ (LFnl‘𝑈) ∣ ( ⊥ ‘( ⊥
‘(𝐿‘𝑓))) = (𝐿‘𝑓)}) |
58 | 9, 57 | ax-mp 5 |
. . . . 5
⊢ {𝑓 ∈ 𝐹 ∣ ( ⊥ ‘( ⊥
‘(𝐿‘𝑓))) = (𝐿‘𝑓)} = {𝑓 ∈ (LFnl‘𝑈) ∣ ( ⊥ ‘( ⊥
‘(𝐿‘𝑓))) = (𝐿‘𝑓)} |
59 | 56, 58 | eqtri 2644 |
. . . 4
⊢ 𝐶 = {𝑓 ∈ (LFnl‘𝑈) ∣ ( ⊥ ‘( ⊥
‘(𝐿‘𝑓))) = (𝐿‘𝑓)} |
60 | 6 | adantr 481 |
. . . 4
⊢ ((𝜑 ∧ (𝑥 ∈ (Base‘(Scalar‘𝑈)) ∧ 𝑎 ∈ 𝑄 ∧ 𝑏 ∈ 𝑄)) → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻)) |
61 | 15 | adantr 481 |
. . . 4
⊢ ((𝜑 ∧ (𝑥 ∈ (Base‘(Scalar‘𝑈)) ∧ 𝑎 ∈ 𝑄 ∧ 𝑏 ∈ 𝑄)) → 𝑅 ∈ 𝑇) |
62 | | lcfr.rs |
. . . . 5
⊢ (𝜑 → 𝑅 ⊆ 𝐶) |
63 | 62 | adantr 481 |
. . . 4
⊢ ((𝜑 ∧ (𝑥 ∈ (Base‘(Scalar‘𝑈)) ∧ 𝑎 ∈ 𝑄 ∧ 𝑏 ∈ 𝑄)) → 𝑅 ⊆ 𝐶) |
64 | | simpr2 1068 |
. . . . 5
⊢ ((𝜑 ∧ (𝑥 ∈ (Base‘(Scalar‘𝑈)) ∧ 𝑎 ∈ 𝑄 ∧ 𝑏 ∈ 𝑄)) → 𝑎 ∈ 𝑄) |
65 | | eqid 2622 |
. . . . 5
⊢
(Scalar‘𝑈) =
(Scalar‘𝑈) |
66 | | eqid 2622 |
. . . . 5
⊢
(Base‘(Scalar‘𝑈)) = (Base‘(Scalar‘𝑈)) |
67 | | eqid 2622 |
. . . . 5
⊢ (
·𝑠 ‘𝑈) = ( ·𝑠
‘𝑈) |
68 | | simpr1 1067 |
. . . . 5
⊢ ((𝜑 ∧ (𝑥 ∈ (Base‘(Scalar‘𝑈)) ∧ 𝑎 ∈ 𝑄 ∧ 𝑏 ∈ 𝑄)) → 𝑥 ∈ (Base‘(Scalar‘𝑈))) |
69 | 11, 25, 12, 8, 9, 10, 20, 17, 60, 61, 5, 64, 65, 66, 67, 68 | lcfrlem5 36835 |
. . . 4
⊢ ((𝜑 ∧ (𝑥 ∈ (Base‘(Scalar‘𝑈)) ∧ 𝑎 ∈ 𝑄 ∧ 𝑏 ∈ 𝑄)) → (𝑥( ·𝑠
‘𝑈)𝑎) ∈ 𝑄) |
70 | | simpr3 1069 |
. . . 4
⊢ ((𝜑 ∧ (𝑥 ∈ (Base‘(Scalar‘𝑈)) ∧ 𝑎 ∈ 𝑄 ∧ 𝑏 ∈ 𝑄)) → 𝑏 ∈ 𝑄) |
71 | 11, 25, 12, 55, 9, 10, 20, 17, 59, 5, 60, 61, 63, 69, 70 | lcfrlem42 36873 |
. . 3
⊢ ((𝜑 ∧ (𝑥 ∈ (Base‘(Scalar‘𝑈)) ∧ 𝑎 ∈ 𝑄 ∧ 𝑏 ∈ 𝑄)) → ((𝑥( ·𝑠
‘𝑈)𝑎)(+g‘𝑈)𝑏) ∈ 𝑄) |
72 | 71 | ralrimivvva 2972 |
. 2
⊢ (𝜑 → ∀𝑥 ∈ (Base‘(Scalar‘𝑈))∀𝑎 ∈ 𝑄 ∀𝑏 ∈ 𝑄 ((𝑥( ·𝑠
‘𝑈)𝑎)(+g‘𝑈)𝑏) ∈ 𝑄) |
73 | 65, 66, 8, 55, 67, 39 | islss 18935 |
. 2
⊢ (𝑄 ∈ 𝑆 ↔ (𝑄 ⊆ (Base‘𝑈) ∧ 𝑄 ≠ ∅ ∧ ∀𝑥 ∈
(Base‘(Scalar‘𝑈))∀𝑎 ∈ 𝑄 ∀𝑏 ∈ 𝑄 ((𝑥( ·𝑠
‘𝑈)𝑎)(+g‘𝑈)𝑏) ∈ 𝑄)) |
74 | 31, 54, 72, 73 | syl3anbrc 1246 |
1
⊢ (𝜑 → 𝑄 ∈ 𝑆) |