| Step | Hyp | Ref | Expression | 
|---|
| 1 |  | issubassa.s | . . . 4
⊢ 𝑆 = (𝑊 ↾s 𝐴) | 
| 2 | 1 | subrgbas 20581 | . . 3
⊢ (𝐴 ∈ (SubRing‘𝑊) → 𝐴 = (Base‘𝑆)) | 
| 3 | 2 | ad2antrl 728 | . 2
⊢ ((𝑊 ∈ AssAlg ∧ (𝐴 ∈ (SubRing‘𝑊) ∧ 𝐴 ∈ 𝐿)) → 𝐴 = (Base‘𝑆)) | 
| 4 |  | eqid 2737 | . . . 4
⊢
(Scalar‘𝑊) =
(Scalar‘𝑊) | 
| 5 | 1, 4 | resssca 17387 | . . 3
⊢ (𝐴 ∈ (SubRing‘𝑊) → (Scalar‘𝑊) = (Scalar‘𝑆)) | 
| 6 | 5 | ad2antrl 728 | . 2
⊢ ((𝑊 ∈ AssAlg ∧ (𝐴 ∈ (SubRing‘𝑊) ∧ 𝐴 ∈ 𝐿)) → (Scalar‘𝑊) = (Scalar‘𝑆)) | 
| 7 |  | eqidd 2738 | . 2
⊢ ((𝑊 ∈ AssAlg ∧ (𝐴 ∈ (SubRing‘𝑊) ∧ 𝐴 ∈ 𝐿)) → (Base‘(Scalar‘𝑊)) =
(Base‘(Scalar‘𝑊))) | 
| 8 |  | eqid 2737 | . . . 4
⊢ (
·𝑠 ‘𝑊) = ( ·𝑠
‘𝑊) | 
| 9 | 1, 8 | ressvsca 17388 | . . 3
⊢ (𝐴 ∈ (SubRing‘𝑊) → (
·𝑠 ‘𝑊) = ( ·𝑠
‘𝑆)) | 
| 10 | 9 | ad2antrl 728 | . 2
⊢ ((𝑊 ∈ AssAlg ∧ (𝐴 ∈ (SubRing‘𝑊) ∧ 𝐴 ∈ 𝐿)) → (
·𝑠 ‘𝑊) = ( ·𝑠
‘𝑆)) | 
| 11 |  | eqid 2737 | . . . 4
⊢
(.r‘𝑊) = (.r‘𝑊) | 
| 12 | 1, 11 | ressmulr 17351 | . . 3
⊢ (𝐴 ∈ (SubRing‘𝑊) →
(.r‘𝑊) =
(.r‘𝑆)) | 
| 13 | 12 | ad2antrl 728 | . 2
⊢ ((𝑊 ∈ AssAlg ∧ (𝐴 ∈ (SubRing‘𝑊) ∧ 𝐴 ∈ 𝐿)) → (.r‘𝑊) = (.r‘𝑆)) | 
| 14 |  | assalmod 21880 | . . 3
⊢ (𝑊 ∈ AssAlg → 𝑊 ∈ LMod) | 
| 15 |  | simpr 484 | . . 3
⊢ ((𝐴 ∈ (SubRing‘𝑊) ∧ 𝐴 ∈ 𝐿) → 𝐴 ∈ 𝐿) | 
| 16 |  | issubassa.l | . . . 4
⊢ 𝐿 = (LSubSp‘𝑊) | 
| 17 | 1, 16 | lsslmod 20958 | . . 3
⊢ ((𝑊 ∈ LMod ∧ 𝐴 ∈ 𝐿) → 𝑆 ∈ LMod) | 
| 18 | 14, 15, 17 | syl2an 596 | . 2
⊢ ((𝑊 ∈ AssAlg ∧ (𝐴 ∈ (SubRing‘𝑊) ∧ 𝐴 ∈ 𝐿)) → 𝑆 ∈ LMod) | 
| 19 | 1 | subrgring 20574 | . . 3
⊢ (𝐴 ∈ (SubRing‘𝑊) → 𝑆 ∈ Ring) | 
| 20 | 19 | ad2antrl 728 | . 2
⊢ ((𝑊 ∈ AssAlg ∧ (𝐴 ∈ (SubRing‘𝑊) ∧ 𝐴 ∈ 𝐿)) → 𝑆 ∈ Ring) | 
| 21 |  | idd 24 | . . . . 5
⊢ ((𝑊 ∈ AssAlg ∧ (𝐴 ∈ (SubRing‘𝑊) ∧ 𝐴 ∈ 𝐿)) → (𝑥 ∈ (Base‘(Scalar‘𝑊)) → 𝑥 ∈ (Base‘(Scalar‘𝑊)))) | 
| 22 |  | eqid 2737 | . . . . . . . 8
⊢
(Base‘𝑊) =
(Base‘𝑊) | 
| 23 | 22 | subrgss 20572 | . . . . . . 7
⊢ (𝐴 ∈ (SubRing‘𝑊) → 𝐴 ⊆ (Base‘𝑊)) | 
| 24 | 23 | ad2antrl 728 | . . . . . 6
⊢ ((𝑊 ∈ AssAlg ∧ (𝐴 ∈ (SubRing‘𝑊) ∧ 𝐴 ∈ 𝐿)) → 𝐴 ⊆ (Base‘𝑊)) | 
| 25 | 24 | sseld 3982 | . . . . 5
⊢ ((𝑊 ∈ AssAlg ∧ (𝐴 ∈ (SubRing‘𝑊) ∧ 𝐴 ∈ 𝐿)) → (𝑦 ∈ 𝐴 → 𝑦 ∈ (Base‘𝑊))) | 
| 26 | 24 | sseld 3982 | . . . . 5
⊢ ((𝑊 ∈ AssAlg ∧ (𝐴 ∈ (SubRing‘𝑊) ∧ 𝐴 ∈ 𝐿)) → (𝑧 ∈ 𝐴 → 𝑧 ∈ (Base‘𝑊))) | 
| 27 | 21, 25, 26 | 3anim123d 1445 | . . . 4
⊢ ((𝑊 ∈ AssAlg ∧ (𝐴 ∈ (SubRing‘𝑊) ∧ 𝐴 ∈ 𝐿)) → ((𝑥 ∈ (Base‘(Scalar‘𝑊)) ∧ 𝑦 ∈ 𝐴 ∧ 𝑧 ∈ 𝐴) → (𝑥 ∈ (Base‘(Scalar‘𝑊)) ∧ 𝑦 ∈ (Base‘𝑊) ∧ 𝑧 ∈ (Base‘𝑊)))) | 
| 28 | 27 | imp 406 | . . 3
⊢ (((𝑊 ∈ AssAlg ∧ (𝐴 ∈ (SubRing‘𝑊) ∧ 𝐴 ∈ 𝐿)) ∧ (𝑥 ∈ (Base‘(Scalar‘𝑊)) ∧ 𝑦 ∈ 𝐴 ∧ 𝑧 ∈ 𝐴)) → (𝑥 ∈ (Base‘(Scalar‘𝑊)) ∧ 𝑦 ∈ (Base‘𝑊) ∧ 𝑧 ∈ (Base‘𝑊))) | 
| 29 |  | eqid 2737 | . . . . 5
⊢
(Base‘(Scalar‘𝑊)) = (Base‘(Scalar‘𝑊)) | 
| 30 | 22, 4, 29, 8, 11 | assaass 21878 | . . . 4
⊢ ((𝑊 ∈ AssAlg ∧ (𝑥 ∈
(Base‘(Scalar‘𝑊)) ∧ 𝑦 ∈ (Base‘𝑊) ∧ 𝑧 ∈ (Base‘𝑊))) → ((𝑥( ·𝑠
‘𝑊)𝑦)(.r‘𝑊)𝑧) = (𝑥( ·𝑠
‘𝑊)(𝑦(.r‘𝑊)𝑧))) | 
| 31 | 30 | adantlr 715 | . . 3
⊢ (((𝑊 ∈ AssAlg ∧ (𝐴 ∈ (SubRing‘𝑊) ∧ 𝐴 ∈ 𝐿)) ∧ (𝑥 ∈ (Base‘(Scalar‘𝑊)) ∧ 𝑦 ∈ (Base‘𝑊) ∧ 𝑧 ∈ (Base‘𝑊))) → ((𝑥( ·𝑠
‘𝑊)𝑦)(.r‘𝑊)𝑧) = (𝑥( ·𝑠
‘𝑊)(𝑦(.r‘𝑊)𝑧))) | 
| 32 | 28, 31 | syldan 591 | . 2
⊢ (((𝑊 ∈ AssAlg ∧ (𝐴 ∈ (SubRing‘𝑊) ∧ 𝐴 ∈ 𝐿)) ∧ (𝑥 ∈ (Base‘(Scalar‘𝑊)) ∧ 𝑦 ∈ 𝐴 ∧ 𝑧 ∈ 𝐴)) → ((𝑥( ·𝑠
‘𝑊)𝑦)(.r‘𝑊)𝑧) = (𝑥( ·𝑠
‘𝑊)(𝑦(.r‘𝑊)𝑧))) | 
| 33 | 22, 4, 29, 8, 11 | assaassr 21879 | . . . 4
⊢ ((𝑊 ∈ AssAlg ∧ (𝑥 ∈
(Base‘(Scalar‘𝑊)) ∧ 𝑦 ∈ (Base‘𝑊) ∧ 𝑧 ∈ (Base‘𝑊))) → (𝑦(.r‘𝑊)(𝑥( ·𝑠
‘𝑊)𝑧)) = (𝑥( ·𝑠
‘𝑊)(𝑦(.r‘𝑊)𝑧))) | 
| 34 | 33 | adantlr 715 | . . 3
⊢ (((𝑊 ∈ AssAlg ∧ (𝐴 ∈ (SubRing‘𝑊) ∧ 𝐴 ∈ 𝐿)) ∧ (𝑥 ∈ (Base‘(Scalar‘𝑊)) ∧ 𝑦 ∈ (Base‘𝑊) ∧ 𝑧 ∈ (Base‘𝑊))) → (𝑦(.r‘𝑊)(𝑥( ·𝑠
‘𝑊)𝑧)) = (𝑥( ·𝑠
‘𝑊)(𝑦(.r‘𝑊)𝑧))) | 
| 35 | 28, 34 | syldan 591 | . 2
⊢ (((𝑊 ∈ AssAlg ∧ (𝐴 ∈ (SubRing‘𝑊) ∧ 𝐴 ∈ 𝐿)) ∧ (𝑥 ∈ (Base‘(Scalar‘𝑊)) ∧ 𝑦 ∈ 𝐴 ∧ 𝑧 ∈ 𝐴)) → (𝑦(.r‘𝑊)(𝑥( ·𝑠
‘𝑊)𝑧)) = (𝑥( ·𝑠
‘𝑊)(𝑦(.r‘𝑊)𝑧))) | 
| 36 | 3, 6, 7, 10, 13, 18, 20, 32, 35 | isassad 21885 | 1
⊢ ((𝑊 ∈ AssAlg ∧ (𝐴 ∈ (SubRing‘𝑊) ∧ 𝐴 ∈ 𝐿)) → 𝑆 ∈ AssAlg) |