Proof of Theorem frlmssuvc2
Step | Hyp | Ref
| Expression |
1 | | frlmssuvc2.l |
. . . . . . 7
⊢ (𝜑 → 𝐿 ∈ (𝐼 ∖ 𝐽)) |
2 | 1 | eldifad 3552 |
. . . . . 6
⊢ (𝜑 → 𝐿 ∈ 𝐼) |
3 | | frlmssuvc1.f |
. . . . . . . . 9
⊢ 𝐹 = (𝑅 freeLMod 𝐼) |
4 | | frlmssuvc1.b |
. . . . . . . . 9
⊢ 𝐵 = (Base‘𝐹) |
5 | | frlmssuvc1.k |
. . . . . . . . 9
⊢ 𝐾 = (Base‘𝑅) |
6 | | frlmssuvc1.i |
. . . . . . . . 9
⊢ (𝜑 → 𝐼 ∈ 𝑉) |
7 | | frlmssuvc2.x |
. . . . . . . . . 10
⊢ (𝜑 → 𝑋 ∈ (𝐾 ∖ { 0 })) |
8 | 7 | eldifad 3552 |
. . . . . . . . 9
⊢ (𝜑 → 𝑋 ∈ 𝐾) |
9 | | frlmssuvc1.r |
. . . . . . . . . . 11
⊢ (𝜑 → 𝑅 ∈ Ring) |
10 | | frlmssuvc1.u |
. . . . . . . . . . . 12
⊢ 𝑈 = (𝑅 unitVec 𝐼) |
11 | 10, 3, 4 | uvcff 19949 |
. . . . . . . . . . 11
⊢ ((𝑅 ∈ Ring ∧ 𝐼 ∈ 𝑉) → 𝑈:𝐼⟶𝐵) |
12 | 9, 6, 11 | syl2anc 691 |
. . . . . . . . . 10
⊢ (𝜑 → 𝑈:𝐼⟶𝐵) |
13 | 12, 2 | ffvelrnd 6268 |
. . . . . . . . 9
⊢ (𝜑 → (𝑈‘𝐿) ∈ 𝐵) |
14 | | frlmssuvc1.t |
. . . . . . . . 9
⊢ · = (
·𝑠 ‘𝐹) |
15 | | eqid 2610 |
. . . . . . . . 9
⊢
(.r‘𝑅) = (.r‘𝑅) |
16 | 3, 4, 5, 6, 8, 13,
2, 14, 15 | frlmvscaval 19929 |
. . . . . . . 8
⊢ (𝜑 → ((𝑋 · (𝑈‘𝐿))‘𝐿) = (𝑋(.r‘𝑅)((𝑈‘𝐿)‘𝐿))) |
17 | | eqid 2610 |
. . . . . . . . . 10
⊢
(1r‘𝑅) = (1r‘𝑅) |
18 | 10, 9, 6, 2, 17 | uvcvv1 19947 |
. . . . . . . . 9
⊢ (𝜑 → ((𝑈‘𝐿)‘𝐿) = (1r‘𝑅)) |
19 | 18 | oveq2d 6565 |
. . . . . . . 8
⊢ (𝜑 → (𝑋(.r‘𝑅)((𝑈‘𝐿)‘𝐿)) = (𝑋(.r‘𝑅)(1r‘𝑅))) |
20 | 5, 15, 17 | ringridm 18395 |
. . . . . . . . 9
⊢ ((𝑅 ∈ Ring ∧ 𝑋 ∈ 𝐾) → (𝑋(.r‘𝑅)(1r‘𝑅)) = 𝑋) |
21 | 9, 8, 20 | syl2anc 691 |
. . . . . . . 8
⊢ (𝜑 → (𝑋(.r‘𝑅)(1r‘𝑅)) = 𝑋) |
22 | 16, 19, 21 | 3eqtrd 2648 |
. . . . . . 7
⊢ (𝜑 → ((𝑋 · (𝑈‘𝐿))‘𝐿) = 𝑋) |
23 | | eldifsni 4261 |
. . . . . . . 8
⊢ (𝑋 ∈ (𝐾 ∖ { 0 }) → 𝑋 ≠ 0 ) |
24 | 7, 23 | syl 17 |
. . . . . . 7
⊢ (𝜑 → 𝑋 ≠ 0 ) |
25 | 22, 24 | eqnetrd 2849 |
. . . . . 6
⊢ (𝜑 → ((𝑋 · (𝑈‘𝐿))‘𝐿) ≠ 0 ) |
26 | | fveq2 6103 |
. . . . . . . 8
⊢ (𝑥 = 𝐿 → ((𝑋 · (𝑈‘𝐿))‘𝑥) = ((𝑋 · (𝑈‘𝐿))‘𝐿)) |
27 | 26 | neeq1d 2841 |
. . . . . . 7
⊢ (𝑥 = 𝐿 → (((𝑋 · (𝑈‘𝐿))‘𝑥) ≠ 0 ↔ ((𝑋 · (𝑈‘𝐿))‘𝐿) ≠ 0 )) |
28 | 27 | elrab 3331 |
. . . . . 6
⊢ (𝐿 ∈ {𝑥 ∈ 𝐼 ∣ ((𝑋 · (𝑈‘𝐿))‘𝑥) ≠ 0 } ↔ (𝐿 ∈ 𝐼 ∧ ((𝑋 · (𝑈‘𝐿))‘𝐿) ≠ 0 )) |
29 | 2, 25, 28 | sylanbrc 695 |
. . . . 5
⊢ (𝜑 → 𝐿 ∈ {𝑥 ∈ 𝐼 ∣ ((𝑋 · (𝑈‘𝐿))‘𝑥) ≠ 0 }) |
30 | 1 | eldifbd 3553 |
. . . . 5
⊢ (𝜑 → ¬ 𝐿 ∈ 𝐽) |
31 | | nelss 3627 |
. . . . 5
⊢ ((𝐿 ∈ {𝑥 ∈ 𝐼 ∣ ((𝑋 · (𝑈‘𝐿))‘𝑥) ≠ 0 } ∧ ¬ 𝐿 ∈ 𝐽) → ¬ {𝑥 ∈ 𝐼 ∣ ((𝑋 · (𝑈‘𝐿))‘𝑥) ≠ 0 } ⊆ 𝐽) |
32 | 29, 30, 31 | syl2anc 691 |
. . . 4
⊢ (𝜑 → ¬ {𝑥 ∈ 𝐼 ∣ ((𝑋 · (𝑈‘𝐿))‘𝑥) ≠ 0 } ⊆ 𝐽) |
33 | 3 | frlmlmod 19912 |
. . . . . . . . . 10
⊢ ((𝑅 ∈ Ring ∧ 𝐼 ∈ 𝑉) → 𝐹 ∈ LMod) |
34 | 9, 6, 33 | syl2anc 691 |
. . . . . . . . 9
⊢ (𝜑 → 𝐹 ∈ LMod) |
35 | 3 | frlmsca 19916 |
. . . . . . . . . . . . 13
⊢ ((𝑅 ∈ Ring ∧ 𝐼 ∈ 𝑉) → 𝑅 = (Scalar‘𝐹)) |
36 | 9, 6, 35 | syl2anc 691 |
. . . . . . . . . . . 12
⊢ (𝜑 → 𝑅 = (Scalar‘𝐹)) |
37 | 36 | fveq2d 6107 |
. . . . . . . . . . 11
⊢ (𝜑 → (Base‘𝑅) =
(Base‘(Scalar‘𝐹))) |
38 | 5, 37 | syl5eq 2656 |
. . . . . . . . . 10
⊢ (𝜑 → 𝐾 = (Base‘(Scalar‘𝐹))) |
39 | 8, 38 | eleqtrd 2690 |
. . . . . . . . 9
⊢ (𝜑 → 𝑋 ∈ (Base‘(Scalar‘𝐹))) |
40 | | eqid 2610 |
. . . . . . . . . 10
⊢
(Scalar‘𝐹) =
(Scalar‘𝐹) |
41 | | eqid 2610 |
. . . . . . . . . 10
⊢
(Base‘(Scalar‘𝐹)) = (Base‘(Scalar‘𝐹)) |
42 | 4, 40, 14, 41 | lmodvscl 18703 |
. . . . . . . . 9
⊢ ((𝐹 ∈ LMod ∧ 𝑋 ∈
(Base‘(Scalar‘𝐹)) ∧ (𝑈‘𝐿) ∈ 𝐵) → (𝑋 · (𝑈‘𝐿)) ∈ 𝐵) |
43 | 34, 39, 13, 42 | syl3anc 1318 |
. . . . . . . 8
⊢ (𝜑 → (𝑋 · (𝑈‘𝐿)) ∈ 𝐵) |
44 | 3, 5, 4 | frlmbasf 19923 |
. . . . . . . 8
⊢ ((𝐼 ∈ 𝑉 ∧ (𝑋 · (𝑈‘𝐿)) ∈ 𝐵) → (𝑋 · (𝑈‘𝐿)):𝐼⟶𝐾) |
45 | 6, 43, 44 | syl2anc 691 |
. . . . . . 7
⊢ (𝜑 → (𝑋 · (𝑈‘𝐿)):𝐼⟶𝐾) |
46 | | ffn 5958 |
. . . . . . 7
⊢ ((𝑋 · (𝑈‘𝐿)):𝐼⟶𝐾 → (𝑋 · (𝑈‘𝐿)) Fn 𝐼) |
47 | 45, 46 | syl 17 |
. . . . . 6
⊢ (𝜑 → (𝑋 · (𝑈‘𝐿)) Fn 𝐼) |
48 | | frlmssuvc1.z |
. . . . . . . 8
⊢ 0 =
(0g‘𝑅) |
49 | | fvex 6113 |
. . . . . . . 8
⊢
(0g‘𝑅) ∈ V |
50 | 48, 49 | eqeltri 2684 |
. . . . . . 7
⊢ 0 ∈
V |
51 | 50 | a1i 11 |
. . . . . 6
⊢ (𝜑 → 0 ∈ V) |
52 | | suppvalfn 7189 |
. . . . . 6
⊢ (((𝑋 · (𝑈‘𝐿)) Fn 𝐼 ∧ 𝐼 ∈ 𝑉 ∧ 0 ∈ V) → ((𝑋 · (𝑈‘𝐿)) supp 0 ) = {𝑥 ∈ 𝐼 ∣ ((𝑋 · (𝑈‘𝐿))‘𝑥) ≠ 0 }) |
53 | 47, 6, 51, 52 | syl3anc 1318 |
. . . . 5
⊢ (𝜑 → ((𝑋 · (𝑈‘𝐿)) supp 0 ) = {𝑥 ∈ 𝐼 ∣ ((𝑋 · (𝑈‘𝐿))‘𝑥) ≠ 0 }) |
54 | 53 | sseq1d 3595 |
. . . 4
⊢ (𝜑 → (((𝑋 · (𝑈‘𝐿)) supp 0 ) ⊆ 𝐽 ↔ {𝑥 ∈ 𝐼 ∣ ((𝑋 · (𝑈‘𝐿))‘𝑥) ≠ 0 } ⊆ 𝐽)) |
55 | 32, 54 | mtbird 314 |
. . 3
⊢ (𝜑 → ¬ ((𝑋 · (𝑈‘𝐿)) supp 0 ) ⊆ 𝐽) |
56 | 55 | intnand 953 |
. 2
⊢ (𝜑 → ¬ ((𝑋 · (𝑈‘𝐿)) ∈ 𝐵 ∧ ((𝑋 · (𝑈‘𝐿)) supp 0 ) ⊆ 𝐽)) |
57 | | oveq1 6556 |
. . . 4
⊢ (𝑥 = (𝑋 · (𝑈‘𝐿)) → (𝑥 supp 0 ) = ((𝑋 · (𝑈‘𝐿)) supp 0 )) |
58 | 57 | sseq1d 3595 |
. . 3
⊢ (𝑥 = (𝑋 · (𝑈‘𝐿)) → ((𝑥 supp 0 ) ⊆ 𝐽 ↔ ((𝑋 · (𝑈‘𝐿)) supp 0 ) ⊆ 𝐽)) |
59 | | frlmssuvc1.c |
. . 3
⊢ 𝐶 = {𝑥 ∈ 𝐵 ∣ (𝑥 supp 0 ) ⊆ 𝐽} |
60 | 58, 59 | elrab2 3333 |
. 2
⊢ ((𝑋 · (𝑈‘𝐿)) ∈ 𝐶 ↔ ((𝑋 · (𝑈‘𝐿)) ∈ 𝐵 ∧ ((𝑋 · (𝑈‘𝐿)) supp 0 ) ⊆ 𝐽)) |
61 | 56, 60 | sylnibr 318 |
1
⊢ (𝜑 → ¬ (𝑋 · (𝑈‘𝐿)) ∈ 𝐶) |