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 20851 |
. . . 4
⊢ (𝑊 ∈ AssAlg → ran 𝐴 = ((LSpan‘𝑊)‘{(1r‘𝑊)})) |
5 | 4 | ad2antrr 726 |
. . 3
⊢ (((𝑊 ∈ AssAlg ∧ 𝑆 ∈ (SubRing‘𝑊)) ∧ 𝑆 ∈ 𝐿) → ran 𝐴 = ((LSpan‘𝑊)‘{(1r‘𝑊)})) |
6 | | issubassa2.l |
. . . 4
⊢ 𝐿 = (LSubSp‘𝑊) |
7 | | assalmod 20822 |
. . . . 5
⊢ (𝑊 ∈ AssAlg → 𝑊 ∈ LMod) |
8 | 7 | ad2antrr 726 |
. . . 4
⊢ (((𝑊 ∈ AssAlg ∧ 𝑆 ∈ (SubRing‘𝑊)) ∧ 𝑆 ∈ 𝐿) → 𝑊 ∈ LMod) |
9 | | simpr 488 |
. . . 4
⊢ (((𝑊 ∈ AssAlg ∧ 𝑆 ∈ (SubRing‘𝑊)) ∧ 𝑆 ∈ 𝐿) → 𝑆 ∈ 𝐿) |
10 | 2 | subrg1cl 19808 |
. . . . 5
⊢ (𝑆 ∈ (SubRing‘𝑊) →
(1r‘𝑊)
∈ 𝑆) |
11 | 10 | ad2antlr 727 |
. . . 4
⊢ (((𝑊 ∈ AssAlg ∧ 𝑆 ∈ (SubRing‘𝑊)) ∧ 𝑆 ∈ 𝐿) → (1r‘𝑊) ∈ 𝑆) |
12 | 6, 3, 8, 9, 11 | lspsnel5a 20033 |
. . 3
⊢ (((𝑊 ∈ AssAlg ∧ 𝑆 ∈ (SubRing‘𝑊)) ∧ 𝑆 ∈ 𝐿) → ((LSpan‘𝑊)‘{(1r‘𝑊)}) ⊆ 𝑆) |
13 | 5, 12 | eqsstrd 3939 |
. 2
⊢ (((𝑊 ∈ AssAlg ∧ 𝑆 ∈ (SubRing‘𝑊)) ∧ 𝑆 ∈ 𝐿) → ran 𝐴 ⊆ 𝑆) |
14 | | subrgsubg 19806 |
. . . 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 19801 |
. . . . . . . . 9
⊢ (𝑆 ∈ (SubRing‘𝑊) → 𝑆 ⊆ (Base‘𝑊)) |
20 | 19 | ad2antlr 727 |
. . . . . . . 8
⊢ (((𝑊 ∈ AssAlg ∧ 𝑆 ∈ (SubRing‘𝑊)) ∧ ran 𝐴 ⊆ 𝑆) → 𝑆 ⊆ (Base‘𝑊)) |
21 | 20 | sselda 3901 |
. . . . . . 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 20845 |
. . . . . 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 20840 |
. . . . . . . . . 10
⊢ 𝐴 Fn
(Base‘(Scalar‘𝑊)) |
32 | 31 | a1i 11 |
. . . . . . . . 9
⊢ (((𝑊 ∈ AssAlg ∧ 𝑆 ∈ (SubRing‘𝑊)) ∧ ran 𝐴 ⊆ 𝑆) → 𝐴 Fn (Base‘(Scalar‘𝑊))) |
33 | | fnfvelrn 6901 |
. . . . . . . . 9
⊢ ((𝐴 Fn
(Base‘(Scalar‘𝑊)) ∧ 𝑥 ∈ (Base‘(Scalar‘𝑊))) → (𝐴‘𝑥) ∈ ran 𝐴) |
34 | 32, 33 | sylan 583 |
. . . . . . . 8
⊢ ((((𝑊 ∈ AssAlg ∧ 𝑆 ∈ (SubRing‘𝑊)) ∧ ran 𝐴 ⊆ 𝑆) ∧ 𝑥 ∈ (Base‘(Scalar‘𝑊))) → (𝐴‘𝑥) ∈ ran 𝐴) |
35 | 30, 34 | sseldd 3902 |
. . . . . . 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 19812 |
. . . . . 6
⊢ ((𝑆 ∈ (SubRing‘𝑊) ∧ (𝐴‘𝑥) ∈ 𝑆 ∧ 𝑦 ∈ 𝑆) → ((𝐴‘𝑥)(.r‘𝑊)𝑦) ∈ 𝑆) |
39 | 29, 36, 37, 38 | syl3anc 1373 |
. . . . 5
⊢ ((((𝑊 ∈ AssAlg ∧ 𝑆 ∈ (SubRing‘𝑊)) ∧ ran 𝐴 ⊆ 𝑆) ∧ (𝑥 ∈ (Base‘(Scalar‘𝑊)) ∧ 𝑦 ∈ 𝑆)) → ((𝐴‘𝑥)(.r‘𝑊)𝑦) ∈ 𝑆) |
40 | 28, 39 | eqeltrrd 2839 |
. . . 4
⊢ ((((𝑊 ∈ AssAlg ∧ 𝑆 ∈ (SubRing‘𝑊)) ∧ ran 𝐴 ⊆ 𝑆) ∧ (𝑥 ∈ (Base‘(Scalar‘𝑊)) ∧ 𝑦 ∈ 𝑆)) → (𝑥( ·𝑠
‘𝑊)𝑦) ∈ 𝑆) |
41 | 40 | ralrimivva 3112 |
. . 3
⊢ (((𝑊 ∈ AssAlg ∧ 𝑆 ∈ (SubRing‘𝑊)) ∧ ran 𝐴 ⊆ 𝑆) → ∀𝑥 ∈ (Base‘(Scalar‘𝑊))∀𝑦 ∈ 𝑆 (𝑥( ·𝑠
‘𝑊)𝑦) ∈ 𝑆) |
42 | 23, 24, 18, 26, 6 | islss4 19999 |
. . . . 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 𝐴 ⊆ 𝑆)) |