Proof of Theorem lclkrslem2
Step | Hyp | Ref
| Expression |
1 | | lclkrslem1.h |
. . 3
⊢ 𝐻 = (LHyp‘𝐾) |
2 | | lclkrslem1.o |
. . 3
⊢ ⊥ =
((ocH‘𝐾)‘𝑊) |
3 | | lclkrslem1.u |
. . 3
⊢ 𝑈 = ((DVecH‘𝐾)‘𝑊) |
4 | | lclkrslem1.f |
. . 3
⊢ 𝐹 = (LFnl‘𝑈) |
5 | | lclkrslem1.l |
. . 3
⊢ 𝐿 = (LKer‘𝑈) |
6 | | lclkrslem1.d |
. . 3
⊢ 𝐷 = (LDual‘𝑈) |
7 | | lclkrslem2.p |
. . 3
⊢ + =
(+g‘𝐷) |
8 | | eqid 2738 |
. . 3
⊢ {𝑓 ∈ 𝐹 ∣ ( ⊥ ‘( ⊥
‘(𝐿‘𝑓))) = (𝐿‘𝑓)} = {𝑓 ∈ 𝐹 ∣ ( ⊥ ‘( ⊥
‘(𝐿‘𝑓))) = (𝐿‘𝑓)} |
9 | | lclkrslem1.k |
. . 3
⊢ (𝜑 → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻)) |
10 | | lclkrslem2.e |
. . . 4
⊢ (𝜑 → 𝐸 ∈ 𝐶) |
11 | | lclkrslem1.c |
. . . . . 6
⊢ 𝐶 = {𝑓 ∈ 𝐹 ∣ (( ⊥ ‘( ⊥
‘(𝐿‘𝑓))) = (𝐿‘𝑓) ∧ ( ⊥ ‘(𝐿‘𝑓)) ⊆ 𝑄)} |
12 | 11, 8 | lcfls1c 39550 |
. . . . 5
⊢ (𝐸 ∈ 𝐶 ↔ (𝐸 ∈ {𝑓 ∈ 𝐹 ∣ ( ⊥ ‘( ⊥
‘(𝐿‘𝑓))) = (𝐿‘𝑓)} ∧ ( ⊥ ‘(𝐿‘𝐸)) ⊆ 𝑄)) |
13 | 12 | simplbi 498 |
. . . 4
⊢ (𝐸 ∈ 𝐶 → 𝐸 ∈ {𝑓 ∈ 𝐹 ∣ ( ⊥ ‘( ⊥
‘(𝐿‘𝑓))) = (𝐿‘𝑓)}) |
14 | 10, 13 | syl 17 |
. . 3
⊢ (𝜑 → 𝐸 ∈ {𝑓 ∈ 𝐹 ∣ ( ⊥ ‘( ⊥
‘(𝐿‘𝑓))) = (𝐿‘𝑓)}) |
15 | | lclkrslem1.g |
. . . 4
⊢ (𝜑 → 𝐺 ∈ 𝐶) |
16 | 11, 8 | lcfls1c 39550 |
. . . . 5
⊢ (𝐺 ∈ 𝐶 ↔ (𝐺 ∈ {𝑓 ∈ 𝐹 ∣ ( ⊥ ‘( ⊥
‘(𝐿‘𝑓))) = (𝐿‘𝑓)} ∧ ( ⊥ ‘(𝐿‘𝐺)) ⊆ 𝑄)) |
17 | 16 | simplbi 498 |
. . . 4
⊢ (𝐺 ∈ 𝐶 → 𝐺 ∈ {𝑓 ∈ 𝐹 ∣ ( ⊥ ‘( ⊥
‘(𝐿‘𝑓))) = (𝐿‘𝑓)}) |
18 | 15, 17 | syl 17 |
. . 3
⊢ (𝜑 → 𝐺 ∈ {𝑓 ∈ 𝐹 ∣ ( ⊥ ‘( ⊥
‘(𝐿‘𝑓))) = (𝐿‘𝑓)}) |
19 | 1, 2, 3, 4, 5, 6, 7, 8, 9, 14,
18 | lclkrlem2 39546 |
. 2
⊢ (𝜑 → (𝐸 + 𝐺) ∈ {𝑓 ∈ 𝐹 ∣ ( ⊥ ‘( ⊥
‘(𝐿‘𝑓))) = (𝐿‘𝑓)}) |
20 | | eqid 2738 |
. . . . 5
⊢
(Base‘𝑈) =
(Base‘𝑈) |
21 | 1, 3, 9 | dvhlmod 39124 |
. . . . 5
⊢ (𝜑 → 𝑈 ∈ LMod) |
22 | 11 | lcfls1lem 39548 |
. . . . . . . 8
⊢ (𝐸 ∈ 𝐶 ↔ (𝐸 ∈ 𝐹 ∧ ( ⊥ ‘( ⊥
‘(𝐿‘𝐸))) = (𝐿‘𝐸) ∧ ( ⊥ ‘(𝐿‘𝐸)) ⊆ 𝑄)) |
23 | 10, 22 | sylib 217 |
. . . . . . 7
⊢ (𝜑 → (𝐸 ∈ 𝐹 ∧ ( ⊥ ‘( ⊥
‘(𝐿‘𝐸))) = (𝐿‘𝐸) ∧ ( ⊥ ‘(𝐿‘𝐸)) ⊆ 𝑄)) |
24 | 23 | simp1d 1141 |
. . . . . 6
⊢ (𝜑 → 𝐸 ∈ 𝐹) |
25 | 11 | lcfls1lem 39548 |
. . . . . . . 8
⊢ (𝐺 ∈ 𝐶 ↔ (𝐺 ∈ 𝐹 ∧ ( ⊥ ‘( ⊥
‘(𝐿‘𝐺))) = (𝐿‘𝐺) ∧ ( ⊥ ‘(𝐿‘𝐺)) ⊆ 𝑄)) |
26 | 15, 25 | sylib 217 |
. . . . . . 7
⊢ (𝜑 → (𝐺 ∈ 𝐹 ∧ ( ⊥ ‘( ⊥
‘(𝐿‘𝐺))) = (𝐿‘𝐺) ∧ ( ⊥ ‘(𝐿‘𝐺)) ⊆ 𝑄)) |
27 | 26 | simp1d 1141 |
. . . . . 6
⊢ (𝜑 → 𝐺 ∈ 𝐹) |
28 | 4, 6, 7, 21, 24, 27 | ldualvaddcl 37144 |
. . . . 5
⊢ (𝜑 → (𝐸 + 𝐺) ∈ 𝐹) |
29 | 20, 4, 5, 21, 28 | lkrssv 37110 |
. . . 4
⊢ (𝜑 → (𝐿‘(𝐸 + 𝐺)) ⊆ (Base‘𝑈)) |
30 | 4, 5, 6, 7, 21, 24, 27 | lkrin 37178 |
. . . 4
⊢ (𝜑 → ((𝐿‘𝐸) ∩ (𝐿‘𝐺)) ⊆ (𝐿‘(𝐸 + 𝐺))) |
31 | 1, 3, 20, 2 | dochss 39379 |
. . . 4
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝐿‘(𝐸 + 𝐺)) ⊆ (Base‘𝑈) ∧ ((𝐿‘𝐸) ∩ (𝐿‘𝐺)) ⊆ (𝐿‘(𝐸 + 𝐺))) → ( ⊥ ‘(𝐿‘(𝐸 + 𝐺))) ⊆ ( ⊥ ‘((𝐿‘𝐸) ∩ (𝐿‘𝐺)))) |
32 | 9, 29, 30, 31 | syl3anc 1370 |
. . 3
⊢ (𝜑 → ( ⊥ ‘(𝐿‘(𝐸 + 𝐺))) ⊆ ( ⊥ ‘((𝐿‘𝐸) ∩ (𝐿‘𝐺)))) |
33 | | eqid 2738 |
. . . . . 6
⊢
((DIsoH‘𝐾)‘𝑊) = ((DIsoH‘𝐾)‘𝑊) |
34 | | eqid 2738 |
. . . . . 6
⊢
((joinH‘𝐾)‘𝑊) = ((joinH‘𝐾)‘𝑊) |
35 | 23 | simp2d 1142 |
. . . . . . 7
⊢ (𝜑 → ( ⊥ ‘( ⊥
‘(𝐿‘𝐸))) = (𝐿‘𝐸)) |
36 | 1, 33, 2, 3, 4, 5, 9, 24 | lcfl5a 39511 |
. . . . . . 7
⊢ (𝜑 → (( ⊥ ‘( ⊥
‘(𝐿‘𝐸))) = (𝐿‘𝐸) ↔ (𝐿‘𝐸) ∈ ran ((DIsoH‘𝐾)‘𝑊))) |
37 | 35, 36 | mpbid 231 |
. . . . . 6
⊢ (𝜑 → (𝐿‘𝐸) ∈ ran ((DIsoH‘𝐾)‘𝑊)) |
38 | 26 | simp2d 1142 |
. . . . . . 7
⊢ (𝜑 → ( ⊥ ‘( ⊥
‘(𝐿‘𝐺))) = (𝐿‘𝐺)) |
39 | 1, 33, 2, 3, 4, 5, 9, 27 | lcfl5a 39511 |
. . . . . . 7
⊢ (𝜑 → (( ⊥ ‘( ⊥
‘(𝐿‘𝐺))) = (𝐿‘𝐺) ↔ (𝐿‘𝐺) ∈ ran ((DIsoH‘𝐾)‘𝑊))) |
40 | 38, 39 | mpbid 231 |
. . . . . 6
⊢ (𝜑 → (𝐿‘𝐺) ∈ ran ((DIsoH‘𝐾)‘𝑊)) |
41 | 1, 33, 3, 20, 2, 34, 9, 37, 40 | dochdmm1 39424 |
. . . . 5
⊢ (𝜑 → ( ⊥ ‘((𝐿‘𝐸) ∩ (𝐿‘𝐺))) = (( ⊥ ‘(𝐿‘𝐸))((joinH‘𝐾)‘𝑊)( ⊥ ‘(𝐿‘𝐺)))) |
42 | | eqid 2738 |
. . . . . . 7
⊢
(LSSum‘𝑈) =
(LSSum‘𝑈) |
43 | 20, 4, 5, 21, 24 | lkrssv 37110 |
. . . . . . . 8
⊢ (𝜑 → (𝐿‘𝐸) ⊆ (Base‘𝑈)) |
44 | 1, 33, 3, 20, 2 | dochcl 39367 |
. . . . . . . 8
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝐿‘𝐸) ⊆ (Base‘𝑈)) → ( ⊥ ‘(𝐿‘𝐸)) ∈ ran ((DIsoH‘𝐾)‘𝑊)) |
45 | 9, 43, 44 | syl2anc 584 |
. . . . . . 7
⊢ (𝜑 → ( ⊥ ‘(𝐿‘𝐸)) ∈ ran ((DIsoH‘𝐾)‘𝑊)) |
46 | 1, 33, 2, 3, 42, 4,
5, 9, 45, 27 | dochkrsm 39472 |
. . . . . 6
⊢ (𝜑 → (( ⊥ ‘(𝐿‘𝐸))(LSSum‘𝑈)( ⊥ ‘(𝐿‘𝐺))) ∈ ran ((DIsoH‘𝐾)‘𝑊)) |
47 | | lclkrslem1.s |
. . . . . . 7
⊢ 𝑆 = (LSubSp‘𝑈) |
48 | 1, 3, 20, 47, 2 | dochlss 39368 |
. . . . . . . 8
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝐿‘𝐸) ⊆ (Base‘𝑈)) → ( ⊥ ‘(𝐿‘𝐸)) ∈ 𝑆) |
49 | 9, 43, 48 | syl2anc 584 |
. . . . . . 7
⊢ (𝜑 → ( ⊥ ‘(𝐿‘𝐸)) ∈ 𝑆) |
50 | 20, 4, 5, 21, 27 | lkrssv 37110 |
. . . . . . . 8
⊢ (𝜑 → (𝐿‘𝐺) ⊆ (Base‘𝑈)) |
51 | 1, 3, 20, 47, 2 | dochlss 39368 |
. . . . . . . 8
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝐿‘𝐺) ⊆ (Base‘𝑈)) → ( ⊥ ‘(𝐿‘𝐺)) ∈ 𝑆) |
52 | 9, 50, 51 | syl2anc 584 |
. . . . . . 7
⊢ (𝜑 → ( ⊥ ‘(𝐿‘𝐺)) ∈ 𝑆) |
53 | 1, 3, 20, 47, 42, 33, 34, 9, 49, 52 | djhlsmcl 39428 |
. . . . . 6
⊢ (𝜑 → ((( ⊥ ‘(𝐿‘𝐸))(LSSum‘𝑈)( ⊥ ‘(𝐿‘𝐺))) ∈ ran ((DIsoH‘𝐾)‘𝑊) ↔ (( ⊥ ‘(𝐿‘𝐸))(LSSum‘𝑈)( ⊥ ‘(𝐿‘𝐺))) = (( ⊥ ‘(𝐿‘𝐸))((joinH‘𝐾)‘𝑊)( ⊥ ‘(𝐿‘𝐺))))) |
54 | 46, 53 | mpbid 231 |
. . . . 5
⊢ (𝜑 → (( ⊥ ‘(𝐿‘𝐸))(LSSum‘𝑈)( ⊥ ‘(𝐿‘𝐺))) = (( ⊥ ‘(𝐿‘𝐸))((joinH‘𝐾)‘𝑊)( ⊥ ‘(𝐿‘𝐺)))) |
55 | 41, 54 | eqtr4d 2781 |
. . . 4
⊢ (𝜑 → ( ⊥ ‘((𝐿‘𝐸) ∩ (𝐿‘𝐺))) = (( ⊥ ‘(𝐿‘𝐸))(LSSum‘𝑈)( ⊥ ‘(𝐿‘𝐺)))) |
56 | 23 | simp3d 1143 |
. . . . 5
⊢ (𝜑 → ( ⊥ ‘(𝐿‘𝐸)) ⊆ 𝑄) |
57 | 26 | simp3d 1143 |
. . . . 5
⊢ (𝜑 → ( ⊥ ‘(𝐿‘𝐺)) ⊆ 𝑄) |
58 | 47 | lsssssubg 20220 |
. . . . . . . 8
⊢ (𝑈 ∈ LMod → 𝑆 ⊆ (SubGrp‘𝑈)) |
59 | 21, 58 | syl 17 |
. . . . . . 7
⊢ (𝜑 → 𝑆 ⊆ (SubGrp‘𝑈)) |
60 | 59, 49 | sseldd 3922 |
. . . . . 6
⊢ (𝜑 → ( ⊥ ‘(𝐿‘𝐸)) ∈ (SubGrp‘𝑈)) |
61 | 59, 52 | sseldd 3922 |
. . . . . 6
⊢ (𝜑 → ( ⊥ ‘(𝐿‘𝐺)) ∈ (SubGrp‘𝑈)) |
62 | | lclkrslem1.q |
. . . . . . 7
⊢ (𝜑 → 𝑄 ∈ 𝑆) |
63 | 59, 62 | sseldd 3922 |
. . . . . 6
⊢ (𝜑 → 𝑄 ∈ (SubGrp‘𝑈)) |
64 | 42 | lsmlub 19270 |
. . . . . 6
⊢ ((( ⊥
‘(𝐿‘𝐸)) ∈ (SubGrp‘𝑈) ∧ ( ⊥ ‘(𝐿‘𝐺)) ∈ (SubGrp‘𝑈) ∧ 𝑄 ∈ (SubGrp‘𝑈)) → ((( ⊥ ‘(𝐿‘𝐸)) ⊆ 𝑄 ∧ ( ⊥ ‘(𝐿‘𝐺)) ⊆ 𝑄) ↔ (( ⊥ ‘(𝐿‘𝐸))(LSSum‘𝑈)( ⊥ ‘(𝐿‘𝐺))) ⊆ 𝑄)) |
65 | 60, 61, 63, 64 | syl3anc 1370 |
. . . . 5
⊢ (𝜑 → ((( ⊥ ‘(𝐿‘𝐸)) ⊆ 𝑄 ∧ ( ⊥ ‘(𝐿‘𝐺)) ⊆ 𝑄) ↔ (( ⊥ ‘(𝐿‘𝐸))(LSSum‘𝑈)( ⊥ ‘(𝐿‘𝐺))) ⊆ 𝑄)) |
66 | 56, 57, 65 | mpbi2and 709 |
. . . 4
⊢ (𝜑 → (( ⊥ ‘(𝐿‘𝐸))(LSSum‘𝑈)( ⊥ ‘(𝐿‘𝐺))) ⊆ 𝑄) |
67 | 55, 66 | eqsstrd 3959 |
. . 3
⊢ (𝜑 → ( ⊥ ‘((𝐿‘𝐸) ∩ (𝐿‘𝐺))) ⊆ 𝑄) |
68 | 32, 67 | sstrd 3931 |
. 2
⊢ (𝜑 → ( ⊥ ‘(𝐿‘(𝐸 + 𝐺))) ⊆ 𝑄) |
69 | 11, 8 | lcfls1c 39550 |
. 2
⊢ ((𝐸 + 𝐺) ∈ 𝐶 ↔ ((𝐸 + 𝐺) ∈ {𝑓 ∈ 𝐹 ∣ ( ⊥ ‘( ⊥
‘(𝐿‘𝑓))) = (𝐿‘𝑓)} ∧ ( ⊥ ‘(𝐿‘(𝐸 + 𝐺))) ⊆ 𝑄)) |
70 | 19, 68, 69 | sylanbrc 583 |
1
⊢ (𝜑 → (𝐸 + 𝐺) ∈ 𝐶) |