Step | Hyp | Ref
| Expression |
1 | | lcfr.q |
. . . 4
⊢ 𝑄 = ∪ 𝑔 ∈ 𝑅 ( ⊥ ‘(𝐿‘𝑔)) |
2 | | 2fveq3 6773 |
. . . . 5
⊢ (𝑔 = ℎ → ( ⊥ ‘(𝐿‘𝑔)) = ( ⊥ ‘(𝐿‘ℎ))) |
3 | 2 | cbviunv 4974 |
. . . 4
⊢ ∪ 𝑔 ∈ 𝑅 ( ⊥ ‘(𝐿‘𝑔)) = ∪
ℎ ∈ 𝑅 ( ⊥ ‘(𝐿‘ℎ)) |
4 | 1, 3 | eqtri 2767 |
. . 3
⊢ 𝑄 = ∪ ℎ
∈ 𝑅 ( ⊥
‘(𝐿‘ℎ)) |
5 | | lcfr.k |
. . . . . . 7
⊢ (𝜑 → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻)) |
6 | 5 | adantr 480 |
. . . . . 6
⊢ ((𝜑 ∧ ℎ ∈ 𝑅) → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻)) |
7 | | eqid 2739 |
. . . . . . 7
⊢
(Base‘𝑈) =
(Base‘𝑈) |
8 | | lcfr.f |
. . . . . . 7
⊢ 𝐹 = (LFnl‘𝑈) |
9 | | lcfr.l |
. . . . . . 7
⊢ 𝐿 = (LKer‘𝑈) |
10 | | lcfr.h |
. . . . . . . . 9
⊢ 𝐻 = (LHyp‘𝐾) |
11 | | lcfr.u |
. . . . . . . . 9
⊢ 𝑈 = ((DVecH‘𝐾)‘𝑊) |
12 | 10, 11, 5 | dvhlmod 39103 |
. . . . . . . 8
⊢ (𝜑 → 𝑈 ∈ LMod) |
13 | 12 | adantr 480 |
. . . . . . 7
⊢ ((𝜑 ∧ ℎ ∈ 𝑅) → 𝑈 ∈ LMod) |
14 | | lcfr.r |
. . . . . . . . . 10
⊢ (𝜑 → 𝑅 ∈ 𝑇) |
15 | | eqid 2739 |
. . . . . . . . . . 11
⊢
(Base‘𝐷) =
(Base‘𝐷) |
16 | | lcfr.t |
. . . . . . . . . . 11
⊢ 𝑇 = (LSubSp‘𝐷) |
17 | 15, 16 | lssss 20179 |
. . . . . . . . . 10
⊢ (𝑅 ∈ 𝑇 → 𝑅 ⊆ (Base‘𝐷)) |
18 | 14, 17 | syl 17 |
. . . . . . . . 9
⊢ (𝜑 → 𝑅 ⊆ (Base‘𝐷)) |
19 | | lcfr.d |
. . . . . . . . . 10
⊢ 𝐷 = (LDual‘𝑈) |
20 | 8, 19, 15, 12 | ldualvbase 37119 |
. . . . . . . . 9
⊢ (𝜑 → (Base‘𝐷) = 𝐹) |
21 | 18, 20 | sseqtrd 3965 |
. . . . . . . 8
⊢ (𝜑 → 𝑅 ⊆ 𝐹) |
22 | 21 | sselda 3925 |
. . . . . . 7
⊢ ((𝜑 ∧ ℎ ∈ 𝑅) → ℎ ∈ 𝐹) |
23 | 7, 8, 9, 13, 22 | lkrssv 37089 |
. . . . . 6
⊢ ((𝜑 ∧ ℎ ∈ 𝑅) → (𝐿‘ℎ) ⊆ (Base‘𝑈)) |
24 | | lcfr.o |
. . . . . . 7
⊢ ⊥ =
((ocH‘𝐾)‘𝑊) |
25 | 10, 11, 7, 24 | dochssv 39348 |
. . . . . 6
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝐿‘ℎ) ⊆ (Base‘𝑈)) → ( ⊥ ‘(𝐿‘ℎ)) ⊆ (Base‘𝑈)) |
26 | 6, 23, 25 | syl2anc 583 |
. . . . 5
⊢ ((𝜑 ∧ ℎ ∈ 𝑅) → ( ⊥ ‘(𝐿‘ℎ)) ⊆ (Base‘𝑈)) |
27 | 26 | ralrimiva 3109 |
. . . 4
⊢ (𝜑 → ∀ℎ ∈ 𝑅 ( ⊥ ‘(𝐿‘ℎ)) ⊆ (Base‘𝑈)) |
28 | | iunss 4979 |
. . . 4
⊢ (∪ ℎ
∈ 𝑅 ( ⊥
‘(𝐿‘ℎ)) ⊆ (Base‘𝑈) ↔ ∀ℎ ∈ 𝑅 ( ⊥ ‘(𝐿‘ℎ)) ⊆ (Base‘𝑈)) |
29 | 27, 28 | sylibr 233 |
. . 3
⊢ (𝜑 → ∪ ℎ
∈ 𝑅 ( ⊥
‘(𝐿‘ℎ)) ⊆ (Base‘𝑈)) |
30 | 4, 29 | eqsstrid 3973 |
. 2
⊢ (𝜑 → 𝑄 ⊆ (Base‘𝑈)) |
31 | 4 | a1i 11 |
. . 3
⊢ (𝜑 → 𝑄 = ∪ ℎ ∈ 𝑅 ( ⊥ ‘(𝐿‘ℎ))) |
32 | 19, 12 | lduallmod 37146 |
. . . . . . 7
⊢ (𝜑 → 𝐷 ∈ LMod) |
33 | | eqid 2739 |
. . . . . . . 8
⊢
(0g‘𝐷) = (0g‘𝐷) |
34 | 33, 16 | lss0cl 20189 |
. . . . . . 7
⊢ ((𝐷 ∈ LMod ∧ 𝑅 ∈ 𝑇) → (0g‘𝐷) ∈ 𝑅) |
35 | 32, 14, 34 | syl2anc 583 |
. . . . . 6
⊢ (𝜑 → (0g‘𝐷) ∈ 𝑅) |
36 | 8, 19, 33, 12 | ldual0vcl 37144 |
. . . . . . . . 9
⊢ (𝜑 → (0g‘𝐷) ∈ 𝐹) |
37 | 7, 8, 9, 12, 36 | lkrssv 37089 |
. . . . . . . 8
⊢ (𝜑 → (𝐿‘(0g‘𝐷)) ⊆ (Base‘𝑈)) |
38 | | lcfr.s |
. . . . . . . . 9
⊢ 𝑆 = (LSubSp‘𝑈) |
39 | 10, 11, 7, 38, 24 | dochlss 39347 |
. . . . . . . 8
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝐿‘(0g‘𝐷)) ⊆ (Base‘𝑈)) → ( ⊥ ‘(𝐿‘(0g‘𝐷))) ∈ 𝑆) |
40 | 5, 37, 39 | syl2anc 583 |
. . . . . . 7
⊢ (𝜑 → ( ⊥ ‘(𝐿‘(0g‘𝐷))) ∈ 𝑆) |
41 | | eqid 2739 |
. . . . . . . 8
⊢
(0g‘𝑈) = (0g‘𝑈) |
42 | 41, 38 | lss0cl 20189 |
. . . . . . 7
⊢ ((𝑈 ∈ LMod ∧ ( ⊥
‘(𝐿‘(0g‘𝐷))) ∈ 𝑆) → (0g‘𝑈) ∈ ( ⊥ ‘(𝐿‘(0g‘𝐷)))) |
43 | 12, 40, 42 | syl2anc 583 |
. . . . . 6
⊢ (𝜑 → (0g‘𝑈) ∈ ( ⊥ ‘(𝐿‘(0g‘𝐷)))) |
44 | | 2fveq3 6773 |
. . . . . . . 8
⊢ (ℎ = (0g‘𝐷) → ( ⊥ ‘(𝐿‘ℎ)) = ( ⊥ ‘(𝐿‘(0g‘𝐷)))) |
45 | 44 | eleq2d 2825 |
. . . . . . 7
⊢ (ℎ = (0g‘𝐷) →
((0g‘𝑈)
∈ ( ⊥ ‘(𝐿‘ℎ)) ↔ (0g‘𝑈) ∈ ( ⊥ ‘(𝐿‘(0g‘𝐷))))) |
46 | 45 | rspcev 3560 |
. . . . . 6
⊢
(((0g‘𝐷) ∈ 𝑅 ∧ (0g‘𝑈) ∈ ( ⊥ ‘(𝐿‘(0g‘𝐷)))) → ∃ℎ ∈ 𝑅 (0g‘𝑈) ∈ ( ⊥ ‘(𝐿‘ℎ))) |
47 | 35, 43, 46 | syl2anc 583 |
. . . . 5
⊢ (𝜑 → ∃ℎ ∈ 𝑅 (0g‘𝑈) ∈ ( ⊥ ‘(𝐿‘ℎ))) |
48 | | eliun 4933 |
. . . . 5
⊢
((0g‘𝑈) ∈ ∪
ℎ ∈ 𝑅 ( ⊥ ‘(𝐿‘ℎ)) ↔ ∃ℎ ∈ 𝑅 (0g‘𝑈) ∈ ( ⊥ ‘(𝐿‘ℎ))) |
49 | 47, 48 | sylibr 233 |
. . . 4
⊢ (𝜑 → (0g‘𝑈) ∈ ∪ ℎ
∈ 𝑅 ( ⊥
‘(𝐿‘ℎ))) |
50 | 49 | ne0d 4274 |
. . 3
⊢ (𝜑 → ∪ ℎ
∈ 𝑅 ( ⊥
‘(𝐿‘ℎ)) ≠ ∅) |
51 | 31, 50 | eqnetrd 3012 |
. 2
⊢ (𝜑 → 𝑄 ≠ ∅) |
52 | | eqid 2739 |
. . . 4
⊢
(+g‘𝑈) = (+g‘𝑈) |
53 | | lcfr.c |
. . . . 5
⊢ 𝐶 = {𝑓 ∈ 𝐹 ∣ ( ⊥ ‘( ⊥
‘(𝐿‘𝑓))) = (𝐿‘𝑓)} |
54 | | rabeq 3416 |
. . . . . 6
⊢ (𝐹 = (LFnl‘𝑈) → {𝑓 ∈ 𝐹 ∣ ( ⊥ ‘( ⊥
‘(𝐿‘𝑓))) = (𝐿‘𝑓)} = {𝑓 ∈ (LFnl‘𝑈) ∣ ( ⊥ ‘( ⊥
‘(𝐿‘𝑓))) = (𝐿‘𝑓)}) |
55 | 8, 54 | ax-mp 5 |
. . . . 5
⊢ {𝑓 ∈ 𝐹 ∣ ( ⊥ ‘( ⊥
‘(𝐿‘𝑓))) = (𝐿‘𝑓)} = {𝑓 ∈ (LFnl‘𝑈) ∣ ( ⊥ ‘( ⊥
‘(𝐿‘𝑓))) = (𝐿‘𝑓)} |
56 | 53, 55 | eqtri 2767 |
. . . 4
⊢ 𝐶 = {𝑓 ∈ (LFnl‘𝑈) ∣ ( ⊥ ‘( ⊥
‘(𝐿‘𝑓))) = (𝐿‘𝑓)} |
57 | 5 | adantr 480 |
. . . 4
⊢ ((𝜑 ∧ (𝑥 ∈ (Base‘(Scalar‘𝑈)) ∧ 𝑎 ∈ 𝑄 ∧ 𝑏 ∈ 𝑄)) → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻)) |
58 | 14 | adantr 480 |
. . . 4
⊢ ((𝜑 ∧ (𝑥 ∈ (Base‘(Scalar‘𝑈)) ∧ 𝑎 ∈ 𝑄 ∧ 𝑏 ∈ 𝑄)) → 𝑅 ∈ 𝑇) |
59 | | lcfr.rs |
. . . . 5
⊢ (𝜑 → 𝑅 ⊆ 𝐶) |
60 | 59 | adantr 480 |
. . . 4
⊢ ((𝜑 ∧ (𝑥 ∈ (Base‘(Scalar‘𝑈)) ∧ 𝑎 ∈ 𝑄 ∧ 𝑏 ∈ 𝑄)) → 𝑅 ⊆ 𝐶) |
61 | | simpr2 1193 |
. . . . 5
⊢ ((𝜑 ∧ (𝑥 ∈ (Base‘(Scalar‘𝑈)) ∧ 𝑎 ∈ 𝑄 ∧ 𝑏 ∈ 𝑄)) → 𝑎 ∈ 𝑄) |
62 | | eqid 2739 |
. . . . 5
⊢
(Scalar‘𝑈) =
(Scalar‘𝑈) |
63 | | eqid 2739 |
. . . . 5
⊢
(Base‘(Scalar‘𝑈)) = (Base‘(Scalar‘𝑈)) |
64 | | eqid 2739 |
. . . . 5
⊢ (
·𝑠 ‘𝑈) = ( ·𝑠
‘𝑈) |
65 | | simpr1 1192 |
. . . . 5
⊢ ((𝜑 ∧ (𝑥 ∈ (Base‘(Scalar‘𝑈)) ∧ 𝑎 ∈ 𝑄 ∧ 𝑏 ∈ 𝑄)) → 𝑥 ∈ (Base‘(Scalar‘𝑈))) |
66 | 10, 24, 11, 7, 8, 9,
19, 16, 57, 58, 4, 61, 62, 63, 64, 65 | lcfrlem5 39539 |
. . . 4
⊢ ((𝜑 ∧ (𝑥 ∈ (Base‘(Scalar‘𝑈)) ∧ 𝑎 ∈ 𝑄 ∧ 𝑏 ∈ 𝑄)) → (𝑥( ·𝑠
‘𝑈)𝑎) ∈ 𝑄) |
67 | | simpr3 1194 |
. . . 4
⊢ ((𝜑 ∧ (𝑥 ∈ (Base‘(Scalar‘𝑈)) ∧ 𝑎 ∈ 𝑄 ∧ 𝑏 ∈ 𝑄)) → 𝑏 ∈ 𝑄) |
68 | 10, 24, 11, 52, 8, 9, 19, 16, 56, 4, 57, 58, 60, 66, 67 | lcfrlem42 39577 |
. . 3
⊢ ((𝜑 ∧ (𝑥 ∈ (Base‘(Scalar‘𝑈)) ∧ 𝑎 ∈ 𝑄 ∧ 𝑏 ∈ 𝑄)) → ((𝑥( ·𝑠
‘𝑈)𝑎)(+g‘𝑈)𝑏) ∈ 𝑄) |
69 | 68 | ralrimivvva 3117 |
. 2
⊢ (𝜑 → ∀𝑥 ∈ (Base‘(Scalar‘𝑈))∀𝑎 ∈ 𝑄 ∀𝑏 ∈ 𝑄 ((𝑥( ·𝑠
‘𝑈)𝑎)(+g‘𝑈)𝑏) ∈ 𝑄) |
70 | 62, 63, 7, 52, 64, 38 | islss 20177 |
. 2
⊢ (𝑄 ∈ 𝑆 ↔ (𝑄 ⊆ (Base‘𝑈) ∧ 𝑄 ≠ ∅ ∧ ∀𝑥 ∈
(Base‘(Scalar‘𝑈))∀𝑎 ∈ 𝑄 ∀𝑏 ∈ 𝑄 ((𝑥( ·𝑠
‘𝑈)𝑎)(+g‘𝑈)𝑏) ∈ 𝑄)) |
71 | 30, 51, 69, 70 | syl3anbrc 1341 |
1
⊢ (𝜑 → 𝑄 ∈ 𝑆) |