Proof of Theorem ldepsnlinc
Step | Hyp | Ref
| Expression |
1 | | eqid 2737 |
. . . 4
⊢
(ℤring freeLMod {0, 1}) = (ℤring
freeLMod {0, 1}) |
2 | 1 | zlmodzxzlmod 45363 |
. . 3
⊢
((ℤring freeLMod {0, 1}) ∈ LMod ∧
ℤring = (Scalar‘(ℤring freeLMod {0,
1}))) |
3 | 2 | simpli 487 |
. 2
⊢
(ℤring freeLMod {0, 1}) ∈ LMod |
4 | | 3z 12210 |
. . . . 5
⊢ 3 ∈
ℤ |
5 | | 6nn 11919 |
. . . . . 6
⊢ 6 ∈
ℕ |
6 | 5 | nnzi 12201 |
. . . . 5
⊢ 6 ∈
ℤ |
7 | 1 | zlmodzxzel 45364 |
. . . . 5
⊢ ((3
∈ ℤ ∧ 6 ∈ ℤ) → {〈0, 3〉, 〈1,
6〉} ∈ (Base‘(ℤring freeLMod {0,
1}))) |
8 | 4, 6, 7 | mp2an 692 |
. . . 4
⊢ {〈0,
3〉, 〈1, 6〉} ∈ (Base‘(ℤring freeLMod
{0, 1})) |
9 | | 2z 12209 |
. . . . 5
⊢ 2 ∈
ℤ |
10 | | 4z 12211 |
. . . . 5
⊢ 4 ∈
ℤ |
11 | 1 | zlmodzxzel 45364 |
. . . . 5
⊢ ((2
∈ ℤ ∧ 4 ∈ ℤ) → {〈0, 2〉, 〈1,
4〉} ∈ (Base‘(ℤring freeLMod {0,
1}))) |
12 | 9, 10, 11 | mp2an 692 |
. . . 4
⊢ {〈0,
2〉, 〈1, 4〉} ∈ (Base‘(ℤring freeLMod
{0, 1})) |
13 | | prelpwi 5332 |
. . . 4
⊢
(({〈0, 3〉, 〈1, 6〉} ∈
(Base‘(ℤring freeLMod {0, 1})) ∧ {〈0, 2〉,
〈1, 4〉} ∈ (Base‘(ℤring freeLMod {0, 1})))
→ {{〈0, 3〉, 〈1, 6〉}, {〈0, 2〉, 〈1,
4〉}} ∈ 𝒫 (Base‘(ℤring freeLMod {0,
1}))) |
14 | 8, 12, 13 | mp2an 692 |
. . 3
⊢
{{〈0, 3〉, 〈1, 6〉}, {〈0, 2〉, 〈1,
4〉}} ∈ 𝒫 (Base‘(ℤring freeLMod {0,
1})) |
15 | | eqid 2737 |
. . . . 5
⊢ {〈0,
3〉, 〈1, 6〉} = {〈0, 3〉, 〈1,
6〉} |
16 | | eqid 2737 |
. . . . 5
⊢ {〈0,
2〉, 〈1, 4〉} = {〈0, 2〉, 〈1,
4〉} |
17 | 1, 15, 16 | zlmodzxzldep 45518 |
. . . 4
⊢
{{〈0, 3〉, 〈1, 6〉}, {〈0, 2〉, 〈1,
4〉}} linDepS (ℤring freeLMod {0, 1}) |
18 | 1, 15, 16 | ldepsnlinclem1 45519 |
. . . . . . . 8
⊢ (𝑓 ∈
((Base‘ℤring) ↑m {{〈0, 2〉,
〈1, 4〉}}) → (𝑓( linC ‘(ℤring
freeLMod {0, 1})){{〈0, 2〉, 〈1, 4〉}}) ≠ {〈0,
3〉, 〈1, 6〉}) |
19 | | simpr 488 |
. . . . . . . . . . . 12
⊢
(((ℤring freeLMod {0, 1}) ∈ LMod ∧
ℤring = (Scalar‘(ℤring freeLMod {0,
1}))) → ℤring = (Scalar‘(ℤring
freeLMod {0, 1}))) |
20 | 19 | eqcomd 2743 |
. . . . . . . . . . 11
⊢
(((ℤring freeLMod {0, 1}) ∈ LMod ∧
ℤring = (Scalar‘(ℤring freeLMod {0,
1}))) → (Scalar‘(ℤring freeLMod {0, 1})) =
ℤring) |
21 | 2, 20 | ax-mp 5 |
. . . . . . . . . 10
⊢
(Scalar‘(ℤring freeLMod {0, 1})) =
ℤring |
22 | 21 | fveq2i 6720 |
. . . . . . . . 9
⊢
(Base‘(Scalar‘(ℤring freeLMod {0, 1}))) =
(Base‘ℤring) |
23 | 22 | oveq1i 7223 |
. . . . . . . 8
⊢
((Base‘(Scalar‘(ℤring freeLMod {0, 1})))
↑m {{〈0, 2〉, 〈1, 4〉}}) =
((Base‘ℤring) ↑m {{〈0, 2〉,
〈1, 4〉}}) |
24 | 18, 23 | eleq2s 2856 |
. . . . . . 7
⊢ (𝑓 ∈
((Base‘(Scalar‘(ℤring freeLMod {0, 1})))
↑m {{〈0, 2〉, 〈1, 4〉}}) → (𝑓( linC
‘(ℤring freeLMod {0, 1})){{〈0, 2〉, 〈1,
4〉}}) ≠ {〈0, 3〉, 〈1, 6〉}) |
25 | 24 | a1d 25 |
. . . . . 6
⊢ (𝑓 ∈
((Base‘(Scalar‘(ℤring freeLMod {0, 1})))
↑m {{〈0, 2〉, 〈1, 4〉}}) → (𝑓 finSupp
(0g‘(Scalar‘(ℤring freeLMod {0, 1})))
→ (𝑓( linC
‘(ℤring freeLMod {0, 1})){{〈0, 2〉, 〈1,
4〉}}) ≠ {〈0, 3〉, 〈1, 6〉})) |
26 | 25 | rgen 3071 |
. . . . 5
⊢
∀𝑓 ∈
((Base‘(Scalar‘(ℤring freeLMod {0, 1})))
↑m {{〈0, 2〉, 〈1, 4〉}})(𝑓 finSupp
(0g‘(Scalar‘(ℤring freeLMod {0, 1})))
→ (𝑓( linC
‘(ℤring freeLMod {0, 1})){{〈0, 2〉, 〈1,
4〉}}) ≠ {〈0, 3〉, 〈1, 6〉}) |
27 | 1, 15, 16 | ldepsnlinclem2 45520 |
. . . . . . . 8
⊢ (𝑓 ∈
((Base‘ℤring) ↑m {{〈0, 3〉,
〈1, 6〉}}) → (𝑓( linC ‘(ℤring
freeLMod {0, 1})){{〈0, 3〉, 〈1, 6〉}}) ≠ {〈0,
2〉, 〈1, 4〉}) |
28 | 22 | oveq1i 7223 |
. . . . . . . 8
⊢
((Base‘(Scalar‘(ℤring freeLMod {0, 1})))
↑m {{〈0, 3〉, 〈1, 6〉}}) =
((Base‘ℤring) ↑m {{〈0, 3〉,
〈1, 6〉}}) |
29 | 27, 28 | eleq2s 2856 |
. . . . . . 7
⊢ (𝑓 ∈
((Base‘(Scalar‘(ℤring freeLMod {0, 1})))
↑m {{〈0, 3〉, 〈1, 6〉}}) → (𝑓( linC
‘(ℤring freeLMod {0, 1})){{〈0, 3〉, 〈1,
6〉}}) ≠ {〈0, 2〉, 〈1, 4〉}) |
30 | 29 | a1d 25 |
. . . . . 6
⊢ (𝑓 ∈
((Base‘(Scalar‘(ℤring freeLMod {0, 1})))
↑m {{〈0, 3〉, 〈1, 6〉}}) → (𝑓 finSupp
(0g‘(Scalar‘(ℤring freeLMod {0, 1})))
→ (𝑓( linC
‘(ℤring freeLMod {0, 1})){{〈0, 3〉, 〈1,
6〉}}) ≠ {〈0, 2〉, 〈1, 4〉})) |
31 | 30 | rgen 3071 |
. . . . 5
⊢
∀𝑓 ∈
((Base‘(Scalar‘(ℤring freeLMod {0, 1})))
↑m {{〈0, 3〉, 〈1, 6〉}})(𝑓 finSupp
(0g‘(Scalar‘(ℤring freeLMod {0, 1})))
→ (𝑓( linC
‘(ℤring freeLMod {0, 1})){{〈0, 3〉, 〈1,
6〉}}) ≠ {〈0, 2〉, 〈1, 4〉}) |
32 | | prex 5325 |
. . . . . 6
⊢ {〈0,
3〉, 〈1, 6〉} ∈ V |
33 | | prex 5325 |
. . . . . 6
⊢ {〈0,
2〉, 〈1, 4〉} ∈ V |
34 | | sneq 4551 |
. . . . . . . . . 10
⊢ (𝑣 = {〈0, 3〉, 〈1,
6〉} → {𝑣} =
{{〈0, 3〉, 〈1, 6〉}}) |
35 | 34 | difeq2d 4037 |
. . . . . . . . 9
⊢ (𝑣 = {〈0, 3〉, 〈1,
6〉} → ({{〈0, 3〉, 〈1, 6〉}, {〈0, 2〉,
〈1, 4〉}} ∖ {𝑣}) = ({{〈0, 3〉, 〈1, 6〉},
{〈0, 2〉, 〈1, 4〉}} ∖ {{〈0, 3〉, 〈1,
6〉}})) |
36 | 1, 15, 16 | zlmodzxzldeplem 45512 |
. . . . . . . . . 10
⊢ {〈0,
3〉, 〈1, 6〉} ≠ {〈0, 2〉, 〈1,
4〉} |
37 | | difprsn1 4713 |
. . . . . . . . . 10
⊢
({〈0, 3〉, 〈1, 6〉} ≠ {〈0, 2〉, 〈1,
4〉} → ({{〈0, 3〉, 〈1, 6〉}, {〈0, 2〉,
〈1, 4〉}} ∖ {{〈0, 3〉, 〈1, 6〉}}) = {{〈0,
2〉, 〈1, 4〉}}) |
38 | 36, 37 | ax-mp 5 |
. . . . . . . . 9
⊢
({{〈0, 3〉, 〈1, 6〉}, {〈0, 2〉, 〈1,
4〉}} ∖ {{〈0, 3〉, 〈1, 6〉}}) = {{〈0, 2〉,
〈1, 4〉}} |
39 | 35, 38 | eqtrdi 2794 |
. . . . . . . 8
⊢ (𝑣 = {〈0, 3〉, 〈1,
6〉} → ({{〈0, 3〉, 〈1, 6〉}, {〈0, 2〉,
〈1, 4〉}} ∖ {𝑣}) = {{〈0, 2〉, 〈1,
4〉}}) |
40 | 39 | oveq2d 7229 |
. . . . . . 7
⊢ (𝑣 = {〈0, 3〉, 〈1,
6〉} → ((Base‘(Scalar‘(ℤring freeLMod {0,
1}))) ↑m ({{〈0, 3〉, 〈1, 6〉}, {〈0,
2〉, 〈1, 4〉}} ∖ {𝑣})) =
((Base‘(Scalar‘(ℤring freeLMod {0, 1})))
↑m {{〈0, 2〉, 〈1, 4〉}})) |
41 | 39 | oveq2d 7229 |
. . . . . . . . 9
⊢ (𝑣 = {〈0, 3〉, 〈1,
6〉} → (𝑓( linC
‘(ℤring freeLMod {0, 1}))({{〈0, 3〉, 〈1,
6〉}, {〈0, 2〉, 〈1, 4〉}} ∖ {𝑣})) = (𝑓( linC ‘(ℤring
freeLMod {0, 1})){{〈0, 2〉, 〈1, 4〉}})) |
42 | | id 22 |
. . . . . . . . 9
⊢ (𝑣 = {〈0, 3〉, 〈1,
6〉} → 𝑣 =
{〈0, 3〉, 〈1, 6〉}) |
43 | 41, 42 | neeq12d 3002 |
. . . . . . . 8
⊢ (𝑣 = {〈0, 3〉, 〈1,
6〉} → ((𝑓( linC
‘(ℤring freeLMod {0, 1}))({{〈0, 3〉, 〈1,
6〉}, {〈0, 2〉, 〈1, 4〉}} ∖ {𝑣})) ≠ 𝑣 ↔ (𝑓( linC ‘(ℤring
freeLMod {0, 1})){{〈0, 2〉, 〈1, 4〉}}) ≠ {〈0,
3〉, 〈1, 6〉})) |
44 | 43 | imbi2d 344 |
. . . . . . 7
⊢ (𝑣 = {〈0, 3〉, 〈1,
6〉} → ((𝑓 finSupp
(0g‘(Scalar‘(ℤring freeLMod {0, 1})))
→ (𝑓( linC
‘(ℤring freeLMod {0, 1}))({{〈0, 3〉, 〈1,
6〉}, {〈0, 2〉, 〈1, 4〉}} ∖ {𝑣})) ≠ 𝑣) ↔ (𝑓 finSupp
(0g‘(Scalar‘(ℤring freeLMod {0, 1})))
→ (𝑓( linC
‘(ℤring freeLMod {0, 1})){{〈0, 2〉, 〈1,
4〉}}) ≠ {〈0, 3〉, 〈1, 6〉}))) |
45 | 40, 44 | raleqbidv 3313 |
. . . . . 6
⊢ (𝑣 = {〈0, 3〉, 〈1,
6〉} → (∀𝑓
∈ ((Base‘(Scalar‘(ℤring freeLMod {0, 1})))
↑m ({{〈0, 3〉, 〈1, 6〉}, {〈0, 2〉,
〈1, 4〉}} ∖ {𝑣}))(𝑓 finSupp
(0g‘(Scalar‘(ℤring freeLMod {0, 1})))
→ (𝑓( linC
‘(ℤring freeLMod {0, 1}))({{〈0, 3〉, 〈1,
6〉}, {〈0, 2〉, 〈1, 4〉}} ∖ {𝑣})) ≠ 𝑣) ↔ ∀𝑓 ∈
((Base‘(Scalar‘(ℤring freeLMod {0, 1})))
↑m {{〈0, 2〉, 〈1, 4〉}})(𝑓 finSupp
(0g‘(Scalar‘(ℤring freeLMod {0, 1})))
→ (𝑓( linC
‘(ℤring freeLMod {0, 1})){{〈0, 2〉, 〈1,
4〉}}) ≠ {〈0, 3〉, 〈1, 6〉}))) |
46 | | sneq 4551 |
. . . . . . . . . 10
⊢ (𝑣 = {〈0, 2〉, 〈1,
4〉} → {𝑣} =
{{〈0, 2〉, 〈1, 4〉}}) |
47 | 46 | difeq2d 4037 |
. . . . . . . . 9
⊢ (𝑣 = {〈0, 2〉, 〈1,
4〉} → ({{〈0, 3〉, 〈1, 6〉}, {〈0, 2〉,
〈1, 4〉}} ∖ {𝑣}) = ({{〈0, 3〉, 〈1, 6〉},
{〈0, 2〉, 〈1, 4〉}} ∖ {{〈0, 2〉, 〈1,
4〉}})) |
48 | | difprsn2 4714 |
. . . . . . . . . 10
⊢
({〈0, 3〉, 〈1, 6〉} ≠ {〈0, 2〉, 〈1,
4〉} → ({{〈0, 3〉, 〈1, 6〉}, {〈0, 2〉,
〈1, 4〉}} ∖ {{〈0, 2〉, 〈1, 4〉}}) = {{〈0,
3〉, 〈1, 6〉}}) |
49 | 36, 48 | ax-mp 5 |
. . . . . . . . 9
⊢
({{〈0, 3〉, 〈1, 6〉}, {〈0, 2〉, 〈1,
4〉}} ∖ {{〈0, 2〉, 〈1, 4〉}}) = {{〈0, 3〉,
〈1, 6〉}} |
50 | 47, 49 | eqtrdi 2794 |
. . . . . . . 8
⊢ (𝑣 = {〈0, 2〉, 〈1,
4〉} → ({{〈0, 3〉, 〈1, 6〉}, {〈0, 2〉,
〈1, 4〉}} ∖ {𝑣}) = {{〈0, 3〉, 〈1,
6〉}}) |
51 | 50 | oveq2d 7229 |
. . . . . . 7
⊢ (𝑣 = {〈0, 2〉, 〈1,
4〉} → ((Base‘(Scalar‘(ℤring freeLMod {0,
1}))) ↑m ({{〈0, 3〉, 〈1, 6〉}, {〈0,
2〉, 〈1, 4〉}} ∖ {𝑣})) =
((Base‘(Scalar‘(ℤring freeLMod {0, 1})))
↑m {{〈0, 3〉, 〈1, 6〉}})) |
52 | 50 | oveq2d 7229 |
. . . . . . . . 9
⊢ (𝑣 = {〈0, 2〉, 〈1,
4〉} → (𝑓( linC
‘(ℤring freeLMod {0, 1}))({{〈0, 3〉, 〈1,
6〉}, {〈0, 2〉, 〈1, 4〉}} ∖ {𝑣})) = (𝑓( linC ‘(ℤring
freeLMod {0, 1})){{〈0, 3〉, 〈1, 6〉}})) |
53 | | id 22 |
. . . . . . . . 9
⊢ (𝑣 = {〈0, 2〉, 〈1,
4〉} → 𝑣 =
{〈0, 2〉, 〈1, 4〉}) |
54 | 52, 53 | neeq12d 3002 |
. . . . . . . 8
⊢ (𝑣 = {〈0, 2〉, 〈1,
4〉} → ((𝑓( linC
‘(ℤring freeLMod {0, 1}))({{〈0, 3〉, 〈1,
6〉}, {〈0, 2〉, 〈1, 4〉}} ∖ {𝑣})) ≠ 𝑣 ↔ (𝑓( linC ‘(ℤring
freeLMod {0, 1})){{〈0, 3〉, 〈1, 6〉}}) ≠ {〈0,
2〉, 〈1, 4〉})) |
55 | 54 | imbi2d 344 |
. . . . . . 7
⊢ (𝑣 = {〈0, 2〉, 〈1,
4〉} → ((𝑓 finSupp
(0g‘(Scalar‘(ℤring freeLMod {0, 1})))
→ (𝑓( linC
‘(ℤring freeLMod {0, 1}))({{〈0, 3〉, 〈1,
6〉}, {〈0, 2〉, 〈1, 4〉}} ∖ {𝑣})) ≠ 𝑣) ↔ (𝑓 finSupp
(0g‘(Scalar‘(ℤring freeLMod {0, 1})))
→ (𝑓( linC
‘(ℤring freeLMod {0, 1})){{〈0, 3〉, 〈1,
6〉}}) ≠ {〈0, 2〉, 〈1, 4〉}))) |
56 | 51, 55 | raleqbidv 3313 |
. . . . . 6
⊢ (𝑣 = {〈0, 2〉, 〈1,
4〉} → (∀𝑓
∈ ((Base‘(Scalar‘(ℤring freeLMod {0, 1})))
↑m ({{〈0, 3〉, 〈1, 6〉}, {〈0, 2〉,
〈1, 4〉}} ∖ {𝑣}))(𝑓 finSupp
(0g‘(Scalar‘(ℤring freeLMod {0, 1})))
→ (𝑓( linC
‘(ℤring freeLMod {0, 1}))({{〈0, 3〉, 〈1,
6〉}, {〈0, 2〉, 〈1, 4〉}} ∖ {𝑣})) ≠ 𝑣) ↔ ∀𝑓 ∈
((Base‘(Scalar‘(ℤring freeLMod {0, 1})))
↑m {{〈0, 3〉, 〈1, 6〉}})(𝑓 finSupp
(0g‘(Scalar‘(ℤring freeLMod {0, 1})))
→ (𝑓( linC
‘(ℤring freeLMod {0, 1})){{〈0, 3〉, 〈1,
6〉}}) ≠ {〈0, 2〉, 〈1, 4〉}))) |
57 | 32, 33, 45, 56 | ralpr 4616 |
. . . . 5
⊢
(∀𝑣 ∈
{{〈0, 3〉, 〈1, 6〉}, {〈0, 2〉, 〈1,
4〉}}∀𝑓 ∈
((Base‘(Scalar‘(ℤring freeLMod {0, 1})))
↑m ({{〈0, 3〉, 〈1, 6〉}, {〈0, 2〉,
〈1, 4〉}} ∖ {𝑣}))(𝑓 finSupp
(0g‘(Scalar‘(ℤring freeLMod {0, 1})))
→ (𝑓( linC
‘(ℤring freeLMod {0, 1}))({{〈0, 3〉, 〈1,
6〉}, {〈0, 2〉, 〈1, 4〉}} ∖ {𝑣})) ≠ 𝑣) ↔ (∀𝑓 ∈
((Base‘(Scalar‘(ℤring freeLMod {0, 1})))
↑m {{〈0, 2〉, 〈1, 4〉}})(𝑓 finSupp
(0g‘(Scalar‘(ℤring freeLMod {0, 1})))
→ (𝑓( linC
‘(ℤring freeLMod {0, 1})){{〈0, 2〉, 〈1,
4〉}}) ≠ {〈0, 3〉, 〈1, 6〉}) ∧ ∀𝑓 ∈
((Base‘(Scalar‘(ℤring freeLMod {0, 1})))
↑m {{〈0, 3〉, 〈1, 6〉}})(𝑓 finSupp
(0g‘(Scalar‘(ℤring freeLMod {0, 1})))
→ (𝑓( linC
‘(ℤring freeLMod {0, 1})){{〈0, 3〉, 〈1,
6〉}}) ≠ {〈0, 2〉, 〈1, 4〉}))) |
58 | 26, 31, 57 | mpbir2an 711 |
. . . 4
⊢
∀𝑣 ∈
{{〈0, 3〉, 〈1, 6〉}, {〈0, 2〉, 〈1,
4〉}}∀𝑓 ∈
((Base‘(Scalar‘(ℤring freeLMod {0, 1})))
↑m ({{〈0, 3〉, 〈1, 6〉}, {〈0, 2〉,
〈1, 4〉}} ∖ {𝑣}))(𝑓 finSupp
(0g‘(Scalar‘(ℤring freeLMod {0, 1})))
→ (𝑓( linC
‘(ℤring freeLMod {0, 1}))({{〈0, 3〉, 〈1,
6〉}, {〈0, 2〉, 〈1, 4〉}} ∖ {𝑣})) ≠ 𝑣) |
59 | 17, 58 | pm3.2i 474 |
. . 3
⊢
({{〈0, 3〉, 〈1, 6〉}, {〈0, 2〉, 〈1,
4〉}} linDepS (ℤring freeLMod {0, 1}) ∧ ∀𝑣 ∈ {{〈0, 3〉,
〈1, 6〉}, {〈0, 2〉, 〈1, 4〉}}∀𝑓 ∈
((Base‘(Scalar‘(ℤring freeLMod {0, 1})))
↑m ({{〈0, 3〉, 〈1, 6〉}, {〈0, 2〉,
〈1, 4〉}} ∖ {𝑣}))(𝑓 finSupp
(0g‘(Scalar‘(ℤring freeLMod {0, 1})))
→ (𝑓( linC
‘(ℤring freeLMod {0, 1}))({{〈0, 3〉, 〈1,
6〉}, {〈0, 2〉, 〈1, 4〉}} ∖ {𝑣})) ≠ 𝑣)) |
60 | | breq1 5056 |
. . . . 5
⊢ (𝑠 = {{〈0, 3〉, 〈1,
6〉}, {〈0, 2〉, 〈1, 4〉}} → (𝑠 linDepS (ℤring freeLMod {0,
1}) ↔ {{〈0, 3〉, 〈1, 6〉}, {〈0, 2〉, 〈1,
4〉}} linDepS (ℤring freeLMod {0, 1}))) |
61 | | id 22 |
. . . . . 6
⊢ (𝑠 = {{〈0, 3〉, 〈1,
6〉}, {〈0, 2〉, 〈1, 4〉}} → 𝑠 = {{〈0, 3〉, 〈1, 6〉},
{〈0, 2〉, 〈1, 4〉}}) |
62 | | difeq1 4030 |
. . . . . . . 8
⊢ (𝑠 = {{〈0, 3〉, 〈1,
6〉}, {〈0, 2〉, 〈1, 4〉}} → (𝑠 ∖ {𝑣}) = ({{〈0, 3〉, 〈1, 6〉},
{〈0, 2〉, 〈1, 4〉}} ∖ {𝑣})) |
63 | 62 | oveq2d 7229 |
. . . . . . 7
⊢ (𝑠 = {{〈0, 3〉, 〈1,
6〉}, {〈0, 2〉, 〈1, 4〉}} →
((Base‘(Scalar‘(ℤring freeLMod {0, 1})))
↑m (𝑠
∖ {𝑣})) =
((Base‘(Scalar‘(ℤring freeLMod {0, 1})))
↑m ({{〈0, 3〉, 〈1, 6〉}, {〈0, 2〉,
〈1, 4〉}} ∖ {𝑣}))) |
64 | 62 | oveq2d 7229 |
. . . . . . . . 9
⊢ (𝑠 = {{〈0, 3〉, 〈1,
6〉}, {〈0, 2〉, 〈1, 4〉}} → (𝑓( linC ‘(ℤring
freeLMod {0, 1}))(𝑠 ∖
{𝑣})) = (𝑓( linC ‘(ℤring
freeLMod {0, 1}))({{〈0, 3〉, 〈1, 6〉}, {〈0, 2〉,
〈1, 4〉}} ∖ {𝑣}))) |
65 | 64 | neeq1d 3000 |
. . . . . . . 8
⊢ (𝑠 = {{〈0, 3〉, 〈1,
6〉}, {〈0, 2〉, 〈1, 4〉}} → ((𝑓( linC ‘(ℤring
freeLMod {0, 1}))(𝑠 ∖
{𝑣})) ≠ 𝑣 ↔ (𝑓( linC ‘(ℤring
freeLMod {0, 1}))({{〈0, 3〉, 〈1, 6〉}, {〈0, 2〉,
〈1, 4〉}} ∖ {𝑣})) ≠ 𝑣)) |
66 | 65 | imbi2d 344 |
. . . . . . 7
⊢ (𝑠 = {{〈0, 3〉, 〈1,
6〉}, {〈0, 2〉, 〈1, 4〉}} → ((𝑓 finSupp
(0g‘(Scalar‘(ℤring freeLMod {0, 1})))
→ (𝑓( linC
‘(ℤring freeLMod {0, 1}))(𝑠 ∖ {𝑣})) ≠ 𝑣) ↔ (𝑓 finSupp
(0g‘(Scalar‘(ℤring freeLMod {0, 1})))
→ (𝑓( linC
‘(ℤring freeLMod {0, 1}))({{〈0, 3〉, 〈1,
6〉}, {〈0, 2〉, 〈1, 4〉}} ∖ {𝑣})) ≠ 𝑣))) |
67 | 63, 66 | raleqbidv 3313 |
. . . . . 6
⊢ (𝑠 = {{〈0, 3〉, 〈1,
6〉}, {〈0, 2〉, 〈1, 4〉}} → (∀𝑓 ∈
((Base‘(Scalar‘(ℤring freeLMod {0, 1})))
↑m (𝑠
∖ {𝑣}))(𝑓 finSupp
(0g‘(Scalar‘(ℤring freeLMod {0, 1})))
→ (𝑓( linC
‘(ℤring freeLMod {0, 1}))(𝑠 ∖ {𝑣})) ≠ 𝑣) ↔ ∀𝑓 ∈
((Base‘(Scalar‘(ℤring freeLMod {0, 1})))
↑m ({{〈0, 3〉, 〈1, 6〉}, {〈0, 2〉,
〈1, 4〉}} ∖ {𝑣}))(𝑓 finSupp
(0g‘(Scalar‘(ℤring freeLMod {0, 1})))
→ (𝑓( linC
‘(ℤring freeLMod {0, 1}))({{〈0, 3〉, 〈1,
6〉}, {〈0, 2〉, 〈1, 4〉}} ∖ {𝑣})) ≠ 𝑣))) |
68 | 61, 67 | raleqbidv 3313 |
. . . . 5
⊢ (𝑠 = {{〈0, 3〉, 〈1,
6〉}, {〈0, 2〉, 〈1, 4〉}} → (∀𝑣 ∈ 𝑠 ∀𝑓 ∈
((Base‘(Scalar‘(ℤring freeLMod {0, 1})))
↑m (𝑠
∖ {𝑣}))(𝑓 finSupp
(0g‘(Scalar‘(ℤring freeLMod {0, 1})))
→ (𝑓( linC
‘(ℤring freeLMod {0, 1}))(𝑠 ∖ {𝑣})) ≠ 𝑣) ↔ ∀𝑣 ∈ {{〈0, 3〉, 〈1,
6〉}, {〈0, 2〉, 〈1, 4〉}}∀𝑓 ∈
((Base‘(Scalar‘(ℤring freeLMod {0, 1})))
↑m ({{〈0, 3〉, 〈1, 6〉}, {〈0, 2〉,
〈1, 4〉}} ∖ {𝑣}))(𝑓 finSupp
(0g‘(Scalar‘(ℤring freeLMod {0, 1})))
→ (𝑓( linC
‘(ℤring freeLMod {0, 1}))({{〈0, 3〉, 〈1,
6〉}, {〈0, 2〉, 〈1, 4〉}} ∖ {𝑣})) ≠ 𝑣))) |
69 | 60, 68 | anbi12d 634 |
. . . 4
⊢ (𝑠 = {{〈0, 3〉, 〈1,
6〉}, {〈0, 2〉, 〈1, 4〉}} → ((𝑠 linDepS (ℤring freeLMod {0,
1}) ∧ ∀𝑣 ∈
𝑠 ∀𝑓 ∈
((Base‘(Scalar‘(ℤring freeLMod {0, 1})))
↑m (𝑠
∖ {𝑣}))(𝑓 finSupp
(0g‘(Scalar‘(ℤring freeLMod {0, 1})))
→ (𝑓( linC
‘(ℤring freeLMod {0, 1}))(𝑠 ∖ {𝑣})) ≠ 𝑣)) ↔ ({{〈0, 3〉, 〈1,
6〉}, {〈0, 2〉, 〈1, 4〉}} linDepS (ℤring
freeLMod {0, 1}) ∧ ∀𝑣 ∈ {{〈0, 3〉, 〈1,
6〉}, {〈0, 2〉, 〈1, 4〉}}∀𝑓 ∈
((Base‘(Scalar‘(ℤring freeLMod {0, 1})))
↑m ({{〈0, 3〉, 〈1, 6〉}, {〈0, 2〉,
〈1, 4〉}} ∖ {𝑣}))(𝑓 finSupp
(0g‘(Scalar‘(ℤring freeLMod {0, 1})))
→ (𝑓( linC
‘(ℤring freeLMod {0, 1}))({{〈0, 3〉, 〈1,
6〉}, {〈0, 2〉, 〈1, 4〉}} ∖ {𝑣})) ≠ 𝑣)))) |
70 | 69 | rspcev 3537 |
. . 3
⊢
(({{〈0, 3〉, 〈1, 6〉}, {〈0, 2〉, 〈1,
4〉}} ∈ 𝒫 (Base‘(ℤring freeLMod {0,
1})) ∧ ({{〈0, 3〉, 〈1, 6〉}, {〈0, 2〉, 〈1,
4〉}} linDepS (ℤring freeLMod {0, 1}) ∧ ∀𝑣 ∈ {{〈0, 3〉,
〈1, 6〉}, {〈0, 2〉, 〈1, 4〉}}∀𝑓 ∈
((Base‘(Scalar‘(ℤring freeLMod {0, 1})))
↑m ({{〈0, 3〉, 〈1, 6〉}, {〈0, 2〉,
〈1, 4〉}} ∖ {𝑣}))(𝑓 finSupp
(0g‘(Scalar‘(ℤring freeLMod {0, 1})))
→ (𝑓( linC
‘(ℤring freeLMod {0, 1}))({{〈0, 3〉, 〈1,
6〉}, {〈0, 2〉, 〈1, 4〉}} ∖ {𝑣})) ≠ 𝑣))) → ∃𝑠 ∈ 𝒫
(Base‘(ℤring freeLMod {0, 1}))(𝑠 linDepS (ℤring freeLMod {0,
1}) ∧ ∀𝑣 ∈
𝑠 ∀𝑓 ∈
((Base‘(Scalar‘(ℤring freeLMod {0, 1})))
↑m (𝑠
∖ {𝑣}))(𝑓 finSupp
(0g‘(Scalar‘(ℤring freeLMod {0, 1})))
→ (𝑓( linC
‘(ℤring freeLMod {0, 1}))(𝑠 ∖ {𝑣})) ≠ 𝑣))) |
71 | 14, 59, 70 | mp2an 692 |
. 2
⊢
∃𝑠 ∈
𝒫 (Base‘(ℤring freeLMod {0, 1}))(𝑠 linDepS (ℤring
freeLMod {0, 1}) ∧ ∀𝑣 ∈ 𝑠 ∀𝑓 ∈
((Base‘(Scalar‘(ℤring freeLMod {0, 1})))
↑m (𝑠
∖ {𝑣}))(𝑓 finSupp
(0g‘(Scalar‘(ℤring freeLMod {0, 1})))
→ (𝑓( linC
‘(ℤring freeLMod {0, 1}))(𝑠 ∖ {𝑣})) ≠ 𝑣)) |
72 | | fveq2 6717 |
. . . . 5
⊢ (𝑚 = (ℤring
freeLMod {0, 1}) → (Base‘𝑚) = (Base‘(ℤring
freeLMod {0, 1}))) |
73 | 72 | pweqd 4532 |
. . . 4
⊢ (𝑚 = (ℤring
freeLMod {0, 1}) → 𝒫 (Base‘𝑚) = 𝒫
(Base‘(ℤring freeLMod {0, 1}))) |
74 | | breq2 5057 |
. . . . 5
⊢ (𝑚 = (ℤring
freeLMod {0, 1}) → (𝑠
linDepS 𝑚 ↔ 𝑠 linDepS (ℤring
freeLMod {0, 1}))) |
75 | | 2fveq3 6722 |
. . . . . . . 8
⊢ (𝑚 = (ℤring
freeLMod {0, 1}) → (Base‘(Scalar‘𝑚)) =
(Base‘(Scalar‘(ℤring freeLMod {0,
1})))) |
76 | 75 | oveq1d 7228 |
. . . . . . 7
⊢ (𝑚 = (ℤring
freeLMod {0, 1}) → ((Base‘(Scalar‘𝑚)) ↑m (𝑠 ∖ {𝑣})) =
((Base‘(Scalar‘(ℤring freeLMod {0, 1})))
↑m (𝑠
∖ {𝑣}))) |
77 | | 2fveq3 6722 |
. . . . . . . . 9
⊢ (𝑚 = (ℤring
freeLMod {0, 1}) → (0g‘(Scalar‘𝑚)) =
(0g‘(Scalar‘(ℤring freeLMod {0,
1})))) |
78 | 77 | breq2d 5065 |
. . . . . . . 8
⊢ (𝑚 = (ℤring
freeLMod {0, 1}) → (𝑓
finSupp (0g‘(Scalar‘𝑚)) ↔ 𝑓 finSupp
(0g‘(Scalar‘(ℤring freeLMod {0,
1}))))) |
79 | | fveq2 6717 |
. . . . . . . . . 10
⊢ (𝑚 = (ℤring
freeLMod {0, 1}) → ( linC ‘𝑚) = ( linC ‘(ℤring
freeLMod {0, 1}))) |
80 | 79 | oveqd 7230 |
. . . . . . . . 9
⊢ (𝑚 = (ℤring
freeLMod {0, 1}) → (𝑓(
linC ‘𝑚)(𝑠 ∖ {𝑣})) = (𝑓( linC ‘(ℤring
freeLMod {0, 1}))(𝑠 ∖
{𝑣}))) |
81 | 80 | neeq1d 3000 |
. . . . . . . 8
⊢ (𝑚 = (ℤring
freeLMod {0, 1}) → ((𝑓( linC ‘𝑚)(𝑠 ∖ {𝑣})) ≠ 𝑣 ↔ (𝑓( linC ‘(ℤring
freeLMod {0, 1}))(𝑠 ∖
{𝑣})) ≠ 𝑣)) |
82 | 78, 81 | imbi12d 348 |
. . . . . . 7
⊢ (𝑚 = (ℤring
freeLMod {0, 1}) → ((𝑓
finSupp (0g‘(Scalar‘𝑚)) → (𝑓( linC ‘𝑚)(𝑠 ∖ {𝑣})) ≠ 𝑣) ↔ (𝑓 finSupp
(0g‘(Scalar‘(ℤring freeLMod {0, 1})))
→ (𝑓( linC
‘(ℤring freeLMod {0, 1}))(𝑠 ∖ {𝑣})) ≠ 𝑣))) |
83 | 76, 82 | raleqbidv 3313 |
. . . . . 6
⊢ (𝑚 = (ℤring
freeLMod {0, 1}) → (∀𝑓 ∈ ((Base‘(Scalar‘𝑚)) ↑m (𝑠 ∖ {𝑣}))(𝑓 finSupp
(0g‘(Scalar‘𝑚)) → (𝑓( linC ‘𝑚)(𝑠 ∖ {𝑣})) ≠ 𝑣) ↔ ∀𝑓 ∈
((Base‘(Scalar‘(ℤring freeLMod {0, 1})))
↑m (𝑠
∖ {𝑣}))(𝑓 finSupp
(0g‘(Scalar‘(ℤring freeLMod {0, 1})))
→ (𝑓( linC
‘(ℤring freeLMod {0, 1}))(𝑠 ∖ {𝑣})) ≠ 𝑣))) |
84 | 83 | ralbidv 3118 |
. . . . 5
⊢ (𝑚 = (ℤring
freeLMod {0, 1}) → (∀𝑣 ∈ 𝑠 ∀𝑓 ∈ ((Base‘(Scalar‘𝑚)) ↑m (𝑠 ∖ {𝑣}))(𝑓 finSupp
(0g‘(Scalar‘𝑚)) → (𝑓( linC ‘𝑚)(𝑠 ∖ {𝑣})) ≠ 𝑣) ↔ ∀𝑣 ∈ 𝑠 ∀𝑓 ∈
((Base‘(Scalar‘(ℤring freeLMod {0, 1})))
↑m (𝑠
∖ {𝑣}))(𝑓 finSupp
(0g‘(Scalar‘(ℤring freeLMod {0, 1})))
→ (𝑓( linC
‘(ℤring freeLMod {0, 1}))(𝑠 ∖ {𝑣})) ≠ 𝑣))) |
85 | 74, 84 | anbi12d 634 |
. . . 4
⊢ (𝑚 = (ℤring
freeLMod {0, 1}) → ((𝑠
linDepS 𝑚 ∧
∀𝑣 ∈ 𝑠 ∀𝑓 ∈ ((Base‘(Scalar‘𝑚)) ↑m (𝑠 ∖ {𝑣}))(𝑓 finSupp
(0g‘(Scalar‘𝑚)) → (𝑓( linC ‘𝑚)(𝑠 ∖ {𝑣})) ≠ 𝑣)) ↔ (𝑠 linDepS (ℤring freeLMod {0,
1}) ∧ ∀𝑣 ∈
𝑠 ∀𝑓 ∈
((Base‘(Scalar‘(ℤring freeLMod {0, 1})))
↑m (𝑠
∖ {𝑣}))(𝑓 finSupp
(0g‘(Scalar‘(ℤring freeLMod {0, 1})))
→ (𝑓( linC
‘(ℤring freeLMod {0, 1}))(𝑠 ∖ {𝑣})) ≠ 𝑣)))) |
86 | 73, 85 | rexeqbidv 3314 |
. . 3
⊢ (𝑚 = (ℤring
freeLMod {0, 1}) → (∃𝑠 ∈ 𝒫 (Base‘𝑚)(𝑠 linDepS 𝑚 ∧ ∀𝑣 ∈ 𝑠 ∀𝑓 ∈ ((Base‘(Scalar‘𝑚)) ↑m (𝑠 ∖ {𝑣}))(𝑓 finSupp
(0g‘(Scalar‘𝑚)) → (𝑓( linC ‘𝑚)(𝑠 ∖ {𝑣})) ≠ 𝑣)) ↔ ∃𝑠 ∈ 𝒫
(Base‘(ℤring freeLMod {0, 1}))(𝑠 linDepS (ℤring freeLMod {0,
1}) ∧ ∀𝑣 ∈
𝑠 ∀𝑓 ∈
((Base‘(Scalar‘(ℤring freeLMod {0, 1})))
↑m (𝑠
∖ {𝑣}))(𝑓 finSupp
(0g‘(Scalar‘(ℤring freeLMod {0, 1})))
→ (𝑓( linC
‘(ℤring freeLMod {0, 1}))(𝑠 ∖ {𝑣})) ≠ 𝑣)))) |
87 | 86 | rspcev 3537 |
. 2
⊢
(((ℤring freeLMod {0, 1}) ∈ LMod ∧
∃𝑠 ∈ 𝒫
(Base‘(ℤring freeLMod {0, 1}))(𝑠 linDepS (ℤring freeLMod {0,
1}) ∧ ∀𝑣 ∈
𝑠 ∀𝑓 ∈
((Base‘(Scalar‘(ℤring freeLMod {0, 1})))
↑m (𝑠
∖ {𝑣}))(𝑓 finSupp
(0g‘(Scalar‘(ℤring freeLMod {0, 1})))
→ (𝑓( linC
‘(ℤring freeLMod {0, 1}))(𝑠 ∖ {𝑣})) ≠ 𝑣))) → ∃𝑚 ∈ LMod ∃𝑠 ∈ 𝒫 (Base‘𝑚)(𝑠 linDepS 𝑚 ∧ ∀𝑣 ∈ 𝑠 ∀𝑓 ∈ ((Base‘(Scalar‘𝑚)) ↑m (𝑠 ∖ {𝑣}))(𝑓 finSupp
(0g‘(Scalar‘𝑚)) → (𝑓( linC ‘𝑚)(𝑠 ∖ {𝑣})) ≠ 𝑣))) |
88 | 3, 71, 87 | mp2an 692 |
1
⊢
∃𝑚 ∈ LMod
∃𝑠 ∈ 𝒫
(Base‘𝑚)(𝑠 linDepS 𝑚 ∧ ∀𝑣 ∈ 𝑠 ∀𝑓 ∈ ((Base‘(Scalar‘𝑚)) ↑m (𝑠 ∖ {𝑣}))(𝑓 finSupp
(0g‘(Scalar‘𝑚)) → (𝑓( linC ‘𝑚)(𝑠 ∖ {𝑣})) ≠ 𝑣)) |