Metamath Proof Explorer

Theorem zlmodzxzldep

Description: { A , B } is a linearly dependent set within the ZZ-module ZZ X. ZZ (see example in Roman p. 112). (Contributed by AV, 22-May-2019) (Revised by AV, 10-Jun-2019)

Ref Expression
Hypotheses zlmodzxzldep.z ⊢ 𝑍 = ( ℤring freeLMod { 0 , 1 } )
zlmodzxzldep.a ⊢ 𝐴 = { ⟨ 0 , 3 ⟩ , ⟨ 1 , 6 ⟩ }
zlmodzxzldep.b ⊢ 𝐵 = { ⟨ 0 , 2 ⟩ , ⟨ 1 , 4 ⟩ }
Assertion zlmodzxzldep { 𝐴 , 𝐵 } linDepS 𝑍

Proof

Step Hyp Ref Expression
1 zlmodzxzldep.z ⊢ 𝑍 = ( ℤring freeLMod { 0 , 1 } )
2 zlmodzxzldep.a ⊢ 𝐴 = { ⟨ 0 , 3 ⟩ , ⟨ 1 , 6 ⟩ }
3 zlmodzxzldep.b ⊢ 𝐵 = { ⟨ 0 , 2 ⟩ , ⟨ 1 , 4 ⟩ }
4 eqid ⊢ { ⟨ 𝐴 , 2 ⟩ , ⟨ 𝐵 , - 3 ⟩ } = { ⟨ 𝐴 , 2 ⟩ , ⟨ 𝐵 , - 3 ⟩ }
5 1 2 3 4 zlmodzxzldeplem1 ⊢ { ⟨ 𝐴 , 2 ⟩ , ⟨ 𝐵 , - 3 ⟩ } ∈ ( ℤ ↑m { 𝐴 , 𝐵 } )
6 1 2 3 4 zlmodzxzldeplem2 ⊢ { ⟨ 𝐴 , 2 ⟩ , ⟨ 𝐵 , - 3 ⟩ } finSupp 0
7 1 2 3 4 zlmodzxzldeplem3 ⊢ ( { ⟨ 𝐴 , 2 ⟩ , ⟨ 𝐵 , - 3 ⟩ } ( linC ‘ 𝑍 ) { 𝐴 , 𝐵 } ) = ( 0g ‘ 𝑍 )
8 1 2 3 4 zlmodzxzldeplem4 ⊢ ∃ 𝑦 ∈ { 𝐴 , 𝐵 } ( { ⟨ 𝐴 , 2 ⟩ , ⟨ 𝐵 , - 3 ⟩ } ‘ 𝑦 ) ≠ 0
9 6 7 8 3pm3.2i ⊢ ( { ⟨ 𝐴 , 2 ⟩ , ⟨ 𝐵 , - 3 ⟩ } finSupp 0 ∧ ( { ⟨ 𝐴 , 2 ⟩ , ⟨ 𝐵 , - 3 ⟩ } ( linC ‘ 𝑍 ) { 𝐴 , 𝐵 } ) = ( 0g ‘ 𝑍 ) ∧ ∃ 𝑦 ∈ { 𝐴 , 𝐵 } ( { ⟨ 𝐴 , 2 ⟩ , ⟨ 𝐵 , - 3 ⟩ } ‘ 𝑦 ) ≠ 0 )
10 breq1 ⊢ ( 𝑥 = { ⟨ 𝐴 , 2 ⟩ , ⟨ 𝐵 , - 3 ⟩ } → ( 𝑥 finSupp 0 ↔ { ⟨ 𝐴 , 2 ⟩ , ⟨ 𝐵 , - 3 ⟩ } finSupp 0 ) )
11 oveq1 ⊢ ( 𝑥 = { ⟨ 𝐴 , 2 ⟩ , ⟨ 𝐵 , - 3 ⟩ } → ( 𝑥 ( linC ‘ 𝑍 ) { 𝐴 , 𝐵 } ) = ( { ⟨ 𝐴 , 2 ⟩ , ⟨ 𝐵 , - 3 ⟩ } ( linC ‘ 𝑍 ) { 𝐴 , 𝐵 } ) )
12 11 eqeq1d ⊢ ( 𝑥 = { ⟨ 𝐴 , 2 ⟩ , ⟨ 𝐵 , - 3 ⟩ } → ( ( 𝑥 ( linC ‘ 𝑍 ) { 𝐴 , 𝐵 } ) = ( 0g ‘ 𝑍 ) ↔ ( { ⟨ 𝐴 , 2 ⟩ , ⟨ 𝐵 , - 3 ⟩ } ( linC ‘ 𝑍 ) { 𝐴 , 𝐵 } ) = ( 0g ‘ 𝑍 ) ) )
13 fveq1 ⊢ ( 𝑥 = { ⟨ 𝐴 , 2 ⟩ , ⟨ 𝐵 , - 3 ⟩ } → ( 𝑥 ‘ 𝑦 ) = ( { ⟨ 𝐴 , 2 ⟩ , ⟨ 𝐵 , - 3 ⟩ } ‘ 𝑦 ) )
14 13 neeq1d ⊢ ( 𝑥 = { ⟨ 𝐴 , 2 ⟩ , ⟨ 𝐵 , - 3 ⟩ } → ( ( 𝑥 ‘ 𝑦 ) ≠ 0 ↔ ( { ⟨ 𝐴 , 2 ⟩ , ⟨ 𝐵 , - 3 ⟩ } ‘ 𝑦 ) ≠ 0 ) )
15 14 rexbidv ⊢ ( 𝑥 = { ⟨ 𝐴 , 2 ⟩ , ⟨ 𝐵 , - 3 ⟩ } → ( ∃ 𝑦 ∈ { 𝐴 , 𝐵 } ( 𝑥 ‘ 𝑦 ) ≠ 0 ↔ ∃ 𝑦 ∈ { 𝐴 , 𝐵 } ( { ⟨ 𝐴 , 2 ⟩ , ⟨ 𝐵 , - 3 ⟩ } ‘ 𝑦 ) ≠ 0 ) )
16 10 12 15 3anbi123d ⊢ ( 𝑥 = { ⟨ 𝐴 , 2 ⟩ , ⟨ 𝐵 , - 3 ⟩ } → ( ( 𝑥 finSupp 0 ∧ ( 𝑥 ( linC ‘ 𝑍 ) { 𝐴 , 𝐵 } ) = ( 0g ‘ 𝑍 ) ∧ ∃ 𝑦 ∈ { 𝐴 , 𝐵 } ( 𝑥 ‘ 𝑦 ) ≠ 0 ) ↔ ( { ⟨ 𝐴 , 2 ⟩ , ⟨ 𝐵 , - 3 ⟩ } finSupp 0 ∧ ( { ⟨ 𝐴 , 2 ⟩ , ⟨ 𝐵 , - 3 ⟩ } ( linC ‘ 𝑍 ) { 𝐴 , 𝐵 } ) = ( 0g ‘ 𝑍 ) ∧ ∃ 𝑦 ∈ { 𝐴 , 𝐵 } ( { ⟨ 𝐴 , 2 ⟩ , ⟨ 𝐵 , - 3 ⟩ } ‘ 𝑦 ) ≠ 0 ) ) )
17 16 rspcev ⊢ ( ( { ⟨ 𝐴 , 2 ⟩ , ⟨ 𝐵 , - 3 ⟩ } ∈ ( ℤ ↑m { 𝐴 , 𝐵 } ) ∧ ( { ⟨ 𝐴 , 2 ⟩ , ⟨ 𝐵 , - 3 ⟩ } finSupp 0 ∧ ( { ⟨ 𝐴 , 2 ⟩ , ⟨ 𝐵 , - 3 ⟩ } ( linC ‘ 𝑍 ) { 𝐴 , 𝐵 } ) = ( 0g ‘ 𝑍 ) ∧ ∃ 𝑦 ∈ { 𝐴 , 𝐵 } ( { ⟨ 𝐴 , 2 ⟩ , ⟨ 𝐵 , - 3 ⟩ } ‘ 𝑦 ) ≠ 0 ) ) → ∃ 𝑥 ∈ ( ℤ ↑m { 𝐴 , 𝐵 } ) ( 𝑥 finSupp 0 ∧ ( 𝑥 ( linC ‘ 𝑍 ) { 𝐴 , 𝐵 } ) = ( 0g ‘ 𝑍 ) ∧ ∃ 𝑦 ∈ { 𝐴 , 𝐵 } ( 𝑥 ‘ 𝑦 ) ≠ 0 ) )
18 5 9 17 mp2an ⊢ ∃ 𝑥 ∈ ( ℤ ↑m { 𝐴 , 𝐵 } ) ( 𝑥 finSupp 0 ∧ ( 𝑥 ( linC ‘ 𝑍 ) { 𝐴 , 𝐵 } ) = ( 0g ‘ 𝑍 ) ∧ ∃ 𝑦 ∈ { 𝐴 , 𝐵 } ( 𝑥 ‘ 𝑦 ) ≠ 0 )
19 ovex ⊢ ( ℤring freeLMod { 0 , 1 } ) ∈ V
20 1 19 eqeltri ⊢ 𝑍 ∈ V
21 3z ⊢ 3 ∈ ℤ
22 6nn ⊢ 6 ∈ ℕ
23 22 nnzi ⊢ 6 ∈ ℤ
24 1 zlmodzxzel ⊢ ( ( 3 ∈ ℤ ∧ 6 ∈ ℤ ) → { ⟨ 0 , 3 ⟩ , ⟨ 1 , 6 ⟩ } ∈ ( Base ‘ 𝑍 ) )
25 21 23 24 mp2an ⊢ { ⟨ 0 , 3 ⟩ , ⟨ 1 , 6 ⟩ } ∈ ( Base ‘ 𝑍 )
26 2 25 eqeltri ⊢ 𝐴 ∈ ( Base ‘ 𝑍 )
27 2z ⊢ 2 ∈ ℤ
28 4z ⊢ 4 ∈ ℤ
29 1 zlmodzxzel ⊢ ( ( 2 ∈ ℤ ∧ 4 ∈ ℤ ) → { ⟨ 0 , 2 ⟩ , ⟨ 1 , 4 ⟩ } ∈ ( Base ‘ 𝑍 ) )
30 27 28 29 mp2an ⊢ { ⟨ 0 , 2 ⟩ , ⟨ 1 , 4 ⟩ } ∈ ( Base ‘ 𝑍 )
31 3 30 eqeltri ⊢ 𝐵 ∈ ( Base ‘ 𝑍 )
32 prelpwi ⊢ ( ( 𝐴 ∈ ( Base ‘ 𝑍 ) ∧ 𝐵 ∈ ( Base ‘ 𝑍 ) ) → { 𝐴 , 𝐵 } ∈ 𝒫 ( Base ‘ 𝑍 ) )
33 26 31 32 mp2an ⊢ { 𝐴 , 𝐵 } ∈ 𝒫 ( Base ‘ 𝑍 )
34 eqid ⊢ ( Base ‘ 𝑍 ) = ( Base ‘ 𝑍 )
35 eqid ⊢ ( 0g ‘ 𝑍 ) = ( 0g ‘ 𝑍 )
36 1 zlmodzxzlmod ⊢ ( 𝑍 ∈ LMod ∧ ℤring = ( Scalar ‘ 𝑍 ) )
37 36 simpri ⊢ ℤring = ( Scalar ‘ 𝑍 )
38 zringbas ⊢ ℤ = ( Base ‘ ℤring )
39 zring0 ⊢ 0 = ( 0g ‘ ℤring )
40 34 35 37 38 39 islindeps ⊢ ( ( 𝑍 ∈ V ∧ { 𝐴 , 𝐵 } ∈ 𝒫 ( Base ‘ 𝑍 ) ) → ( { 𝐴 , 𝐵 } linDepS 𝑍 ↔ ∃ 𝑥 ∈ ( ℤ ↑m { 𝐴 , 𝐵 } ) ( 𝑥 finSupp 0 ∧ ( 𝑥 ( linC ‘ 𝑍 ) { 𝐴 , 𝐵 } ) = ( 0g ‘ 𝑍 ) ∧ ∃ 𝑦 ∈ { 𝐴 , 𝐵 } ( 𝑥 ‘ 𝑦 ) ≠ 0 ) ) )
41 20 33 40 mp2an ⊢ ( { 𝐴 , 𝐵 } linDepS 𝑍 ↔ ∃ 𝑥 ∈ ( ℤ ↑m { 𝐴 , 𝐵 } ) ( 𝑥 finSupp 0 ∧ ( 𝑥 ( linC ‘ 𝑍 ) { 𝐴 , 𝐵 } ) = ( 0g ‘ 𝑍 ) ∧ ∃ 𝑦 ∈ { 𝐴 , 𝐵 } ( 𝑥 ‘ 𝑦 ) ≠ 0 ) )
42 18 41 mpbir ⊢ { 𝐴 , 𝐵 } linDepS 𝑍