Step |
Hyp |
Ref |
Expression |
1 |
|
lveclmod |
⊢ ( 𝑣 ∈ LVec → 𝑣 ∈ LMod ) |
2 |
1
|
ssriv |
⊢ LVec ⊆ LMod |
3 |
|
vex |
⊢ 𝑖 ∈ V |
4 |
|
vex |
⊢ 𝑧 ∈ V |
5 |
3 4
|
pm3.2i |
⊢ ( 𝑖 ∈ V ∧ 𝑧 ∈ V ) |
6 |
|
eqid |
⊢ { 〈 ( Base ‘ ndx ) , { 𝑧 } 〉 , 〈 ( +g ‘ ndx ) , { 〈 〈 𝑧 , 𝑧 〉 , 𝑧 〉 } 〉 , 〈 ( .r ‘ ndx ) , { 〈 〈 𝑧 , 𝑧 〉 , 𝑧 〉 } 〉 } = { 〈 ( Base ‘ ndx ) , { 𝑧 } 〉 , 〈 ( +g ‘ ndx ) , { 〈 〈 𝑧 , 𝑧 〉 , 𝑧 〉 } 〉 , 〈 ( .r ‘ ndx ) , { 〈 〈 𝑧 , 𝑧 〉 , 𝑧 〉 } 〉 } |
7 |
|
eqid |
⊢ ( { 〈 ( Base ‘ ndx ) , { 𝑖 } 〉 , 〈 ( +g ‘ ndx ) , { 〈 〈 𝑖 , 𝑖 〉 , 𝑖 〉 } 〉 , 〈 ( Scalar ‘ ndx ) , { 〈 ( Base ‘ ndx ) , { 𝑧 } 〉 , 〈 ( +g ‘ ndx ) , { 〈 〈 𝑧 , 𝑧 〉 , 𝑧 〉 } 〉 , 〈 ( .r ‘ ndx ) , { 〈 〈 𝑧 , 𝑧 〉 , 𝑧 〉 } 〉 } 〉 } ∪ { 〈 ( ·𝑠 ‘ ndx ) , { 〈 〈 𝑧 , 𝑖 〉 , 𝑖 〉 } 〉 } ) = ( { 〈 ( Base ‘ ndx ) , { 𝑖 } 〉 , 〈 ( +g ‘ ndx ) , { 〈 〈 𝑖 , 𝑖 〉 , 𝑖 〉 } 〉 , 〈 ( Scalar ‘ ndx ) , { 〈 ( Base ‘ ndx ) , { 𝑧 } 〉 , 〈 ( +g ‘ ndx ) , { 〈 〈 𝑧 , 𝑧 〉 , 𝑧 〉 } 〉 , 〈 ( .r ‘ ndx ) , { 〈 〈 𝑧 , 𝑧 〉 , 𝑧 〉 } 〉 } 〉 } ∪ { 〈 ( ·𝑠 ‘ ndx ) , { 〈 〈 𝑧 , 𝑖 〉 , 𝑖 〉 } 〉 } ) |
8 |
6 7
|
lmod1zr |
⊢ ( ( 𝑖 ∈ V ∧ 𝑧 ∈ V ) → ( { 〈 ( Base ‘ ndx ) , { 𝑖 } 〉 , 〈 ( +g ‘ ndx ) , { 〈 〈 𝑖 , 𝑖 〉 , 𝑖 〉 } 〉 , 〈 ( Scalar ‘ ndx ) , { 〈 ( Base ‘ ndx ) , { 𝑧 } 〉 , 〈 ( +g ‘ ndx ) , { 〈 〈 𝑧 , 𝑧 〉 , 𝑧 〉 } 〉 , 〈 ( .r ‘ ndx ) , { 〈 〈 𝑧 , 𝑧 〉 , 𝑧 〉 } 〉 } 〉 } ∪ { 〈 ( ·𝑠 ‘ ndx ) , { 〈 〈 𝑧 , 𝑖 〉 , 𝑖 〉 } 〉 } ) ∈ LMod ) |
9 |
6 7
|
lmod1zrnlvec |
⊢ ( ( 𝑖 ∈ V ∧ 𝑧 ∈ V ) → ( { 〈 ( Base ‘ ndx ) , { 𝑖 } 〉 , 〈 ( +g ‘ ndx ) , { 〈 〈 𝑖 , 𝑖 〉 , 𝑖 〉 } 〉 , 〈 ( Scalar ‘ ndx ) , { 〈 ( Base ‘ ndx ) , { 𝑧 } 〉 , 〈 ( +g ‘ ndx ) , { 〈 〈 𝑧 , 𝑧 〉 , 𝑧 〉 } 〉 , 〈 ( .r ‘ ndx ) , { 〈 〈 𝑧 , 𝑧 〉 , 𝑧 〉 } 〉 } 〉 } ∪ { 〈 ( ·𝑠 ‘ ndx ) , { 〈 〈 𝑧 , 𝑖 〉 , 𝑖 〉 } 〉 } ) ∉ LVec ) |
10 |
|
df-nel |
⊢ ( ( { 〈 ( Base ‘ ndx ) , { 𝑖 } 〉 , 〈 ( +g ‘ ndx ) , { 〈 〈 𝑖 , 𝑖 〉 , 𝑖 〉 } 〉 , 〈 ( Scalar ‘ ndx ) , { 〈 ( Base ‘ ndx ) , { 𝑧 } 〉 , 〈 ( +g ‘ ndx ) , { 〈 〈 𝑧 , 𝑧 〉 , 𝑧 〉 } 〉 , 〈 ( .r ‘ ndx ) , { 〈 〈 𝑧 , 𝑧 〉 , 𝑧 〉 } 〉 } 〉 } ∪ { 〈 ( ·𝑠 ‘ ndx ) , { 〈 〈 𝑧 , 𝑖 〉 , 𝑖 〉 } 〉 } ) ∉ LVec ↔ ¬ ( { 〈 ( Base ‘ ndx ) , { 𝑖 } 〉 , 〈 ( +g ‘ ndx ) , { 〈 〈 𝑖 , 𝑖 〉 , 𝑖 〉 } 〉 , 〈 ( Scalar ‘ ndx ) , { 〈 ( Base ‘ ndx ) , { 𝑧 } 〉 , 〈 ( +g ‘ ndx ) , { 〈 〈 𝑧 , 𝑧 〉 , 𝑧 〉 } 〉 , 〈 ( .r ‘ ndx ) , { 〈 〈 𝑧 , 𝑧 〉 , 𝑧 〉 } 〉 } 〉 } ∪ { 〈 ( ·𝑠 ‘ ndx ) , { 〈 〈 𝑧 , 𝑖 〉 , 𝑖 〉 } 〉 } ) ∈ LVec ) |
11 |
9 10
|
sylib |
⊢ ( ( 𝑖 ∈ V ∧ 𝑧 ∈ V ) → ¬ ( { 〈 ( Base ‘ ndx ) , { 𝑖 } 〉 , 〈 ( +g ‘ ndx ) , { 〈 〈 𝑖 , 𝑖 〉 , 𝑖 〉 } 〉 , 〈 ( Scalar ‘ ndx ) , { 〈 ( Base ‘ ndx ) , { 𝑧 } 〉 , 〈 ( +g ‘ ndx ) , { 〈 〈 𝑧 , 𝑧 〉 , 𝑧 〉 } 〉 , 〈 ( .r ‘ ndx ) , { 〈 〈 𝑧 , 𝑧 〉 , 𝑧 〉 } 〉 } 〉 } ∪ { 〈 ( ·𝑠 ‘ ndx ) , { 〈 〈 𝑧 , 𝑖 〉 , 𝑖 〉 } 〉 } ) ∈ LVec ) |
12 |
8 11
|
jca |
⊢ ( ( 𝑖 ∈ V ∧ 𝑧 ∈ V ) → ( ( { 〈 ( Base ‘ ndx ) , { 𝑖 } 〉 , 〈 ( +g ‘ ndx ) , { 〈 〈 𝑖 , 𝑖 〉 , 𝑖 〉 } 〉 , 〈 ( Scalar ‘ ndx ) , { 〈 ( Base ‘ ndx ) , { 𝑧 } 〉 , 〈 ( +g ‘ ndx ) , { 〈 〈 𝑧 , 𝑧 〉 , 𝑧 〉 } 〉 , 〈 ( .r ‘ ndx ) , { 〈 〈 𝑧 , 𝑧 〉 , 𝑧 〉 } 〉 } 〉 } ∪ { 〈 ( ·𝑠 ‘ ndx ) , { 〈 〈 𝑧 , 𝑖 〉 , 𝑖 〉 } 〉 } ) ∈ LMod ∧ ¬ ( { 〈 ( Base ‘ ndx ) , { 𝑖 } 〉 , 〈 ( +g ‘ ndx ) , { 〈 〈 𝑖 , 𝑖 〉 , 𝑖 〉 } 〉 , 〈 ( Scalar ‘ ndx ) , { 〈 ( Base ‘ ndx ) , { 𝑧 } 〉 , 〈 ( +g ‘ ndx ) , { 〈 〈 𝑧 , 𝑧 〉 , 𝑧 〉 } 〉 , 〈 ( .r ‘ ndx ) , { 〈 〈 𝑧 , 𝑧 〉 , 𝑧 〉 } 〉 } 〉 } ∪ { 〈 ( ·𝑠 ‘ ndx ) , { 〈 〈 𝑧 , 𝑖 〉 , 𝑖 〉 } 〉 } ) ∈ LVec ) ) |
13 |
|
nelne1 |
⊢ ( ( ( { 〈 ( Base ‘ ndx ) , { 𝑖 } 〉 , 〈 ( +g ‘ ndx ) , { 〈 〈 𝑖 , 𝑖 〉 , 𝑖 〉 } 〉 , 〈 ( Scalar ‘ ndx ) , { 〈 ( Base ‘ ndx ) , { 𝑧 } 〉 , 〈 ( +g ‘ ndx ) , { 〈 〈 𝑧 , 𝑧 〉 , 𝑧 〉 } 〉 , 〈 ( .r ‘ ndx ) , { 〈 〈 𝑧 , 𝑧 〉 , 𝑧 〉 } 〉 } 〉 } ∪ { 〈 ( ·𝑠 ‘ ndx ) , { 〈 〈 𝑧 , 𝑖 〉 , 𝑖 〉 } 〉 } ) ∈ LMod ∧ ¬ ( { 〈 ( Base ‘ ndx ) , { 𝑖 } 〉 , 〈 ( +g ‘ ndx ) , { 〈 〈 𝑖 , 𝑖 〉 , 𝑖 〉 } 〉 , 〈 ( Scalar ‘ ndx ) , { 〈 ( Base ‘ ndx ) , { 𝑧 } 〉 , 〈 ( +g ‘ ndx ) , { 〈 〈 𝑧 , 𝑧 〉 , 𝑧 〉 } 〉 , 〈 ( .r ‘ ndx ) , { 〈 〈 𝑧 , 𝑧 〉 , 𝑧 〉 } 〉 } 〉 } ∪ { 〈 ( ·𝑠 ‘ ndx ) , { 〈 〈 𝑧 , 𝑖 〉 , 𝑖 〉 } 〉 } ) ∈ LVec ) → LMod ≠ LVec ) |
14 |
13
|
necomd |
⊢ ( ( ( { 〈 ( Base ‘ ndx ) , { 𝑖 } 〉 , 〈 ( +g ‘ ndx ) , { 〈 〈 𝑖 , 𝑖 〉 , 𝑖 〉 } 〉 , 〈 ( Scalar ‘ ndx ) , { 〈 ( Base ‘ ndx ) , { 𝑧 } 〉 , 〈 ( +g ‘ ndx ) , { 〈 〈 𝑧 , 𝑧 〉 , 𝑧 〉 } 〉 , 〈 ( .r ‘ ndx ) , { 〈 〈 𝑧 , 𝑧 〉 , 𝑧 〉 } 〉 } 〉 } ∪ { 〈 ( ·𝑠 ‘ ndx ) , { 〈 〈 𝑧 , 𝑖 〉 , 𝑖 〉 } 〉 } ) ∈ LMod ∧ ¬ ( { 〈 ( Base ‘ ndx ) , { 𝑖 } 〉 , 〈 ( +g ‘ ndx ) , { 〈 〈 𝑖 , 𝑖 〉 , 𝑖 〉 } 〉 , 〈 ( Scalar ‘ ndx ) , { 〈 ( Base ‘ ndx ) , { 𝑧 } 〉 , 〈 ( +g ‘ ndx ) , { 〈 〈 𝑧 , 𝑧 〉 , 𝑧 〉 } 〉 , 〈 ( .r ‘ ndx ) , { 〈 〈 𝑧 , 𝑧 〉 , 𝑧 〉 } 〉 } 〉 } ∪ { 〈 ( ·𝑠 ‘ ndx ) , { 〈 〈 𝑧 , 𝑖 〉 , 𝑖 〉 } 〉 } ) ∈ LVec ) → LVec ≠ LMod ) |
15 |
5 12 14
|
mp2b |
⊢ LVec ≠ LMod |
16 |
|
df-pss |
⊢ ( LVec ⊊ LMod ↔ ( LVec ⊆ LMod ∧ LVec ≠ LMod ) ) |
17 |
2 15 16
|
mpbir2an |
⊢ LVec ⊊ LMod |