Step |
Hyp |
Ref |
Expression |
1 |
|
lflsccl.v |
⊢ 𝑉 = ( Base ‘ 𝑊 ) |
2 |
|
lflsccl.d |
⊢ 𝐷 = ( Scalar ‘ 𝑊 ) |
3 |
|
lflsccl.k |
⊢ 𝐾 = ( Base ‘ 𝐷 ) |
4 |
|
lflsccl.t |
⊢ · = ( .r ‘ 𝐷 ) |
5 |
|
lflsccl.f |
⊢ 𝐹 = ( LFnl ‘ 𝑊 ) |
6 |
|
lflsccl.w |
⊢ ( 𝜑 → 𝑊 ∈ LMod ) |
7 |
|
lflsccl.g |
⊢ ( 𝜑 → 𝐺 ∈ 𝐹 ) |
8 |
|
lflsccl.r |
⊢ ( 𝜑 → 𝑅 ∈ 𝐾 ) |
9 |
1
|
a1i |
⊢ ( 𝜑 → 𝑉 = ( Base ‘ 𝑊 ) ) |
10 |
|
eqidd |
⊢ ( 𝜑 → ( +g ‘ 𝑊 ) = ( +g ‘ 𝑊 ) ) |
11 |
2
|
a1i |
⊢ ( 𝜑 → 𝐷 = ( Scalar ‘ 𝑊 ) ) |
12 |
|
eqidd |
⊢ ( 𝜑 → ( ·𝑠 ‘ 𝑊 ) = ( ·𝑠 ‘ 𝑊 ) ) |
13 |
3
|
a1i |
⊢ ( 𝜑 → 𝐾 = ( Base ‘ 𝐷 ) ) |
14 |
|
eqidd |
⊢ ( 𝜑 → ( +g ‘ 𝐷 ) = ( +g ‘ 𝐷 ) ) |
15 |
4
|
a1i |
⊢ ( 𝜑 → · = ( .r ‘ 𝐷 ) ) |
16 |
5
|
a1i |
⊢ ( 𝜑 → 𝐹 = ( LFnl ‘ 𝑊 ) ) |
17 |
2
|
lmodring |
⊢ ( 𝑊 ∈ LMod → 𝐷 ∈ Ring ) |
18 |
6 17
|
syl |
⊢ ( 𝜑 → 𝐷 ∈ Ring ) |
19 |
3 4
|
ringcl |
⊢ ( ( 𝐷 ∈ Ring ∧ 𝑥 ∈ 𝐾 ∧ 𝑦 ∈ 𝐾 ) → ( 𝑥 · 𝑦 ) ∈ 𝐾 ) |
20 |
19
|
3expb |
⊢ ( ( 𝐷 ∈ Ring ∧ ( 𝑥 ∈ 𝐾 ∧ 𝑦 ∈ 𝐾 ) ) → ( 𝑥 · 𝑦 ) ∈ 𝐾 ) |
21 |
18 20
|
sylan |
⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝐾 ∧ 𝑦 ∈ 𝐾 ) ) → ( 𝑥 · 𝑦 ) ∈ 𝐾 ) |
22 |
2 3 1 5
|
lflf |
⊢ ( ( 𝑊 ∈ LMod ∧ 𝐺 ∈ 𝐹 ) → 𝐺 : 𝑉 ⟶ 𝐾 ) |
23 |
6 7 22
|
syl2anc |
⊢ ( 𝜑 → 𝐺 : 𝑉 ⟶ 𝐾 ) |
24 |
|
fconst6g |
⊢ ( 𝑅 ∈ 𝐾 → ( 𝑉 × { 𝑅 } ) : 𝑉 ⟶ 𝐾 ) |
25 |
8 24
|
syl |
⊢ ( 𝜑 → ( 𝑉 × { 𝑅 } ) : 𝑉 ⟶ 𝐾 ) |
26 |
1
|
fvexi |
⊢ 𝑉 ∈ V |
27 |
26
|
a1i |
⊢ ( 𝜑 → 𝑉 ∈ V ) |
28 |
|
inidm |
⊢ ( 𝑉 ∩ 𝑉 ) = 𝑉 |
29 |
21 23 25 27 27 28
|
off |
⊢ ( 𝜑 → ( 𝐺 ∘f · ( 𝑉 × { 𝑅 } ) ) : 𝑉 ⟶ 𝐾 ) |
30 |
6
|
adantr |
⊢ ( ( 𝜑 ∧ ( 𝑟 ∈ 𝐾 ∧ 𝑥 ∈ 𝑉 ∧ 𝑦 ∈ 𝑉 ) ) → 𝑊 ∈ LMod ) |
31 |
7
|
adantr |
⊢ ( ( 𝜑 ∧ ( 𝑟 ∈ 𝐾 ∧ 𝑥 ∈ 𝑉 ∧ 𝑦 ∈ 𝑉 ) ) → 𝐺 ∈ 𝐹 ) |
32 |
|
simpr1 |
⊢ ( ( 𝜑 ∧ ( 𝑟 ∈ 𝐾 ∧ 𝑥 ∈ 𝑉 ∧ 𝑦 ∈ 𝑉 ) ) → 𝑟 ∈ 𝐾 ) |
33 |
|
simpr2 |
⊢ ( ( 𝜑 ∧ ( 𝑟 ∈ 𝐾 ∧ 𝑥 ∈ 𝑉 ∧ 𝑦 ∈ 𝑉 ) ) → 𝑥 ∈ 𝑉 ) |
34 |
|
simpr3 |
⊢ ( ( 𝜑 ∧ ( 𝑟 ∈ 𝐾 ∧ 𝑥 ∈ 𝑉 ∧ 𝑦 ∈ 𝑉 ) ) → 𝑦 ∈ 𝑉 ) |
35 |
|
eqid |
⊢ ( +g ‘ 𝑊 ) = ( +g ‘ 𝑊 ) |
36 |
|
eqid |
⊢ ( ·𝑠 ‘ 𝑊 ) = ( ·𝑠 ‘ 𝑊 ) |
37 |
|
eqid |
⊢ ( +g ‘ 𝐷 ) = ( +g ‘ 𝐷 ) |
38 |
1 35 2 36 3 37 4 5
|
lfli |
⊢ ( ( 𝑊 ∈ LMod ∧ 𝐺 ∈ 𝐹 ∧ ( 𝑟 ∈ 𝐾 ∧ 𝑥 ∈ 𝑉 ∧ 𝑦 ∈ 𝑉 ) ) → ( 𝐺 ‘ ( ( 𝑟 ( ·𝑠 ‘ 𝑊 ) 𝑥 ) ( +g ‘ 𝑊 ) 𝑦 ) ) = ( ( 𝑟 · ( 𝐺 ‘ 𝑥 ) ) ( +g ‘ 𝐷 ) ( 𝐺 ‘ 𝑦 ) ) ) |
39 |
30 31 32 33 34 38
|
syl113anc |
⊢ ( ( 𝜑 ∧ ( 𝑟 ∈ 𝐾 ∧ 𝑥 ∈ 𝑉 ∧ 𝑦 ∈ 𝑉 ) ) → ( 𝐺 ‘ ( ( 𝑟 ( ·𝑠 ‘ 𝑊 ) 𝑥 ) ( +g ‘ 𝑊 ) 𝑦 ) ) = ( ( 𝑟 · ( 𝐺 ‘ 𝑥 ) ) ( +g ‘ 𝐷 ) ( 𝐺 ‘ 𝑦 ) ) ) |
40 |
39
|
oveq1d |
⊢ ( ( 𝜑 ∧ ( 𝑟 ∈ 𝐾 ∧ 𝑥 ∈ 𝑉 ∧ 𝑦 ∈ 𝑉 ) ) → ( ( 𝐺 ‘ ( ( 𝑟 ( ·𝑠 ‘ 𝑊 ) 𝑥 ) ( +g ‘ 𝑊 ) 𝑦 ) ) · 𝑅 ) = ( ( ( 𝑟 · ( 𝐺 ‘ 𝑥 ) ) ( +g ‘ 𝐷 ) ( 𝐺 ‘ 𝑦 ) ) · 𝑅 ) ) |
41 |
18
|
adantr |
⊢ ( ( 𝜑 ∧ ( 𝑟 ∈ 𝐾 ∧ 𝑥 ∈ 𝑉 ∧ 𝑦 ∈ 𝑉 ) ) → 𝐷 ∈ Ring ) |
42 |
2 3 1 5
|
lflcl |
⊢ ( ( 𝑊 ∈ LMod ∧ 𝐺 ∈ 𝐹 ∧ 𝑥 ∈ 𝑉 ) → ( 𝐺 ‘ 𝑥 ) ∈ 𝐾 ) |
43 |
30 31 33 42
|
syl3anc |
⊢ ( ( 𝜑 ∧ ( 𝑟 ∈ 𝐾 ∧ 𝑥 ∈ 𝑉 ∧ 𝑦 ∈ 𝑉 ) ) → ( 𝐺 ‘ 𝑥 ) ∈ 𝐾 ) |
44 |
3 4
|
ringcl |
⊢ ( ( 𝐷 ∈ Ring ∧ 𝑟 ∈ 𝐾 ∧ ( 𝐺 ‘ 𝑥 ) ∈ 𝐾 ) → ( 𝑟 · ( 𝐺 ‘ 𝑥 ) ) ∈ 𝐾 ) |
45 |
41 32 43 44
|
syl3anc |
⊢ ( ( 𝜑 ∧ ( 𝑟 ∈ 𝐾 ∧ 𝑥 ∈ 𝑉 ∧ 𝑦 ∈ 𝑉 ) ) → ( 𝑟 · ( 𝐺 ‘ 𝑥 ) ) ∈ 𝐾 ) |
46 |
2 3 1 5
|
lflcl |
⊢ ( ( 𝑊 ∈ LMod ∧ 𝐺 ∈ 𝐹 ∧ 𝑦 ∈ 𝑉 ) → ( 𝐺 ‘ 𝑦 ) ∈ 𝐾 ) |
47 |
30 31 34 46
|
syl3anc |
⊢ ( ( 𝜑 ∧ ( 𝑟 ∈ 𝐾 ∧ 𝑥 ∈ 𝑉 ∧ 𝑦 ∈ 𝑉 ) ) → ( 𝐺 ‘ 𝑦 ) ∈ 𝐾 ) |
48 |
8
|
adantr |
⊢ ( ( 𝜑 ∧ ( 𝑟 ∈ 𝐾 ∧ 𝑥 ∈ 𝑉 ∧ 𝑦 ∈ 𝑉 ) ) → 𝑅 ∈ 𝐾 ) |
49 |
3 37 4
|
ringdir |
⊢ ( ( 𝐷 ∈ Ring ∧ ( ( 𝑟 · ( 𝐺 ‘ 𝑥 ) ) ∈ 𝐾 ∧ ( 𝐺 ‘ 𝑦 ) ∈ 𝐾 ∧ 𝑅 ∈ 𝐾 ) ) → ( ( ( 𝑟 · ( 𝐺 ‘ 𝑥 ) ) ( +g ‘ 𝐷 ) ( 𝐺 ‘ 𝑦 ) ) · 𝑅 ) = ( ( ( 𝑟 · ( 𝐺 ‘ 𝑥 ) ) · 𝑅 ) ( +g ‘ 𝐷 ) ( ( 𝐺 ‘ 𝑦 ) · 𝑅 ) ) ) |
50 |
41 45 47 48 49
|
syl13anc |
⊢ ( ( 𝜑 ∧ ( 𝑟 ∈ 𝐾 ∧ 𝑥 ∈ 𝑉 ∧ 𝑦 ∈ 𝑉 ) ) → ( ( ( 𝑟 · ( 𝐺 ‘ 𝑥 ) ) ( +g ‘ 𝐷 ) ( 𝐺 ‘ 𝑦 ) ) · 𝑅 ) = ( ( ( 𝑟 · ( 𝐺 ‘ 𝑥 ) ) · 𝑅 ) ( +g ‘ 𝐷 ) ( ( 𝐺 ‘ 𝑦 ) · 𝑅 ) ) ) |
51 |
3 4
|
ringass |
⊢ ( ( 𝐷 ∈ Ring ∧ ( 𝑟 ∈ 𝐾 ∧ ( 𝐺 ‘ 𝑥 ) ∈ 𝐾 ∧ 𝑅 ∈ 𝐾 ) ) → ( ( 𝑟 · ( 𝐺 ‘ 𝑥 ) ) · 𝑅 ) = ( 𝑟 · ( ( 𝐺 ‘ 𝑥 ) · 𝑅 ) ) ) |
52 |
41 32 43 48 51
|
syl13anc |
⊢ ( ( 𝜑 ∧ ( 𝑟 ∈ 𝐾 ∧ 𝑥 ∈ 𝑉 ∧ 𝑦 ∈ 𝑉 ) ) → ( ( 𝑟 · ( 𝐺 ‘ 𝑥 ) ) · 𝑅 ) = ( 𝑟 · ( ( 𝐺 ‘ 𝑥 ) · 𝑅 ) ) ) |
53 |
52
|
oveq1d |
⊢ ( ( 𝜑 ∧ ( 𝑟 ∈ 𝐾 ∧ 𝑥 ∈ 𝑉 ∧ 𝑦 ∈ 𝑉 ) ) → ( ( ( 𝑟 · ( 𝐺 ‘ 𝑥 ) ) · 𝑅 ) ( +g ‘ 𝐷 ) ( ( 𝐺 ‘ 𝑦 ) · 𝑅 ) ) = ( ( 𝑟 · ( ( 𝐺 ‘ 𝑥 ) · 𝑅 ) ) ( +g ‘ 𝐷 ) ( ( 𝐺 ‘ 𝑦 ) · 𝑅 ) ) ) |
54 |
40 50 53
|
3eqtrd |
⊢ ( ( 𝜑 ∧ ( 𝑟 ∈ 𝐾 ∧ 𝑥 ∈ 𝑉 ∧ 𝑦 ∈ 𝑉 ) ) → ( ( 𝐺 ‘ ( ( 𝑟 ( ·𝑠 ‘ 𝑊 ) 𝑥 ) ( +g ‘ 𝑊 ) 𝑦 ) ) · 𝑅 ) = ( ( 𝑟 · ( ( 𝐺 ‘ 𝑥 ) · 𝑅 ) ) ( +g ‘ 𝐷 ) ( ( 𝐺 ‘ 𝑦 ) · 𝑅 ) ) ) |
55 |
1 2 36 3
|
lmodvscl |
⊢ ( ( 𝑊 ∈ LMod ∧ 𝑟 ∈ 𝐾 ∧ 𝑥 ∈ 𝑉 ) → ( 𝑟 ( ·𝑠 ‘ 𝑊 ) 𝑥 ) ∈ 𝑉 ) |
56 |
30 32 33 55
|
syl3anc |
⊢ ( ( 𝜑 ∧ ( 𝑟 ∈ 𝐾 ∧ 𝑥 ∈ 𝑉 ∧ 𝑦 ∈ 𝑉 ) ) → ( 𝑟 ( ·𝑠 ‘ 𝑊 ) 𝑥 ) ∈ 𝑉 ) |
57 |
1 35
|
lmodvacl |
⊢ ( ( 𝑊 ∈ LMod ∧ ( 𝑟 ( ·𝑠 ‘ 𝑊 ) 𝑥 ) ∈ 𝑉 ∧ 𝑦 ∈ 𝑉 ) → ( ( 𝑟 ( ·𝑠 ‘ 𝑊 ) 𝑥 ) ( +g ‘ 𝑊 ) 𝑦 ) ∈ 𝑉 ) |
58 |
30 56 34 57
|
syl3anc |
⊢ ( ( 𝜑 ∧ ( 𝑟 ∈ 𝐾 ∧ 𝑥 ∈ 𝑉 ∧ 𝑦 ∈ 𝑉 ) ) → ( ( 𝑟 ( ·𝑠 ‘ 𝑊 ) 𝑥 ) ( +g ‘ 𝑊 ) 𝑦 ) ∈ 𝑉 ) |
59 |
23
|
ffnd |
⊢ ( 𝜑 → 𝐺 Fn 𝑉 ) |
60 |
|
eqidd |
⊢ ( ( 𝜑 ∧ ( ( 𝑟 ( ·𝑠 ‘ 𝑊 ) 𝑥 ) ( +g ‘ 𝑊 ) 𝑦 ) ∈ 𝑉 ) → ( 𝐺 ‘ ( ( 𝑟 ( ·𝑠 ‘ 𝑊 ) 𝑥 ) ( +g ‘ 𝑊 ) 𝑦 ) ) = ( 𝐺 ‘ ( ( 𝑟 ( ·𝑠 ‘ 𝑊 ) 𝑥 ) ( +g ‘ 𝑊 ) 𝑦 ) ) ) |
61 |
27 8 59 60
|
ofc2 |
⊢ ( ( 𝜑 ∧ ( ( 𝑟 ( ·𝑠 ‘ 𝑊 ) 𝑥 ) ( +g ‘ 𝑊 ) 𝑦 ) ∈ 𝑉 ) → ( ( 𝐺 ∘f · ( 𝑉 × { 𝑅 } ) ) ‘ ( ( 𝑟 ( ·𝑠 ‘ 𝑊 ) 𝑥 ) ( +g ‘ 𝑊 ) 𝑦 ) ) = ( ( 𝐺 ‘ ( ( 𝑟 ( ·𝑠 ‘ 𝑊 ) 𝑥 ) ( +g ‘ 𝑊 ) 𝑦 ) ) · 𝑅 ) ) |
62 |
58 61
|
syldan |
⊢ ( ( 𝜑 ∧ ( 𝑟 ∈ 𝐾 ∧ 𝑥 ∈ 𝑉 ∧ 𝑦 ∈ 𝑉 ) ) → ( ( 𝐺 ∘f · ( 𝑉 × { 𝑅 } ) ) ‘ ( ( 𝑟 ( ·𝑠 ‘ 𝑊 ) 𝑥 ) ( +g ‘ 𝑊 ) 𝑦 ) ) = ( ( 𝐺 ‘ ( ( 𝑟 ( ·𝑠 ‘ 𝑊 ) 𝑥 ) ( +g ‘ 𝑊 ) 𝑦 ) ) · 𝑅 ) ) |
63 |
|
eqidd |
⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑉 ) → ( 𝐺 ‘ 𝑥 ) = ( 𝐺 ‘ 𝑥 ) ) |
64 |
27 8 59 63
|
ofc2 |
⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑉 ) → ( ( 𝐺 ∘f · ( 𝑉 × { 𝑅 } ) ) ‘ 𝑥 ) = ( ( 𝐺 ‘ 𝑥 ) · 𝑅 ) ) |
65 |
33 64
|
syldan |
⊢ ( ( 𝜑 ∧ ( 𝑟 ∈ 𝐾 ∧ 𝑥 ∈ 𝑉 ∧ 𝑦 ∈ 𝑉 ) ) → ( ( 𝐺 ∘f · ( 𝑉 × { 𝑅 } ) ) ‘ 𝑥 ) = ( ( 𝐺 ‘ 𝑥 ) · 𝑅 ) ) |
66 |
65
|
oveq2d |
⊢ ( ( 𝜑 ∧ ( 𝑟 ∈ 𝐾 ∧ 𝑥 ∈ 𝑉 ∧ 𝑦 ∈ 𝑉 ) ) → ( 𝑟 · ( ( 𝐺 ∘f · ( 𝑉 × { 𝑅 } ) ) ‘ 𝑥 ) ) = ( 𝑟 · ( ( 𝐺 ‘ 𝑥 ) · 𝑅 ) ) ) |
67 |
|
eqidd |
⊢ ( ( 𝜑 ∧ 𝑦 ∈ 𝑉 ) → ( 𝐺 ‘ 𝑦 ) = ( 𝐺 ‘ 𝑦 ) ) |
68 |
27 8 59 67
|
ofc2 |
⊢ ( ( 𝜑 ∧ 𝑦 ∈ 𝑉 ) → ( ( 𝐺 ∘f · ( 𝑉 × { 𝑅 } ) ) ‘ 𝑦 ) = ( ( 𝐺 ‘ 𝑦 ) · 𝑅 ) ) |
69 |
34 68
|
syldan |
⊢ ( ( 𝜑 ∧ ( 𝑟 ∈ 𝐾 ∧ 𝑥 ∈ 𝑉 ∧ 𝑦 ∈ 𝑉 ) ) → ( ( 𝐺 ∘f · ( 𝑉 × { 𝑅 } ) ) ‘ 𝑦 ) = ( ( 𝐺 ‘ 𝑦 ) · 𝑅 ) ) |
70 |
66 69
|
oveq12d |
⊢ ( ( 𝜑 ∧ ( 𝑟 ∈ 𝐾 ∧ 𝑥 ∈ 𝑉 ∧ 𝑦 ∈ 𝑉 ) ) → ( ( 𝑟 · ( ( 𝐺 ∘f · ( 𝑉 × { 𝑅 } ) ) ‘ 𝑥 ) ) ( +g ‘ 𝐷 ) ( ( 𝐺 ∘f · ( 𝑉 × { 𝑅 } ) ) ‘ 𝑦 ) ) = ( ( 𝑟 · ( ( 𝐺 ‘ 𝑥 ) · 𝑅 ) ) ( +g ‘ 𝐷 ) ( ( 𝐺 ‘ 𝑦 ) · 𝑅 ) ) ) |
71 |
54 62 70
|
3eqtr4d |
⊢ ( ( 𝜑 ∧ ( 𝑟 ∈ 𝐾 ∧ 𝑥 ∈ 𝑉 ∧ 𝑦 ∈ 𝑉 ) ) → ( ( 𝐺 ∘f · ( 𝑉 × { 𝑅 } ) ) ‘ ( ( 𝑟 ( ·𝑠 ‘ 𝑊 ) 𝑥 ) ( +g ‘ 𝑊 ) 𝑦 ) ) = ( ( 𝑟 · ( ( 𝐺 ∘f · ( 𝑉 × { 𝑅 } ) ) ‘ 𝑥 ) ) ( +g ‘ 𝐷 ) ( ( 𝐺 ∘f · ( 𝑉 × { 𝑅 } ) ) ‘ 𝑦 ) ) ) |
72 |
9 10 11 12 13 14 15 16 29 71 6
|
islfld |
⊢ ( 𝜑 → ( 𝐺 ∘f · ( 𝑉 × { 𝑅 } ) ) ∈ 𝐹 ) |