Step |
Hyp |
Ref |
Expression |
1 |
|
frlmsslsp.y |
⊢ 𝑌 = ( 𝑅 freeLMod 𝐼 ) |
2 |
|
frlmsslsp.u |
⊢ 𝑈 = ( 𝑅 unitVec 𝐼 ) |
3 |
|
frlmsslsp.k |
⊢ 𝐾 = ( LSpan ‘ 𝑌 ) |
4 |
|
frlmsslsp.b |
⊢ 𝐵 = ( Base ‘ 𝑌 ) |
5 |
|
frlmsslsp.z |
⊢ 0 = ( 0g ‘ 𝑅 ) |
6 |
|
frlmsslsp.c |
⊢ 𝐶 = { 𝑥 ∈ 𝐵 ∣ ( 𝑥 supp 0 ) ⊆ 𝐽 } |
7 |
1
|
frlmlmod |
⊢ ( ( 𝑅 ∈ Ring ∧ 𝐼 ∈ 𝑉 ) → 𝑌 ∈ LMod ) |
8 |
7
|
3adant3 |
⊢ ( ( 𝑅 ∈ Ring ∧ 𝐼 ∈ 𝑉 ∧ 𝐽 ⊆ 𝐼 ) → 𝑌 ∈ LMod ) |
9 |
|
eqid |
⊢ ( LSubSp ‘ 𝑌 ) = ( LSubSp ‘ 𝑌 ) |
10 |
1 9 4 5 6
|
frlmsslss2 |
⊢ ( ( 𝑅 ∈ Ring ∧ 𝐼 ∈ 𝑉 ∧ 𝐽 ⊆ 𝐼 ) → 𝐶 ∈ ( LSubSp ‘ 𝑌 ) ) |
11 |
2 1 4
|
uvcff |
⊢ ( ( 𝑅 ∈ Ring ∧ 𝐼 ∈ 𝑉 ) → 𝑈 : 𝐼 ⟶ 𝐵 ) |
12 |
11
|
3adant3 |
⊢ ( ( 𝑅 ∈ Ring ∧ 𝐼 ∈ 𝑉 ∧ 𝐽 ⊆ 𝐼 ) → 𝑈 : 𝐼 ⟶ 𝐵 ) |
13 |
12
|
adantr |
⊢ ( ( ( 𝑅 ∈ Ring ∧ 𝐼 ∈ 𝑉 ∧ 𝐽 ⊆ 𝐼 ) ∧ 𝑦 ∈ 𝐽 ) → 𝑈 : 𝐼 ⟶ 𝐵 ) |
14 |
|
simp3 |
⊢ ( ( 𝑅 ∈ Ring ∧ 𝐼 ∈ 𝑉 ∧ 𝐽 ⊆ 𝐼 ) → 𝐽 ⊆ 𝐼 ) |
15 |
14
|
sselda |
⊢ ( ( ( 𝑅 ∈ Ring ∧ 𝐼 ∈ 𝑉 ∧ 𝐽 ⊆ 𝐼 ) ∧ 𝑦 ∈ 𝐽 ) → 𝑦 ∈ 𝐼 ) |
16 |
13 15
|
ffvelrnd |
⊢ ( ( ( 𝑅 ∈ Ring ∧ 𝐼 ∈ 𝑉 ∧ 𝐽 ⊆ 𝐼 ) ∧ 𝑦 ∈ 𝐽 ) → ( 𝑈 ‘ 𝑦 ) ∈ 𝐵 ) |
17 |
|
simpl2 |
⊢ ( ( ( 𝑅 ∈ Ring ∧ 𝐼 ∈ 𝑉 ∧ 𝐽 ⊆ 𝐼 ) ∧ 𝑦 ∈ 𝐽 ) → 𝐼 ∈ 𝑉 ) |
18 |
|
eqid |
⊢ ( Base ‘ 𝑅 ) = ( Base ‘ 𝑅 ) |
19 |
1 18 4
|
frlmbasf |
⊢ ( ( 𝐼 ∈ 𝑉 ∧ ( 𝑈 ‘ 𝑦 ) ∈ 𝐵 ) → ( 𝑈 ‘ 𝑦 ) : 𝐼 ⟶ ( Base ‘ 𝑅 ) ) |
20 |
17 16 19
|
syl2anc |
⊢ ( ( ( 𝑅 ∈ Ring ∧ 𝐼 ∈ 𝑉 ∧ 𝐽 ⊆ 𝐼 ) ∧ 𝑦 ∈ 𝐽 ) → ( 𝑈 ‘ 𝑦 ) : 𝐼 ⟶ ( Base ‘ 𝑅 ) ) |
21 |
|
simpll1 |
⊢ ( ( ( ( 𝑅 ∈ Ring ∧ 𝐼 ∈ 𝑉 ∧ 𝐽 ⊆ 𝐼 ) ∧ 𝑦 ∈ 𝐽 ) ∧ 𝑥 ∈ ( 𝐼 ∖ 𝐽 ) ) → 𝑅 ∈ Ring ) |
22 |
|
simpll2 |
⊢ ( ( ( ( 𝑅 ∈ Ring ∧ 𝐼 ∈ 𝑉 ∧ 𝐽 ⊆ 𝐼 ) ∧ 𝑦 ∈ 𝐽 ) ∧ 𝑥 ∈ ( 𝐼 ∖ 𝐽 ) ) → 𝐼 ∈ 𝑉 ) |
23 |
15
|
adantr |
⊢ ( ( ( ( 𝑅 ∈ Ring ∧ 𝐼 ∈ 𝑉 ∧ 𝐽 ⊆ 𝐼 ) ∧ 𝑦 ∈ 𝐽 ) ∧ 𝑥 ∈ ( 𝐼 ∖ 𝐽 ) ) → 𝑦 ∈ 𝐼 ) |
24 |
|
eldifi |
⊢ ( 𝑥 ∈ ( 𝐼 ∖ 𝐽 ) → 𝑥 ∈ 𝐼 ) |
25 |
24
|
adantl |
⊢ ( ( ( ( 𝑅 ∈ Ring ∧ 𝐼 ∈ 𝑉 ∧ 𝐽 ⊆ 𝐼 ) ∧ 𝑦 ∈ 𝐽 ) ∧ 𝑥 ∈ ( 𝐼 ∖ 𝐽 ) ) → 𝑥 ∈ 𝐼 ) |
26 |
|
elneeldif |
⊢ ( ( 𝑦 ∈ 𝐽 ∧ 𝑥 ∈ ( 𝐼 ∖ 𝐽 ) ) → 𝑦 ≠ 𝑥 ) |
27 |
26
|
adantll |
⊢ ( ( ( ( 𝑅 ∈ Ring ∧ 𝐼 ∈ 𝑉 ∧ 𝐽 ⊆ 𝐼 ) ∧ 𝑦 ∈ 𝐽 ) ∧ 𝑥 ∈ ( 𝐼 ∖ 𝐽 ) ) → 𝑦 ≠ 𝑥 ) |
28 |
2 21 22 23 25 27 5
|
uvcvv0 |
⊢ ( ( ( ( 𝑅 ∈ Ring ∧ 𝐼 ∈ 𝑉 ∧ 𝐽 ⊆ 𝐼 ) ∧ 𝑦 ∈ 𝐽 ) ∧ 𝑥 ∈ ( 𝐼 ∖ 𝐽 ) ) → ( ( 𝑈 ‘ 𝑦 ) ‘ 𝑥 ) = 0 ) |
29 |
20 28
|
suppss |
⊢ ( ( ( 𝑅 ∈ Ring ∧ 𝐼 ∈ 𝑉 ∧ 𝐽 ⊆ 𝐼 ) ∧ 𝑦 ∈ 𝐽 ) → ( ( 𝑈 ‘ 𝑦 ) supp 0 ) ⊆ 𝐽 ) |
30 |
|
oveq1 |
⊢ ( 𝑥 = ( 𝑈 ‘ 𝑦 ) → ( 𝑥 supp 0 ) = ( ( 𝑈 ‘ 𝑦 ) supp 0 ) ) |
31 |
30
|
sseq1d |
⊢ ( 𝑥 = ( 𝑈 ‘ 𝑦 ) → ( ( 𝑥 supp 0 ) ⊆ 𝐽 ↔ ( ( 𝑈 ‘ 𝑦 ) supp 0 ) ⊆ 𝐽 ) ) |
32 |
31 6
|
elrab2 |
⊢ ( ( 𝑈 ‘ 𝑦 ) ∈ 𝐶 ↔ ( ( 𝑈 ‘ 𝑦 ) ∈ 𝐵 ∧ ( ( 𝑈 ‘ 𝑦 ) supp 0 ) ⊆ 𝐽 ) ) |
33 |
16 29 32
|
sylanbrc |
⊢ ( ( ( 𝑅 ∈ Ring ∧ 𝐼 ∈ 𝑉 ∧ 𝐽 ⊆ 𝐼 ) ∧ 𝑦 ∈ 𝐽 ) → ( 𝑈 ‘ 𝑦 ) ∈ 𝐶 ) |
34 |
33
|
ralrimiva |
⊢ ( ( 𝑅 ∈ Ring ∧ 𝐼 ∈ 𝑉 ∧ 𝐽 ⊆ 𝐼 ) → ∀ 𝑦 ∈ 𝐽 ( 𝑈 ‘ 𝑦 ) ∈ 𝐶 ) |
35 |
12
|
ffund |
⊢ ( ( 𝑅 ∈ Ring ∧ 𝐼 ∈ 𝑉 ∧ 𝐽 ⊆ 𝐼 ) → Fun 𝑈 ) |
36 |
12
|
fdmd |
⊢ ( ( 𝑅 ∈ Ring ∧ 𝐼 ∈ 𝑉 ∧ 𝐽 ⊆ 𝐼 ) → dom 𝑈 = 𝐼 ) |
37 |
14 36
|
sseqtrrd |
⊢ ( ( 𝑅 ∈ Ring ∧ 𝐼 ∈ 𝑉 ∧ 𝐽 ⊆ 𝐼 ) → 𝐽 ⊆ dom 𝑈 ) |
38 |
|
funimass4 |
⊢ ( ( Fun 𝑈 ∧ 𝐽 ⊆ dom 𝑈 ) → ( ( 𝑈 “ 𝐽 ) ⊆ 𝐶 ↔ ∀ 𝑦 ∈ 𝐽 ( 𝑈 ‘ 𝑦 ) ∈ 𝐶 ) ) |
39 |
35 37 38
|
syl2anc |
⊢ ( ( 𝑅 ∈ Ring ∧ 𝐼 ∈ 𝑉 ∧ 𝐽 ⊆ 𝐼 ) → ( ( 𝑈 “ 𝐽 ) ⊆ 𝐶 ↔ ∀ 𝑦 ∈ 𝐽 ( 𝑈 ‘ 𝑦 ) ∈ 𝐶 ) ) |
40 |
34 39
|
mpbird |
⊢ ( ( 𝑅 ∈ Ring ∧ 𝐼 ∈ 𝑉 ∧ 𝐽 ⊆ 𝐼 ) → ( 𝑈 “ 𝐽 ) ⊆ 𝐶 ) |
41 |
9 3
|
lspssp |
⊢ ( ( 𝑌 ∈ LMod ∧ 𝐶 ∈ ( LSubSp ‘ 𝑌 ) ∧ ( 𝑈 “ 𝐽 ) ⊆ 𝐶 ) → ( 𝐾 ‘ ( 𝑈 “ 𝐽 ) ) ⊆ 𝐶 ) |
42 |
8 10 40 41
|
syl3anc |
⊢ ( ( 𝑅 ∈ Ring ∧ 𝐼 ∈ 𝑉 ∧ 𝐽 ⊆ 𝐼 ) → ( 𝐾 ‘ ( 𝑈 “ 𝐽 ) ) ⊆ 𝐶 ) |
43 |
|
simpl1 |
⊢ ( ( ( 𝑅 ∈ Ring ∧ 𝐼 ∈ 𝑉 ∧ 𝐽 ⊆ 𝐼 ) ∧ 𝑦 ∈ 𝐶 ) → 𝑅 ∈ Ring ) |
44 |
|
simpl2 |
⊢ ( ( ( 𝑅 ∈ Ring ∧ 𝐼 ∈ 𝑉 ∧ 𝐽 ⊆ 𝐼 ) ∧ 𝑦 ∈ 𝐶 ) → 𝐼 ∈ 𝑉 ) |
45 |
6
|
ssrab3 |
⊢ 𝐶 ⊆ 𝐵 |
46 |
45
|
a1i |
⊢ ( ( 𝑅 ∈ Ring ∧ 𝐼 ∈ 𝑉 ∧ 𝐽 ⊆ 𝐼 ) → 𝐶 ⊆ 𝐵 ) |
47 |
46
|
sselda |
⊢ ( ( ( 𝑅 ∈ Ring ∧ 𝐼 ∈ 𝑉 ∧ 𝐽 ⊆ 𝐼 ) ∧ 𝑦 ∈ 𝐶 ) → 𝑦 ∈ 𝐵 ) |
48 |
|
eqid |
⊢ ( ·𝑠 ‘ 𝑌 ) = ( ·𝑠 ‘ 𝑌 ) |
49 |
2 1 4 48
|
uvcresum |
⊢ ( ( 𝑅 ∈ Ring ∧ 𝐼 ∈ 𝑉 ∧ 𝑦 ∈ 𝐵 ) → 𝑦 = ( 𝑌 Σg ( 𝑦 ∘f ( ·𝑠 ‘ 𝑌 ) 𝑈 ) ) ) |
50 |
43 44 47 49
|
syl3anc |
⊢ ( ( ( 𝑅 ∈ Ring ∧ 𝐼 ∈ 𝑉 ∧ 𝐽 ⊆ 𝐼 ) ∧ 𝑦 ∈ 𝐶 ) → 𝑦 = ( 𝑌 Σg ( 𝑦 ∘f ( ·𝑠 ‘ 𝑌 ) 𝑈 ) ) ) |
51 |
|
eqid |
⊢ ( 0g ‘ 𝑌 ) = ( 0g ‘ 𝑌 ) |
52 |
|
lmodabl |
⊢ ( 𝑌 ∈ LMod → 𝑌 ∈ Abel ) |
53 |
8 52
|
syl |
⊢ ( ( 𝑅 ∈ Ring ∧ 𝐼 ∈ 𝑉 ∧ 𝐽 ⊆ 𝐼 ) → 𝑌 ∈ Abel ) |
54 |
53
|
adantr |
⊢ ( ( ( 𝑅 ∈ Ring ∧ 𝐼 ∈ 𝑉 ∧ 𝐽 ⊆ 𝐼 ) ∧ 𝑦 ∈ 𝐶 ) → 𝑌 ∈ Abel ) |
55 |
|
imassrn |
⊢ ( 𝑈 “ 𝐽 ) ⊆ ran 𝑈 |
56 |
12
|
frnd |
⊢ ( ( 𝑅 ∈ Ring ∧ 𝐼 ∈ 𝑉 ∧ 𝐽 ⊆ 𝐼 ) → ran 𝑈 ⊆ 𝐵 ) |
57 |
55 56
|
sstrid |
⊢ ( ( 𝑅 ∈ Ring ∧ 𝐼 ∈ 𝑉 ∧ 𝐽 ⊆ 𝐼 ) → ( 𝑈 “ 𝐽 ) ⊆ 𝐵 ) |
58 |
4 9 3
|
lspcl |
⊢ ( ( 𝑌 ∈ LMod ∧ ( 𝑈 “ 𝐽 ) ⊆ 𝐵 ) → ( 𝐾 ‘ ( 𝑈 “ 𝐽 ) ) ∈ ( LSubSp ‘ 𝑌 ) ) |
59 |
8 57 58
|
syl2anc |
⊢ ( ( 𝑅 ∈ Ring ∧ 𝐼 ∈ 𝑉 ∧ 𝐽 ⊆ 𝐼 ) → ( 𝐾 ‘ ( 𝑈 “ 𝐽 ) ) ∈ ( LSubSp ‘ 𝑌 ) ) |
60 |
9
|
lsssubg |
⊢ ( ( 𝑌 ∈ LMod ∧ ( 𝐾 ‘ ( 𝑈 “ 𝐽 ) ) ∈ ( LSubSp ‘ 𝑌 ) ) → ( 𝐾 ‘ ( 𝑈 “ 𝐽 ) ) ∈ ( SubGrp ‘ 𝑌 ) ) |
61 |
8 59 60
|
syl2anc |
⊢ ( ( 𝑅 ∈ Ring ∧ 𝐼 ∈ 𝑉 ∧ 𝐽 ⊆ 𝐼 ) → ( 𝐾 ‘ ( 𝑈 “ 𝐽 ) ) ∈ ( SubGrp ‘ 𝑌 ) ) |
62 |
61
|
adantr |
⊢ ( ( ( 𝑅 ∈ Ring ∧ 𝐼 ∈ 𝑉 ∧ 𝐽 ⊆ 𝐼 ) ∧ 𝑦 ∈ 𝐶 ) → ( 𝐾 ‘ ( 𝑈 “ 𝐽 ) ) ∈ ( SubGrp ‘ 𝑌 ) ) |
63 |
1 18 4
|
frlmbasf |
⊢ ( ( 𝐼 ∈ 𝑉 ∧ 𝑦 ∈ 𝐵 ) → 𝑦 : 𝐼 ⟶ ( Base ‘ 𝑅 ) ) |
64 |
63
|
3ad2antl2 |
⊢ ( ( ( 𝑅 ∈ Ring ∧ 𝐼 ∈ 𝑉 ∧ 𝐽 ⊆ 𝐼 ) ∧ 𝑦 ∈ 𝐵 ) → 𝑦 : 𝐼 ⟶ ( Base ‘ 𝑅 ) ) |
65 |
64
|
ffnd |
⊢ ( ( ( 𝑅 ∈ Ring ∧ 𝐼 ∈ 𝑉 ∧ 𝐽 ⊆ 𝐼 ) ∧ 𝑦 ∈ 𝐵 ) → 𝑦 Fn 𝐼 ) |
66 |
12
|
ffnd |
⊢ ( ( 𝑅 ∈ Ring ∧ 𝐼 ∈ 𝑉 ∧ 𝐽 ⊆ 𝐼 ) → 𝑈 Fn 𝐼 ) |
67 |
66
|
adantr |
⊢ ( ( ( 𝑅 ∈ Ring ∧ 𝐼 ∈ 𝑉 ∧ 𝐽 ⊆ 𝐼 ) ∧ 𝑦 ∈ 𝐵 ) → 𝑈 Fn 𝐼 ) |
68 |
|
simpl2 |
⊢ ( ( ( 𝑅 ∈ Ring ∧ 𝐼 ∈ 𝑉 ∧ 𝐽 ⊆ 𝐼 ) ∧ 𝑦 ∈ 𝐵 ) → 𝐼 ∈ 𝑉 ) |
69 |
|
inidm |
⊢ ( 𝐼 ∩ 𝐼 ) = 𝐼 |
70 |
65 67 68 68 69
|
offn |
⊢ ( ( ( 𝑅 ∈ Ring ∧ 𝐼 ∈ 𝑉 ∧ 𝐽 ⊆ 𝐼 ) ∧ 𝑦 ∈ 𝐵 ) → ( 𝑦 ∘f ( ·𝑠 ‘ 𝑌 ) 𝑈 ) Fn 𝐼 ) |
71 |
47 70
|
syldan |
⊢ ( ( ( 𝑅 ∈ Ring ∧ 𝐼 ∈ 𝑉 ∧ 𝐽 ⊆ 𝐼 ) ∧ 𝑦 ∈ 𝐶 ) → ( 𝑦 ∘f ( ·𝑠 ‘ 𝑌 ) 𝑈 ) Fn 𝐼 ) |
72 |
47 65
|
syldan |
⊢ ( ( ( 𝑅 ∈ Ring ∧ 𝐼 ∈ 𝑉 ∧ 𝐽 ⊆ 𝐼 ) ∧ 𝑦 ∈ 𝐶 ) → 𝑦 Fn 𝐼 ) |
73 |
72
|
adantrr |
⊢ ( ( ( 𝑅 ∈ Ring ∧ 𝐼 ∈ 𝑉 ∧ 𝐽 ⊆ 𝐼 ) ∧ ( 𝑦 ∈ 𝐶 ∧ 𝑧 ∈ 𝐼 ) ) → 𝑦 Fn 𝐼 ) |
74 |
66
|
adantr |
⊢ ( ( ( 𝑅 ∈ Ring ∧ 𝐼 ∈ 𝑉 ∧ 𝐽 ⊆ 𝐼 ) ∧ ( 𝑦 ∈ 𝐶 ∧ 𝑧 ∈ 𝐼 ) ) → 𝑈 Fn 𝐼 ) |
75 |
|
simpl2 |
⊢ ( ( ( 𝑅 ∈ Ring ∧ 𝐼 ∈ 𝑉 ∧ 𝐽 ⊆ 𝐼 ) ∧ ( 𝑦 ∈ 𝐶 ∧ 𝑧 ∈ 𝐼 ) ) → 𝐼 ∈ 𝑉 ) |
76 |
|
simprr |
⊢ ( ( ( 𝑅 ∈ Ring ∧ 𝐼 ∈ 𝑉 ∧ 𝐽 ⊆ 𝐼 ) ∧ ( 𝑦 ∈ 𝐶 ∧ 𝑧 ∈ 𝐼 ) ) → 𝑧 ∈ 𝐼 ) |
77 |
|
fnfvof |
⊢ ( ( ( 𝑦 Fn 𝐼 ∧ 𝑈 Fn 𝐼 ) ∧ ( 𝐼 ∈ 𝑉 ∧ 𝑧 ∈ 𝐼 ) ) → ( ( 𝑦 ∘f ( ·𝑠 ‘ 𝑌 ) 𝑈 ) ‘ 𝑧 ) = ( ( 𝑦 ‘ 𝑧 ) ( ·𝑠 ‘ 𝑌 ) ( 𝑈 ‘ 𝑧 ) ) ) |
78 |
73 74 75 76 77
|
syl22anc |
⊢ ( ( ( 𝑅 ∈ Ring ∧ 𝐼 ∈ 𝑉 ∧ 𝐽 ⊆ 𝐼 ) ∧ ( 𝑦 ∈ 𝐶 ∧ 𝑧 ∈ 𝐼 ) ) → ( ( 𝑦 ∘f ( ·𝑠 ‘ 𝑌 ) 𝑈 ) ‘ 𝑧 ) = ( ( 𝑦 ‘ 𝑧 ) ( ·𝑠 ‘ 𝑌 ) ( 𝑈 ‘ 𝑧 ) ) ) |
79 |
8
|
adantr |
⊢ ( ( ( 𝑅 ∈ Ring ∧ 𝐼 ∈ 𝑉 ∧ 𝐽 ⊆ 𝐼 ) ∧ ( 𝑦 ∈ 𝐶 ∧ 𝑧 ∈ 𝐽 ) ) → 𝑌 ∈ LMod ) |
80 |
59
|
adantr |
⊢ ( ( ( 𝑅 ∈ Ring ∧ 𝐼 ∈ 𝑉 ∧ 𝐽 ⊆ 𝐼 ) ∧ ( 𝑦 ∈ 𝐶 ∧ 𝑧 ∈ 𝐽 ) ) → ( 𝐾 ‘ ( 𝑈 “ 𝐽 ) ) ∈ ( LSubSp ‘ 𝑌 ) ) |
81 |
45
|
sseli |
⊢ ( 𝑦 ∈ 𝐶 → 𝑦 ∈ 𝐵 ) |
82 |
81 64
|
sylan2 |
⊢ ( ( ( 𝑅 ∈ Ring ∧ 𝐼 ∈ 𝑉 ∧ 𝐽 ⊆ 𝐼 ) ∧ 𝑦 ∈ 𝐶 ) → 𝑦 : 𝐼 ⟶ ( Base ‘ 𝑅 ) ) |
83 |
82
|
adantrr |
⊢ ( ( ( 𝑅 ∈ Ring ∧ 𝐼 ∈ 𝑉 ∧ 𝐽 ⊆ 𝐼 ) ∧ ( 𝑦 ∈ 𝐶 ∧ 𝑧 ∈ 𝐽 ) ) → 𝑦 : 𝐼 ⟶ ( Base ‘ 𝑅 ) ) |
84 |
14
|
sselda |
⊢ ( ( ( 𝑅 ∈ Ring ∧ 𝐼 ∈ 𝑉 ∧ 𝐽 ⊆ 𝐼 ) ∧ 𝑧 ∈ 𝐽 ) → 𝑧 ∈ 𝐼 ) |
85 |
84
|
adantrl |
⊢ ( ( ( 𝑅 ∈ Ring ∧ 𝐼 ∈ 𝑉 ∧ 𝐽 ⊆ 𝐼 ) ∧ ( 𝑦 ∈ 𝐶 ∧ 𝑧 ∈ 𝐽 ) ) → 𝑧 ∈ 𝐼 ) |
86 |
83 85
|
ffvelrnd |
⊢ ( ( ( 𝑅 ∈ Ring ∧ 𝐼 ∈ 𝑉 ∧ 𝐽 ⊆ 𝐼 ) ∧ ( 𝑦 ∈ 𝐶 ∧ 𝑧 ∈ 𝐽 ) ) → ( 𝑦 ‘ 𝑧 ) ∈ ( Base ‘ 𝑅 ) ) |
87 |
1
|
frlmsca |
⊢ ( ( 𝑅 ∈ Ring ∧ 𝐼 ∈ 𝑉 ) → 𝑅 = ( Scalar ‘ 𝑌 ) ) |
88 |
87
|
3adant3 |
⊢ ( ( 𝑅 ∈ Ring ∧ 𝐼 ∈ 𝑉 ∧ 𝐽 ⊆ 𝐼 ) → 𝑅 = ( Scalar ‘ 𝑌 ) ) |
89 |
88
|
fveq2d |
⊢ ( ( 𝑅 ∈ Ring ∧ 𝐼 ∈ 𝑉 ∧ 𝐽 ⊆ 𝐼 ) → ( Base ‘ 𝑅 ) = ( Base ‘ ( Scalar ‘ 𝑌 ) ) ) |
90 |
89
|
adantr |
⊢ ( ( ( 𝑅 ∈ Ring ∧ 𝐼 ∈ 𝑉 ∧ 𝐽 ⊆ 𝐼 ) ∧ ( 𝑦 ∈ 𝐶 ∧ 𝑧 ∈ 𝐽 ) ) → ( Base ‘ 𝑅 ) = ( Base ‘ ( Scalar ‘ 𝑌 ) ) ) |
91 |
86 90
|
eleqtrd |
⊢ ( ( ( 𝑅 ∈ Ring ∧ 𝐼 ∈ 𝑉 ∧ 𝐽 ⊆ 𝐼 ) ∧ ( 𝑦 ∈ 𝐶 ∧ 𝑧 ∈ 𝐽 ) ) → ( 𝑦 ‘ 𝑧 ) ∈ ( Base ‘ ( Scalar ‘ 𝑌 ) ) ) |
92 |
4 3
|
lspssid |
⊢ ( ( 𝑌 ∈ LMod ∧ ( 𝑈 “ 𝐽 ) ⊆ 𝐵 ) → ( 𝑈 “ 𝐽 ) ⊆ ( 𝐾 ‘ ( 𝑈 “ 𝐽 ) ) ) |
93 |
8 57 92
|
syl2anc |
⊢ ( ( 𝑅 ∈ Ring ∧ 𝐼 ∈ 𝑉 ∧ 𝐽 ⊆ 𝐼 ) → ( 𝑈 “ 𝐽 ) ⊆ ( 𝐾 ‘ ( 𝑈 “ 𝐽 ) ) ) |
94 |
93
|
adantr |
⊢ ( ( ( 𝑅 ∈ Ring ∧ 𝐼 ∈ 𝑉 ∧ 𝐽 ⊆ 𝐼 ) ∧ ( 𝑦 ∈ 𝐶 ∧ 𝑧 ∈ 𝐽 ) ) → ( 𝑈 “ 𝐽 ) ⊆ ( 𝐾 ‘ ( 𝑈 “ 𝐽 ) ) ) |
95 |
|
funfvima2 |
⊢ ( ( Fun 𝑈 ∧ 𝐽 ⊆ dom 𝑈 ) → ( 𝑧 ∈ 𝐽 → ( 𝑈 ‘ 𝑧 ) ∈ ( 𝑈 “ 𝐽 ) ) ) |
96 |
35 37 95
|
syl2anc |
⊢ ( ( 𝑅 ∈ Ring ∧ 𝐼 ∈ 𝑉 ∧ 𝐽 ⊆ 𝐼 ) → ( 𝑧 ∈ 𝐽 → ( 𝑈 ‘ 𝑧 ) ∈ ( 𝑈 “ 𝐽 ) ) ) |
97 |
96
|
imp |
⊢ ( ( ( 𝑅 ∈ Ring ∧ 𝐼 ∈ 𝑉 ∧ 𝐽 ⊆ 𝐼 ) ∧ 𝑧 ∈ 𝐽 ) → ( 𝑈 ‘ 𝑧 ) ∈ ( 𝑈 “ 𝐽 ) ) |
98 |
97
|
adantrl |
⊢ ( ( ( 𝑅 ∈ Ring ∧ 𝐼 ∈ 𝑉 ∧ 𝐽 ⊆ 𝐼 ) ∧ ( 𝑦 ∈ 𝐶 ∧ 𝑧 ∈ 𝐽 ) ) → ( 𝑈 ‘ 𝑧 ) ∈ ( 𝑈 “ 𝐽 ) ) |
99 |
94 98
|
sseldd |
⊢ ( ( ( 𝑅 ∈ Ring ∧ 𝐼 ∈ 𝑉 ∧ 𝐽 ⊆ 𝐼 ) ∧ ( 𝑦 ∈ 𝐶 ∧ 𝑧 ∈ 𝐽 ) ) → ( 𝑈 ‘ 𝑧 ) ∈ ( 𝐾 ‘ ( 𝑈 “ 𝐽 ) ) ) |
100 |
|
eqid |
⊢ ( Scalar ‘ 𝑌 ) = ( Scalar ‘ 𝑌 ) |
101 |
|
eqid |
⊢ ( Base ‘ ( Scalar ‘ 𝑌 ) ) = ( Base ‘ ( Scalar ‘ 𝑌 ) ) |
102 |
100 48 101 9
|
lssvscl |
⊢ ( ( ( 𝑌 ∈ LMod ∧ ( 𝐾 ‘ ( 𝑈 “ 𝐽 ) ) ∈ ( LSubSp ‘ 𝑌 ) ) ∧ ( ( 𝑦 ‘ 𝑧 ) ∈ ( Base ‘ ( Scalar ‘ 𝑌 ) ) ∧ ( 𝑈 ‘ 𝑧 ) ∈ ( 𝐾 ‘ ( 𝑈 “ 𝐽 ) ) ) ) → ( ( 𝑦 ‘ 𝑧 ) ( ·𝑠 ‘ 𝑌 ) ( 𝑈 ‘ 𝑧 ) ) ∈ ( 𝐾 ‘ ( 𝑈 “ 𝐽 ) ) ) |
103 |
79 80 91 99 102
|
syl22anc |
⊢ ( ( ( 𝑅 ∈ Ring ∧ 𝐼 ∈ 𝑉 ∧ 𝐽 ⊆ 𝐼 ) ∧ ( 𝑦 ∈ 𝐶 ∧ 𝑧 ∈ 𝐽 ) ) → ( ( 𝑦 ‘ 𝑧 ) ( ·𝑠 ‘ 𝑌 ) ( 𝑈 ‘ 𝑧 ) ) ∈ ( 𝐾 ‘ ( 𝑈 “ 𝐽 ) ) ) |
104 |
103
|
anassrs |
⊢ ( ( ( ( 𝑅 ∈ Ring ∧ 𝐼 ∈ 𝑉 ∧ 𝐽 ⊆ 𝐼 ) ∧ 𝑦 ∈ 𝐶 ) ∧ 𝑧 ∈ 𝐽 ) → ( ( 𝑦 ‘ 𝑧 ) ( ·𝑠 ‘ 𝑌 ) ( 𝑈 ‘ 𝑧 ) ) ∈ ( 𝐾 ‘ ( 𝑈 “ 𝐽 ) ) ) |
105 |
104
|
adantlrr |
⊢ ( ( ( ( 𝑅 ∈ Ring ∧ 𝐼 ∈ 𝑉 ∧ 𝐽 ⊆ 𝐼 ) ∧ ( 𝑦 ∈ 𝐶 ∧ 𝑧 ∈ 𝐼 ) ) ∧ 𝑧 ∈ 𝐽 ) → ( ( 𝑦 ‘ 𝑧 ) ( ·𝑠 ‘ 𝑌 ) ( 𝑈 ‘ 𝑧 ) ) ∈ ( 𝐾 ‘ ( 𝑈 “ 𝐽 ) ) ) |
106 |
|
id |
⊢ ( ( ( 𝑅 ∈ Ring ∧ 𝐼 ∈ 𝑉 ∧ 𝐽 ⊆ 𝐼 ) ∧ 𝑦 ∈ 𝐶 ) → ( ( 𝑅 ∈ Ring ∧ 𝐼 ∈ 𝑉 ∧ 𝐽 ⊆ 𝐼 ) ∧ 𝑦 ∈ 𝐶 ) ) |
107 |
106
|
adantrr |
⊢ ( ( ( 𝑅 ∈ Ring ∧ 𝐼 ∈ 𝑉 ∧ 𝐽 ⊆ 𝐼 ) ∧ ( 𝑦 ∈ 𝐶 ∧ 𝑧 ∈ 𝐼 ) ) → ( ( 𝑅 ∈ Ring ∧ 𝐼 ∈ 𝑉 ∧ 𝐽 ⊆ 𝐼 ) ∧ 𝑦 ∈ 𝐶 ) ) |
108 |
107
|
adantr |
⊢ ( ( ( ( 𝑅 ∈ Ring ∧ 𝐼 ∈ 𝑉 ∧ 𝐽 ⊆ 𝐼 ) ∧ ( 𝑦 ∈ 𝐶 ∧ 𝑧 ∈ 𝐼 ) ) ∧ ¬ 𝑧 ∈ 𝐽 ) → ( ( 𝑅 ∈ Ring ∧ 𝐼 ∈ 𝑉 ∧ 𝐽 ⊆ 𝐼 ) ∧ 𝑦 ∈ 𝐶 ) ) |
109 |
|
simplrr |
⊢ ( ( ( ( 𝑅 ∈ Ring ∧ 𝐼 ∈ 𝑉 ∧ 𝐽 ⊆ 𝐼 ) ∧ ( 𝑦 ∈ 𝐶 ∧ 𝑧 ∈ 𝐼 ) ) ∧ ¬ 𝑧 ∈ 𝐽 ) → 𝑧 ∈ 𝐼 ) |
110 |
|
simpr |
⊢ ( ( ( ( 𝑅 ∈ Ring ∧ 𝐼 ∈ 𝑉 ∧ 𝐽 ⊆ 𝐼 ) ∧ ( 𝑦 ∈ 𝐶 ∧ 𝑧 ∈ 𝐼 ) ) ∧ ¬ 𝑧 ∈ 𝐽 ) → ¬ 𝑧 ∈ 𝐽 ) |
111 |
109 110
|
eldifd |
⊢ ( ( ( ( 𝑅 ∈ Ring ∧ 𝐼 ∈ 𝑉 ∧ 𝐽 ⊆ 𝐼 ) ∧ ( 𝑦 ∈ 𝐶 ∧ 𝑧 ∈ 𝐼 ) ) ∧ ¬ 𝑧 ∈ 𝐽 ) → 𝑧 ∈ ( 𝐼 ∖ 𝐽 ) ) |
112 |
|
oveq1 |
⊢ ( 𝑥 = 𝑦 → ( 𝑥 supp 0 ) = ( 𝑦 supp 0 ) ) |
113 |
112
|
sseq1d |
⊢ ( 𝑥 = 𝑦 → ( ( 𝑥 supp 0 ) ⊆ 𝐽 ↔ ( 𝑦 supp 0 ) ⊆ 𝐽 ) ) |
114 |
113 6
|
elrab2 |
⊢ ( 𝑦 ∈ 𝐶 ↔ ( 𝑦 ∈ 𝐵 ∧ ( 𝑦 supp 0 ) ⊆ 𝐽 ) ) |
115 |
114
|
simprbi |
⊢ ( 𝑦 ∈ 𝐶 → ( 𝑦 supp 0 ) ⊆ 𝐽 ) |
116 |
115
|
adantl |
⊢ ( ( ( 𝑅 ∈ Ring ∧ 𝐼 ∈ 𝑉 ∧ 𝐽 ⊆ 𝐼 ) ∧ 𝑦 ∈ 𝐶 ) → ( 𝑦 supp 0 ) ⊆ 𝐽 ) |
117 |
5
|
fvexi |
⊢ 0 ∈ V |
118 |
117
|
a1i |
⊢ ( ( ( 𝑅 ∈ Ring ∧ 𝐼 ∈ 𝑉 ∧ 𝐽 ⊆ 𝐼 ) ∧ 𝑦 ∈ 𝐶 ) → 0 ∈ V ) |
119 |
82 116 44 118
|
suppssr |
⊢ ( ( ( ( 𝑅 ∈ Ring ∧ 𝐼 ∈ 𝑉 ∧ 𝐽 ⊆ 𝐼 ) ∧ 𝑦 ∈ 𝐶 ) ∧ 𝑧 ∈ ( 𝐼 ∖ 𝐽 ) ) → ( 𝑦 ‘ 𝑧 ) = 0 ) |
120 |
108 111 119
|
syl2anc |
⊢ ( ( ( ( 𝑅 ∈ Ring ∧ 𝐼 ∈ 𝑉 ∧ 𝐽 ⊆ 𝐼 ) ∧ ( 𝑦 ∈ 𝐶 ∧ 𝑧 ∈ 𝐼 ) ) ∧ ¬ 𝑧 ∈ 𝐽 ) → ( 𝑦 ‘ 𝑧 ) = 0 ) |
121 |
88
|
fveq2d |
⊢ ( ( 𝑅 ∈ Ring ∧ 𝐼 ∈ 𝑉 ∧ 𝐽 ⊆ 𝐼 ) → ( 0g ‘ 𝑅 ) = ( 0g ‘ ( Scalar ‘ 𝑌 ) ) ) |
122 |
5 121
|
syl5eq |
⊢ ( ( 𝑅 ∈ Ring ∧ 𝐼 ∈ 𝑉 ∧ 𝐽 ⊆ 𝐼 ) → 0 = ( 0g ‘ ( Scalar ‘ 𝑌 ) ) ) |
123 |
122
|
ad2antrr |
⊢ ( ( ( ( 𝑅 ∈ Ring ∧ 𝐼 ∈ 𝑉 ∧ 𝐽 ⊆ 𝐼 ) ∧ ( 𝑦 ∈ 𝐶 ∧ 𝑧 ∈ 𝐼 ) ) ∧ ¬ 𝑧 ∈ 𝐽 ) → 0 = ( 0g ‘ ( Scalar ‘ 𝑌 ) ) ) |
124 |
120 123
|
eqtrd |
⊢ ( ( ( ( 𝑅 ∈ Ring ∧ 𝐼 ∈ 𝑉 ∧ 𝐽 ⊆ 𝐼 ) ∧ ( 𝑦 ∈ 𝐶 ∧ 𝑧 ∈ 𝐼 ) ) ∧ ¬ 𝑧 ∈ 𝐽 ) → ( 𝑦 ‘ 𝑧 ) = ( 0g ‘ ( Scalar ‘ 𝑌 ) ) ) |
125 |
124
|
oveq1d |
⊢ ( ( ( ( 𝑅 ∈ Ring ∧ 𝐼 ∈ 𝑉 ∧ 𝐽 ⊆ 𝐼 ) ∧ ( 𝑦 ∈ 𝐶 ∧ 𝑧 ∈ 𝐼 ) ) ∧ ¬ 𝑧 ∈ 𝐽 ) → ( ( 𝑦 ‘ 𝑧 ) ( ·𝑠 ‘ 𝑌 ) ( 𝑈 ‘ 𝑧 ) ) = ( ( 0g ‘ ( Scalar ‘ 𝑌 ) ) ( ·𝑠 ‘ 𝑌 ) ( 𝑈 ‘ 𝑧 ) ) ) |
126 |
8
|
ad2antrr |
⊢ ( ( ( ( 𝑅 ∈ Ring ∧ 𝐼 ∈ 𝑉 ∧ 𝐽 ⊆ 𝐼 ) ∧ ( 𝑦 ∈ 𝐶 ∧ 𝑧 ∈ 𝐼 ) ) ∧ ¬ 𝑧 ∈ 𝐽 ) → 𝑌 ∈ LMod ) |
127 |
12
|
ffvelrnda |
⊢ ( ( ( 𝑅 ∈ Ring ∧ 𝐼 ∈ 𝑉 ∧ 𝐽 ⊆ 𝐼 ) ∧ 𝑧 ∈ 𝐼 ) → ( 𝑈 ‘ 𝑧 ) ∈ 𝐵 ) |
128 |
127
|
adantrl |
⊢ ( ( ( 𝑅 ∈ Ring ∧ 𝐼 ∈ 𝑉 ∧ 𝐽 ⊆ 𝐼 ) ∧ ( 𝑦 ∈ 𝐶 ∧ 𝑧 ∈ 𝐼 ) ) → ( 𝑈 ‘ 𝑧 ) ∈ 𝐵 ) |
129 |
128
|
adantr |
⊢ ( ( ( ( 𝑅 ∈ Ring ∧ 𝐼 ∈ 𝑉 ∧ 𝐽 ⊆ 𝐼 ) ∧ ( 𝑦 ∈ 𝐶 ∧ 𝑧 ∈ 𝐼 ) ) ∧ ¬ 𝑧 ∈ 𝐽 ) → ( 𝑈 ‘ 𝑧 ) ∈ 𝐵 ) |
130 |
|
eqid |
⊢ ( 0g ‘ ( Scalar ‘ 𝑌 ) ) = ( 0g ‘ ( Scalar ‘ 𝑌 ) ) |
131 |
4 100 48 130 51
|
lmod0vs |
⊢ ( ( 𝑌 ∈ LMod ∧ ( 𝑈 ‘ 𝑧 ) ∈ 𝐵 ) → ( ( 0g ‘ ( Scalar ‘ 𝑌 ) ) ( ·𝑠 ‘ 𝑌 ) ( 𝑈 ‘ 𝑧 ) ) = ( 0g ‘ 𝑌 ) ) |
132 |
126 129 131
|
syl2anc |
⊢ ( ( ( ( 𝑅 ∈ Ring ∧ 𝐼 ∈ 𝑉 ∧ 𝐽 ⊆ 𝐼 ) ∧ ( 𝑦 ∈ 𝐶 ∧ 𝑧 ∈ 𝐼 ) ) ∧ ¬ 𝑧 ∈ 𝐽 ) → ( ( 0g ‘ ( Scalar ‘ 𝑌 ) ) ( ·𝑠 ‘ 𝑌 ) ( 𝑈 ‘ 𝑧 ) ) = ( 0g ‘ 𝑌 ) ) |
133 |
125 132
|
eqtrd |
⊢ ( ( ( ( 𝑅 ∈ Ring ∧ 𝐼 ∈ 𝑉 ∧ 𝐽 ⊆ 𝐼 ) ∧ ( 𝑦 ∈ 𝐶 ∧ 𝑧 ∈ 𝐼 ) ) ∧ ¬ 𝑧 ∈ 𝐽 ) → ( ( 𝑦 ‘ 𝑧 ) ( ·𝑠 ‘ 𝑌 ) ( 𝑈 ‘ 𝑧 ) ) = ( 0g ‘ 𝑌 ) ) |
134 |
59
|
ad2antrr |
⊢ ( ( ( ( 𝑅 ∈ Ring ∧ 𝐼 ∈ 𝑉 ∧ 𝐽 ⊆ 𝐼 ) ∧ ( 𝑦 ∈ 𝐶 ∧ 𝑧 ∈ 𝐼 ) ) ∧ ¬ 𝑧 ∈ 𝐽 ) → ( 𝐾 ‘ ( 𝑈 “ 𝐽 ) ) ∈ ( LSubSp ‘ 𝑌 ) ) |
135 |
51 9
|
lss0cl |
⊢ ( ( 𝑌 ∈ LMod ∧ ( 𝐾 ‘ ( 𝑈 “ 𝐽 ) ) ∈ ( LSubSp ‘ 𝑌 ) ) → ( 0g ‘ 𝑌 ) ∈ ( 𝐾 ‘ ( 𝑈 “ 𝐽 ) ) ) |
136 |
126 134 135
|
syl2anc |
⊢ ( ( ( ( 𝑅 ∈ Ring ∧ 𝐼 ∈ 𝑉 ∧ 𝐽 ⊆ 𝐼 ) ∧ ( 𝑦 ∈ 𝐶 ∧ 𝑧 ∈ 𝐼 ) ) ∧ ¬ 𝑧 ∈ 𝐽 ) → ( 0g ‘ 𝑌 ) ∈ ( 𝐾 ‘ ( 𝑈 “ 𝐽 ) ) ) |
137 |
133 136
|
eqeltrd |
⊢ ( ( ( ( 𝑅 ∈ Ring ∧ 𝐼 ∈ 𝑉 ∧ 𝐽 ⊆ 𝐼 ) ∧ ( 𝑦 ∈ 𝐶 ∧ 𝑧 ∈ 𝐼 ) ) ∧ ¬ 𝑧 ∈ 𝐽 ) → ( ( 𝑦 ‘ 𝑧 ) ( ·𝑠 ‘ 𝑌 ) ( 𝑈 ‘ 𝑧 ) ) ∈ ( 𝐾 ‘ ( 𝑈 “ 𝐽 ) ) ) |
138 |
105 137
|
pm2.61dan |
⊢ ( ( ( 𝑅 ∈ Ring ∧ 𝐼 ∈ 𝑉 ∧ 𝐽 ⊆ 𝐼 ) ∧ ( 𝑦 ∈ 𝐶 ∧ 𝑧 ∈ 𝐼 ) ) → ( ( 𝑦 ‘ 𝑧 ) ( ·𝑠 ‘ 𝑌 ) ( 𝑈 ‘ 𝑧 ) ) ∈ ( 𝐾 ‘ ( 𝑈 “ 𝐽 ) ) ) |
139 |
78 138
|
eqeltrd |
⊢ ( ( ( 𝑅 ∈ Ring ∧ 𝐼 ∈ 𝑉 ∧ 𝐽 ⊆ 𝐼 ) ∧ ( 𝑦 ∈ 𝐶 ∧ 𝑧 ∈ 𝐼 ) ) → ( ( 𝑦 ∘f ( ·𝑠 ‘ 𝑌 ) 𝑈 ) ‘ 𝑧 ) ∈ ( 𝐾 ‘ ( 𝑈 “ 𝐽 ) ) ) |
140 |
139
|
expr |
⊢ ( ( ( 𝑅 ∈ Ring ∧ 𝐼 ∈ 𝑉 ∧ 𝐽 ⊆ 𝐼 ) ∧ 𝑦 ∈ 𝐶 ) → ( 𝑧 ∈ 𝐼 → ( ( 𝑦 ∘f ( ·𝑠 ‘ 𝑌 ) 𝑈 ) ‘ 𝑧 ) ∈ ( 𝐾 ‘ ( 𝑈 “ 𝐽 ) ) ) ) |
141 |
140
|
ralrimiv |
⊢ ( ( ( 𝑅 ∈ Ring ∧ 𝐼 ∈ 𝑉 ∧ 𝐽 ⊆ 𝐼 ) ∧ 𝑦 ∈ 𝐶 ) → ∀ 𝑧 ∈ 𝐼 ( ( 𝑦 ∘f ( ·𝑠 ‘ 𝑌 ) 𝑈 ) ‘ 𝑧 ) ∈ ( 𝐾 ‘ ( 𝑈 “ 𝐽 ) ) ) |
142 |
|
ffnfv |
⊢ ( ( 𝑦 ∘f ( ·𝑠 ‘ 𝑌 ) 𝑈 ) : 𝐼 ⟶ ( 𝐾 ‘ ( 𝑈 “ 𝐽 ) ) ↔ ( ( 𝑦 ∘f ( ·𝑠 ‘ 𝑌 ) 𝑈 ) Fn 𝐼 ∧ ∀ 𝑧 ∈ 𝐼 ( ( 𝑦 ∘f ( ·𝑠 ‘ 𝑌 ) 𝑈 ) ‘ 𝑧 ) ∈ ( 𝐾 ‘ ( 𝑈 “ 𝐽 ) ) ) ) |
143 |
71 141 142
|
sylanbrc |
⊢ ( ( ( 𝑅 ∈ Ring ∧ 𝐼 ∈ 𝑉 ∧ 𝐽 ⊆ 𝐼 ) ∧ 𝑦 ∈ 𝐶 ) → ( 𝑦 ∘f ( ·𝑠 ‘ 𝑌 ) 𝑈 ) : 𝐼 ⟶ ( 𝐾 ‘ ( 𝑈 “ 𝐽 ) ) ) |
144 |
1 5 4
|
frlmbasfsupp |
⊢ ( ( 𝐼 ∈ 𝑉 ∧ 𝑦 ∈ 𝐵 ) → 𝑦 finSupp 0 ) |
145 |
144
|
fsuppimpd |
⊢ ( ( 𝐼 ∈ 𝑉 ∧ 𝑦 ∈ 𝐵 ) → ( 𝑦 supp 0 ) ∈ Fin ) |
146 |
44 47 145
|
syl2anc |
⊢ ( ( ( 𝑅 ∈ Ring ∧ 𝐼 ∈ 𝑉 ∧ 𝐽 ⊆ 𝐼 ) ∧ 𝑦 ∈ 𝐶 ) → ( 𝑦 supp 0 ) ∈ Fin ) |
147 |
|
dffn2 |
⊢ ( ( 𝑦 ∘f ( ·𝑠 ‘ 𝑌 ) 𝑈 ) Fn 𝐼 ↔ ( 𝑦 ∘f ( ·𝑠 ‘ 𝑌 ) 𝑈 ) : 𝐼 ⟶ V ) |
148 |
70 147
|
sylib |
⊢ ( ( ( 𝑅 ∈ Ring ∧ 𝐼 ∈ 𝑉 ∧ 𝐽 ⊆ 𝐼 ) ∧ 𝑦 ∈ 𝐵 ) → ( 𝑦 ∘f ( ·𝑠 ‘ 𝑌 ) 𝑈 ) : 𝐼 ⟶ V ) |
149 |
65
|
adantr |
⊢ ( ( ( ( 𝑅 ∈ Ring ∧ 𝐼 ∈ 𝑉 ∧ 𝐽 ⊆ 𝐼 ) ∧ 𝑦 ∈ 𝐵 ) ∧ 𝑥 ∈ ( 𝐼 ∖ ( 𝑦 supp 0 ) ) ) → 𝑦 Fn 𝐼 ) |
150 |
66
|
ad2antrr |
⊢ ( ( ( ( 𝑅 ∈ Ring ∧ 𝐼 ∈ 𝑉 ∧ 𝐽 ⊆ 𝐼 ) ∧ 𝑦 ∈ 𝐵 ) ∧ 𝑥 ∈ ( 𝐼 ∖ ( 𝑦 supp 0 ) ) ) → 𝑈 Fn 𝐼 ) |
151 |
|
simpll2 |
⊢ ( ( ( ( 𝑅 ∈ Ring ∧ 𝐼 ∈ 𝑉 ∧ 𝐽 ⊆ 𝐼 ) ∧ 𝑦 ∈ 𝐵 ) ∧ 𝑥 ∈ ( 𝐼 ∖ ( 𝑦 supp 0 ) ) ) → 𝐼 ∈ 𝑉 ) |
152 |
|
eldifi |
⊢ ( 𝑥 ∈ ( 𝐼 ∖ ( 𝑦 supp 0 ) ) → 𝑥 ∈ 𝐼 ) |
153 |
152
|
adantl |
⊢ ( ( ( ( 𝑅 ∈ Ring ∧ 𝐼 ∈ 𝑉 ∧ 𝐽 ⊆ 𝐼 ) ∧ 𝑦 ∈ 𝐵 ) ∧ 𝑥 ∈ ( 𝐼 ∖ ( 𝑦 supp 0 ) ) ) → 𝑥 ∈ 𝐼 ) |
154 |
|
fnfvof |
⊢ ( ( ( 𝑦 Fn 𝐼 ∧ 𝑈 Fn 𝐼 ) ∧ ( 𝐼 ∈ 𝑉 ∧ 𝑥 ∈ 𝐼 ) ) → ( ( 𝑦 ∘f ( ·𝑠 ‘ 𝑌 ) 𝑈 ) ‘ 𝑥 ) = ( ( 𝑦 ‘ 𝑥 ) ( ·𝑠 ‘ 𝑌 ) ( 𝑈 ‘ 𝑥 ) ) ) |
155 |
149 150 151 153 154
|
syl22anc |
⊢ ( ( ( ( 𝑅 ∈ Ring ∧ 𝐼 ∈ 𝑉 ∧ 𝐽 ⊆ 𝐼 ) ∧ 𝑦 ∈ 𝐵 ) ∧ 𝑥 ∈ ( 𝐼 ∖ ( 𝑦 supp 0 ) ) ) → ( ( 𝑦 ∘f ( ·𝑠 ‘ 𝑌 ) 𝑈 ) ‘ 𝑥 ) = ( ( 𝑦 ‘ 𝑥 ) ( ·𝑠 ‘ 𝑌 ) ( 𝑈 ‘ 𝑥 ) ) ) |
156 |
|
ssidd |
⊢ ( ( ( 𝑅 ∈ Ring ∧ 𝐼 ∈ 𝑉 ∧ 𝐽 ⊆ 𝐼 ) ∧ 𝑦 ∈ 𝐵 ) → ( 𝑦 supp 0 ) ⊆ ( 𝑦 supp 0 ) ) |
157 |
117
|
a1i |
⊢ ( ( ( 𝑅 ∈ Ring ∧ 𝐼 ∈ 𝑉 ∧ 𝐽 ⊆ 𝐼 ) ∧ 𝑦 ∈ 𝐵 ) → 0 ∈ V ) |
158 |
64 156 68 157
|
suppssr |
⊢ ( ( ( ( 𝑅 ∈ Ring ∧ 𝐼 ∈ 𝑉 ∧ 𝐽 ⊆ 𝐼 ) ∧ 𝑦 ∈ 𝐵 ) ∧ 𝑥 ∈ ( 𝐼 ∖ ( 𝑦 supp 0 ) ) ) → ( 𝑦 ‘ 𝑥 ) = 0 ) |
159 |
122
|
ad2antrr |
⊢ ( ( ( ( 𝑅 ∈ Ring ∧ 𝐼 ∈ 𝑉 ∧ 𝐽 ⊆ 𝐼 ) ∧ 𝑦 ∈ 𝐵 ) ∧ 𝑥 ∈ ( 𝐼 ∖ ( 𝑦 supp 0 ) ) ) → 0 = ( 0g ‘ ( Scalar ‘ 𝑌 ) ) ) |
160 |
158 159
|
eqtrd |
⊢ ( ( ( ( 𝑅 ∈ Ring ∧ 𝐼 ∈ 𝑉 ∧ 𝐽 ⊆ 𝐼 ) ∧ 𝑦 ∈ 𝐵 ) ∧ 𝑥 ∈ ( 𝐼 ∖ ( 𝑦 supp 0 ) ) ) → ( 𝑦 ‘ 𝑥 ) = ( 0g ‘ ( Scalar ‘ 𝑌 ) ) ) |
161 |
160
|
oveq1d |
⊢ ( ( ( ( 𝑅 ∈ Ring ∧ 𝐼 ∈ 𝑉 ∧ 𝐽 ⊆ 𝐼 ) ∧ 𝑦 ∈ 𝐵 ) ∧ 𝑥 ∈ ( 𝐼 ∖ ( 𝑦 supp 0 ) ) ) → ( ( 𝑦 ‘ 𝑥 ) ( ·𝑠 ‘ 𝑌 ) ( 𝑈 ‘ 𝑥 ) ) = ( ( 0g ‘ ( Scalar ‘ 𝑌 ) ) ( ·𝑠 ‘ 𝑌 ) ( 𝑈 ‘ 𝑥 ) ) ) |
162 |
8
|
ad2antrr |
⊢ ( ( ( ( 𝑅 ∈ Ring ∧ 𝐼 ∈ 𝑉 ∧ 𝐽 ⊆ 𝐼 ) ∧ 𝑦 ∈ 𝐵 ) ∧ 𝑥 ∈ ( 𝐼 ∖ ( 𝑦 supp 0 ) ) ) → 𝑌 ∈ LMod ) |
163 |
12
|
adantr |
⊢ ( ( ( 𝑅 ∈ Ring ∧ 𝐼 ∈ 𝑉 ∧ 𝐽 ⊆ 𝐼 ) ∧ 𝑦 ∈ 𝐵 ) → 𝑈 : 𝐼 ⟶ 𝐵 ) |
164 |
|
ffvelrn |
⊢ ( ( 𝑈 : 𝐼 ⟶ 𝐵 ∧ 𝑥 ∈ 𝐼 ) → ( 𝑈 ‘ 𝑥 ) ∈ 𝐵 ) |
165 |
163 152 164
|
syl2an |
⊢ ( ( ( ( 𝑅 ∈ Ring ∧ 𝐼 ∈ 𝑉 ∧ 𝐽 ⊆ 𝐼 ) ∧ 𝑦 ∈ 𝐵 ) ∧ 𝑥 ∈ ( 𝐼 ∖ ( 𝑦 supp 0 ) ) ) → ( 𝑈 ‘ 𝑥 ) ∈ 𝐵 ) |
166 |
4 100 48 130 51
|
lmod0vs |
⊢ ( ( 𝑌 ∈ LMod ∧ ( 𝑈 ‘ 𝑥 ) ∈ 𝐵 ) → ( ( 0g ‘ ( Scalar ‘ 𝑌 ) ) ( ·𝑠 ‘ 𝑌 ) ( 𝑈 ‘ 𝑥 ) ) = ( 0g ‘ 𝑌 ) ) |
167 |
162 165 166
|
syl2anc |
⊢ ( ( ( ( 𝑅 ∈ Ring ∧ 𝐼 ∈ 𝑉 ∧ 𝐽 ⊆ 𝐼 ) ∧ 𝑦 ∈ 𝐵 ) ∧ 𝑥 ∈ ( 𝐼 ∖ ( 𝑦 supp 0 ) ) ) → ( ( 0g ‘ ( Scalar ‘ 𝑌 ) ) ( ·𝑠 ‘ 𝑌 ) ( 𝑈 ‘ 𝑥 ) ) = ( 0g ‘ 𝑌 ) ) |
168 |
155 161 167
|
3eqtrd |
⊢ ( ( ( ( 𝑅 ∈ Ring ∧ 𝐼 ∈ 𝑉 ∧ 𝐽 ⊆ 𝐼 ) ∧ 𝑦 ∈ 𝐵 ) ∧ 𝑥 ∈ ( 𝐼 ∖ ( 𝑦 supp 0 ) ) ) → ( ( 𝑦 ∘f ( ·𝑠 ‘ 𝑌 ) 𝑈 ) ‘ 𝑥 ) = ( 0g ‘ 𝑌 ) ) |
169 |
148 168
|
suppss |
⊢ ( ( ( 𝑅 ∈ Ring ∧ 𝐼 ∈ 𝑉 ∧ 𝐽 ⊆ 𝐼 ) ∧ 𝑦 ∈ 𝐵 ) → ( ( 𝑦 ∘f ( ·𝑠 ‘ 𝑌 ) 𝑈 ) supp ( 0g ‘ 𝑌 ) ) ⊆ ( 𝑦 supp 0 ) ) |
170 |
47 169
|
syldan |
⊢ ( ( ( 𝑅 ∈ Ring ∧ 𝐼 ∈ 𝑉 ∧ 𝐽 ⊆ 𝐼 ) ∧ 𝑦 ∈ 𝐶 ) → ( ( 𝑦 ∘f ( ·𝑠 ‘ 𝑌 ) 𝑈 ) supp ( 0g ‘ 𝑌 ) ) ⊆ ( 𝑦 supp 0 ) ) |
171 |
146 170
|
ssfid |
⊢ ( ( ( 𝑅 ∈ Ring ∧ 𝐼 ∈ 𝑉 ∧ 𝐽 ⊆ 𝐼 ) ∧ 𝑦 ∈ 𝐶 ) → ( ( 𝑦 ∘f ( ·𝑠 ‘ 𝑌 ) 𝑈 ) supp ( 0g ‘ 𝑌 ) ) ∈ Fin ) |
172 |
|
simp2 |
⊢ ( ( 𝑅 ∈ Ring ∧ 𝐼 ∈ 𝑉 ∧ 𝐽 ⊆ 𝐼 ) → 𝐼 ∈ 𝑉 ) |
173 |
1 18 4
|
frlmbasmap |
⊢ ( ( 𝐼 ∈ 𝑉 ∧ 𝑦 ∈ 𝐵 ) → 𝑦 ∈ ( ( Base ‘ 𝑅 ) ↑m 𝐼 ) ) |
174 |
172 81 173
|
syl2an |
⊢ ( ( ( 𝑅 ∈ Ring ∧ 𝐼 ∈ 𝑉 ∧ 𝐽 ⊆ 𝐼 ) ∧ 𝑦 ∈ 𝐶 ) → 𝑦 ∈ ( ( Base ‘ 𝑅 ) ↑m 𝐼 ) ) |
175 |
|
elmapfn |
⊢ ( 𝑦 ∈ ( ( Base ‘ 𝑅 ) ↑m 𝐼 ) → 𝑦 Fn 𝐼 ) |
176 |
174 175
|
syl |
⊢ ( ( ( 𝑅 ∈ Ring ∧ 𝐼 ∈ 𝑉 ∧ 𝐽 ⊆ 𝐼 ) ∧ 𝑦 ∈ 𝐶 ) → 𝑦 Fn 𝐼 ) |
177 |
12
|
adantr |
⊢ ( ( ( 𝑅 ∈ Ring ∧ 𝐼 ∈ 𝑉 ∧ 𝐽 ⊆ 𝐼 ) ∧ 𝑦 ∈ 𝐶 ) → 𝑈 : 𝐼 ⟶ 𝐵 ) |
178 |
177
|
ffnd |
⊢ ( ( ( 𝑅 ∈ Ring ∧ 𝐼 ∈ 𝑉 ∧ 𝐽 ⊆ 𝐼 ) ∧ 𝑦 ∈ 𝐶 ) → 𝑈 Fn 𝐼 ) |
179 |
176 178 44 44
|
offun |
⊢ ( ( ( 𝑅 ∈ Ring ∧ 𝐼 ∈ 𝑉 ∧ 𝐽 ⊆ 𝐼 ) ∧ 𝑦 ∈ 𝐶 ) → Fun ( 𝑦 ∘f ( ·𝑠 ‘ 𝑌 ) 𝑈 ) ) |
180 |
|
ovexd |
⊢ ( ( ( 𝑅 ∈ Ring ∧ 𝐼 ∈ 𝑉 ∧ 𝐽 ⊆ 𝐼 ) ∧ 𝑦 ∈ 𝐶 ) → ( 𝑦 ∘f ( ·𝑠 ‘ 𝑌 ) 𝑈 ) ∈ V ) |
181 |
|
fvexd |
⊢ ( ( ( 𝑅 ∈ Ring ∧ 𝐼 ∈ 𝑉 ∧ 𝐽 ⊆ 𝐼 ) ∧ 𝑦 ∈ 𝐶 ) → ( 0g ‘ 𝑌 ) ∈ V ) |
182 |
|
funisfsupp |
⊢ ( ( Fun ( 𝑦 ∘f ( ·𝑠 ‘ 𝑌 ) 𝑈 ) ∧ ( 𝑦 ∘f ( ·𝑠 ‘ 𝑌 ) 𝑈 ) ∈ V ∧ ( 0g ‘ 𝑌 ) ∈ V ) → ( ( 𝑦 ∘f ( ·𝑠 ‘ 𝑌 ) 𝑈 ) finSupp ( 0g ‘ 𝑌 ) ↔ ( ( 𝑦 ∘f ( ·𝑠 ‘ 𝑌 ) 𝑈 ) supp ( 0g ‘ 𝑌 ) ) ∈ Fin ) ) |
183 |
179 180 181 182
|
syl3anc |
⊢ ( ( ( 𝑅 ∈ Ring ∧ 𝐼 ∈ 𝑉 ∧ 𝐽 ⊆ 𝐼 ) ∧ 𝑦 ∈ 𝐶 ) → ( ( 𝑦 ∘f ( ·𝑠 ‘ 𝑌 ) 𝑈 ) finSupp ( 0g ‘ 𝑌 ) ↔ ( ( 𝑦 ∘f ( ·𝑠 ‘ 𝑌 ) 𝑈 ) supp ( 0g ‘ 𝑌 ) ) ∈ Fin ) ) |
184 |
171 183
|
mpbird |
⊢ ( ( ( 𝑅 ∈ Ring ∧ 𝐼 ∈ 𝑉 ∧ 𝐽 ⊆ 𝐼 ) ∧ 𝑦 ∈ 𝐶 ) → ( 𝑦 ∘f ( ·𝑠 ‘ 𝑌 ) 𝑈 ) finSupp ( 0g ‘ 𝑌 ) ) |
185 |
51 54 44 62 143 184
|
gsumsubgcl |
⊢ ( ( ( 𝑅 ∈ Ring ∧ 𝐼 ∈ 𝑉 ∧ 𝐽 ⊆ 𝐼 ) ∧ 𝑦 ∈ 𝐶 ) → ( 𝑌 Σg ( 𝑦 ∘f ( ·𝑠 ‘ 𝑌 ) 𝑈 ) ) ∈ ( 𝐾 ‘ ( 𝑈 “ 𝐽 ) ) ) |
186 |
50 185
|
eqeltrd |
⊢ ( ( ( 𝑅 ∈ Ring ∧ 𝐼 ∈ 𝑉 ∧ 𝐽 ⊆ 𝐼 ) ∧ 𝑦 ∈ 𝐶 ) → 𝑦 ∈ ( 𝐾 ‘ ( 𝑈 “ 𝐽 ) ) ) |
187 |
42 186
|
eqelssd |
⊢ ( ( 𝑅 ∈ Ring ∧ 𝐼 ∈ 𝑉 ∧ 𝐽 ⊆ 𝐼 ) → ( 𝐾 ‘ ( 𝑈 “ 𝐽 ) ) = 𝐶 ) |