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 |
|
elmapi |
⊢ ( 𝐹 ∈ ( ( Base ‘ ℤring ) ↑m { 𝐴 } ) → 𝐹 : { 𝐴 } ⟶ ( Base ‘ ℤring ) ) |
5 |
|
prex |
⊢ { 〈 0 , 3 〉 , 〈 1 , 6 〉 } ∈ V |
6 |
2 5
|
eqeltri |
⊢ 𝐴 ∈ V |
7 |
6
|
fsn2 |
⊢ ( 𝐹 : { 𝐴 } ⟶ ( Base ‘ ℤring ) ↔ ( ( 𝐹 ‘ 𝐴 ) ∈ ( Base ‘ ℤring ) ∧ 𝐹 = { 〈 𝐴 , ( 𝐹 ‘ 𝐴 ) 〉 } ) ) |
8 |
|
oveq1 |
⊢ ( 𝐹 = { 〈 𝐴 , ( 𝐹 ‘ 𝐴 ) 〉 } → ( 𝐹 ( linC ‘ 𝑍 ) { 𝐴 } ) = ( { 〈 𝐴 , ( 𝐹 ‘ 𝐴 ) 〉 } ( linC ‘ 𝑍 ) { 𝐴 } ) ) |
9 |
8
|
adantl |
⊢ ( ( ( 𝐹 ‘ 𝐴 ) ∈ ( Base ‘ ℤring ) ∧ 𝐹 = { 〈 𝐴 , ( 𝐹 ‘ 𝐴 ) 〉 } ) → ( 𝐹 ( linC ‘ 𝑍 ) { 𝐴 } ) = ( { 〈 𝐴 , ( 𝐹 ‘ 𝐴 ) 〉 } ( linC ‘ 𝑍 ) { 𝐴 } ) ) |
10 |
1
|
zlmodzxzlmod |
⊢ ( 𝑍 ∈ LMod ∧ ℤring = ( Scalar ‘ 𝑍 ) ) |
11 |
10
|
simpli |
⊢ 𝑍 ∈ LMod |
12 |
11
|
a1i |
⊢ ( ( ( 𝐹 ‘ 𝐴 ) ∈ ( Base ‘ ℤring ) ∧ 𝐹 = { 〈 𝐴 , ( 𝐹 ‘ 𝐴 ) 〉 } ) → 𝑍 ∈ LMod ) |
13 |
|
3z |
⊢ 3 ∈ ℤ |
14 |
|
6nn |
⊢ 6 ∈ ℕ |
15 |
14
|
nnzi |
⊢ 6 ∈ ℤ |
16 |
1
|
zlmodzxzel |
⊢ ( ( 3 ∈ ℤ ∧ 6 ∈ ℤ ) → { 〈 0 , 3 〉 , 〈 1 , 6 〉 } ∈ ( Base ‘ 𝑍 ) ) |
17 |
13 15 16
|
mp2an |
⊢ { 〈 0 , 3 〉 , 〈 1 , 6 〉 } ∈ ( Base ‘ 𝑍 ) |
18 |
2 17
|
eqeltri |
⊢ 𝐴 ∈ ( Base ‘ 𝑍 ) |
19 |
18
|
a1i |
⊢ ( ( ( 𝐹 ‘ 𝐴 ) ∈ ( Base ‘ ℤring ) ∧ 𝐹 = { 〈 𝐴 , ( 𝐹 ‘ 𝐴 ) 〉 } ) → 𝐴 ∈ ( Base ‘ 𝑍 ) ) |
20 |
|
simpl |
⊢ ( ( ( 𝐹 ‘ 𝐴 ) ∈ ( Base ‘ ℤring ) ∧ 𝐹 = { 〈 𝐴 , ( 𝐹 ‘ 𝐴 ) 〉 } ) → ( 𝐹 ‘ 𝐴 ) ∈ ( Base ‘ ℤring ) ) |
21 |
|
eqid |
⊢ ( Base ‘ 𝑍 ) = ( Base ‘ 𝑍 ) |
22 |
10
|
simpri |
⊢ ℤring = ( Scalar ‘ 𝑍 ) |
23 |
|
eqid |
⊢ ( Base ‘ ℤring ) = ( Base ‘ ℤring ) |
24 |
|
eqid |
⊢ ( ·𝑠 ‘ 𝑍 ) = ( ·𝑠 ‘ 𝑍 ) |
25 |
21 22 23 24
|
lincvalsng |
⊢ ( ( 𝑍 ∈ LMod ∧ 𝐴 ∈ ( Base ‘ 𝑍 ) ∧ ( 𝐹 ‘ 𝐴 ) ∈ ( Base ‘ ℤring ) ) → ( { 〈 𝐴 , ( 𝐹 ‘ 𝐴 ) 〉 } ( linC ‘ 𝑍 ) { 𝐴 } ) = ( ( 𝐹 ‘ 𝐴 ) ( ·𝑠 ‘ 𝑍 ) 𝐴 ) ) |
26 |
12 19 20 25
|
syl3anc |
⊢ ( ( ( 𝐹 ‘ 𝐴 ) ∈ ( Base ‘ ℤring ) ∧ 𝐹 = { 〈 𝐴 , ( 𝐹 ‘ 𝐴 ) 〉 } ) → ( { 〈 𝐴 , ( 𝐹 ‘ 𝐴 ) 〉 } ( linC ‘ 𝑍 ) { 𝐴 } ) = ( ( 𝐹 ‘ 𝐴 ) ( ·𝑠 ‘ 𝑍 ) 𝐴 ) ) |
27 |
9 26
|
eqtrd |
⊢ ( ( ( 𝐹 ‘ 𝐴 ) ∈ ( Base ‘ ℤring ) ∧ 𝐹 = { 〈 𝐴 , ( 𝐹 ‘ 𝐴 ) 〉 } ) → ( 𝐹 ( linC ‘ 𝑍 ) { 𝐴 } ) = ( ( 𝐹 ‘ 𝐴 ) ( ·𝑠 ‘ 𝑍 ) 𝐴 ) ) |
28 |
|
eqid |
⊢ { 〈 0 , 0 〉 , 〈 1 , 0 〉 } = { 〈 0 , 0 〉 , 〈 1 , 0 〉 } |
29 |
|
eqid |
⊢ ( -g ‘ 𝑍 ) = ( -g ‘ 𝑍 ) |
30 |
1 28 24 29 2 3
|
zlmodzxznm |
⊢ ∀ 𝑖 ∈ ℤ ( ( 𝑖 ( ·𝑠 ‘ 𝑍 ) 𝐴 ) ≠ 𝐵 ∧ ( 𝑖 ( ·𝑠 ‘ 𝑍 ) 𝐵 ) ≠ 𝐴 ) |
31 |
|
r19.26 |
⊢ ( ∀ 𝑖 ∈ ℤ ( ( 𝑖 ( ·𝑠 ‘ 𝑍 ) 𝐴 ) ≠ 𝐵 ∧ ( 𝑖 ( ·𝑠 ‘ 𝑍 ) 𝐵 ) ≠ 𝐴 ) ↔ ( ∀ 𝑖 ∈ ℤ ( 𝑖 ( ·𝑠 ‘ 𝑍 ) 𝐴 ) ≠ 𝐵 ∧ ∀ 𝑖 ∈ ℤ ( 𝑖 ( ·𝑠 ‘ 𝑍 ) 𝐵 ) ≠ 𝐴 ) ) |
32 |
|
oveq1 |
⊢ ( 𝑖 = ( 𝐹 ‘ 𝐴 ) → ( 𝑖 ( ·𝑠 ‘ 𝑍 ) 𝐴 ) = ( ( 𝐹 ‘ 𝐴 ) ( ·𝑠 ‘ 𝑍 ) 𝐴 ) ) |
33 |
32
|
neeq1d |
⊢ ( 𝑖 = ( 𝐹 ‘ 𝐴 ) → ( ( 𝑖 ( ·𝑠 ‘ 𝑍 ) 𝐴 ) ≠ 𝐵 ↔ ( ( 𝐹 ‘ 𝐴 ) ( ·𝑠 ‘ 𝑍 ) 𝐴 ) ≠ 𝐵 ) ) |
34 |
33
|
rspcv |
⊢ ( ( 𝐹 ‘ 𝐴 ) ∈ ℤ → ( ∀ 𝑖 ∈ ℤ ( 𝑖 ( ·𝑠 ‘ 𝑍 ) 𝐴 ) ≠ 𝐵 → ( ( 𝐹 ‘ 𝐴 ) ( ·𝑠 ‘ 𝑍 ) 𝐴 ) ≠ 𝐵 ) ) |
35 |
|
zringbas |
⊢ ℤ = ( Base ‘ ℤring ) |
36 |
35
|
eqcomi |
⊢ ( Base ‘ ℤring ) = ℤ |
37 |
36
|
eleq2i |
⊢ ( ( 𝐹 ‘ 𝐴 ) ∈ ( Base ‘ ℤring ) ↔ ( 𝐹 ‘ 𝐴 ) ∈ ℤ ) |
38 |
37
|
biimpi |
⊢ ( ( 𝐹 ‘ 𝐴 ) ∈ ( Base ‘ ℤring ) → ( 𝐹 ‘ 𝐴 ) ∈ ℤ ) |
39 |
38
|
adantr |
⊢ ( ( ( 𝐹 ‘ 𝐴 ) ∈ ( Base ‘ ℤring ) ∧ 𝐹 = { 〈 𝐴 , ( 𝐹 ‘ 𝐴 ) 〉 } ) → ( 𝐹 ‘ 𝐴 ) ∈ ℤ ) |
40 |
34 39
|
syl11 |
⊢ ( ∀ 𝑖 ∈ ℤ ( 𝑖 ( ·𝑠 ‘ 𝑍 ) 𝐴 ) ≠ 𝐵 → ( ( ( 𝐹 ‘ 𝐴 ) ∈ ( Base ‘ ℤring ) ∧ 𝐹 = { 〈 𝐴 , ( 𝐹 ‘ 𝐴 ) 〉 } ) → ( ( 𝐹 ‘ 𝐴 ) ( ·𝑠 ‘ 𝑍 ) 𝐴 ) ≠ 𝐵 ) ) |
41 |
40
|
adantr |
⊢ ( ( ∀ 𝑖 ∈ ℤ ( 𝑖 ( ·𝑠 ‘ 𝑍 ) 𝐴 ) ≠ 𝐵 ∧ ∀ 𝑖 ∈ ℤ ( 𝑖 ( ·𝑠 ‘ 𝑍 ) 𝐵 ) ≠ 𝐴 ) → ( ( ( 𝐹 ‘ 𝐴 ) ∈ ( Base ‘ ℤring ) ∧ 𝐹 = { 〈 𝐴 , ( 𝐹 ‘ 𝐴 ) 〉 } ) → ( ( 𝐹 ‘ 𝐴 ) ( ·𝑠 ‘ 𝑍 ) 𝐴 ) ≠ 𝐵 ) ) |
42 |
31 41
|
sylbi |
⊢ ( ∀ 𝑖 ∈ ℤ ( ( 𝑖 ( ·𝑠 ‘ 𝑍 ) 𝐴 ) ≠ 𝐵 ∧ ( 𝑖 ( ·𝑠 ‘ 𝑍 ) 𝐵 ) ≠ 𝐴 ) → ( ( ( 𝐹 ‘ 𝐴 ) ∈ ( Base ‘ ℤring ) ∧ 𝐹 = { 〈 𝐴 , ( 𝐹 ‘ 𝐴 ) 〉 } ) → ( ( 𝐹 ‘ 𝐴 ) ( ·𝑠 ‘ 𝑍 ) 𝐴 ) ≠ 𝐵 ) ) |
43 |
30 42
|
ax-mp |
⊢ ( ( ( 𝐹 ‘ 𝐴 ) ∈ ( Base ‘ ℤring ) ∧ 𝐹 = { 〈 𝐴 , ( 𝐹 ‘ 𝐴 ) 〉 } ) → ( ( 𝐹 ‘ 𝐴 ) ( ·𝑠 ‘ 𝑍 ) 𝐴 ) ≠ 𝐵 ) |
44 |
27 43
|
eqnetrd |
⊢ ( ( ( 𝐹 ‘ 𝐴 ) ∈ ( Base ‘ ℤring ) ∧ 𝐹 = { 〈 𝐴 , ( 𝐹 ‘ 𝐴 ) 〉 } ) → ( 𝐹 ( linC ‘ 𝑍 ) { 𝐴 } ) ≠ 𝐵 ) |
45 |
7 44
|
sylbi |
⊢ ( 𝐹 : { 𝐴 } ⟶ ( Base ‘ ℤring ) → ( 𝐹 ( linC ‘ 𝑍 ) { 𝐴 } ) ≠ 𝐵 ) |
46 |
4 45
|
syl |
⊢ ( 𝐹 ∈ ( ( Base ‘ ℤring ) ↑m { 𝐴 } ) → ( 𝐹 ( linC ‘ 𝑍 ) { 𝐴 } ) ≠ 𝐵 ) |