Proof of Theorem ldepsnlinc
| Step | Hyp | Ref | Expression | 
|---|
| 1 |  | eqid 2737 | . . . 4
⊢
(ℤring freeLMod {0, 1}) = (ℤring
freeLMod {0, 1}) | 
| 2 | 1 | zlmodzxzlmod 48270 | . . 3
⊢
((ℤring freeLMod {0, 1}) ∈ LMod ∧
ℤring = (Scalar‘(ℤring freeLMod {0,
1}))) | 
| 3 | 2 | simpli 483 | . 2
⊢
(ℤring freeLMod {0, 1}) ∈ LMod | 
| 4 |  | 3z 12650 | . . . . 5
⊢ 3 ∈
ℤ | 
| 5 |  | 6nn 12355 | . . . . . 6
⊢ 6 ∈
ℕ | 
| 6 | 5 | nnzi 12641 | . . . . 5
⊢ 6 ∈
ℤ | 
| 7 | 1 | zlmodzxzel 48271 | . . . . 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 12649 | . . . . 5
⊢ 2 ∈
ℤ | 
| 10 |  | 4z 12651 | . . . . 5
⊢ 4 ∈
ℤ | 
| 11 | 1 | zlmodzxzel 48271 | . . . . 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 5452 | . . . 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 48421 | . . . 4
⊢
{{〈0, 3〉, 〈1, 6〉}, {〈0, 2〉, 〈1,
4〉}} linDepS (ℤring freeLMod {0, 1}) | 
| 18 | 1, 15, 16 | ldepsnlinclem1 48422 | . . . . . . . 8
⊢ (𝑓 ∈
((Base‘ℤring) ↑m {{〈0, 2〉,
〈1, 4〉}}) → (𝑓( linC ‘(ℤring
freeLMod {0, 1})){{〈0, 2〉, 〈1, 4〉}}) ≠ {〈0,
3〉, 〈1, 6〉}) | 
| 19 |  | simpr 484 | . . . . . . . . . . . 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 6909 | . . . . . . . . 9
⊢
(Base‘(Scalar‘(ℤring freeLMod {0, 1}))) =
(Base‘ℤring) | 
| 23 | 22 | oveq1i 7441 | . . . . . . . 8
⊢
((Base‘(Scalar‘(ℤring freeLMod {0, 1})))
↑m {{〈0, 2〉, 〈1, 4〉}}) =
((Base‘ℤring) ↑m {{〈0, 2〉,
〈1, 4〉}}) | 
| 24 | 18, 23 | eleq2s 2859 | . . . . . . 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 3063 | . . . . 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 48423 | . . . . . . . 8
⊢ (𝑓 ∈
((Base‘ℤring) ↑m {{〈0, 3〉,
〈1, 6〉}}) → (𝑓( linC ‘(ℤring
freeLMod {0, 1})){{〈0, 3〉, 〈1, 6〉}}) ≠ {〈0,
2〉, 〈1, 4〉}) | 
| 28 | 22 | oveq1i 7441 | . . . . . . . 8
⊢
((Base‘(Scalar‘(ℤring freeLMod {0, 1})))
↑m {{〈0, 3〉, 〈1, 6〉}}) =
((Base‘ℤring) ↑m {{〈0, 3〉,
〈1, 6〉}}) | 
| 29 | 27, 28 | eleq2s 2859 | . . . . . . 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 3063 | . . . . 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 5437 | . . . . . 6
⊢ {〈0,
3〉, 〈1, 6〉} ∈ V | 
| 33 |  | prex 5437 | . . . . . 6
⊢ {〈0,
2〉, 〈1, 4〉} ∈ V | 
| 34 |  | sneq 4636 | . . . . . . . . . 10
⊢ (𝑣 = {〈0, 3〉, 〈1,
6〉} → {𝑣} =
{{〈0, 3〉, 〈1, 6〉}}) | 
| 35 | 34 | difeq2d 4126 | . . . . . . . . 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 48415 | . . . . . . . . . 10
⊢ {〈0,
3〉, 〈1, 6〉} ≠ {〈0, 2〉, 〈1,
4〉} | 
| 37 |  | difprsn1 4800 | . . . . . . . . . 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 2793 | . . . . . . . 8
⊢ (𝑣 = {〈0, 3〉, 〈1,
6〉} → ({{〈0, 3〉, 〈1, 6〉}, {〈0, 2〉,
〈1, 4〉}} ∖ {𝑣}) = {{〈0, 2〉, 〈1,
4〉}}) | 
| 40 | 39 | oveq2d 7447 | . . . . . . 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 7447 | . . . . . . . . 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 340 | . . . . . . 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 3346 | . . . . . 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 4636 | . . . . . . . . . 10
⊢ (𝑣 = {〈0, 2〉, 〈1,
4〉} → {𝑣} =
{{〈0, 2〉, 〈1, 4〉}}) | 
| 47 | 46 | difeq2d 4126 | . . . . . . . . 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 4801 | . . . . . . . . . 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 2793 | . . . . . . . 8
⊢ (𝑣 = {〈0, 2〉, 〈1,
4〉} → ({{〈0, 3〉, 〈1, 6〉}, {〈0, 2〉,
〈1, 4〉}} ∖ {𝑣}) = {{〈0, 3〉, 〈1,
6〉}}) | 
| 51 | 50 | oveq2d 7447 | . . . . . . 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 7447 | . . . . . . . . 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 340 | . . . . . . 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 3346 | . . . . . 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 4700 | . . . . 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 470 | . . 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 5146 | . . . . 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 4119 | . . . . . . . 8
⊢ (𝑠 = {{〈0, 3〉, 〈1,
6〉}, {〈0, 2〉, 〈1, 4〉}} → (𝑠 ∖ {𝑣}) = ({{〈0, 3〉, 〈1, 6〉},
{〈0, 2〉, 〈1, 4〉}} ∖ {𝑣})) | 
| 63 | 62 | oveq2d 7447 | . . . . . . 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 7447 | . . . . . . . . 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 340 | . . . . . . 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 3346 | . . . . . 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 3346 | . . . . 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 632 | . . . 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 3622 | . . 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 6906 | . . . . 5
⊢ (𝑚 = (ℤring
freeLMod {0, 1}) → (Base‘𝑚) = (Base‘(ℤring
freeLMod {0, 1}))) | 
| 73 | 72 | pweqd 4617 | . . . 4
⊢ (𝑚 = (ℤring
freeLMod {0, 1}) → 𝒫 (Base‘𝑚) = 𝒫
(Base‘(ℤring freeLMod {0, 1}))) | 
| 74 |  | breq2 5147 | . . . . 5
⊢ (𝑚 = (ℤring
freeLMod {0, 1}) → (𝑠
linDepS 𝑚 ↔ 𝑠 linDepS (ℤring
freeLMod {0, 1}))) | 
| 75 |  | 2fveq3 6911 | . . . . . . . 8
⊢ (𝑚 = (ℤring
freeLMod {0, 1}) → (Base‘(Scalar‘𝑚)) =
(Base‘(Scalar‘(ℤring freeLMod {0,
1})))) | 
| 76 | 75 | oveq1d 7446 | . . . . . . 7
⊢ (𝑚 = (ℤring
freeLMod {0, 1}) → ((Base‘(Scalar‘𝑚)) ↑m (𝑠 ∖ {𝑣})) =
((Base‘(Scalar‘(ℤring freeLMod {0, 1})))
↑m (𝑠
∖ {𝑣}))) | 
| 77 |  | 2fveq3 6911 | . . . . . . . . 9
⊢ (𝑚 = (ℤring
freeLMod {0, 1}) → (0g‘(Scalar‘𝑚)) =
(0g‘(Scalar‘(ℤring freeLMod {0,
1})))) | 
| 78 | 77 | breq2d 5155 | . . . . . . . 8
⊢ (𝑚 = (ℤring
freeLMod {0, 1}) → (𝑓
finSupp (0g‘(Scalar‘𝑚)) ↔ 𝑓 finSupp
(0g‘(Scalar‘(ℤring freeLMod {0,
1}))))) | 
| 79 |  | fveq2 6906 | . . . . . . . . . 10
⊢ (𝑚 = (ℤring
freeLMod {0, 1}) → ( linC ‘𝑚) = ( linC ‘(ℤring
freeLMod {0, 1}))) | 
| 80 | 79 | oveqd 7448 | . . . . . . . . 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 344 | . . . . . . 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 3346 | . . . . . 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 3178 | . . . . 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 632 | . . . 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 3347 | . . 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 3622 | . 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 ‘𝑚)(𝑠 ∖ {𝑣})) ≠ 𝑣)) |