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