Step | Hyp | Ref
| Expression |
1 | | lcfrlem30.c |
. . . . . . 7
⊢ 𝐶 = ((𝐽‘𝑋) − (((𝐹‘((𝐽‘𝑌)‘𝐼))(.r‘𝑆)((𝐽‘𝑋)‘𝐼))( ·𝑠
‘𝐷)(𝐽‘𝑌))) |
2 | | lcfrlem31.cn |
. . . . . . 7
⊢ (𝜑 → 𝐶 = (0g‘𝐷)) |
3 | 1, 2 | eqtr3id 2794 |
. . . . . 6
⊢ (𝜑 → ((𝐽‘𝑋) − (((𝐹‘((𝐽‘𝑌)‘𝐼))(.r‘𝑆)((𝐽‘𝑋)‘𝐼))( ·𝑠
‘𝐷)(𝐽‘𝑌))) = (0g‘𝐷)) |
4 | | lcfrlem25.d |
. . . . . . . 8
⊢ 𝐷 = (LDual‘𝑈) |
5 | | lcfrlem17.h |
. . . . . . . . 9
⊢ 𝐻 = (LHyp‘𝐾) |
6 | | lcfrlem17.u |
. . . . . . . . 9
⊢ 𝑈 = ((DVecH‘𝐾)‘𝑊) |
7 | | lcfrlem17.k |
. . . . . . . . 9
⊢ (𝜑 → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻)) |
8 | 5, 6, 7 | dvhlmod 39133 |
. . . . . . . 8
⊢ (𝜑 → 𝑈 ∈ LMod) |
9 | 4, 8 | lduallmod 37176 |
. . . . . . 7
⊢ (𝜑 → 𝐷 ∈ LMod) |
10 | | eqid 2740 |
. . . . . . . 8
⊢
(LFnl‘𝑈) =
(LFnl‘𝑈) |
11 | | eqid 2740 |
. . . . . . . 8
⊢
(Base‘𝐷) =
(Base‘𝐷) |
12 | | lcfrlem17.o |
. . . . . . . . 9
⊢ ⊥ =
((ocH‘𝐾)‘𝑊) |
13 | | lcfrlem17.v |
. . . . . . . . 9
⊢ 𝑉 = (Base‘𝑈) |
14 | | lcfrlem17.p |
. . . . . . . . 9
⊢ + =
(+g‘𝑈) |
15 | | lcfrlem24.t |
. . . . . . . . 9
⊢ · = (
·𝑠 ‘𝑈) |
16 | | lcfrlem24.s |
. . . . . . . . 9
⊢ 𝑆 = (Scalar‘𝑈) |
17 | | lcfrlem24.r |
. . . . . . . . 9
⊢ 𝑅 = (Base‘𝑆) |
18 | | lcfrlem17.z |
. . . . . . . . 9
⊢ 0 =
(0g‘𝑈) |
19 | | lcfrlem24.l |
. . . . . . . . 9
⊢ 𝐿 = (LKer‘𝑈) |
20 | | eqid 2740 |
. . . . . . . . 9
⊢
(0g‘𝐷) = (0g‘𝐷) |
21 | | eqid 2740 |
. . . . . . . . 9
⊢ {𝑓 ∈ (LFnl‘𝑈) ∣ ( ⊥ ‘( ⊥
‘(𝐿‘𝑓))) = (𝐿‘𝑓)} = {𝑓 ∈ (LFnl‘𝑈) ∣ ( ⊥ ‘( ⊥
‘(𝐿‘𝑓))) = (𝐿‘𝑓)} |
22 | | lcfrlem24.j |
. . . . . . . . 9
⊢ 𝐽 = (𝑥 ∈ (𝑉 ∖ { 0 }) ↦ (𝑣 ∈ 𝑉 ↦ (℩𝑘 ∈ 𝑅 ∃𝑤 ∈ ( ⊥ ‘{𝑥})𝑣 = (𝑤 + (𝑘 · 𝑥))))) |
23 | | lcfrlem17.x |
. . . . . . . . 9
⊢ (𝜑 → 𝑋 ∈ (𝑉 ∖ { 0 })) |
24 | 5, 12, 6, 13, 14, 15, 16, 17, 18, 10, 19, 4, 20, 21, 22, 7, 23 | lcfrlem10 39575 |
. . . . . . . 8
⊢ (𝜑 → (𝐽‘𝑋) ∈ (LFnl‘𝑈)) |
25 | 10, 4, 11, 8, 24 | ldualelvbase 37150 |
. . . . . . 7
⊢ (𝜑 → (𝐽‘𝑋) ∈ (Base‘𝐷)) |
26 | | eqid 2740 |
. . . . . . . . 9
⊢ (
·𝑠 ‘𝐷) = ( ·𝑠
‘𝐷) |
27 | | lcfrlem17.n |
. . . . . . . . . 10
⊢ 𝑁 = (LSpan‘𝑈) |
28 | | lcfrlem17.a |
. . . . . . . . . 10
⊢ 𝐴 = (LSAtoms‘𝑈) |
29 | | lcfrlem17.y |
. . . . . . . . . 10
⊢ (𝜑 → 𝑌 ∈ (𝑉 ∖ { 0 })) |
30 | | lcfrlem17.ne |
. . . . . . . . . 10
⊢ (𝜑 → (𝑁‘{𝑋}) ≠ (𝑁‘{𝑌})) |
31 | | lcfrlem22.b |
. . . . . . . . . 10
⊢ 𝐵 = ((𝑁‘{𝑋, 𝑌}) ∩ ( ⊥ ‘{(𝑋 + 𝑌)})) |
32 | | lcfrlem24.q |
. . . . . . . . . 10
⊢ 𝑄 = (0g‘𝑆) |
33 | | lcfrlem24.ib |
. . . . . . . . . 10
⊢ (𝜑 → 𝐼 ∈ 𝐵) |
34 | | lcfrlem28.jn |
. . . . . . . . . 10
⊢ (𝜑 → ((𝐽‘𝑌)‘𝐼) ≠ 𝑄) |
35 | | lcfrlem29.i |
. . . . . . . . . 10
⊢ 𝐹 = (invr‘𝑆) |
36 | 5, 12, 6, 13, 14, 18, 27, 28, 7, 23, 29, 30, 31, 15, 16, 32, 17, 22, 33, 19, 4, 34, 35 | lcfrlem29 39594 |
. . . . . . . . 9
⊢ (𝜑 → ((𝐹‘((𝐽‘𝑌)‘𝐼))(.r‘𝑆)((𝐽‘𝑋)‘𝐼)) ∈ 𝑅) |
37 | 5, 12, 6, 13, 14, 15, 16, 17, 18, 10, 19, 4, 20, 21, 22, 7, 29 | lcfrlem10 39575 |
. . . . . . . . 9
⊢ (𝜑 → (𝐽‘𝑌) ∈ (LFnl‘𝑈)) |
38 | 10, 16, 17, 4, 26, 8, 36, 37 | ldualvscl 37162 |
. . . . . . . 8
⊢ (𝜑 → (((𝐹‘((𝐽‘𝑌)‘𝐼))(.r‘𝑆)((𝐽‘𝑋)‘𝐼))( ·𝑠
‘𝐷)(𝐽‘𝑌)) ∈ (LFnl‘𝑈)) |
39 | 10, 4, 11, 8, 38 | ldualelvbase 37150 |
. . . . . . 7
⊢ (𝜑 → (((𝐹‘((𝐽‘𝑌)‘𝐼))(.r‘𝑆)((𝐽‘𝑋)‘𝐼))( ·𝑠
‘𝐷)(𝐽‘𝑌)) ∈ (Base‘𝐷)) |
40 | | lcfrlem30.m |
. . . . . . . 8
⊢ − =
(-g‘𝐷) |
41 | 11, 20, 40 | lmodsubeq0 20193 |
. . . . . . 7
⊢ ((𝐷 ∈ LMod ∧ (𝐽‘𝑋) ∈ (Base‘𝐷) ∧ (((𝐹‘((𝐽‘𝑌)‘𝐼))(.r‘𝑆)((𝐽‘𝑋)‘𝐼))( ·𝑠
‘𝐷)(𝐽‘𝑌)) ∈ (Base‘𝐷)) → (((𝐽‘𝑋) − (((𝐹‘((𝐽‘𝑌)‘𝐼))(.r‘𝑆)((𝐽‘𝑋)‘𝐼))( ·𝑠
‘𝐷)(𝐽‘𝑌))) = (0g‘𝐷) ↔ (𝐽‘𝑋) = (((𝐹‘((𝐽‘𝑌)‘𝐼))(.r‘𝑆)((𝐽‘𝑋)‘𝐼))( ·𝑠
‘𝐷)(𝐽‘𝑌)))) |
42 | 9, 25, 39, 41 | syl3anc 1370 |
. . . . . 6
⊢ (𝜑 → (((𝐽‘𝑋) − (((𝐹‘((𝐽‘𝑌)‘𝐼))(.r‘𝑆)((𝐽‘𝑋)‘𝐼))( ·𝑠
‘𝐷)(𝐽‘𝑌))) = (0g‘𝐷) ↔ (𝐽‘𝑋) = (((𝐹‘((𝐽‘𝑌)‘𝐼))(.r‘𝑆)((𝐽‘𝑋)‘𝐼))( ·𝑠
‘𝐷)(𝐽‘𝑌)))) |
43 | 3, 42 | mpbid 231 |
. . . . 5
⊢ (𝜑 → (𝐽‘𝑋) = (((𝐹‘((𝐽‘𝑌)‘𝐼))(.r‘𝑆)((𝐽‘𝑋)‘𝐼))( ·𝑠
‘𝐷)(𝐽‘𝑌))) |
44 | 43 | fveq2d 6775 |
. . . 4
⊢ (𝜑 → (𝐿‘(𝐽‘𝑋)) = (𝐿‘(((𝐹‘((𝐽‘𝑌)‘𝐼))(.r‘𝑆)((𝐽‘𝑋)‘𝐼))( ·𝑠
‘𝐷)(𝐽‘𝑌)))) |
45 | 5, 6, 7 | dvhlvec 39132 |
. . . . 5
⊢ (𝜑 → 𝑈 ∈ LVec) |
46 | 16 | lvecdrng 20378 |
. . . . . . . 8
⊢ (𝑈 ∈ LVec → 𝑆 ∈
DivRing) |
47 | 45, 46 | syl 17 |
. . . . . . 7
⊢ (𝜑 → 𝑆 ∈ DivRing) |
48 | 5, 12, 6, 13, 14, 18, 27, 28, 7, 23, 29, 30, 31 | lcfrlem22 39587 |
. . . . . . . . . 10
⊢ (𝜑 → 𝐵 ∈ 𝐴) |
49 | 13, 28, 8, 48 | lsatssv 37021 |
. . . . . . . . 9
⊢ (𝜑 → 𝐵 ⊆ 𝑉) |
50 | 49, 33 | sseldd 3927 |
. . . . . . . 8
⊢ (𝜑 → 𝐼 ∈ 𝑉) |
51 | 16, 17, 13, 10 | lflcl 37087 |
. . . . . . . 8
⊢ ((𝑈 ∈ LMod ∧ (𝐽‘𝑌) ∈ (LFnl‘𝑈) ∧ 𝐼 ∈ 𝑉) → ((𝐽‘𝑌)‘𝐼) ∈ 𝑅) |
52 | 8, 37, 50, 51 | syl3anc 1370 |
. . . . . . 7
⊢ (𝜑 → ((𝐽‘𝑌)‘𝐼) ∈ 𝑅) |
53 | 17, 32, 35 | drnginvrn0 20020 |
. . . . . . 7
⊢ ((𝑆 ∈ DivRing ∧ ((𝐽‘𝑌)‘𝐼) ∈ 𝑅 ∧ ((𝐽‘𝑌)‘𝐼) ≠ 𝑄) → (𝐹‘((𝐽‘𝑌)‘𝐼)) ≠ 𝑄) |
54 | 47, 52, 34, 53 | syl3anc 1370 |
. . . . . 6
⊢ (𝜑 → (𝐹‘((𝐽‘𝑌)‘𝐼)) ≠ 𝑄) |
55 | | lcfrlem31.xi |
. . . . . 6
⊢ (𝜑 → ((𝐽‘𝑋)‘𝐼) ≠ 𝑄) |
56 | | eqid 2740 |
. . . . . . 7
⊢
(.r‘𝑆) = (.r‘𝑆) |
57 | 17, 32, 35 | drnginvrcl 20019 |
. . . . . . . 8
⊢ ((𝑆 ∈ DivRing ∧ ((𝐽‘𝑌)‘𝐼) ∈ 𝑅 ∧ ((𝐽‘𝑌)‘𝐼) ≠ 𝑄) → (𝐹‘((𝐽‘𝑌)‘𝐼)) ∈ 𝑅) |
58 | 47, 52, 34, 57 | syl3anc 1370 |
. . . . . . 7
⊢ (𝜑 → (𝐹‘((𝐽‘𝑌)‘𝐼)) ∈ 𝑅) |
59 | 16, 17, 13, 10 | lflcl 37087 |
. . . . . . . 8
⊢ ((𝑈 ∈ LMod ∧ (𝐽‘𝑋) ∈ (LFnl‘𝑈) ∧ 𝐼 ∈ 𝑉) → ((𝐽‘𝑋)‘𝐼) ∈ 𝑅) |
60 | 8, 24, 50, 59 | syl3anc 1370 |
. . . . . . 7
⊢ (𝜑 → ((𝐽‘𝑋)‘𝐼) ∈ 𝑅) |
61 | 17, 32, 56, 47, 58, 60 | drngmulne0 20024 |
. . . . . 6
⊢ (𝜑 → (((𝐹‘((𝐽‘𝑌)‘𝐼))(.r‘𝑆)((𝐽‘𝑋)‘𝐼)) ≠ 𝑄 ↔ ((𝐹‘((𝐽‘𝑌)‘𝐼)) ≠ 𝑄 ∧ ((𝐽‘𝑋)‘𝐼) ≠ 𝑄))) |
62 | 54, 55, 61 | mpbir2and 710 |
. . . . 5
⊢ (𝜑 → ((𝐹‘((𝐽‘𝑌)‘𝐼))(.r‘𝑆)((𝐽‘𝑋)‘𝐼)) ≠ 𝑄) |
63 | 16, 17, 32, 10, 19, 4, 26, 45, 37, 36, 62 | ldualkrsc 37190 |
. . . 4
⊢ (𝜑 → (𝐿‘(((𝐹‘((𝐽‘𝑌)‘𝐼))(.r‘𝑆)((𝐽‘𝑋)‘𝐼))( ·𝑠
‘𝐷)(𝐽‘𝑌))) = (𝐿‘(𝐽‘𝑌))) |
64 | 44, 63 | eqtrd 2780 |
. . 3
⊢ (𝜑 → (𝐿‘(𝐽‘𝑋)) = (𝐿‘(𝐽‘𝑌))) |
65 | 64 | fveq2d 6775 |
. 2
⊢ (𝜑 → ( ⊥ ‘(𝐿‘(𝐽‘𝑋))) = ( ⊥ ‘(𝐿‘(𝐽‘𝑌)))) |
66 | 5, 12, 6, 13, 14, 15, 16, 17, 18, 10, 19, 4, 20, 21, 22, 7, 23, 27 | lcfrlem14 39579 |
. 2
⊢ (𝜑 → ( ⊥ ‘(𝐿‘(𝐽‘𝑋))) = (𝑁‘{𝑋})) |
67 | 5, 12, 6, 13, 14, 15, 16, 17, 18, 10, 19, 4, 20, 21, 22, 7, 29, 27 | lcfrlem14 39579 |
. 2
⊢ (𝜑 → ( ⊥ ‘(𝐿‘(𝐽‘𝑌))) = (𝑁‘{𝑌})) |
68 | 65, 66, 67 | 3eqtr3d 2788 |
1
⊢ (𝜑 → (𝑁‘{𝑋}) = (𝑁‘{𝑌})) |