Step |
Hyp |
Ref |
Expression |
1 |
|
lflset.v |
⊢ 𝑉 = ( Base ‘ 𝑊 ) |
2 |
|
lflset.a |
⊢ + = ( +g ‘ 𝑊 ) |
3 |
|
lflset.d |
⊢ 𝐷 = ( Scalar ‘ 𝑊 ) |
4 |
|
lflset.s |
⊢ · = ( ·𝑠 ‘ 𝑊 ) |
5 |
|
lflset.k |
⊢ 𝐾 = ( Base ‘ 𝐷 ) |
6 |
|
lflset.p |
⊢ ⨣ = ( +g ‘ 𝐷 ) |
7 |
|
lflset.t |
⊢ × = ( .r ‘ 𝐷 ) |
8 |
|
lflset.f |
⊢ 𝐹 = ( LFnl ‘ 𝑊 ) |
9 |
1 2 3 4 5 6 7 8
|
islfl |
⊢ ( 𝑊 ∈ 𝑍 → ( 𝐺 ∈ 𝐹 ↔ ( 𝐺 : 𝑉 ⟶ 𝐾 ∧ ∀ 𝑟 ∈ 𝐾 ∀ 𝑥 ∈ 𝑉 ∀ 𝑦 ∈ 𝑉 ( 𝐺 ‘ ( ( 𝑟 · 𝑥 ) + 𝑦 ) ) = ( ( 𝑟 × ( 𝐺 ‘ 𝑥 ) ) ⨣ ( 𝐺 ‘ 𝑦 ) ) ) ) ) |
10 |
9
|
simplbda |
⊢ ( ( 𝑊 ∈ 𝑍 ∧ 𝐺 ∈ 𝐹 ) → ∀ 𝑟 ∈ 𝐾 ∀ 𝑥 ∈ 𝑉 ∀ 𝑦 ∈ 𝑉 ( 𝐺 ‘ ( ( 𝑟 · 𝑥 ) + 𝑦 ) ) = ( ( 𝑟 × ( 𝐺 ‘ 𝑥 ) ) ⨣ ( 𝐺 ‘ 𝑦 ) ) ) |
11 |
10
|
3adant3 |
⊢ ( ( 𝑊 ∈ 𝑍 ∧ 𝐺 ∈ 𝐹 ∧ ( 𝑅 ∈ 𝐾 ∧ 𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑉 ) ) → ∀ 𝑟 ∈ 𝐾 ∀ 𝑥 ∈ 𝑉 ∀ 𝑦 ∈ 𝑉 ( 𝐺 ‘ ( ( 𝑟 · 𝑥 ) + 𝑦 ) ) = ( ( 𝑟 × ( 𝐺 ‘ 𝑥 ) ) ⨣ ( 𝐺 ‘ 𝑦 ) ) ) |
12 |
|
oveq1 |
⊢ ( 𝑟 = 𝑅 → ( 𝑟 · 𝑥 ) = ( 𝑅 · 𝑥 ) ) |
13 |
12
|
fvoveq1d |
⊢ ( 𝑟 = 𝑅 → ( 𝐺 ‘ ( ( 𝑟 · 𝑥 ) + 𝑦 ) ) = ( 𝐺 ‘ ( ( 𝑅 · 𝑥 ) + 𝑦 ) ) ) |
14 |
|
oveq1 |
⊢ ( 𝑟 = 𝑅 → ( 𝑟 × ( 𝐺 ‘ 𝑥 ) ) = ( 𝑅 × ( 𝐺 ‘ 𝑥 ) ) ) |
15 |
14
|
oveq1d |
⊢ ( 𝑟 = 𝑅 → ( ( 𝑟 × ( 𝐺 ‘ 𝑥 ) ) ⨣ ( 𝐺 ‘ 𝑦 ) ) = ( ( 𝑅 × ( 𝐺 ‘ 𝑥 ) ) ⨣ ( 𝐺 ‘ 𝑦 ) ) ) |
16 |
13 15
|
eqeq12d |
⊢ ( 𝑟 = 𝑅 → ( ( 𝐺 ‘ ( ( 𝑟 · 𝑥 ) + 𝑦 ) ) = ( ( 𝑟 × ( 𝐺 ‘ 𝑥 ) ) ⨣ ( 𝐺 ‘ 𝑦 ) ) ↔ ( 𝐺 ‘ ( ( 𝑅 · 𝑥 ) + 𝑦 ) ) = ( ( 𝑅 × ( 𝐺 ‘ 𝑥 ) ) ⨣ ( 𝐺 ‘ 𝑦 ) ) ) ) |
17 |
|
oveq2 |
⊢ ( 𝑥 = 𝑋 → ( 𝑅 · 𝑥 ) = ( 𝑅 · 𝑋 ) ) |
18 |
17
|
fvoveq1d |
⊢ ( 𝑥 = 𝑋 → ( 𝐺 ‘ ( ( 𝑅 · 𝑥 ) + 𝑦 ) ) = ( 𝐺 ‘ ( ( 𝑅 · 𝑋 ) + 𝑦 ) ) ) |
19 |
|
fveq2 |
⊢ ( 𝑥 = 𝑋 → ( 𝐺 ‘ 𝑥 ) = ( 𝐺 ‘ 𝑋 ) ) |
20 |
19
|
oveq2d |
⊢ ( 𝑥 = 𝑋 → ( 𝑅 × ( 𝐺 ‘ 𝑥 ) ) = ( 𝑅 × ( 𝐺 ‘ 𝑋 ) ) ) |
21 |
20
|
oveq1d |
⊢ ( 𝑥 = 𝑋 → ( ( 𝑅 × ( 𝐺 ‘ 𝑥 ) ) ⨣ ( 𝐺 ‘ 𝑦 ) ) = ( ( 𝑅 × ( 𝐺 ‘ 𝑋 ) ) ⨣ ( 𝐺 ‘ 𝑦 ) ) ) |
22 |
18 21
|
eqeq12d |
⊢ ( 𝑥 = 𝑋 → ( ( 𝐺 ‘ ( ( 𝑅 · 𝑥 ) + 𝑦 ) ) = ( ( 𝑅 × ( 𝐺 ‘ 𝑥 ) ) ⨣ ( 𝐺 ‘ 𝑦 ) ) ↔ ( 𝐺 ‘ ( ( 𝑅 · 𝑋 ) + 𝑦 ) ) = ( ( 𝑅 × ( 𝐺 ‘ 𝑋 ) ) ⨣ ( 𝐺 ‘ 𝑦 ) ) ) ) |
23 |
|
oveq2 |
⊢ ( 𝑦 = 𝑌 → ( ( 𝑅 · 𝑋 ) + 𝑦 ) = ( ( 𝑅 · 𝑋 ) + 𝑌 ) ) |
24 |
23
|
fveq2d |
⊢ ( 𝑦 = 𝑌 → ( 𝐺 ‘ ( ( 𝑅 · 𝑋 ) + 𝑦 ) ) = ( 𝐺 ‘ ( ( 𝑅 · 𝑋 ) + 𝑌 ) ) ) |
25 |
|
fveq2 |
⊢ ( 𝑦 = 𝑌 → ( 𝐺 ‘ 𝑦 ) = ( 𝐺 ‘ 𝑌 ) ) |
26 |
25
|
oveq2d |
⊢ ( 𝑦 = 𝑌 → ( ( 𝑅 × ( 𝐺 ‘ 𝑋 ) ) ⨣ ( 𝐺 ‘ 𝑦 ) ) = ( ( 𝑅 × ( 𝐺 ‘ 𝑋 ) ) ⨣ ( 𝐺 ‘ 𝑌 ) ) ) |
27 |
24 26
|
eqeq12d |
⊢ ( 𝑦 = 𝑌 → ( ( 𝐺 ‘ ( ( 𝑅 · 𝑋 ) + 𝑦 ) ) = ( ( 𝑅 × ( 𝐺 ‘ 𝑋 ) ) ⨣ ( 𝐺 ‘ 𝑦 ) ) ↔ ( 𝐺 ‘ ( ( 𝑅 · 𝑋 ) + 𝑌 ) ) = ( ( 𝑅 × ( 𝐺 ‘ 𝑋 ) ) ⨣ ( 𝐺 ‘ 𝑌 ) ) ) ) |
28 |
16 22 27
|
rspc3v |
⊢ ( ( 𝑅 ∈ 𝐾 ∧ 𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑉 ) → ( ∀ 𝑟 ∈ 𝐾 ∀ 𝑥 ∈ 𝑉 ∀ 𝑦 ∈ 𝑉 ( 𝐺 ‘ ( ( 𝑟 · 𝑥 ) + 𝑦 ) ) = ( ( 𝑟 × ( 𝐺 ‘ 𝑥 ) ) ⨣ ( 𝐺 ‘ 𝑦 ) ) → ( 𝐺 ‘ ( ( 𝑅 · 𝑋 ) + 𝑌 ) ) = ( ( 𝑅 × ( 𝐺 ‘ 𝑋 ) ) ⨣ ( 𝐺 ‘ 𝑌 ) ) ) ) |
29 |
28
|
3ad2ant3 |
⊢ ( ( 𝑊 ∈ 𝑍 ∧ 𝐺 ∈ 𝐹 ∧ ( 𝑅 ∈ 𝐾 ∧ 𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑉 ) ) → ( ∀ 𝑟 ∈ 𝐾 ∀ 𝑥 ∈ 𝑉 ∀ 𝑦 ∈ 𝑉 ( 𝐺 ‘ ( ( 𝑟 · 𝑥 ) + 𝑦 ) ) = ( ( 𝑟 × ( 𝐺 ‘ 𝑥 ) ) ⨣ ( 𝐺 ‘ 𝑦 ) ) → ( 𝐺 ‘ ( ( 𝑅 · 𝑋 ) + 𝑌 ) ) = ( ( 𝑅 × ( 𝐺 ‘ 𝑋 ) ) ⨣ ( 𝐺 ‘ 𝑌 ) ) ) ) |
30 |
11 29
|
mpd |
⊢ ( ( 𝑊 ∈ 𝑍 ∧ 𝐺 ∈ 𝐹 ∧ ( 𝑅 ∈ 𝐾 ∧ 𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑉 ) ) → ( 𝐺 ‘ ( ( 𝑅 · 𝑋 ) + 𝑌 ) ) = ( ( 𝑅 × ( 𝐺 ‘ 𝑋 ) ) ⨣ ( 𝐺 ‘ 𝑌 ) ) ) |