| Step | Hyp | Ref | Expression | 
|---|
| 1 |  | issubassa2.a | . . . . 5
⊢ 𝐴 = (algSc‘𝑊) | 
| 2 |  | eqid 2737 | . . . . 5
⊢
(1r‘𝑊) = (1r‘𝑊) | 
| 3 |  | eqid 2737 | . . . . 5
⊢
(LSpan‘𝑊) =
(LSpan‘𝑊) | 
| 4 | 1, 2, 3 | rnascl 21911 | . . . 4
⊢ (𝑊 ∈ AssAlg → ran 𝐴 = ((LSpan‘𝑊)‘{(1r‘𝑊)})) | 
| 5 | 4 | ad2antrr 726 | . . 3
⊢ (((𝑊 ∈ AssAlg ∧ 𝑆 ∈ (SubRing‘𝑊)) ∧ 𝑆 ∈ 𝐿) → ran 𝐴 = ((LSpan‘𝑊)‘{(1r‘𝑊)})) | 
| 6 |  | issubassa2.l | . . . 4
⊢ 𝐿 = (LSubSp‘𝑊) | 
| 7 |  | assalmod 21880 | . . . . 5
⊢ (𝑊 ∈ AssAlg → 𝑊 ∈ LMod) | 
| 8 | 7 | ad2antrr 726 | . . . 4
⊢ (((𝑊 ∈ AssAlg ∧ 𝑆 ∈ (SubRing‘𝑊)) ∧ 𝑆 ∈ 𝐿) → 𝑊 ∈ LMod) | 
| 9 |  | simpr 484 | . . . 4
⊢ (((𝑊 ∈ AssAlg ∧ 𝑆 ∈ (SubRing‘𝑊)) ∧ 𝑆 ∈ 𝐿) → 𝑆 ∈ 𝐿) | 
| 10 | 2 | subrg1cl 20580 | . . . . 5
⊢ (𝑆 ∈ (SubRing‘𝑊) →
(1r‘𝑊)
∈ 𝑆) | 
| 11 | 10 | ad2antlr 727 | . . . 4
⊢ (((𝑊 ∈ AssAlg ∧ 𝑆 ∈ (SubRing‘𝑊)) ∧ 𝑆 ∈ 𝐿) → (1r‘𝑊) ∈ 𝑆) | 
| 12 | 6, 3, 8, 9, 11 | ellspsn5 20994 | . . 3
⊢ (((𝑊 ∈ AssAlg ∧ 𝑆 ∈ (SubRing‘𝑊)) ∧ 𝑆 ∈ 𝐿) → ((LSpan‘𝑊)‘{(1r‘𝑊)}) ⊆ 𝑆) | 
| 13 | 5, 12 | eqsstrd 4018 | . 2
⊢ (((𝑊 ∈ AssAlg ∧ 𝑆 ∈ (SubRing‘𝑊)) ∧ 𝑆 ∈ 𝐿) → ran 𝐴 ⊆ 𝑆) | 
| 14 |  | subrgsubg 20577 | . . . 4
⊢ (𝑆 ∈ (SubRing‘𝑊) → 𝑆 ∈ (SubGrp‘𝑊)) | 
| 15 | 14 | ad2antlr 727 | . . 3
⊢ (((𝑊 ∈ AssAlg ∧ 𝑆 ∈ (SubRing‘𝑊)) ∧ ran 𝐴 ⊆ 𝑆) → 𝑆 ∈ (SubGrp‘𝑊)) | 
| 16 |  | simplll 775 | . . . . . 6
⊢ ((((𝑊 ∈ AssAlg ∧ 𝑆 ∈ (SubRing‘𝑊)) ∧ ran 𝐴 ⊆ 𝑆) ∧ (𝑥 ∈ (Base‘(Scalar‘𝑊)) ∧ 𝑦 ∈ 𝑆)) → 𝑊 ∈ AssAlg) | 
| 17 |  | simprl 771 | . . . . . 6
⊢ ((((𝑊 ∈ AssAlg ∧ 𝑆 ∈ (SubRing‘𝑊)) ∧ ran 𝐴 ⊆ 𝑆) ∧ (𝑥 ∈ (Base‘(Scalar‘𝑊)) ∧ 𝑦 ∈ 𝑆)) → 𝑥 ∈ (Base‘(Scalar‘𝑊))) | 
| 18 |  | eqid 2737 | . . . . . . . . . 10
⊢
(Base‘𝑊) =
(Base‘𝑊) | 
| 19 | 18 | subrgss 20572 | . . . . . . . . 9
⊢ (𝑆 ∈ (SubRing‘𝑊) → 𝑆 ⊆ (Base‘𝑊)) | 
| 20 | 19 | ad2antlr 727 | . . . . . . . 8
⊢ (((𝑊 ∈ AssAlg ∧ 𝑆 ∈ (SubRing‘𝑊)) ∧ ran 𝐴 ⊆ 𝑆) → 𝑆 ⊆ (Base‘𝑊)) | 
| 21 | 20 | sselda 3983 | . . . . . . 7
⊢ ((((𝑊 ∈ AssAlg ∧ 𝑆 ∈ (SubRing‘𝑊)) ∧ ran 𝐴 ⊆ 𝑆) ∧ 𝑦 ∈ 𝑆) → 𝑦 ∈ (Base‘𝑊)) | 
| 22 | 21 | adantrl 716 | . . . . . 6
⊢ ((((𝑊 ∈ AssAlg ∧ 𝑆 ∈ (SubRing‘𝑊)) ∧ ran 𝐴 ⊆ 𝑆) ∧ (𝑥 ∈ (Base‘(Scalar‘𝑊)) ∧ 𝑦 ∈ 𝑆)) → 𝑦 ∈ (Base‘𝑊)) | 
| 23 |  | eqid 2737 | . . . . . . 7
⊢
(Scalar‘𝑊) =
(Scalar‘𝑊) | 
| 24 |  | eqid 2737 | . . . . . . 7
⊢
(Base‘(Scalar‘𝑊)) = (Base‘(Scalar‘𝑊)) | 
| 25 |  | eqid 2737 | . . . . . . 7
⊢
(.r‘𝑊) = (.r‘𝑊) | 
| 26 |  | eqid 2737 | . . . . . . 7
⊢ (
·𝑠 ‘𝑊) = ( ·𝑠
‘𝑊) | 
| 27 | 1, 23, 24, 18, 25, 26 | asclmul1 21906 | . . . . . 6
⊢ ((𝑊 ∈ AssAlg ∧ 𝑥 ∈
(Base‘(Scalar‘𝑊)) ∧ 𝑦 ∈ (Base‘𝑊)) → ((𝐴‘𝑥)(.r‘𝑊)𝑦) = (𝑥( ·𝑠
‘𝑊)𝑦)) | 
| 28 | 16, 17, 22, 27 | syl3anc 1373 | . . . . 5
⊢ ((((𝑊 ∈ AssAlg ∧ 𝑆 ∈ (SubRing‘𝑊)) ∧ ran 𝐴 ⊆ 𝑆) ∧ (𝑥 ∈ (Base‘(Scalar‘𝑊)) ∧ 𝑦 ∈ 𝑆)) → ((𝐴‘𝑥)(.r‘𝑊)𝑦) = (𝑥( ·𝑠
‘𝑊)𝑦)) | 
| 29 |  | simpllr 776 | . . . . . 6
⊢ ((((𝑊 ∈ AssAlg ∧ 𝑆 ∈ (SubRing‘𝑊)) ∧ ran 𝐴 ⊆ 𝑆) ∧ (𝑥 ∈ (Base‘(Scalar‘𝑊)) ∧ 𝑦 ∈ 𝑆)) → 𝑆 ∈ (SubRing‘𝑊)) | 
| 30 |  | simplr 769 | . . . . . . . 8
⊢ ((((𝑊 ∈ AssAlg ∧ 𝑆 ∈ (SubRing‘𝑊)) ∧ ran 𝐴 ⊆ 𝑆) ∧ 𝑥 ∈ (Base‘(Scalar‘𝑊))) → ran 𝐴 ⊆ 𝑆) | 
| 31 | 1, 23, 24 | asclfn 21901 | . . . . . . . . . 10
⊢ 𝐴 Fn
(Base‘(Scalar‘𝑊)) | 
| 32 | 31 | a1i 11 | . . . . . . . . 9
⊢ (((𝑊 ∈ AssAlg ∧ 𝑆 ∈ (SubRing‘𝑊)) ∧ ran 𝐴 ⊆ 𝑆) → 𝐴 Fn (Base‘(Scalar‘𝑊))) | 
| 33 |  | fnfvelrn 7100 | . . . . . . . . 9
⊢ ((𝐴 Fn
(Base‘(Scalar‘𝑊)) ∧ 𝑥 ∈ (Base‘(Scalar‘𝑊))) → (𝐴‘𝑥) ∈ ran 𝐴) | 
| 34 | 32, 33 | sylan 580 | . . . . . . . 8
⊢ ((((𝑊 ∈ AssAlg ∧ 𝑆 ∈ (SubRing‘𝑊)) ∧ ran 𝐴 ⊆ 𝑆) ∧ 𝑥 ∈ (Base‘(Scalar‘𝑊))) → (𝐴‘𝑥) ∈ ran 𝐴) | 
| 35 | 30, 34 | sseldd 3984 | . . . . . . 7
⊢ ((((𝑊 ∈ AssAlg ∧ 𝑆 ∈ (SubRing‘𝑊)) ∧ ran 𝐴 ⊆ 𝑆) ∧ 𝑥 ∈ (Base‘(Scalar‘𝑊))) → (𝐴‘𝑥) ∈ 𝑆) | 
| 36 | 35 | adantrr 717 | . . . . . 6
⊢ ((((𝑊 ∈ AssAlg ∧ 𝑆 ∈ (SubRing‘𝑊)) ∧ ran 𝐴 ⊆ 𝑆) ∧ (𝑥 ∈ (Base‘(Scalar‘𝑊)) ∧ 𝑦 ∈ 𝑆)) → (𝐴‘𝑥) ∈ 𝑆) | 
| 37 |  | simprr 773 | . . . . . 6
⊢ ((((𝑊 ∈ AssAlg ∧ 𝑆 ∈ (SubRing‘𝑊)) ∧ ran 𝐴 ⊆ 𝑆) ∧ (𝑥 ∈ (Base‘(Scalar‘𝑊)) ∧ 𝑦 ∈ 𝑆)) → 𝑦 ∈ 𝑆) | 
| 38 | 25 | subrgmcl 20584 | . . . . . 6
⊢ ((𝑆 ∈ (SubRing‘𝑊) ∧ (𝐴‘𝑥) ∈ 𝑆 ∧ 𝑦 ∈ 𝑆) → ((𝐴‘𝑥)(.r‘𝑊)𝑦) ∈ 𝑆) | 
| 39 | 29, 36, 37, 38 | syl3anc 1373 | . . . . 5
⊢ ((((𝑊 ∈ AssAlg ∧ 𝑆 ∈ (SubRing‘𝑊)) ∧ ran 𝐴 ⊆ 𝑆) ∧ (𝑥 ∈ (Base‘(Scalar‘𝑊)) ∧ 𝑦 ∈ 𝑆)) → ((𝐴‘𝑥)(.r‘𝑊)𝑦) ∈ 𝑆) | 
| 40 | 28, 39 | eqeltrrd 2842 | . . . 4
⊢ ((((𝑊 ∈ AssAlg ∧ 𝑆 ∈ (SubRing‘𝑊)) ∧ ran 𝐴 ⊆ 𝑆) ∧ (𝑥 ∈ (Base‘(Scalar‘𝑊)) ∧ 𝑦 ∈ 𝑆)) → (𝑥( ·𝑠
‘𝑊)𝑦) ∈ 𝑆) | 
| 41 | 40 | ralrimivva 3202 | . . 3
⊢ (((𝑊 ∈ AssAlg ∧ 𝑆 ∈ (SubRing‘𝑊)) ∧ ran 𝐴 ⊆ 𝑆) → ∀𝑥 ∈ (Base‘(Scalar‘𝑊))∀𝑦 ∈ 𝑆 (𝑥( ·𝑠
‘𝑊)𝑦) ∈ 𝑆) | 
| 42 | 23, 24, 18, 26, 6 | islss4 20960 | . . . . 5
⊢ (𝑊 ∈ LMod → (𝑆 ∈ 𝐿 ↔ (𝑆 ∈ (SubGrp‘𝑊) ∧ ∀𝑥 ∈ (Base‘(Scalar‘𝑊))∀𝑦 ∈ 𝑆 (𝑥( ·𝑠
‘𝑊)𝑦) ∈ 𝑆))) | 
| 43 | 7, 42 | syl 17 | . . . 4
⊢ (𝑊 ∈ AssAlg → (𝑆 ∈ 𝐿 ↔ (𝑆 ∈ (SubGrp‘𝑊) ∧ ∀𝑥 ∈ (Base‘(Scalar‘𝑊))∀𝑦 ∈ 𝑆 (𝑥( ·𝑠
‘𝑊)𝑦) ∈ 𝑆))) | 
| 44 | 43 | ad2antrr 726 | . . 3
⊢ (((𝑊 ∈ AssAlg ∧ 𝑆 ∈ (SubRing‘𝑊)) ∧ ran 𝐴 ⊆ 𝑆) → (𝑆 ∈ 𝐿 ↔ (𝑆 ∈ (SubGrp‘𝑊) ∧ ∀𝑥 ∈ (Base‘(Scalar‘𝑊))∀𝑦 ∈ 𝑆 (𝑥( ·𝑠
‘𝑊)𝑦) ∈ 𝑆))) | 
| 45 | 15, 41, 44 | mpbir2and 713 | . 2
⊢ (((𝑊 ∈ AssAlg ∧ 𝑆 ∈ (SubRing‘𝑊)) ∧ ran 𝐴 ⊆ 𝑆) → 𝑆 ∈ 𝐿) | 
| 46 | 13, 45 | impbida 801 | 1
⊢ ((𝑊 ∈ AssAlg ∧ 𝑆 ∈ (SubRing‘𝑊)) → (𝑆 ∈ 𝐿 ↔ ran 𝐴 ⊆ 𝑆)) |