| Step |
Hyp |
Ref |
Expression |
| 1 |
|
lmod1.m |
⊢ 𝑀 = ( { ⟨ ( Base ‘ ndx ) , { 𝐼 } ⟩ , ⟨ ( +g ‘ ndx ) , { ⟨ ⟨ 𝐼 , 𝐼 ⟩ , 𝐼 ⟩ } ⟩ , ⟨ ( Scalar ‘ ndx ) , 𝑅 ⟩ } ∪ { ⟨ ( ·𝑠 ‘ ndx ) , ( 𝑥 ∈ ( Base ‘ 𝑅 ) , 𝑦 ∈ { 𝐼 } ↦ 𝑦 ) ⟩ } ) |
| 2 |
|
fvex |
⊢ ( Base ‘ 𝑅 ) ∈ V |
| 3 |
|
snex |
⊢ { 𝐼 } ∈ V |
| 4 |
2 3
|
pm3.2i |
⊢ ( ( Base ‘ 𝑅 ) ∈ V ∧ { 𝐼 } ∈ V ) |
| 5 |
4
|
a1i |
⊢ ( ( ( 𝐼 ∈ 𝑉 ∧ 𝑅 ∈ Ring ) ∧ ( 𝑞 ∈ ( Base ‘ 𝑅 ) ∧ 𝑟 ∈ ( Base ‘ 𝑅 ) ) ) → ( ( Base ‘ 𝑅 ) ∈ V ∧ { 𝐼 } ∈ V ) ) |
| 6 |
|
mpoexga |
⊢ ( ( ( Base ‘ 𝑅 ) ∈ V ∧ { 𝐼 } ∈ V ) → ( 𝑥 ∈ ( Base ‘ 𝑅 ) , 𝑦 ∈ { 𝐼 } ↦ 𝑦 ) ∈ V ) |
| 7 |
1
|
lmodvsca |
⊢ ( ( 𝑥 ∈ ( Base ‘ 𝑅 ) , 𝑦 ∈ { 𝐼 } ↦ 𝑦 ) ∈ V → ( 𝑥 ∈ ( Base ‘ 𝑅 ) , 𝑦 ∈ { 𝐼 } ↦ 𝑦 ) = ( ·𝑠 ‘ 𝑀 ) ) |
| 8 |
5 6 7
|
3syl |
⊢ ( ( ( 𝐼 ∈ 𝑉 ∧ 𝑅 ∈ Ring ) ∧ ( 𝑞 ∈ ( Base ‘ 𝑅 ) ∧ 𝑟 ∈ ( Base ‘ 𝑅 ) ) ) → ( 𝑥 ∈ ( Base ‘ 𝑅 ) , 𝑦 ∈ { 𝐼 } ↦ 𝑦 ) = ( ·𝑠 ‘ 𝑀 ) ) |
| 9 |
8
|
eqcomd |
⊢ ( ( ( 𝐼 ∈ 𝑉 ∧ 𝑅 ∈ Ring ) ∧ ( 𝑞 ∈ ( Base ‘ 𝑅 ) ∧ 𝑟 ∈ ( Base ‘ 𝑅 ) ) ) → ( ·𝑠 ‘ 𝑀 ) = ( 𝑥 ∈ ( Base ‘ 𝑅 ) , 𝑦 ∈ { 𝐼 } ↦ 𝑦 ) ) |
| 10 |
|
simprr |
⊢ ( ( ( ( 𝐼 ∈ 𝑉 ∧ 𝑅 ∈ Ring ) ∧ ( 𝑞 ∈ ( Base ‘ 𝑅 ) ∧ 𝑟 ∈ ( Base ‘ 𝑅 ) ) ) ∧ ( 𝑥 = 𝑞 ∧ 𝑦 = 𝐼 ) ) → 𝑦 = 𝐼 ) |
| 11 |
|
simprl |
⊢ ( ( ( 𝐼 ∈ 𝑉 ∧ 𝑅 ∈ Ring ) ∧ ( 𝑞 ∈ ( Base ‘ 𝑅 ) ∧ 𝑟 ∈ ( Base ‘ 𝑅 ) ) ) → 𝑞 ∈ ( Base ‘ 𝑅 ) ) |
| 12 |
|
snidg |
⊢ ( 𝐼 ∈ 𝑉 → 𝐼 ∈ { 𝐼 } ) |
| 13 |
12
|
ad2antrr |
⊢ ( ( ( 𝐼 ∈ 𝑉 ∧ 𝑅 ∈ Ring ) ∧ ( 𝑞 ∈ ( Base ‘ 𝑅 ) ∧ 𝑟 ∈ ( Base ‘ 𝑅 ) ) ) → 𝐼 ∈ { 𝐼 } ) |
| 14 |
9 10 11 13 13
|
ovmpod |
⊢ ( ( ( 𝐼 ∈ 𝑉 ∧ 𝑅 ∈ Ring ) ∧ ( 𝑞 ∈ ( Base ‘ 𝑅 ) ∧ 𝑟 ∈ ( Base ‘ 𝑅 ) ) ) → ( 𝑞 ( ·𝑠 ‘ 𝑀 ) 𝐼 ) = 𝐼 ) |
| 15 |
|
simprr |
⊢ ( ( ( ( 𝐼 ∈ 𝑉 ∧ 𝑅 ∈ Ring ) ∧ ( 𝑞 ∈ ( Base ‘ 𝑅 ) ∧ 𝑟 ∈ ( Base ‘ 𝑅 ) ) ) ∧ ( 𝑥 = 𝑟 ∧ 𝑦 = 𝐼 ) ) → 𝑦 = 𝐼 ) |
| 16 |
|
simprr |
⊢ ( ( ( 𝐼 ∈ 𝑉 ∧ 𝑅 ∈ Ring ) ∧ ( 𝑞 ∈ ( Base ‘ 𝑅 ) ∧ 𝑟 ∈ ( Base ‘ 𝑅 ) ) ) → 𝑟 ∈ ( Base ‘ 𝑅 ) ) |
| 17 |
9 15 16 13 13
|
ovmpod |
⊢ ( ( ( 𝐼 ∈ 𝑉 ∧ 𝑅 ∈ Ring ) ∧ ( 𝑞 ∈ ( Base ‘ 𝑅 ) ∧ 𝑟 ∈ ( Base ‘ 𝑅 ) ) ) → ( 𝑟 ( ·𝑠 ‘ 𝑀 ) 𝐼 ) = 𝐼 ) |
| 18 |
17
|
oveq2d |
⊢ ( ( ( 𝐼 ∈ 𝑉 ∧ 𝑅 ∈ Ring ) ∧ ( 𝑞 ∈ ( Base ‘ 𝑅 ) ∧ 𝑟 ∈ ( Base ‘ 𝑅 ) ) ) → ( 𝑞 ( ·𝑠 ‘ 𝑀 ) ( 𝑟 ( ·𝑠 ‘ 𝑀 ) 𝐼 ) ) = ( 𝑞 ( ·𝑠 ‘ 𝑀 ) 𝐼 ) ) |
| 19 |
|
simprr |
⊢ ( ( ( ( 𝐼 ∈ 𝑉 ∧ 𝑅 ∈ Ring ) ∧ ( 𝑞 ∈ ( Base ‘ 𝑅 ) ∧ 𝑟 ∈ ( Base ‘ 𝑅 ) ) ) ∧ ( 𝑥 = ( 𝑞 ( .r ‘ ( Scalar ‘ 𝑀 ) ) 𝑟 ) ∧ 𝑦 = 𝐼 ) ) → 𝑦 = 𝐼 ) |
| 20 |
|
simplr |
⊢ ( ( ( 𝐼 ∈ 𝑉 ∧ 𝑅 ∈ Ring ) ∧ ( 𝑞 ∈ ( Base ‘ 𝑅 ) ∧ 𝑟 ∈ ( Base ‘ 𝑅 ) ) ) → 𝑅 ∈ Ring ) |
| 21 |
1
|
lmodsca |
⊢ ( 𝑅 ∈ Ring → 𝑅 = ( Scalar ‘ 𝑀 ) ) |
| 22 |
21
|
fveq2d |
⊢ ( 𝑅 ∈ Ring → ( .r ‘ 𝑅 ) = ( .r ‘ ( Scalar ‘ 𝑀 ) ) ) |
| 23 |
20 22
|
syl |
⊢ ( ( ( 𝐼 ∈ 𝑉 ∧ 𝑅 ∈ Ring ) ∧ ( 𝑞 ∈ ( Base ‘ 𝑅 ) ∧ 𝑟 ∈ ( Base ‘ 𝑅 ) ) ) → ( .r ‘ 𝑅 ) = ( .r ‘ ( Scalar ‘ 𝑀 ) ) ) |
| 24 |
23
|
eqcomd |
⊢ ( ( ( 𝐼 ∈ 𝑉 ∧ 𝑅 ∈ Ring ) ∧ ( 𝑞 ∈ ( Base ‘ 𝑅 ) ∧ 𝑟 ∈ ( Base ‘ 𝑅 ) ) ) → ( .r ‘ ( Scalar ‘ 𝑀 ) ) = ( .r ‘ 𝑅 ) ) |
| 25 |
24
|
oveqd |
⊢ ( ( ( 𝐼 ∈ 𝑉 ∧ 𝑅 ∈ Ring ) ∧ ( 𝑞 ∈ ( Base ‘ 𝑅 ) ∧ 𝑟 ∈ ( Base ‘ 𝑅 ) ) ) → ( 𝑞 ( .r ‘ ( Scalar ‘ 𝑀 ) ) 𝑟 ) = ( 𝑞 ( .r ‘ 𝑅 ) 𝑟 ) ) |
| 26 |
|
eqid |
⊢ ( Base ‘ 𝑅 ) = ( Base ‘ 𝑅 ) |
| 27 |
|
eqid |
⊢ ( .r ‘ 𝑅 ) = ( .r ‘ 𝑅 ) |
| 28 |
26 27
|
ringcl |
⊢ ( ( 𝑅 ∈ Ring ∧ 𝑞 ∈ ( Base ‘ 𝑅 ) ∧ 𝑟 ∈ ( Base ‘ 𝑅 ) ) → ( 𝑞 ( .r ‘ 𝑅 ) 𝑟 ) ∈ ( Base ‘ 𝑅 ) ) |
| 29 |
20 11 16 28
|
syl3anc |
⊢ ( ( ( 𝐼 ∈ 𝑉 ∧ 𝑅 ∈ Ring ) ∧ ( 𝑞 ∈ ( Base ‘ 𝑅 ) ∧ 𝑟 ∈ ( Base ‘ 𝑅 ) ) ) → ( 𝑞 ( .r ‘ 𝑅 ) 𝑟 ) ∈ ( Base ‘ 𝑅 ) ) |
| 30 |
25 29
|
eqeltrd |
⊢ ( ( ( 𝐼 ∈ 𝑉 ∧ 𝑅 ∈ Ring ) ∧ ( 𝑞 ∈ ( Base ‘ 𝑅 ) ∧ 𝑟 ∈ ( Base ‘ 𝑅 ) ) ) → ( 𝑞 ( .r ‘ ( Scalar ‘ 𝑀 ) ) 𝑟 ) ∈ ( Base ‘ 𝑅 ) ) |
| 31 |
9 19 30 13 13
|
ovmpod |
⊢ ( ( ( 𝐼 ∈ 𝑉 ∧ 𝑅 ∈ Ring ) ∧ ( 𝑞 ∈ ( Base ‘ 𝑅 ) ∧ 𝑟 ∈ ( Base ‘ 𝑅 ) ) ) → ( ( 𝑞 ( .r ‘ ( Scalar ‘ 𝑀 ) ) 𝑟 ) ( ·𝑠 ‘ 𝑀 ) 𝐼 ) = 𝐼 ) |
| 32 |
14 18 31
|
3eqtr4rd |
⊢ ( ( ( 𝐼 ∈ 𝑉 ∧ 𝑅 ∈ Ring ) ∧ ( 𝑞 ∈ ( Base ‘ 𝑅 ) ∧ 𝑟 ∈ ( Base ‘ 𝑅 ) ) ) → ( ( 𝑞 ( .r ‘ ( Scalar ‘ 𝑀 ) ) 𝑟 ) ( ·𝑠 ‘ 𝑀 ) 𝐼 ) = ( 𝑞 ( ·𝑠 ‘ 𝑀 ) ( 𝑟 ( ·𝑠 ‘ 𝑀 ) 𝐼 ) ) ) |