Step | Hyp | Ref
| Expression |
1 | | 3simpa 1051 |
. . . . . . 7
⊢ ((𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑋 ≠ 𝑌) → (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵)) |
2 | 1 | ad2antlr 759 |
. . . . . 6
⊢ (((𝑀 ∈ LMod ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑋 ≠ 𝑌)) ∧ (𝐴 ∈ 𝑆 ∧ 𝑋 = (𝐴 · 𝑌))) → (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵)) |
3 | | fvex 6113 |
. . . . . . . 8
⊢
(1r‘𝑅) ∈ V |
4 | | fvex 6113 |
. . . . . . . 8
⊢
((invg‘𝑅)‘𝐴) ∈ V |
5 | 3, 4 | pm3.2i 470 |
. . . . . . 7
⊢
((1r‘𝑅) ∈ V ∧
((invg‘𝑅)‘𝐴) ∈ V) |
6 | 5 | a1i 11 |
. . . . . 6
⊢ (((𝑀 ∈ LMod ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑋 ≠ 𝑌)) ∧ (𝐴 ∈ 𝑆 ∧ 𝑋 = (𝐴 · 𝑌))) → ((1r‘𝑅) ∈ V ∧
((invg‘𝑅)‘𝐴) ∈ V)) |
7 | | simp3 1056 |
. . . . . . 7
⊢ ((𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑋 ≠ 𝑌) → 𝑋 ≠ 𝑌) |
8 | 7 | ad2antlr 759 |
. . . . . 6
⊢ (((𝑀 ∈ LMod ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑋 ≠ 𝑌)) ∧ (𝐴 ∈ 𝑆 ∧ 𝑋 = (𝐴 · 𝑌))) → 𝑋 ≠ 𝑌) |
9 | | fprg 6327 |
. . . . . 6
⊢ (((𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) ∧ ((1r‘𝑅) ∈ V ∧
((invg‘𝑅)‘𝐴) ∈ V) ∧ 𝑋 ≠ 𝑌) → {〈𝑋, (1r‘𝑅)〉, 〈𝑌, ((invg‘𝑅)‘𝐴)〉}:{𝑋, 𝑌}⟶{(1r‘𝑅), ((invg‘𝑅)‘𝐴)}) |
10 | 2, 6, 8, 9 | syl3anc 1318 |
. . . . 5
⊢ (((𝑀 ∈ LMod ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑋 ≠ 𝑌)) ∧ (𝐴 ∈ 𝑆 ∧ 𝑋 = (𝐴 · 𝑌))) → {〈𝑋, (1r‘𝑅)〉, 〈𝑌, ((invg‘𝑅)‘𝐴)〉}:{𝑋, 𝑌}⟶{(1r‘𝑅), ((invg‘𝑅)‘𝐴)}) |
11 | | prfi 8120 |
. . . . . 6
⊢ {𝑋, 𝑌} ∈ Fin |
12 | 11 | a1i 11 |
. . . . 5
⊢ (((𝑀 ∈ LMod ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑋 ≠ 𝑌)) ∧ (𝐴 ∈ 𝑆 ∧ 𝑋 = (𝐴 · 𝑌))) → {𝑋, 𝑌} ∈ Fin) |
13 | | snlindsntor.0 |
. . . . . . 7
⊢ 0 =
(0g‘𝑅) |
14 | | fvex 6113 |
. . . . . . 7
⊢
(0g‘𝑅) ∈ V |
15 | 13, 14 | eqeltri 2684 |
. . . . . 6
⊢ 0 ∈
V |
16 | 15 | a1i 11 |
. . . . 5
⊢ (((𝑀 ∈ LMod ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑋 ≠ 𝑌)) ∧ (𝐴 ∈ 𝑆 ∧ 𝑋 = (𝐴 · 𝑌))) → 0 ∈ V) |
17 | 10, 12, 16 | fdmfifsupp 8168 |
. . . 4
⊢ (((𝑀 ∈ LMod ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑋 ≠ 𝑌)) ∧ (𝐴 ∈ 𝑆 ∧ 𝑋 = (𝐴 · 𝑌))) → {〈𝑋, (1r‘𝑅)〉, 〈𝑌, ((invg‘𝑅)‘𝐴)〉} finSupp 0 ) |
18 | 7 | anim2i 591 |
. . . . . . 7
⊢ ((𝑀 ∈ LMod ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑋 ≠ 𝑌)) → (𝑀 ∈ LMod ∧ 𝑋 ≠ 𝑌)) |
19 | 18 | adantr 480 |
. . . . . 6
⊢ (((𝑀 ∈ LMod ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑋 ≠ 𝑌)) ∧ (𝐴 ∈ 𝑆 ∧ 𝑋 = (𝐴 · 𝑌))) → (𝑀 ∈ LMod ∧ 𝑋 ≠ 𝑌)) |
20 | | snlindsntor.r |
. . . . . . . . 9
⊢ 𝑅 = (Scalar‘𝑀) |
21 | | snlindsntor.s |
. . . . . . . . 9
⊢ 𝑆 = (Base‘𝑅) |
22 | | eqid 2610 |
. . . . . . . . 9
⊢
(1r‘𝑅) = (1r‘𝑅) |
23 | 20, 21, 22 | lmod1cl 18713 |
. . . . . . . 8
⊢ (𝑀 ∈ LMod →
(1r‘𝑅)
∈ 𝑆) |
24 | | simp1 1054 |
. . . . . . . 8
⊢ ((𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑋 ≠ 𝑌) → 𝑋 ∈ 𝐵) |
25 | 23, 24 | anim12ci 589 |
. . . . . . 7
⊢ ((𝑀 ∈ LMod ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑋 ≠ 𝑌)) → (𝑋 ∈ 𝐵 ∧ (1r‘𝑅) ∈ 𝑆)) |
26 | 25 | adantr 480 |
. . . . . 6
⊢ (((𝑀 ∈ LMod ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑋 ≠ 𝑌)) ∧ (𝐴 ∈ 𝑆 ∧ 𝑋 = (𝐴 · 𝑌))) → (𝑋 ∈ 𝐵 ∧ (1r‘𝑅) ∈ 𝑆)) |
27 | | simp2 1055 |
. . . . . . 7
⊢ ((𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑋 ≠ 𝑌) → 𝑌 ∈ 𝐵) |
28 | 27 | ad2antlr 759 |
. . . . . 6
⊢ (((𝑀 ∈ LMod ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑋 ≠ 𝑌)) ∧ (𝐴 ∈ 𝑆 ∧ 𝑋 = (𝐴 · 𝑌))) → 𝑌 ∈ 𝐵) |
29 | 20 | lmodfgrp 18695 |
. . . . . . . 8
⊢ (𝑀 ∈ LMod → 𝑅 ∈ Grp) |
30 | 29 | adantr 480 |
. . . . . . 7
⊢ ((𝑀 ∈ LMod ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑋 ≠ 𝑌)) → 𝑅 ∈ Grp) |
31 | | simpl 472 |
. . . . . . 7
⊢ ((𝐴 ∈ 𝑆 ∧ 𝑋 = (𝐴 · 𝑌)) → 𝐴 ∈ 𝑆) |
32 | | eqid 2610 |
. . . . . . . 8
⊢
(invg‘𝑅) = (invg‘𝑅) |
33 | 21, 32 | grpinvcl 17290 |
. . . . . . 7
⊢ ((𝑅 ∈ Grp ∧ 𝐴 ∈ 𝑆) → ((invg‘𝑅)‘𝐴) ∈ 𝑆) |
34 | 30, 31, 33 | syl2an 493 |
. . . . . 6
⊢ (((𝑀 ∈ LMod ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑋 ≠ 𝑌)) ∧ (𝐴 ∈ 𝑆 ∧ 𝑋 = (𝐴 · 𝑌))) → ((invg‘𝑅)‘𝐴) ∈ 𝑆) |
35 | | snlindsntor.b |
. . . . . . 7
⊢ 𝐵 = (Base‘𝑀) |
36 | | snlindsntor.t |
. . . . . . 7
⊢ · = (
·𝑠 ‘𝑀) |
37 | | eqid 2610 |
. . . . . . 7
⊢
(+g‘𝑀) = (+g‘𝑀) |
38 | | eqid 2610 |
. . . . . . 7
⊢
{〈𝑋,
(1r‘𝑅)〉, 〈𝑌, ((invg‘𝑅)‘𝐴)〉} = {〈𝑋, (1r‘𝑅)〉, 〈𝑌, ((invg‘𝑅)‘𝐴)〉} |
39 | 35, 20, 21, 36, 37, 38 | lincvalpr 42001 |
. . . . . 6
⊢ (((𝑀 ∈ LMod ∧ 𝑋 ≠ 𝑌) ∧ (𝑋 ∈ 𝐵 ∧ (1r‘𝑅) ∈ 𝑆) ∧ (𝑌 ∈ 𝐵 ∧ ((invg‘𝑅)‘𝐴) ∈ 𝑆)) → ({〈𝑋, (1r‘𝑅)〉, 〈𝑌, ((invg‘𝑅)‘𝐴)〉} ( linC ‘𝑀){𝑋, 𝑌}) = (((1r‘𝑅) · 𝑋)(+g‘𝑀)(((invg‘𝑅)‘𝐴) · 𝑌))) |
40 | 19, 26, 28, 34, 39 | syl112anc 1322 |
. . . . 5
⊢ (((𝑀 ∈ LMod ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑋 ≠ 𝑌)) ∧ (𝐴 ∈ 𝑆 ∧ 𝑋 = (𝐴 · 𝑌))) → ({〈𝑋, (1r‘𝑅)〉, 〈𝑌, ((invg‘𝑅)‘𝐴)〉} ( linC ‘𝑀){𝑋, 𝑌}) = (((1r‘𝑅) · 𝑋)(+g‘𝑀)(((invg‘𝑅)‘𝐴) · 𝑌))) |
41 | | simpll 786 |
. . . . . . 7
⊢ (((𝑀 ∈ LMod ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑋 ≠ 𝑌)) ∧ (𝐴 ∈ 𝑆 ∧ 𝑋 = (𝐴 · 𝑌))) → 𝑀 ∈ LMod) |
42 | 24 | ad2antlr 759 |
. . . . . . . 8
⊢ (((𝑀 ∈ LMod ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑋 ≠ 𝑌)) ∧ (𝐴 ∈ 𝑆 ∧ 𝑋 = (𝐴 · 𝑌))) → 𝑋 ∈ 𝐵) |
43 | 31 | adantl 481 |
. . . . . . . 8
⊢ (((𝑀 ∈ LMod ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑋 ≠ 𝑌)) ∧ (𝐴 ∈ 𝑆 ∧ 𝑋 = (𝐴 · 𝑌))) → 𝐴 ∈ 𝑆) |
44 | 42, 28, 43 | 3jca 1235 |
. . . . . . 7
⊢ (((𝑀 ∈ LMod ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑋 ≠ 𝑌)) ∧ (𝐴 ∈ 𝑆 ∧ 𝑋 = (𝐴 · 𝑌))) → (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝐴 ∈ 𝑆)) |
45 | 41, 44 | jca 553 |
. . . . . 6
⊢ (((𝑀 ∈ LMod ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑋 ≠ 𝑌)) ∧ (𝐴 ∈ 𝑆 ∧ 𝑋 = (𝐴 · 𝑌))) → (𝑀 ∈ LMod ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝐴 ∈ 𝑆))) |
46 | | simprr 792 |
. . . . . 6
⊢ (((𝑀 ∈ LMod ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑋 ≠ 𝑌)) ∧ (𝐴 ∈ 𝑆 ∧ 𝑋 = (𝐴 · 𝑌))) → 𝑋 = (𝐴 · 𝑌)) |
47 | | snlindsntor.z |
. . . . . . 7
⊢ 𝑍 = (0g‘𝑀) |
48 | 35, 20, 21, 13, 47, 36, 22, 32 | ldepsprlem 42055 |
. . . . . 6
⊢ ((𝑀 ∈ LMod ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝐴 ∈ 𝑆)) → (𝑋 = (𝐴 · 𝑌) → (((1r‘𝑅) · 𝑋)(+g‘𝑀)(((invg‘𝑅)‘𝐴) · 𝑌)) = 𝑍)) |
49 | 45, 46, 48 | sylc 63 |
. . . . 5
⊢ (((𝑀 ∈ LMod ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑋 ≠ 𝑌)) ∧ (𝐴 ∈ 𝑆 ∧ 𝑋 = (𝐴 · 𝑌))) → (((1r‘𝑅) · 𝑋)(+g‘𝑀)(((invg‘𝑅)‘𝐴) · 𝑌)) = 𝑍) |
50 | 40, 49 | eqtrd 2644 |
. . . 4
⊢ (((𝑀 ∈ LMod ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑋 ≠ 𝑌)) ∧ (𝐴 ∈ 𝑆 ∧ 𝑋 = (𝐴 · 𝑌))) → ({〈𝑋, (1r‘𝑅)〉, 〈𝑌, ((invg‘𝑅)‘𝐴)〉} ( linC ‘𝑀){𝑋, 𝑌}) = 𝑍) |
51 | 20 | lmodring 18694 |
. . . . . . . . . 10
⊢ (𝑀 ∈ LMod → 𝑅 ∈ Ring) |
52 | | eqcom 2617 |
. . . . . . . . . . . 12
⊢
((1r‘𝑅) = (0g‘𝑅) ↔ (0g‘𝑅) = (1r‘𝑅)) |
53 | | eqid 2610 |
. . . . . . . . . . . . . . 15
⊢
(0g‘𝑅) = (0g‘𝑅) |
54 | 21, 53, 22 | 01eq0ring 19093 |
. . . . . . . . . . . . . 14
⊢ ((𝑅 ∈ Ring ∧
(0g‘𝑅) =
(1r‘𝑅))
→ 𝑆 =
{(0g‘𝑅)}) |
55 | | sneq 4135 |
. . . . . . . . . . . . . . . . 17
⊢
((0g‘𝑅) = (1r‘𝑅) → {(0g‘𝑅)} = {(1r‘𝑅)}) |
56 | 55 | eqeq2d 2620 |
. . . . . . . . . . . . . . . 16
⊢
((0g‘𝑅) = (1r‘𝑅) → (𝑆 = {(0g‘𝑅)} ↔ 𝑆 = {(1r‘𝑅)})) |
57 | | eleq2 2677 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑆 = {(1r‘𝑅)} → (𝐴 ∈ 𝑆 ↔ 𝐴 ∈ {(1r‘𝑅)})) |
58 | | elsni 4142 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝐴 ∈
{(1r‘𝑅)}
→ 𝐴 =
(1r‘𝑅)) |
59 | | oveq1 6556 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝐴 = (1r‘𝑅) → (𝐴 · 𝑌) = ((1r‘𝑅) · 𝑌)) |
60 | 59 | eqeq2d 2620 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝐴 = (1r‘𝑅) → (𝑋 = (𝐴 · 𝑌) ↔ 𝑋 = ((1r‘𝑅) · 𝑌))) |
61 | 27 | anim1i 590 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ (((𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑋 ≠ 𝑌) ∧ 𝑀 ∈ LMod) → (𝑌 ∈ 𝐵 ∧ 𝑀 ∈ LMod)) |
62 | 61 | ancomd 466 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ (((𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑋 ≠ 𝑌) ∧ 𝑀 ∈ LMod) → (𝑀 ∈ LMod ∧ 𝑌 ∈ 𝐵)) |
63 | 35, 20, 36, 22 | lmodvs1 18714 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ ((𝑀 ∈ LMod ∧ 𝑌 ∈ 𝐵) → ((1r‘𝑅) · 𝑌) = 𝑌) |
64 | 62, 63 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (((𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑋 ≠ 𝑌) ∧ 𝑀 ∈ LMod) →
((1r‘𝑅)
·
𝑌) = 𝑌) |
65 | 64 | eqeq2d 2620 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (((𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑋 ≠ 𝑌) ∧ 𝑀 ∈ LMod) → (𝑋 = ((1r‘𝑅) · 𝑌) ↔ 𝑋 = 𝑌)) |
66 | | eqneqall 2793 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ (𝑋 = 𝑌 → (𝑋 ≠ 𝑌 → (¬ (1r‘𝑅) = (0g‘𝑅) ∨
((invg‘𝑅)‘𝐴) ≠ 0 ))) |
67 | 66 | com12 32 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ (𝑋 ≠ 𝑌 → (𝑋 = 𝑌 → (¬ (1r‘𝑅) = (0g‘𝑅) ∨
((invg‘𝑅)‘𝐴) ≠ 0 ))) |
68 | 67 | 3ad2ant3 1077 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ ((𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑋 ≠ 𝑌) → (𝑋 = 𝑌 → (¬ (1r‘𝑅) = (0g‘𝑅) ∨
((invg‘𝑅)‘𝐴) ≠ 0 ))) |
69 | 68 | adantr 480 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (((𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑋 ≠ 𝑌) ∧ 𝑀 ∈ LMod) → (𝑋 = 𝑌 → (¬ (1r‘𝑅) = (0g‘𝑅) ∨
((invg‘𝑅)‘𝐴) ≠ 0 ))) |
70 | 65, 69 | sylbid 229 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (((𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑋 ≠ 𝑌) ∧ 𝑀 ∈ LMod) → (𝑋 = ((1r‘𝑅) · 𝑌) → (¬ (1r‘𝑅) = (0g‘𝑅) ∨
((invg‘𝑅)‘𝐴) ≠ 0 ))) |
71 | 70 | ex 449 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑋 ≠ 𝑌) → (𝑀 ∈ LMod → (𝑋 = ((1r‘𝑅) · 𝑌) → (¬ (1r‘𝑅) = (0g‘𝑅) ∨
((invg‘𝑅)‘𝐴) ≠ 0 )))) |
72 | 71 | com3r 85 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑋 = ((1r‘𝑅) · 𝑌) → ((𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑋 ≠ 𝑌) → (𝑀 ∈ LMod → (¬
(1r‘𝑅) =
(0g‘𝑅)
∨ ((invg‘𝑅)‘𝐴) ≠ 0 )))) |
73 | 60, 72 | syl6bi 242 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝐴 = (1r‘𝑅) → (𝑋 = (𝐴 · 𝑌) → ((𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑋 ≠ 𝑌) → (𝑀 ∈ LMod → (¬
(1r‘𝑅) =
(0g‘𝑅)
∨ ((invg‘𝑅)‘𝐴) ≠ 0 ))))) |
74 | 58, 73 | syl 17 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝐴 ∈
{(1r‘𝑅)}
→ (𝑋 = (𝐴 · 𝑌) → ((𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑋 ≠ 𝑌) → (𝑀 ∈ LMod → (¬
(1r‘𝑅) =
(0g‘𝑅)
∨ ((invg‘𝑅)‘𝐴) ≠ 0 ))))) |
75 | 57, 74 | syl6bi 242 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑆 = {(1r‘𝑅)} → (𝐴 ∈ 𝑆 → (𝑋 = (𝐴 · 𝑌) → ((𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑋 ≠ 𝑌) → (𝑀 ∈ LMod → (¬
(1r‘𝑅) =
(0g‘𝑅)
∨ ((invg‘𝑅)‘𝐴) ≠ 0 )))))) |
76 | 75 | impd 446 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑆 = {(1r‘𝑅)} → ((𝐴 ∈ 𝑆 ∧ 𝑋 = (𝐴 · 𝑌)) → ((𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑋 ≠ 𝑌) → (𝑀 ∈ LMod → (¬
(1r‘𝑅) =
(0g‘𝑅)
∨ ((invg‘𝑅)‘𝐴) ≠ 0 ))))) |
77 | 76 | com23 84 |
. . . . . . . . . . . . . . . 16
⊢ (𝑆 = {(1r‘𝑅)} → ((𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑋 ≠ 𝑌) → ((𝐴 ∈ 𝑆 ∧ 𝑋 = (𝐴 · 𝑌)) → (𝑀 ∈ LMod → (¬
(1r‘𝑅) =
(0g‘𝑅)
∨ ((invg‘𝑅)‘𝐴) ≠ 0 ))))) |
78 | 56, 77 | syl6bi 242 |
. . . . . . . . . . . . . . 15
⊢
((0g‘𝑅) = (1r‘𝑅) → (𝑆 = {(0g‘𝑅)} → ((𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑋 ≠ 𝑌) → ((𝐴 ∈ 𝑆 ∧ 𝑋 = (𝐴 · 𝑌)) → (𝑀 ∈ LMod → (¬
(1r‘𝑅) =
(0g‘𝑅)
∨ ((invg‘𝑅)‘𝐴) ≠ 0 )))))) |
79 | 78 | adantl 481 |
. . . . . . . . . . . . . 14
⊢ ((𝑅 ∈ Ring ∧
(0g‘𝑅) =
(1r‘𝑅))
→ (𝑆 =
{(0g‘𝑅)}
→ ((𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑋 ≠ 𝑌) → ((𝐴 ∈ 𝑆 ∧ 𝑋 = (𝐴 · 𝑌)) → (𝑀 ∈ LMod → (¬
(1r‘𝑅) =
(0g‘𝑅)
∨ ((invg‘𝑅)‘𝐴) ≠ 0 )))))) |
80 | 54, 79 | mpd 15 |
. . . . . . . . . . . . 13
⊢ ((𝑅 ∈ Ring ∧
(0g‘𝑅) =
(1r‘𝑅))
→ ((𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑋 ≠ 𝑌) → ((𝐴 ∈ 𝑆 ∧ 𝑋 = (𝐴 · 𝑌)) → (𝑀 ∈ LMod → (¬
(1r‘𝑅) =
(0g‘𝑅)
∨ ((invg‘𝑅)‘𝐴) ≠ 0 ))))) |
81 | 80 | ex 449 |
. . . . . . . . . . . 12
⊢ (𝑅 ∈ Ring →
((0g‘𝑅) =
(1r‘𝑅)
→ ((𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑋 ≠ 𝑌) → ((𝐴 ∈ 𝑆 ∧ 𝑋 = (𝐴 · 𝑌)) → (𝑀 ∈ LMod → (¬
(1r‘𝑅) =
(0g‘𝑅)
∨ ((invg‘𝑅)‘𝐴) ≠ 0 )))))) |
82 | 52, 81 | syl5bi 231 |
. . . . . . . . . . 11
⊢ (𝑅 ∈ Ring →
((1r‘𝑅) =
(0g‘𝑅)
→ ((𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑋 ≠ 𝑌) → ((𝐴 ∈ 𝑆 ∧ 𝑋 = (𝐴 · 𝑌)) → (𝑀 ∈ LMod → (¬
(1r‘𝑅) =
(0g‘𝑅)
∨ ((invg‘𝑅)‘𝐴) ≠ 0 )))))) |
83 | 82 | com25 97 |
. . . . . . . . . 10
⊢ (𝑅 ∈ Ring → (𝑀 ∈ LMod → ((𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑋 ≠ 𝑌) → ((𝐴 ∈ 𝑆 ∧ 𝑋 = (𝐴 · 𝑌)) → ((1r‘𝑅) = (0g‘𝑅) → (¬
(1r‘𝑅) =
(0g‘𝑅)
∨ ((invg‘𝑅)‘𝐴) ≠ 0 )))))) |
84 | 51, 83 | mpcom 37 |
. . . . . . . . 9
⊢ (𝑀 ∈ LMod → ((𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑋 ≠ 𝑌) → ((𝐴 ∈ 𝑆 ∧ 𝑋 = (𝐴 · 𝑌)) → ((1r‘𝑅) = (0g‘𝑅) → (¬
(1r‘𝑅) =
(0g‘𝑅)
∨ ((invg‘𝑅)‘𝐴) ≠ 0 ))))) |
85 | 84 | imp31 447 |
. . . . . . . 8
⊢ (((𝑀 ∈ LMod ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑋 ≠ 𝑌)) ∧ (𝐴 ∈ 𝑆 ∧ 𝑋 = (𝐴 · 𝑌))) → ((1r‘𝑅) = (0g‘𝑅) → (¬
(1r‘𝑅) =
(0g‘𝑅)
∨ ((invg‘𝑅)‘𝐴) ≠ 0 ))) |
86 | | orc 399 |
. . . . . . . 8
⊢ (¬
(1r‘𝑅) =
(0g‘𝑅)
→ (¬ (1r‘𝑅) = (0g‘𝑅) ∨ ((invg‘𝑅)‘𝐴) ≠ 0 )) |
87 | 85, 86 | pm2.61d1 170 |
. . . . . . 7
⊢ (((𝑀 ∈ LMod ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑋 ≠ 𝑌)) ∧ (𝐴 ∈ 𝑆 ∧ 𝑋 = (𝐴 · 𝑌))) → (¬ (1r‘𝑅) = (0g‘𝑅) ∨
((invg‘𝑅)‘𝐴) ≠ 0 )) |
88 | 13 | eqeq2i 2622 |
. . . . . . . . 9
⊢
((1r‘𝑅) = 0 ↔
(1r‘𝑅) =
(0g‘𝑅)) |
89 | 88 | necon3abii 2828 |
. . . . . . . 8
⊢
((1r‘𝑅) ≠ 0 ↔ ¬
(1r‘𝑅) =
(0g‘𝑅)) |
90 | 89 | orbi1i 541 |
. . . . . . 7
⊢
(((1r‘𝑅) ≠ 0 ∨
((invg‘𝑅)‘𝐴) ≠ 0 ) ↔ (¬
(1r‘𝑅) =
(0g‘𝑅)
∨ ((invg‘𝑅)‘𝐴) ≠ 0 )) |
91 | 87, 90 | sylibr 223 |
. . . . . 6
⊢ (((𝑀 ∈ LMod ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑋 ≠ 𝑌)) ∧ (𝐴 ∈ 𝑆 ∧ 𝑋 = (𝐴 · 𝑌))) → ((1r‘𝑅) ≠ 0 ∨
((invg‘𝑅)‘𝐴) ≠ 0 )) |
92 | 3 | a1i 11 |
. . . . . . . . 9
⊢ (((𝑀 ∈ LMod ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑋 ≠ 𝑌)) ∧ (𝐴 ∈ 𝑆 ∧ 𝑋 = (𝐴 · 𝑌))) → (1r‘𝑅) ∈ V) |
93 | | fvpr1g 6363 |
. . . . . . . . 9
⊢ ((𝑋 ∈ 𝐵 ∧ (1r‘𝑅) ∈ V ∧ 𝑋 ≠ 𝑌) → ({〈𝑋, (1r‘𝑅)〉, 〈𝑌, ((invg‘𝑅)‘𝐴)〉}‘𝑋) = (1r‘𝑅)) |
94 | 42, 92, 8, 93 | syl3anc 1318 |
. . . . . . . 8
⊢ (((𝑀 ∈ LMod ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑋 ≠ 𝑌)) ∧ (𝐴 ∈ 𝑆 ∧ 𝑋 = (𝐴 · 𝑌))) → ({〈𝑋, (1r‘𝑅)〉, 〈𝑌, ((invg‘𝑅)‘𝐴)〉}‘𝑋) = (1r‘𝑅)) |
95 | 94 | neeq1d 2841 |
. . . . . . 7
⊢ (((𝑀 ∈ LMod ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑋 ≠ 𝑌)) ∧ (𝐴 ∈ 𝑆 ∧ 𝑋 = (𝐴 · 𝑌))) → (({〈𝑋, (1r‘𝑅)〉, 〈𝑌, ((invg‘𝑅)‘𝐴)〉}‘𝑋) ≠ 0 ↔
(1r‘𝑅)
≠ 0
)) |
96 | 4 | a1i 11 |
. . . . . . . . 9
⊢ (((𝑀 ∈ LMod ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑋 ≠ 𝑌)) ∧ (𝐴 ∈ 𝑆 ∧ 𝑋 = (𝐴 · 𝑌))) → ((invg‘𝑅)‘𝐴) ∈ V) |
97 | | fvpr2g 6364 |
. . . . . . . . 9
⊢ ((𝑌 ∈ 𝐵 ∧ ((invg‘𝑅)‘𝐴) ∈ V ∧ 𝑋 ≠ 𝑌) → ({〈𝑋, (1r‘𝑅)〉, 〈𝑌, ((invg‘𝑅)‘𝐴)〉}‘𝑌) = ((invg‘𝑅)‘𝐴)) |
98 | 28, 96, 8, 97 | syl3anc 1318 |
. . . . . . . 8
⊢ (((𝑀 ∈ LMod ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑋 ≠ 𝑌)) ∧ (𝐴 ∈ 𝑆 ∧ 𝑋 = (𝐴 · 𝑌))) → ({〈𝑋, (1r‘𝑅)〉, 〈𝑌, ((invg‘𝑅)‘𝐴)〉}‘𝑌) = ((invg‘𝑅)‘𝐴)) |
99 | 98 | neeq1d 2841 |
. . . . . . 7
⊢ (((𝑀 ∈ LMod ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑋 ≠ 𝑌)) ∧ (𝐴 ∈ 𝑆 ∧ 𝑋 = (𝐴 · 𝑌))) → (({〈𝑋, (1r‘𝑅)〉, 〈𝑌, ((invg‘𝑅)‘𝐴)〉}‘𝑌) ≠ 0 ↔
((invg‘𝑅)‘𝐴) ≠ 0 )) |
100 | 95, 99 | orbi12d 742 |
. . . . . 6
⊢ (((𝑀 ∈ LMod ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑋 ≠ 𝑌)) ∧ (𝐴 ∈ 𝑆 ∧ 𝑋 = (𝐴 · 𝑌))) → ((({〈𝑋, (1r‘𝑅)〉, 〈𝑌, ((invg‘𝑅)‘𝐴)〉}‘𝑋) ≠ 0 ∨ ({〈𝑋, (1r‘𝑅)〉, 〈𝑌, ((invg‘𝑅)‘𝐴)〉}‘𝑌) ≠ 0 ) ↔
((1r‘𝑅)
≠ 0
∨ ((invg‘𝑅)‘𝐴) ≠ 0 ))) |
101 | 91, 100 | mpbird 246 |
. . . . 5
⊢ (((𝑀 ∈ LMod ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑋 ≠ 𝑌)) ∧ (𝐴 ∈ 𝑆 ∧ 𝑋 = (𝐴 · 𝑌))) → (({〈𝑋, (1r‘𝑅)〉, 〈𝑌, ((invg‘𝑅)‘𝐴)〉}‘𝑋) ≠ 0 ∨ ({〈𝑋, (1r‘𝑅)〉, 〈𝑌, ((invg‘𝑅)‘𝐴)〉}‘𝑌) ≠ 0 )) |
102 | | fveq2 6103 |
. . . . . . . 8
⊢ (𝑣 = 𝑋 → ({〈𝑋, (1r‘𝑅)〉, 〈𝑌, ((invg‘𝑅)‘𝐴)〉}‘𝑣) = ({〈𝑋, (1r‘𝑅)〉, 〈𝑌, ((invg‘𝑅)‘𝐴)〉}‘𝑋)) |
103 | 102 | neeq1d 2841 |
. . . . . . 7
⊢ (𝑣 = 𝑋 → (({〈𝑋, (1r‘𝑅)〉, 〈𝑌, ((invg‘𝑅)‘𝐴)〉}‘𝑣) ≠ 0 ↔ ({〈𝑋, (1r‘𝑅)〉, 〈𝑌, ((invg‘𝑅)‘𝐴)〉}‘𝑋) ≠ 0 )) |
104 | | fveq2 6103 |
. . . . . . . 8
⊢ (𝑣 = 𝑌 → ({〈𝑋, (1r‘𝑅)〉, 〈𝑌, ((invg‘𝑅)‘𝐴)〉}‘𝑣) = ({〈𝑋, (1r‘𝑅)〉, 〈𝑌, ((invg‘𝑅)‘𝐴)〉}‘𝑌)) |
105 | 104 | neeq1d 2841 |
. . . . . . 7
⊢ (𝑣 = 𝑌 → (({〈𝑋, (1r‘𝑅)〉, 〈𝑌, ((invg‘𝑅)‘𝐴)〉}‘𝑣) ≠ 0 ↔ ({〈𝑋, (1r‘𝑅)〉, 〈𝑌, ((invg‘𝑅)‘𝐴)〉}‘𝑌) ≠ 0 )) |
106 | 103, 105 | rexprg 4182 |
. . . . . 6
⊢ ((𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) → (∃𝑣 ∈ {𝑋, 𝑌} ({〈𝑋, (1r‘𝑅)〉, 〈𝑌, ((invg‘𝑅)‘𝐴)〉}‘𝑣) ≠ 0 ↔ (({〈𝑋, (1r‘𝑅)〉, 〈𝑌, ((invg‘𝑅)‘𝐴)〉}‘𝑋) ≠ 0 ∨ ({〈𝑋, (1r‘𝑅)〉, 〈𝑌, ((invg‘𝑅)‘𝐴)〉}‘𝑌) ≠ 0 ))) |
107 | 2, 106 | syl 17 |
. . . . 5
⊢ (((𝑀 ∈ LMod ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑋 ≠ 𝑌)) ∧ (𝐴 ∈ 𝑆 ∧ 𝑋 = (𝐴 · 𝑌))) → (∃𝑣 ∈ {𝑋, 𝑌} ({〈𝑋, (1r‘𝑅)〉, 〈𝑌, ((invg‘𝑅)‘𝐴)〉}‘𝑣) ≠ 0 ↔ (({〈𝑋, (1r‘𝑅)〉, 〈𝑌, ((invg‘𝑅)‘𝐴)〉}‘𝑋) ≠ 0 ∨ ({〈𝑋, (1r‘𝑅)〉, 〈𝑌, ((invg‘𝑅)‘𝐴)〉}‘𝑌) ≠ 0 ))) |
108 | 101, 107 | mpbird 246 |
. . . 4
⊢ (((𝑀 ∈ LMod ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑋 ≠ 𝑌)) ∧ (𝐴 ∈ 𝑆 ∧ 𝑋 = (𝐴 · 𝑌))) → ∃𝑣 ∈ {𝑋, 𝑌} ({〈𝑋, (1r‘𝑅)〉, 〈𝑌, ((invg‘𝑅)‘𝐴)〉}‘𝑣) ≠ 0 ) |
109 | 23 | adantr 480 |
. . . . . . 7
⊢ ((𝑀 ∈ LMod ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑋 ≠ 𝑌)) → (1r‘𝑅) ∈ 𝑆) |
110 | 109 | adantr 480 |
. . . . . 6
⊢ (((𝑀 ∈ LMod ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑋 ≠ 𝑌)) ∧ (𝐴 ∈ 𝑆 ∧ 𝑋 = (𝐴 · 𝑌))) → (1r‘𝑅) ∈ 𝑆) |
111 | | fvex 6113 |
. . . . . . . 8
⊢
(Base‘𝑅)
∈ V |
112 | 21, 111 | eqeltri 2684 |
. . . . . . 7
⊢ 𝑆 ∈ V |
113 | 8, 112 | jctir 559 |
. . . . . 6
⊢ (((𝑀 ∈ LMod ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑋 ≠ 𝑌)) ∧ (𝐴 ∈ 𝑆 ∧ 𝑋 = (𝐴 · 𝑌))) → (𝑋 ≠ 𝑌 ∧ 𝑆 ∈ V)) |
114 | 38 | mapprop 41917 |
. . . . . 6
⊢ (((𝑋 ∈ 𝐵 ∧ (1r‘𝑅) ∈ 𝑆) ∧ (𝑌 ∈ 𝐵 ∧ ((invg‘𝑅)‘𝐴) ∈ 𝑆) ∧ (𝑋 ≠ 𝑌 ∧ 𝑆 ∈ V)) → {〈𝑋, (1r‘𝑅)〉, 〈𝑌, ((invg‘𝑅)‘𝐴)〉} ∈ (𝑆 ↑𝑚 {𝑋, 𝑌})) |
115 | 42, 110, 28, 34, 113, 114 | syl221anc 1329 |
. . . . 5
⊢ (((𝑀 ∈ LMod ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑋 ≠ 𝑌)) ∧ (𝐴 ∈ 𝑆 ∧ 𝑋 = (𝐴 · 𝑌))) → {〈𝑋, (1r‘𝑅)〉, 〈𝑌, ((invg‘𝑅)‘𝐴)〉} ∈ (𝑆 ↑𝑚 {𝑋, 𝑌})) |
116 | | breq1 4586 |
. . . . . . 7
⊢ (𝑓 = {〈𝑋, (1r‘𝑅)〉, 〈𝑌, ((invg‘𝑅)‘𝐴)〉} → (𝑓 finSupp 0 ↔ {〈𝑋, (1r‘𝑅)〉, 〈𝑌, ((invg‘𝑅)‘𝐴)〉} finSupp 0 )) |
117 | | oveq1 6556 |
. . . . . . . 8
⊢ (𝑓 = {〈𝑋, (1r‘𝑅)〉, 〈𝑌, ((invg‘𝑅)‘𝐴)〉} → (𝑓( linC ‘𝑀){𝑋, 𝑌}) = ({〈𝑋, (1r‘𝑅)〉, 〈𝑌, ((invg‘𝑅)‘𝐴)〉} ( linC ‘𝑀){𝑋, 𝑌})) |
118 | 117 | eqeq1d 2612 |
. . . . . . 7
⊢ (𝑓 = {〈𝑋, (1r‘𝑅)〉, 〈𝑌, ((invg‘𝑅)‘𝐴)〉} → ((𝑓( linC ‘𝑀){𝑋, 𝑌}) = 𝑍 ↔ ({〈𝑋, (1r‘𝑅)〉, 〈𝑌, ((invg‘𝑅)‘𝐴)〉} ( linC ‘𝑀){𝑋, 𝑌}) = 𝑍)) |
119 | | fveq1 6102 |
. . . . . . . . 9
⊢ (𝑓 = {〈𝑋, (1r‘𝑅)〉, 〈𝑌, ((invg‘𝑅)‘𝐴)〉} → (𝑓‘𝑣) = ({〈𝑋, (1r‘𝑅)〉, 〈𝑌, ((invg‘𝑅)‘𝐴)〉}‘𝑣)) |
120 | 119 | neeq1d 2841 |
. . . . . . . 8
⊢ (𝑓 = {〈𝑋, (1r‘𝑅)〉, 〈𝑌, ((invg‘𝑅)‘𝐴)〉} → ((𝑓‘𝑣) ≠ 0 ↔ ({〈𝑋, (1r‘𝑅)〉, 〈𝑌, ((invg‘𝑅)‘𝐴)〉}‘𝑣) ≠ 0 )) |
121 | 120 | rexbidv 3034 |
. . . . . . 7
⊢ (𝑓 = {〈𝑋, (1r‘𝑅)〉, 〈𝑌, ((invg‘𝑅)‘𝐴)〉} → (∃𝑣 ∈ {𝑋, 𝑌} (𝑓‘𝑣) ≠ 0 ↔ ∃𝑣 ∈ {𝑋, 𝑌} ({〈𝑋, (1r‘𝑅)〉, 〈𝑌, ((invg‘𝑅)‘𝐴)〉}‘𝑣) ≠ 0 )) |
122 | 116, 118,
121 | 3anbi123d 1391 |
. . . . . 6
⊢ (𝑓 = {〈𝑋, (1r‘𝑅)〉, 〈𝑌, ((invg‘𝑅)‘𝐴)〉} → ((𝑓 finSupp 0 ∧ (𝑓( linC ‘𝑀){𝑋, 𝑌}) = 𝑍 ∧ ∃𝑣 ∈ {𝑋, 𝑌} (𝑓‘𝑣) ≠ 0 ) ↔ ({〈𝑋, (1r‘𝑅)〉, 〈𝑌, ((invg‘𝑅)‘𝐴)〉} finSupp 0 ∧ ({〈𝑋, (1r‘𝑅)〉, 〈𝑌, ((invg‘𝑅)‘𝐴)〉} ( linC ‘𝑀){𝑋, 𝑌}) = 𝑍 ∧ ∃𝑣 ∈ {𝑋, 𝑌} ({〈𝑋, (1r‘𝑅)〉, 〈𝑌, ((invg‘𝑅)‘𝐴)〉}‘𝑣) ≠ 0 ))) |
123 | 122 | adantl 481 |
. . . . 5
⊢ ((((𝑀 ∈ LMod ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑋 ≠ 𝑌)) ∧ (𝐴 ∈ 𝑆 ∧ 𝑋 = (𝐴 · 𝑌))) ∧ 𝑓 = {〈𝑋, (1r‘𝑅)〉, 〈𝑌, ((invg‘𝑅)‘𝐴)〉}) → ((𝑓 finSupp 0 ∧ (𝑓( linC ‘𝑀){𝑋, 𝑌}) = 𝑍 ∧ ∃𝑣 ∈ {𝑋, 𝑌} (𝑓‘𝑣) ≠ 0 ) ↔ ({〈𝑋, (1r‘𝑅)〉, 〈𝑌, ((invg‘𝑅)‘𝐴)〉} finSupp 0 ∧ ({〈𝑋, (1r‘𝑅)〉, 〈𝑌, ((invg‘𝑅)‘𝐴)〉} ( linC ‘𝑀){𝑋, 𝑌}) = 𝑍 ∧ ∃𝑣 ∈ {𝑋, 𝑌} ({〈𝑋, (1r‘𝑅)〉, 〈𝑌, ((invg‘𝑅)‘𝐴)〉}‘𝑣) ≠ 0 ))) |
124 | 115, 123 | rspcedv 3286 |
. . . 4
⊢ (((𝑀 ∈ LMod ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑋 ≠ 𝑌)) ∧ (𝐴 ∈ 𝑆 ∧ 𝑋 = (𝐴 · 𝑌))) → (({〈𝑋, (1r‘𝑅)〉, 〈𝑌, ((invg‘𝑅)‘𝐴)〉} finSupp 0 ∧ ({〈𝑋, (1r‘𝑅)〉, 〈𝑌, ((invg‘𝑅)‘𝐴)〉} ( linC ‘𝑀){𝑋, 𝑌}) = 𝑍 ∧ ∃𝑣 ∈ {𝑋, 𝑌} ({〈𝑋, (1r‘𝑅)〉, 〈𝑌, ((invg‘𝑅)‘𝐴)〉}‘𝑣) ≠ 0 ) → ∃𝑓 ∈ (𝑆 ↑𝑚 {𝑋, 𝑌})(𝑓 finSupp 0 ∧ (𝑓( linC ‘𝑀){𝑋, 𝑌}) = 𝑍 ∧ ∃𝑣 ∈ {𝑋, 𝑌} (𝑓‘𝑣) ≠ 0 ))) |
125 | 17, 50, 108, 124 | mp3and 1419 |
. . 3
⊢ (((𝑀 ∈ LMod ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑋 ≠ 𝑌)) ∧ (𝐴 ∈ 𝑆 ∧ 𝑋 = (𝐴 · 𝑌))) → ∃𝑓 ∈ (𝑆 ↑𝑚 {𝑋, 𝑌})(𝑓 finSupp 0 ∧ (𝑓( linC ‘𝑀){𝑋, 𝑌}) = 𝑍 ∧ ∃𝑣 ∈ {𝑋, 𝑌} (𝑓‘𝑣) ≠ 0 )) |
126 | | prelpwi 4842 |
. . . . . 6
⊢ ((𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) → {𝑋, 𝑌} ∈ 𝒫 𝐵) |
127 | 126 | 3adant3 1074 |
. . . . 5
⊢ ((𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑋 ≠ 𝑌) → {𝑋, 𝑌} ∈ 𝒫 𝐵) |
128 | 127 | ad2antlr 759 |
. . . 4
⊢ (((𝑀 ∈ LMod ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑋 ≠ 𝑌)) ∧ (𝐴 ∈ 𝑆 ∧ 𝑋 = (𝐴 · 𝑌))) → {𝑋, 𝑌} ∈ 𝒫 𝐵) |
129 | 35, 47, 20, 21, 13 | islindeps 42036 |
. . . 4
⊢ ((𝑀 ∈ LMod ∧ {𝑋, 𝑌} ∈ 𝒫 𝐵) → ({𝑋, 𝑌} linDepS 𝑀 ↔ ∃𝑓 ∈ (𝑆 ↑𝑚 {𝑋, 𝑌})(𝑓 finSupp 0 ∧ (𝑓( linC ‘𝑀){𝑋, 𝑌}) = 𝑍 ∧ ∃𝑣 ∈ {𝑋, 𝑌} (𝑓‘𝑣) ≠ 0 ))) |
130 | 41, 128, 129 | syl2anc 691 |
. . 3
⊢ (((𝑀 ∈ LMod ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑋 ≠ 𝑌)) ∧ (𝐴 ∈ 𝑆 ∧ 𝑋 = (𝐴 · 𝑌))) → ({𝑋, 𝑌} linDepS 𝑀 ↔ ∃𝑓 ∈ (𝑆 ↑𝑚 {𝑋, 𝑌})(𝑓 finSupp 0 ∧ (𝑓( linC ‘𝑀){𝑋, 𝑌}) = 𝑍 ∧ ∃𝑣 ∈ {𝑋, 𝑌} (𝑓‘𝑣) ≠ 0 ))) |
131 | 125, 130 | mpbird 246 |
. 2
⊢ (((𝑀 ∈ LMod ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑋 ≠ 𝑌)) ∧ (𝐴 ∈ 𝑆 ∧ 𝑋 = (𝐴 · 𝑌))) → {𝑋, 𝑌} linDepS 𝑀) |
132 | 131 | ex 449 |
1
⊢ ((𝑀 ∈ LMod ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑋 ≠ 𝑌)) → ((𝐴 ∈ 𝑆 ∧ 𝑋 = (𝐴 · 𝑌)) → {𝑋, 𝑌} linDepS 𝑀)) |