Step | Hyp | Ref
| Expression |
1 | | lcfrlem17.h |
. . . 4
⊢ 𝐻 = (LHyp‘𝐾) |
2 | | lcfrlem17.o |
. . . 4
⊢ ⊥ =
((ocH‘𝐾)‘𝑊) |
3 | | lcfrlem17.u |
. . . 4
⊢ 𝑈 = ((DVecH‘𝐾)‘𝑊) |
4 | | lcfrlem17.v |
. . . 4
⊢ 𝑉 = (Base‘𝑈) |
5 | | lcfrlem17.p |
. . . 4
⊢ + =
(+g‘𝑈) |
6 | | lcfrlem17.z |
. . . 4
⊢ 0 =
(0g‘𝑈) |
7 | | lcfrlem17.n |
. . . 4
⊢ 𝑁 = (LSpan‘𝑈) |
8 | | lcfrlem17.a |
. . . 4
⊢ 𝐴 = (LSAtoms‘𝑈) |
9 | | lcfrlem17.k |
. . . 4
⊢ (𝜑 → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻)) |
10 | | lcfrlem17.x |
. . . 4
⊢ (𝜑 → 𝑋 ∈ (𝑉 ∖ { 0 })) |
11 | | lcfrlem17.y |
. . . 4
⊢ (𝜑 → 𝑌 ∈ (𝑉 ∖ { 0 })) |
12 | | lcfrlem17.ne |
. . . 4
⊢ (𝜑 → (𝑁‘{𝑋}) ≠ (𝑁‘{𝑌})) |
13 | | lcfrlem22.b |
. . . 4
⊢ 𝐵 = ((𝑁‘{𝑋, 𝑌}) ∩ ( ⊥ ‘{(𝑋 + 𝑌)})) |
14 | | eqid 2738 |
. . . 4
⊢
(LSSum‘𝑈) =
(LSSum‘𝑈) |
15 | 1, 2, 3, 4, 5, 6, 7, 8, 9, 10,
11, 12, 13, 14 | lcfrlem23 39587 |
. . 3
⊢ (𝜑 → (( ⊥ ‘{𝑋, 𝑌})(LSSum‘𝑈)𝐵) = ( ⊥ ‘{(𝑋 + 𝑌)})) |
16 | | lcfrlem24.t |
. . . . . 6
⊢ · = (
·𝑠 ‘𝑈) |
17 | | lcfrlem24.s |
. . . . . 6
⊢ 𝑆 = (Scalar‘𝑈) |
18 | | lcfrlem24.q |
. . . . . 6
⊢ 𝑄 = (0g‘𝑆) |
19 | | lcfrlem24.r |
. . . . . 6
⊢ 𝑅 = (Base‘𝑆) |
20 | | lcfrlem24.j |
. . . . . 6
⊢ 𝐽 = (𝑥 ∈ (𝑉 ∖ { 0 }) ↦ (𝑣 ∈ 𝑉 ↦ (℩𝑘 ∈ 𝑅 ∃𝑤 ∈ ( ⊥ ‘{𝑥})𝑣 = (𝑤 + (𝑘 · 𝑥))))) |
21 | | lcfrlem24.ib |
. . . . . 6
⊢ (𝜑 → 𝐼 ∈ 𝐵) |
22 | | lcfrlem24.l |
. . . . . 6
⊢ 𝐿 = (LKer‘𝑈) |
23 | 1, 2, 3, 4, 5, 6, 7, 8, 9, 10,
11, 12, 13, 16, 17, 18, 19, 20, 21, 22 | lcfrlem24 39588 |
. . . . 5
⊢ (𝜑 → ( ⊥ ‘{𝑋, 𝑌}) = ((𝐿‘(𝐽‘𝑋)) ∩ (𝐿‘(𝐽‘𝑌)))) |
24 | | inss2 4163 |
. . . . 5
⊢ ((𝐿‘(𝐽‘𝑋)) ∩ (𝐿‘(𝐽‘𝑌))) ⊆ (𝐿‘(𝐽‘𝑌)) |
25 | 23, 24 | eqsstrdi 3974 |
. . . 4
⊢ (𝜑 → ( ⊥ ‘{𝑋, 𝑌}) ⊆ (𝐿‘(𝐽‘𝑌))) |
26 | 1, 3, 9 | dvhlvec 39131 |
. . . . . 6
⊢ (𝜑 → 𝑈 ∈ LVec) |
27 | 1, 2, 3, 4, 5, 6, 7, 8, 9, 10,
11, 12, 13 | lcfrlem22 39586 |
. . . . . 6
⊢ (𝜑 → 𝐵 ∈ 𝐴) |
28 | | lcfrlem25.in |
. . . . . 6
⊢ (𝜑 → 𝐼 ≠ 0 ) |
29 | 6, 7, 8, 26, 27, 21, 28 | lsatel 37027 |
. . . . 5
⊢ (𝜑 → 𝐵 = (𝑁‘{𝐼})) |
30 | | eqid 2738 |
. . . . . 6
⊢
(LSubSp‘𝑈) =
(LSubSp‘𝑈) |
31 | 1, 3, 9 | dvhlmod 39132 |
. . . . . 6
⊢ (𝜑 → 𝑈 ∈ LMod) |
32 | | eqid 2738 |
. . . . . . . 8
⊢
(LFnl‘𝑈) =
(LFnl‘𝑈) |
33 | | lcfrlem25.d |
. . . . . . . 8
⊢ 𝐷 = (LDual‘𝑈) |
34 | | eqid 2738 |
. . . . . . . 8
⊢
(0g‘𝐷) = (0g‘𝐷) |
35 | | eqid 2738 |
. . . . . . . 8
⊢ {𝑓 ∈ (LFnl‘𝑈) ∣ ( ⊥ ‘( ⊥
‘(𝐿‘𝑓))) = (𝐿‘𝑓)} = {𝑓 ∈ (LFnl‘𝑈) ∣ ( ⊥ ‘( ⊥
‘(𝐿‘𝑓))) = (𝐿‘𝑓)} |
36 | 1, 2, 3, 4, 5, 16,
17, 19, 6, 32, 22, 33, 34, 35, 20, 9, 11 | lcfrlem10 39574 |
. . . . . . 7
⊢ (𝜑 → (𝐽‘𝑌) ∈ (LFnl‘𝑈)) |
37 | 32, 22, 30 | lkrlss 37117 |
. . . . . . 7
⊢ ((𝑈 ∈ LMod ∧ (𝐽‘𝑌) ∈ (LFnl‘𝑈)) → (𝐿‘(𝐽‘𝑌)) ∈ (LSubSp‘𝑈)) |
38 | 31, 36, 37 | syl2anc 584 |
. . . . . 6
⊢ (𝜑 → (𝐿‘(𝐽‘𝑌)) ∈ (LSubSp‘𝑈)) |
39 | | lcfrlem25.jz |
. . . . . . 7
⊢ (𝜑 → ((𝐽‘𝑌)‘𝐼) = 𝑄) |
40 | 4, 8, 31, 27 | lsatssv 37020 |
. . . . . . . . 9
⊢ (𝜑 → 𝐵 ⊆ 𝑉) |
41 | 40, 21 | sseldd 3921 |
. . . . . . . 8
⊢ (𝜑 → 𝐼 ∈ 𝑉) |
42 | 4, 17, 18, 32, 22, 31, 36, 41 | ellkr2 37113 |
. . . . . . 7
⊢ (𝜑 → (𝐼 ∈ (𝐿‘(𝐽‘𝑌)) ↔ ((𝐽‘𝑌)‘𝐼) = 𝑄)) |
43 | 39, 42 | mpbird 256 |
. . . . . 6
⊢ (𝜑 → 𝐼 ∈ (𝐿‘(𝐽‘𝑌))) |
44 | 30, 7, 31, 38, 43 | lspsnel5a 20268 |
. . . . 5
⊢ (𝜑 → (𝑁‘{𝐼}) ⊆ (𝐿‘(𝐽‘𝑌))) |
45 | 29, 44 | eqsstrd 3958 |
. . . 4
⊢ (𝜑 → 𝐵 ⊆ (𝐿‘(𝐽‘𝑌))) |
46 | 30 | lsssssubg 20230 |
. . . . . . 7
⊢ (𝑈 ∈ LMod →
(LSubSp‘𝑈) ⊆
(SubGrp‘𝑈)) |
47 | 31, 46 | syl 17 |
. . . . . 6
⊢ (𝜑 → (LSubSp‘𝑈) ⊆ (SubGrp‘𝑈)) |
48 | 10 | eldifad 3898 |
. . . . . . . 8
⊢ (𝜑 → 𝑋 ∈ 𝑉) |
49 | 11 | eldifad 3898 |
. . . . . . . 8
⊢ (𝜑 → 𝑌 ∈ 𝑉) |
50 | | prssi 4754 |
. . . . . . . 8
⊢ ((𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑉) → {𝑋, 𝑌} ⊆ 𝑉) |
51 | 48, 49, 50 | syl2anc 584 |
. . . . . . 7
⊢ (𝜑 → {𝑋, 𝑌} ⊆ 𝑉) |
52 | 1, 3, 4, 30, 2 | dochlss 39376 |
. . . . . . 7
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ {𝑋, 𝑌} ⊆ 𝑉) → ( ⊥ ‘{𝑋, 𝑌}) ∈ (LSubSp‘𝑈)) |
53 | 9, 51, 52 | syl2anc 584 |
. . . . . 6
⊢ (𝜑 → ( ⊥ ‘{𝑋, 𝑌}) ∈ (LSubSp‘𝑈)) |
54 | 47, 53 | sseldd 3921 |
. . . . 5
⊢ (𝜑 → ( ⊥ ‘{𝑋, 𝑌}) ∈ (SubGrp‘𝑈)) |
55 | 4, 30, 7, 31, 48, 49 | lspprcl 20250 |
. . . . . . . 8
⊢ (𝜑 → (𝑁‘{𝑋, 𝑌}) ∈ (LSubSp‘𝑈)) |
56 | 1, 2, 3, 4, 5, 6, 7, 8, 9, 10,
11, 12 | lcfrlem17 39581 |
. . . . . . . . . . 11
⊢ (𝜑 → (𝑋 + 𝑌) ∈ (𝑉 ∖ { 0 })) |
57 | 56 | eldifad 3898 |
. . . . . . . . . 10
⊢ (𝜑 → (𝑋 + 𝑌) ∈ 𝑉) |
58 | 57 | snssd 4742 |
. . . . . . . . 9
⊢ (𝜑 → {(𝑋 + 𝑌)} ⊆ 𝑉) |
59 | 1, 3, 4, 30, 2 | dochlss 39376 |
. . . . . . . . 9
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ {(𝑋 + 𝑌)} ⊆ 𝑉) → ( ⊥ ‘{(𝑋 + 𝑌)}) ∈ (LSubSp‘𝑈)) |
60 | 9, 58, 59 | syl2anc 584 |
. . . . . . . 8
⊢ (𝜑 → ( ⊥ ‘{(𝑋 + 𝑌)}) ∈ (LSubSp‘𝑈)) |
61 | 30 | lssincl 20237 |
. . . . . . . 8
⊢ ((𝑈 ∈ LMod ∧ (𝑁‘{𝑋, 𝑌}) ∈ (LSubSp‘𝑈) ∧ ( ⊥ ‘{(𝑋 + 𝑌)}) ∈ (LSubSp‘𝑈)) → ((𝑁‘{𝑋, 𝑌}) ∩ ( ⊥ ‘{(𝑋 + 𝑌)})) ∈ (LSubSp‘𝑈)) |
62 | 31, 55, 60, 61 | syl3anc 1370 |
. . . . . . 7
⊢ (𝜑 → ((𝑁‘{𝑋, 𝑌}) ∩ ( ⊥ ‘{(𝑋 + 𝑌)})) ∈ (LSubSp‘𝑈)) |
63 | 13, 62 | eqeltrid 2843 |
. . . . . 6
⊢ (𝜑 → 𝐵 ∈ (LSubSp‘𝑈)) |
64 | 47, 63 | sseldd 3921 |
. . . . 5
⊢ (𝜑 → 𝐵 ∈ (SubGrp‘𝑈)) |
65 | 47, 38 | sseldd 3921 |
. . . . 5
⊢ (𝜑 → (𝐿‘(𝐽‘𝑌)) ∈ (SubGrp‘𝑈)) |
66 | 14 | lsmlub 19280 |
. . . . 5
⊢ ((( ⊥
‘{𝑋, 𝑌}) ∈ (SubGrp‘𝑈) ∧ 𝐵 ∈ (SubGrp‘𝑈) ∧ (𝐿‘(𝐽‘𝑌)) ∈ (SubGrp‘𝑈)) → ((( ⊥ ‘{𝑋, 𝑌}) ⊆ (𝐿‘(𝐽‘𝑌)) ∧ 𝐵 ⊆ (𝐿‘(𝐽‘𝑌))) ↔ (( ⊥ ‘{𝑋, 𝑌})(LSSum‘𝑈)𝐵) ⊆ (𝐿‘(𝐽‘𝑌)))) |
67 | 54, 64, 65, 66 | syl3anc 1370 |
. . . 4
⊢ (𝜑 → ((( ⊥ ‘{𝑋, 𝑌}) ⊆ (𝐿‘(𝐽‘𝑌)) ∧ 𝐵 ⊆ (𝐿‘(𝐽‘𝑌))) ↔ (( ⊥ ‘{𝑋, 𝑌})(LSSum‘𝑈)𝐵) ⊆ (𝐿‘(𝐽‘𝑌)))) |
68 | 25, 45, 67 | mpbi2and 709 |
. . 3
⊢ (𝜑 → (( ⊥ ‘{𝑋, 𝑌})(LSSum‘𝑈)𝐵) ⊆ (𝐿‘(𝐽‘𝑌))) |
69 | 15, 68 | eqsstrrd 3959 |
. 2
⊢ (𝜑 → ( ⊥ ‘{(𝑋 + 𝑌)}) ⊆ (𝐿‘(𝐽‘𝑌))) |
70 | | eqid 2738 |
. . 3
⊢
(LSHyp‘𝑈) =
(LSHyp‘𝑈) |
71 | 1, 2, 3, 4, 6, 70,
9, 56 | dochsnshp 39475 |
. . 3
⊢ (𝜑 → ( ⊥ ‘{(𝑋 + 𝑌)}) ∈ (LSHyp‘𝑈)) |
72 | 1, 2, 3, 4, 5, 16,
17, 19, 6, 32, 22, 33, 34, 35, 20, 9, 11 | lcfrlem13 39577 |
. . . . 5
⊢ (𝜑 → (𝐽‘𝑌) ∈ ({𝑓 ∈ (LFnl‘𝑈) ∣ ( ⊥ ‘( ⊥
‘(𝐿‘𝑓))) = (𝐿‘𝑓)} ∖ {(0g‘𝐷)})) |
73 | | eldifsni 4723 |
. . . . 5
⊢ ((𝐽‘𝑌) ∈ ({𝑓 ∈ (LFnl‘𝑈) ∣ ( ⊥ ‘( ⊥
‘(𝐿‘𝑓))) = (𝐿‘𝑓)} ∖ {(0g‘𝐷)}) → (𝐽‘𝑌) ≠ (0g‘𝐷)) |
74 | 72, 73 | syl 17 |
. . . 4
⊢ (𝜑 → (𝐽‘𝑌) ≠ (0g‘𝐷)) |
75 | 70, 32, 22, 33, 34, 26, 36 | lduallkr3 37184 |
. . . 4
⊢ (𝜑 → ((𝐿‘(𝐽‘𝑌)) ∈ (LSHyp‘𝑈) ↔ (𝐽‘𝑌) ≠ (0g‘𝐷))) |
76 | 74, 75 | mpbird 256 |
. . 3
⊢ (𝜑 → (𝐿‘(𝐽‘𝑌)) ∈ (LSHyp‘𝑈)) |
77 | 70, 26, 71, 76 | lshpcmp 37010 |
. 2
⊢ (𝜑 → (( ⊥ ‘{(𝑋 + 𝑌)}) ⊆ (𝐿‘(𝐽‘𝑌)) ↔ ( ⊥ ‘{(𝑋 + 𝑌)}) = (𝐿‘(𝐽‘𝑌)))) |
78 | 69, 77 | mpbid 231 |
1
⊢ (𝜑 → ( ⊥ ‘{(𝑋 + 𝑌)}) = (𝐿‘(𝐽‘𝑌))) |