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 |