Step | Hyp | Ref
| Expression |
1 | | lnoval.1 |
. . . . 5
⊢ 𝑋 = (BaseSet‘𝑈) |
2 | | lnoval.2 |
. . . . 5
⊢ 𝑌 = (BaseSet‘𝑊) |
3 | | lnoval.3 |
. . . . 5
⊢ 𝐺 = ( +𝑣
‘𝑈) |
4 | | lnoval.4 |
. . . . 5
⊢ 𝐻 = ( +𝑣
‘𝑊) |
5 | | lnoval.5 |
. . . . 5
⊢ 𝑅 = (
·𝑠OLD ‘𝑈) |
6 | | lnoval.6 |
. . . . 5
⊢ 𝑆 = (
·𝑠OLD ‘𝑊) |
7 | | lnoval.7 |
. . . . 5
⊢ 𝐿 = (𝑈 LnOp 𝑊) |
8 | 1, 2, 3, 4, 5, 6, 7 | islno 28834 |
. . . 4
⊢ ((𝑈 ∈ NrmCVec ∧ 𝑊 ∈ NrmCVec) → (𝑇 ∈ 𝐿 ↔ (𝑇:𝑋⟶𝑌 ∧ ∀𝑢 ∈ ℂ ∀𝑤 ∈ 𝑋 ∀𝑡 ∈ 𝑋 (𝑇‘((𝑢𝑅𝑤)𝐺𝑡)) = ((𝑢𝑆(𝑇‘𝑤))𝐻(𝑇‘𝑡))))) |
9 | 8 | biimp3a 1471 |
. . 3
⊢ ((𝑈 ∈ NrmCVec ∧ 𝑊 ∈ NrmCVec ∧ 𝑇 ∈ 𝐿) → (𝑇:𝑋⟶𝑌 ∧ ∀𝑢 ∈ ℂ ∀𝑤 ∈ 𝑋 ∀𝑡 ∈ 𝑋 (𝑇‘((𝑢𝑅𝑤)𝐺𝑡)) = ((𝑢𝑆(𝑇‘𝑤))𝐻(𝑇‘𝑡)))) |
10 | 9 | simprd 499 |
. 2
⊢ ((𝑈 ∈ NrmCVec ∧ 𝑊 ∈ NrmCVec ∧ 𝑇 ∈ 𝐿) → ∀𝑢 ∈ ℂ ∀𝑤 ∈ 𝑋 ∀𝑡 ∈ 𝑋 (𝑇‘((𝑢𝑅𝑤)𝐺𝑡)) = ((𝑢𝑆(𝑇‘𝑤))𝐻(𝑇‘𝑡))) |
11 | | oveq1 7220 |
. . . . 5
⊢ (𝑢 = 𝐴 → (𝑢𝑅𝑤) = (𝐴𝑅𝑤)) |
12 | 11 | fvoveq1d 7235 |
. . . 4
⊢ (𝑢 = 𝐴 → (𝑇‘((𝑢𝑅𝑤)𝐺𝑡)) = (𝑇‘((𝐴𝑅𝑤)𝐺𝑡))) |
13 | | oveq1 7220 |
. . . . 5
⊢ (𝑢 = 𝐴 → (𝑢𝑆(𝑇‘𝑤)) = (𝐴𝑆(𝑇‘𝑤))) |
14 | 13 | oveq1d 7228 |
. . . 4
⊢ (𝑢 = 𝐴 → ((𝑢𝑆(𝑇‘𝑤))𝐻(𝑇‘𝑡)) = ((𝐴𝑆(𝑇‘𝑤))𝐻(𝑇‘𝑡))) |
15 | 12, 14 | eqeq12d 2753 |
. . 3
⊢ (𝑢 = 𝐴 → ((𝑇‘((𝑢𝑅𝑤)𝐺𝑡)) = ((𝑢𝑆(𝑇‘𝑤))𝐻(𝑇‘𝑡)) ↔ (𝑇‘((𝐴𝑅𝑤)𝐺𝑡)) = ((𝐴𝑆(𝑇‘𝑤))𝐻(𝑇‘𝑡)))) |
16 | | oveq2 7221 |
. . . . 5
⊢ (𝑤 = 𝐵 → (𝐴𝑅𝑤) = (𝐴𝑅𝐵)) |
17 | 16 | fvoveq1d 7235 |
. . . 4
⊢ (𝑤 = 𝐵 → (𝑇‘((𝐴𝑅𝑤)𝐺𝑡)) = (𝑇‘((𝐴𝑅𝐵)𝐺𝑡))) |
18 | | fveq2 6717 |
. . . . . 6
⊢ (𝑤 = 𝐵 → (𝑇‘𝑤) = (𝑇‘𝐵)) |
19 | 18 | oveq2d 7229 |
. . . . 5
⊢ (𝑤 = 𝐵 → (𝐴𝑆(𝑇‘𝑤)) = (𝐴𝑆(𝑇‘𝐵))) |
20 | 19 | oveq1d 7228 |
. . . 4
⊢ (𝑤 = 𝐵 → ((𝐴𝑆(𝑇‘𝑤))𝐻(𝑇‘𝑡)) = ((𝐴𝑆(𝑇‘𝐵))𝐻(𝑇‘𝑡))) |
21 | 17, 20 | eqeq12d 2753 |
. . 3
⊢ (𝑤 = 𝐵 → ((𝑇‘((𝐴𝑅𝑤)𝐺𝑡)) = ((𝐴𝑆(𝑇‘𝑤))𝐻(𝑇‘𝑡)) ↔ (𝑇‘((𝐴𝑅𝐵)𝐺𝑡)) = ((𝐴𝑆(𝑇‘𝐵))𝐻(𝑇‘𝑡)))) |
22 | | oveq2 7221 |
. . . . 5
⊢ (𝑡 = 𝐶 → ((𝐴𝑅𝐵)𝐺𝑡) = ((𝐴𝑅𝐵)𝐺𝐶)) |
23 | 22 | fveq2d 6721 |
. . . 4
⊢ (𝑡 = 𝐶 → (𝑇‘((𝐴𝑅𝐵)𝐺𝑡)) = (𝑇‘((𝐴𝑅𝐵)𝐺𝐶))) |
24 | | fveq2 6717 |
. . . . 5
⊢ (𝑡 = 𝐶 → (𝑇‘𝑡) = (𝑇‘𝐶)) |
25 | 24 | oveq2d 7229 |
. . . 4
⊢ (𝑡 = 𝐶 → ((𝐴𝑆(𝑇‘𝐵))𝐻(𝑇‘𝑡)) = ((𝐴𝑆(𝑇‘𝐵))𝐻(𝑇‘𝐶))) |
26 | 23, 25 | eqeq12d 2753 |
. . 3
⊢ (𝑡 = 𝐶 → ((𝑇‘((𝐴𝑅𝐵)𝐺𝑡)) = ((𝐴𝑆(𝑇‘𝐵))𝐻(𝑇‘𝑡)) ↔ (𝑇‘((𝐴𝑅𝐵)𝐺𝐶)) = ((𝐴𝑆(𝑇‘𝐵))𝐻(𝑇‘𝐶)))) |
27 | 15, 21, 26 | rspc3v 3550 |
. 2
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ 𝑋 ∧ 𝐶 ∈ 𝑋) → (∀𝑢 ∈ ℂ ∀𝑤 ∈ 𝑋 ∀𝑡 ∈ 𝑋 (𝑇‘((𝑢𝑅𝑤)𝐺𝑡)) = ((𝑢𝑆(𝑇‘𝑤))𝐻(𝑇‘𝑡)) → (𝑇‘((𝐴𝑅𝐵)𝐺𝐶)) = ((𝐴𝑆(𝑇‘𝐵))𝐻(𝑇‘𝐶)))) |
28 | 10, 27 | mpan9 510 |
1
⊢ (((𝑈 ∈ NrmCVec ∧ 𝑊 ∈ NrmCVec ∧ 𝑇 ∈ 𝐿) ∧ (𝐴 ∈ ℂ ∧ 𝐵 ∈ 𝑋 ∧ 𝐶 ∈ 𝑋)) → (𝑇‘((𝐴𝑅𝐵)𝐺𝐶)) = ((𝐴𝑆(𝑇‘𝐵))𝐻(𝑇‘𝐶))) |