| 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 39061 | . . . 4
⊢ (𝑊 ∈ 𝑍 → (𝐺 ∈ 𝐹 ↔ (𝐺:𝑉⟶𝐾 ∧ ∀𝑟 ∈ 𝐾 ∀𝑥 ∈ 𝑉 ∀𝑦 ∈ 𝑉 (𝐺‘((𝑟 · 𝑥) + 𝑦)) = ((𝑟 × (𝐺‘𝑥)) ⨣ (𝐺‘𝑦))))) | 
| 10 | 9 | simplbda 499 | . . 3
⊢ ((𝑊 ∈ 𝑍 ∧ 𝐺 ∈ 𝐹) → ∀𝑟 ∈ 𝐾 ∀𝑥 ∈ 𝑉 ∀𝑦 ∈ 𝑉 (𝐺‘((𝑟 · 𝑥) + 𝑦)) = ((𝑟 × (𝐺‘𝑥)) ⨣ (𝐺‘𝑦))) | 
| 11 | 10 | 3adant3 1133 | . 2
⊢ ((𝑊 ∈ 𝑍 ∧ 𝐺 ∈ 𝐹 ∧ (𝑅 ∈ 𝐾 ∧ 𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑉)) → ∀𝑟 ∈ 𝐾 ∀𝑥 ∈ 𝑉 ∀𝑦 ∈ 𝑉 (𝐺‘((𝑟 · 𝑥) + 𝑦)) = ((𝑟 × (𝐺‘𝑥)) ⨣ (𝐺‘𝑦))) | 
| 12 |  | oveq1 7438 | . . . . . 6
⊢ (𝑟 = 𝑅 → (𝑟 · 𝑥) = (𝑅 · 𝑥)) | 
| 13 | 12 | fvoveq1d 7453 | . . . . 5
⊢ (𝑟 = 𝑅 → (𝐺‘((𝑟 · 𝑥) + 𝑦)) = (𝐺‘((𝑅 · 𝑥) + 𝑦))) | 
| 14 |  | oveq1 7438 | . . . . . 6
⊢ (𝑟 = 𝑅 → (𝑟 × (𝐺‘𝑥)) = (𝑅 × (𝐺‘𝑥))) | 
| 15 | 14 | oveq1d 7446 | . . . . 5
⊢ (𝑟 = 𝑅 → ((𝑟 × (𝐺‘𝑥)) ⨣ (𝐺‘𝑦)) = ((𝑅 × (𝐺‘𝑥)) ⨣ (𝐺‘𝑦))) | 
| 16 | 13, 15 | eqeq12d 2753 | . . . 4
⊢ (𝑟 = 𝑅 → ((𝐺‘((𝑟 · 𝑥) + 𝑦)) = ((𝑟 × (𝐺‘𝑥)) ⨣ (𝐺‘𝑦)) ↔ (𝐺‘((𝑅 · 𝑥) + 𝑦)) = ((𝑅 × (𝐺‘𝑥)) ⨣ (𝐺‘𝑦)))) | 
| 17 |  | oveq2 7439 | . . . . . 6
⊢ (𝑥 = 𝑋 → (𝑅 · 𝑥) = (𝑅 · 𝑋)) | 
| 18 | 17 | fvoveq1d 7453 | . . . . 5
⊢ (𝑥 = 𝑋 → (𝐺‘((𝑅 · 𝑥) + 𝑦)) = (𝐺‘((𝑅 · 𝑋) + 𝑦))) | 
| 19 |  | fveq2 6906 | . . . . . . 7
⊢ (𝑥 = 𝑋 → (𝐺‘𝑥) = (𝐺‘𝑋)) | 
| 20 | 19 | oveq2d 7447 | . . . . . 6
⊢ (𝑥 = 𝑋 → (𝑅 × (𝐺‘𝑥)) = (𝑅 × (𝐺‘𝑋))) | 
| 21 | 20 | oveq1d 7446 | . . . . 5
⊢ (𝑥 = 𝑋 → ((𝑅 × (𝐺‘𝑥)) ⨣ (𝐺‘𝑦)) = ((𝑅 × (𝐺‘𝑋)) ⨣ (𝐺‘𝑦))) | 
| 22 | 18, 21 | eqeq12d 2753 | . . . 4
⊢ (𝑥 = 𝑋 → ((𝐺‘((𝑅 · 𝑥) + 𝑦)) = ((𝑅 × (𝐺‘𝑥)) ⨣ (𝐺‘𝑦)) ↔ (𝐺‘((𝑅 · 𝑋) + 𝑦)) = ((𝑅 × (𝐺‘𝑋)) ⨣ (𝐺‘𝑦)))) | 
| 23 |  | oveq2 7439 | . . . . . 6
⊢ (𝑦 = 𝑌 → ((𝑅 · 𝑋) + 𝑦) = ((𝑅 · 𝑋) + 𝑌)) | 
| 24 | 23 | fveq2d 6910 | . . . . 5
⊢ (𝑦 = 𝑌 → (𝐺‘((𝑅 · 𝑋) + 𝑦)) = (𝐺‘((𝑅 · 𝑋) + 𝑌))) | 
| 25 |  | fveq2 6906 | . . . . . 6
⊢ (𝑦 = 𝑌 → (𝐺‘𝑦) = (𝐺‘𝑌)) | 
| 26 | 25 | oveq2d 7447 | . . . . 5
⊢ (𝑦 = 𝑌 → ((𝑅 × (𝐺‘𝑋)) ⨣ (𝐺‘𝑦)) = ((𝑅 × (𝐺‘𝑋)) ⨣ (𝐺‘𝑌))) | 
| 27 | 24, 26 | eqeq12d 2753 | . . . 4
⊢ (𝑦 = 𝑌 → ((𝐺‘((𝑅 · 𝑋) + 𝑦)) = ((𝑅 × (𝐺‘𝑋)) ⨣ (𝐺‘𝑦)) ↔ (𝐺‘((𝑅 · 𝑋) + 𝑌)) = ((𝑅 × (𝐺‘𝑋)) ⨣ (𝐺‘𝑌)))) | 
| 28 | 16, 22, 27 | rspc3v 3638 | . . 3
⊢ ((𝑅 ∈ 𝐾 ∧ 𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑉) → (∀𝑟 ∈ 𝐾 ∀𝑥 ∈ 𝑉 ∀𝑦 ∈ 𝑉 (𝐺‘((𝑟 · 𝑥) + 𝑦)) = ((𝑟 × (𝐺‘𝑥)) ⨣ (𝐺‘𝑦)) → (𝐺‘((𝑅 · 𝑋) + 𝑌)) = ((𝑅 × (𝐺‘𝑋)) ⨣ (𝐺‘𝑌)))) | 
| 29 | 28 | 3ad2ant3 1136 | . 2
⊢ ((𝑊 ∈ 𝑍 ∧ 𝐺 ∈ 𝐹 ∧ (𝑅 ∈ 𝐾 ∧ 𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑉)) → (∀𝑟 ∈ 𝐾 ∀𝑥 ∈ 𝑉 ∀𝑦 ∈ 𝑉 (𝐺‘((𝑟 · 𝑥) + 𝑦)) = ((𝑟 × (𝐺‘𝑥)) ⨣ (𝐺‘𝑦)) → (𝐺‘((𝑅 · 𝑋) + 𝑌)) = ((𝑅 × (𝐺‘𝑋)) ⨣ (𝐺‘𝑌)))) | 
| 30 | 11, 29 | mpd 15 | 1
⊢ ((𝑊 ∈ 𝑍 ∧ 𝐺 ∈ 𝐹 ∧ (𝑅 ∈ 𝐾 ∧ 𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑉)) → (𝐺‘((𝑅 · 𝑋) + 𝑌)) = ((𝑅 × (𝐺‘𝑋)) ⨣ (𝐺‘𝑌))) |