Step |
Hyp |
Ref |
Expression |
1 |
|
lclkrslem1.h |
⊢ 𝐻 = ( LHyp ‘ 𝐾 ) |
2 |
|
lclkrslem1.o |
⊢ ⊥ = ( ( ocH ‘ 𝐾 ) ‘ 𝑊 ) |
3 |
|
lclkrslem1.u |
⊢ 𝑈 = ( ( DVecH ‘ 𝐾 ) ‘ 𝑊 ) |
4 |
|
lclkrslem1.s |
⊢ 𝑆 = ( LSubSp ‘ 𝑈 ) |
5 |
|
lclkrslem1.f |
⊢ 𝐹 = ( LFnl ‘ 𝑈 ) |
6 |
|
lclkrslem1.l |
⊢ 𝐿 = ( LKer ‘ 𝑈 ) |
7 |
|
lclkrslem1.d |
⊢ 𝐷 = ( LDual ‘ 𝑈 ) |
8 |
|
lclkrslem1.r |
⊢ 𝑅 = ( Scalar ‘ 𝑈 ) |
9 |
|
lclkrslem1.b |
⊢ 𝐵 = ( Base ‘ 𝑅 ) |
10 |
|
lclkrslem1.t |
⊢ · = ( ·𝑠 ‘ 𝐷 ) |
11 |
|
lclkrslem1.c |
⊢ 𝐶 = { 𝑓 ∈ 𝐹 ∣ ( ( ⊥ ‘ ( ⊥ ‘ ( 𝐿 ‘ 𝑓 ) ) ) = ( 𝐿 ‘ 𝑓 ) ∧ ( ⊥ ‘ ( 𝐿 ‘ 𝑓 ) ) ⊆ 𝑄 ) } |
12 |
|
lclkrslem1.k |
⊢ ( 𝜑 → ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ) |
13 |
|
lclkrslem1.q |
⊢ ( 𝜑 → 𝑄 ∈ 𝑆 ) |
14 |
|
lclkrslem1.g |
⊢ ( 𝜑 → 𝐺 ∈ 𝐶 ) |
15 |
|
lclkrslem2.p |
⊢ + = ( +g ‘ 𝐷 ) |
16 |
|
lclkrslem2.e |
⊢ ( 𝜑 → 𝐸 ∈ 𝐶 ) |
17 |
|
eqid |
⊢ { 𝑓 ∈ 𝐹 ∣ ( ⊥ ‘ ( ⊥ ‘ ( 𝐿 ‘ 𝑓 ) ) ) = ( 𝐿 ‘ 𝑓 ) } = { 𝑓 ∈ 𝐹 ∣ ( ⊥ ‘ ( ⊥ ‘ ( 𝐿 ‘ 𝑓 ) ) ) = ( 𝐿 ‘ 𝑓 ) } |
18 |
11 17
|
lcfls1c |
⊢ ( 𝐸 ∈ 𝐶 ↔ ( 𝐸 ∈ { 𝑓 ∈ 𝐹 ∣ ( ⊥ ‘ ( ⊥ ‘ ( 𝐿 ‘ 𝑓 ) ) ) = ( 𝐿 ‘ 𝑓 ) } ∧ ( ⊥ ‘ ( 𝐿 ‘ 𝐸 ) ) ⊆ 𝑄 ) ) |
19 |
18
|
simplbi |
⊢ ( 𝐸 ∈ 𝐶 → 𝐸 ∈ { 𝑓 ∈ 𝐹 ∣ ( ⊥ ‘ ( ⊥ ‘ ( 𝐿 ‘ 𝑓 ) ) ) = ( 𝐿 ‘ 𝑓 ) } ) |
20 |
16 19
|
syl |
⊢ ( 𝜑 → 𝐸 ∈ { 𝑓 ∈ 𝐹 ∣ ( ⊥ ‘ ( ⊥ ‘ ( 𝐿 ‘ 𝑓 ) ) ) = ( 𝐿 ‘ 𝑓 ) } ) |
21 |
11 17
|
lcfls1c |
⊢ ( 𝐺 ∈ 𝐶 ↔ ( 𝐺 ∈ { 𝑓 ∈ 𝐹 ∣ ( ⊥ ‘ ( ⊥ ‘ ( 𝐿 ‘ 𝑓 ) ) ) = ( 𝐿 ‘ 𝑓 ) } ∧ ( ⊥ ‘ ( 𝐿 ‘ 𝐺 ) ) ⊆ 𝑄 ) ) |
22 |
21
|
simplbi |
⊢ ( 𝐺 ∈ 𝐶 → 𝐺 ∈ { 𝑓 ∈ 𝐹 ∣ ( ⊥ ‘ ( ⊥ ‘ ( 𝐿 ‘ 𝑓 ) ) ) = ( 𝐿 ‘ 𝑓 ) } ) |
23 |
14 22
|
syl |
⊢ ( 𝜑 → 𝐺 ∈ { 𝑓 ∈ 𝐹 ∣ ( ⊥ ‘ ( ⊥ ‘ ( 𝐿 ‘ 𝑓 ) ) ) = ( 𝐿 ‘ 𝑓 ) } ) |
24 |
1 2 3 5 6 7 15 17 12 20 23
|
lclkrlem2 |
⊢ ( 𝜑 → ( 𝐸 + 𝐺 ) ∈ { 𝑓 ∈ 𝐹 ∣ ( ⊥ ‘ ( ⊥ ‘ ( 𝐿 ‘ 𝑓 ) ) ) = ( 𝐿 ‘ 𝑓 ) } ) |
25 |
|
eqid |
⊢ ( Base ‘ 𝑈 ) = ( Base ‘ 𝑈 ) |
26 |
1 3 12
|
dvhlmod |
⊢ ( 𝜑 → 𝑈 ∈ LMod ) |
27 |
11
|
lcfls1lem |
⊢ ( 𝐸 ∈ 𝐶 ↔ ( 𝐸 ∈ 𝐹 ∧ ( ⊥ ‘ ( ⊥ ‘ ( 𝐿 ‘ 𝐸 ) ) ) = ( 𝐿 ‘ 𝐸 ) ∧ ( ⊥ ‘ ( 𝐿 ‘ 𝐸 ) ) ⊆ 𝑄 ) ) |
28 |
16 27
|
sylib |
⊢ ( 𝜑 → ( 𝐸 ∈ 𝐹 ∧ ( ⊥ ‘ ( ⊥ ‘ ( 𝐿 ‘ 𝐸 ) ) ) = ( 𝐿 ‘ 𝐸 ) ∧ ( ⊥ ‘ ( 𝐿 ‘ 𝐸 ) ) ⊆ 𝑄 ) ) |
29 |
28
|
simp1d |
⊢ ( 𝜑 → 𝐸 ∈ 𝐹 ) |
30 |
11
|
lcfls1lem |
⊢ ( 𝐺 ∈ 𝐶 ↔ ( 𝐺 ∈ 𝐹 ∧ ( ⊥ ‘ ( ⊥ ‘ ( 𝐿 ‘ 𝐺 ) ) ) = ( 𝐿 ‘ 𝐺 ) ∧ ( ⊥ ‘ ( 𝐿 ‘ 𝐺 ) ) ⊆ 𝑄 ) ) |
31 |
14 30
|
sylib |
⊢ ( 𝜑 → ( 𝐺 ∈ 𝐹 ∧ ( ⊥ ‘ ( ⊥ ‘ ( 𝐿 ‘ 𝐺 ) ) ) = ( 𝐿 ‘ 𝐺 ) ∧ ( ⊥ ‘ ( 𝐿 ‘ 𝐺 ) ) ⊆ 𝑄 ) ) |
32 |
31
|
simp1d |
⊢ ( 𝜑 → 𝐺 ∈ 𝐹 ) |
33 |
5 7 15 26 29 32
|
ldualvaddcl |
⊢ ( 𝜑 → ( 𝐸 + 𝐺 ) ∈ 𝐹 ) |
34 |
25 5 6 26 33
|
lkrssv |
⊢ ( 𝜑 → ( 𝐿 ‘ ( 𝐸 + 𝐺 ) ) ⊆ ( Base ‘ 𝑈 ) ) |
35 |
5 6 7 15 26 29 32
|
lkrin |
⊢ ( 𝜑 → ( ( 𝐿 ‘ 𝐸 ) ∩ ( 𝐿 ‘ 𝐺 ) ) ⊆ ( 𝐿 ‘ ( 𝐸 + 𝐺 ) ) ) |
36 |
1 3 25 2
|
dochss |
⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝐿 ‘ ( 𝐸 + 𝐺 ) ) ⊆ ( Base ‘ 𝑈 ) ∧ ( ( 𝐿 ‘ 𝐸 ) ∩ ( 𝐿 ‘ 𝐺 ) ) ⊆ ( 𝐿 ‘ ( 𝐸 + 𝐺 ) ) ) → ( ⊥ ‘ ( 𝐿 ‘ ( 𝐸 + 𝐺 ) ) ) ⊆ ( ⊥ ‘ ( ( 𝐿 ‘ 𝐸 ) ∩ ( 𝐿 ‘ 𝐺 ) ) ) ) |
37 |
12 34 35 36
|
syl3anc |
⊢ ( 𝜑 → ( ⊥ ‘ ( 𝐿 ‘ ( 𝐸 + 𝐺 ) ) ) ⊆ ( ⊥ ‘ ( ( 𝐿 ‘ 𝐸 ) ∩ ( 𝐿 ‘ 𝐺 ) ) ) ) |
38 |
|
eqid |
⊢ ( ( DIsoH ‘ 𝐾 ) ‘ 𝑊 ) = ( ( DIsoH ‘ 𝐾 ) ‘ 𝑊 ) |
39 |
|
eqid |
⊢ ( ( joinH ‘ 𝐾 ) ‘ 𝑊 ) = ( ( joinH ‘ 𝐾 ) ‘ 𝑊 ) |
40 |
28
|
simp2d |
⊢ ( 𝜑 → ( ⊥ ‘ ( ⊥ ‘ ( 𝐿 ‘ 𝐸 ) ) ) = ( 𝐿 ‘ 𝐸 ) ) |
41 |
1 38 2 3 5 6 12 29
|
lcfl5a |
⊢ ( 𝜑 → ( ( ⊥ ‘ ( ⊥ ‘ ( 𝐿 ‘ 𝐸 ) ) ) = ( 𝐿 ‘ 𝐸 ) ↔ ( 𝐿 ‘ 𝐸 ) ∈ ran ( ( DIsoH ‘ 𝐾 ) ‘ 𝑊 ) ) ) |
42 |
40 41
|
mpbid |
⊢ ( 𝜑 → ( 𝐿 ‘ 𝐸 ) ∈ ran ( ( DIsoH ‘ 𝐾 ) ‘ 𝑊 ) ) |
43 |
31
|
simp2d |
⊢ ( 𝜑 → ( ⊥ ‘ ( ⊥ ‘ ( 𝐿 ‘ 𝐺 ) ) ) = ( 𝐿 ‘ 𝐺 ) ) |
44 |
1 38 2 3 5 6 12 32
|
lcfl5a |
⊢ ( 𝜑 → ( ( ⊥ ‘ ( ⊥ ‘ ( 𝐿 ‘ 𝐺 ) ) ) = ( 𝐿 ‘ 𝐺 ) ↔ ( 𝐿 ‘ 𝐺 ) ∈ ran ( ( DIsoH ‘ 𝐾 ) ‘ 𝑊 ) ) ) |
45 |
43 44
|
mpbid |
⊢ ( 𝜑 → ( 𝐿 ‘ 𝐺 ) ∈ ran ( ( DIsoH ‘ 𝐾 ) ‘ 𝑊 ) ) |
46 |
1 38 3 25 2 39 12 42 45
|
dochdmm1 |
⊢ ( 𝜑 → ( ⊥ ‘ ( ( 𝐿 ‘ 𝐸 ) ∩ ( 𝐿 ‘ 𝐺 ) ) ) = ( ( ⊥ ‘ ( 𝐿 ‘ 𝐸 ) ) ( ( joinH ‘ 𝐾 ) ‘ 𝑊 ) ( ⊥ ‘ ( 𝐿 ‘ 𝐺 ) ) ) ) |
47 |
|
eqid |
⊢ ( LSSum ‘ 𝑈 ) = ( LSSum ‘ 𝑈 ) |
48 |
25 5 6 26 29
|
lkrssv |
⊢ ( 𝜑 → ( 𝐿 ‘ 𝐸 ) ⊆ ( Base ‘ 𝑈 ) ) |
49 |
1 38 3 25 2
|
dochcl |
⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝐿 ‘ 𝐸 ) ⊆ ( Base ‘ 𝑈 ) ) → ( ⊥ ‘ ( 𝐿 ‘ 𝐸 ) ) ∈ ran ( ( DIsoH ‘ 𝐾 ) ‘ 𝑊 ) ) |
50 |
12 48 49
|
syl2anc |
⊢ ( 𝜑 → ( ⊥ ‘ ( 𝐿 ‘ 𝐸 ) ) ∈ ran ( ( DIsoH ‘ 𝐾 ) ‘ 𝑊 ) ) |
51 |
1 38 2 3 47 5 6 12 50 32
|
dochkrsm |
⊢ ( 𝜑 → ( ( ⊥ ‘ ( 𝐿 ‘ 𝐸 ) ) ( LSSum ‘ 𝑈 ) ( ⊥ ‘ ( 𝐿 ‘ 𝐺 ) ) ) ∈ ran ( ( DIsoH ‘ 𝐾 ) ‘ 𝑊 ) ) |
52 |
1 3 25 4 2
|
dochlss |
⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝐿 ‘ 𝐸 ) ⊆ ( Base ‘ 𝑈 ) ) → ( ⊥ ‘ ( 𝐿 ‘ 𝐸 ) ) ∈ 𝑆 ) |
53 |
12 48 52
|
syl2anc |
⊢ ( 𝜑 → ( ⊥ ‘ ( 𝐿 ‘ 𝐸 ) ) ∈ 𝑆 ) |
54 |
25 5 6 26 32
|
lkrssv |
⊢ ( 𝜑 → ( 𝐿 ‘ 𝐺 ) ⊆ ( Base ‘ 𝑈 ) ) |
55 |
1 3 25 4 2
|
dochlss |
⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝐿 ‘ 𝐺 ) ⊆ ( Base ‘ 𝑈 ) ) → ( ⊥ ‘ ( 𝐿 ‘ 𝐺 ) ) ∈ 𝑆 ) |
56 |
12 54 55
|
syl2anc |
⊢ ( 𝜑 → ( ⊥ ‘ ( 𝐿 ‘ 𝐺 ) ) ∈ 𝑆 ) |
57 |
1 3 25 4 47 38 39 12 53 56
|
djhlsmcl |
⊢ ( 𝜑 → ( ( ( ⊥ ‘ ( 𝐿 ‘ 𝐸 ) ) ( LSSum ‘ 𝑈 ) ( ⊥ ‘ ( 𝐿 ‘ 𝐺 ) ) ) ∈ ran ( ( DIsoH ‘ 𝐾 ) ‘ 𝑊 ) ↔ ( ( ⊥ ‘ ( 𝐿 ‘ 𝐸 ) ) ( LSSum ‘ 𝑈 ) ( ⊥ ‘ ( 𝐿 ‘ 𝐺 ) ) ) = ( ( ⊥ ‘ ( 𝐿 ‘ 𝐸 ) ) ( ( joinH ‘ 𝐾 ) ‘ 𝑊 ) ( ⊥ ‘ ( 𝐿 ‘ 𝐺 ) ) ) ) ) |
58 |
51 57
|
mpbid |
⊢ ( 𝜑 → ( ( ⊥ ‘ ( 𝐿 ‘ 𝐸 ) ) ( LSSum ‘ 𝑈 ) ( ⊥ ‘ ( 𝐿 ‘ 𝐺 ) ) ) = ( ( ⊥ ‘ ( 𝐿 ‘ 𝐸 ) ) ( ( joinH ‘ 𝐾 ) ‘ 𝑊 ) ( ⊥ ‘ ( 𝐿 ‘ 𝐺 ) ) ) ) |
59 |
46 58
|
eqtr4d |
⊢ ( 𝜑 → ( ⊥ ‘ ( ( 𝐿 ‘ 𝐸 ) ∩ ( 𝐿 ‘ 𝐺 ) ) ) = ( ( ⊥ ‘ ( 𝐿 ‘ 𝐸 ) ) ( LSSum ‘ 𝑈 ) ( ⊥ ‘ ( 𝐿 ‘ 𝐺 ) ) ) ) |
60 |
28
|
simp3d |
⊢ ( 𝜑 → ( ⊥ ‘ ( 𝐿 ‘ 𝐸 ) ) ⊆ 𝑄 ) |
61 |
31
|
simp3d |
⊢ ( 𝜑 → ( ⊥ ‘ ( 𝐿 ‘ 𝐺 ) ) ⊆ 𝑄 ) |
62 |
4
|
lsssssubg |
⊢ ( 𝑈 ∈ LMod → 𝑆 ⊆ ( SubGrp ‘ 𝑈 ) ) |
63 |
26 62
|
syl |
⊢ ( 𝜑 → 𝑆 ⊆ ( SubGrp ‘ 𝑈 ) ) |
64 |
63 53
|
sseldd |
⊢ ( 𝜑 → ( ⊥ ‘ ( 𝐿 ‘ 𝐸 ) ) ∈ ( SubGrp ‘ 𝑈 ) ) |
65 |
63 56
|
sseldd |
⊢ ( 𝜑 → ( ⊥ ‘ ( 𝐿 ‘ 𝐺 ) ) ∈ ( SubGrp ‘ 𝑈 ) ) |
66 |
63 13
|
sseldd |
⊢ ( 𝜑 → 𝑄 ∈ ( SubGrp ‘ 𝑈 ) ) |
67 |
47
|
lsmlub |
⊢ ( ( ( ⊥ ‘ ( 𝐿 ‘ 𝐸 ) ) ∈ ( SubGrp ‘ 𝑈 ) ∧ ( ⊥ ‘ ( 𝐿 ‘ 𝐺 ) ) ∈ ( SubGrp ‘ 𝑈 ) ∧ 𝑄 ∈ ( SubGrp ‘ 𝑈 ) ) → ( ( ( ⊥ ‘ ( 𝐿 ‘ 𝐸 ) ) ⊆ 𝑄 ∧ ( ⊥ ‘ ( 𝐿 ‘ 𝐺 ) ) ⊆ 𝑄 ) ↔ ( ( ⊥ ‘ ( 𝐿 ‘ 𝐸 ) ) ( LSSum ‘ 𝑈 ) ( ⊥ ‘ ( 𝐿 ‘ 𝐺 ) ) ) ⊆ 𝑄 ) ) |
68 |
64 65 66 67
|
syl3anc |
⊢ ( 𝜑 → ( ( ( ⊥ ‘ ( 𝐿 ‘ 𝐸 ) ) ⊆ 𝑄 ∧ ( ⊥ ‘ ( 𝐿 ‘ 𝐺 ) ) ⊆ 𝑄 ) ↔ ( ( ⊥ ‘ ( 𝐿 ‘ 𝐸 ) ) ( LSSum ‘ 𝑈 ) ( ⊥ ‘ ( 𝐿 ‘ 𝐺 ) ) ) ⊆ 𝑄 ) ) |
69 |
60 61 68
|
mpbi2and |
⊢ ( 𝜑 → ( ( ⊥ ‘ ( 𝐿 ‘ 𝐸 ) ) ( LSSum ‘ 𝑈 ) ( ⊥ ‘ ( 𝐿 ‘ 𝐺 ) ) ) ⊆ 𝑄 ) |
70 |
59 69
|
eqsstrd |
⊢ ( 𝜑 → ( ⊥ ‘ ( ( 𝐿 ‘ 𝐸 ) ∩ ( 𝐿 ‘ 𝐺 ) ) ) ⊆ 𝑄 ) |
71 |
37 70
|
sstrd |
⊢ ( 𝜑 → ( ⊥ ‘ ( 𝐿 ‘ ( 𝐸 + 𝐺 ) ) ) ⊆ 𝑄 ) |
72 |
11 17
|
lcfls1c |
⊢ ( ( 𝐸 + 𝐺 ) ∈ 𝐶 ↔ ( ( 𝐸 + 𝐺 ) ∈ { 𝑓 ∈ 𝐹 ∣ ( ⊥ ‘ ( ⊥ ‘ ( 𝐿 ‘ 𝑓 ) ) ) = ( 𝐿 ‘ 𝑓 ) } ∧ ( ⊥ ‘ ( 𝐿 ‘ ( 𝐸 + 𝐺 ) ) ) ⊆ 𝑄 ) ) |
73 |
24 71 72
|
sylanbrc |
⊢ ( 𝜑 → ( 𝐸 + 𝐺 ) ∈ 𝐶 ) |