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 27608 |
. . . 4
⊢ ((𝑈 ∈ NrmCVec ∧ 𝑊 ∈ NrmCVec) → (𝑇 ∈ 𝐿 ↔ (𝑇:𝑋⟶𝑌 ∧ ∀𝑢 ∈ ℂ ∀𝑤 ∈ 𝑋 ∀𝑡 ∈ 𝑋 (𝑇‘((𝑢𝑅𝑤)𝐺𝑡)) = ((𝑢𝑆(𝑇‘𝑤))𝐻(𝑇‘𝑡))))) |
9 | 8 | biimp3a 1432 |
. . 3
⊢ ((𝑈 ∈ NrmCVec ∧ 𝑊 ∈ NrmCVec ∧ 𝑇 ∈ 𝐿) → (𝑇:𝑋⟶𝑌 ∧ ∀𝑢 ∈ ℂ ∀𝑤 ∈ 𝑋 ∀𝑡 ∈ 𝑋 (𝑇‘((𝑢𝑅𝑤)𝐺𝑡)) = ((𝑢𝑆(𝑇‘𝑤))𝐻(𝑇‘𝑡)))) |
10 | 9 | simprd 479 |
. 2
⊢ ((𝑈 ∈ NrmCVec ∧ 𝑊 ∈ NrmCVec ∧ 𝑇 ∈ 𝐿) → ∀𝑢 ∈ ℂ ∀𝑤 ∈ 𝑋 ∀𝑡 ∈ 𝑋 (𝑇‘((𝑢𝑅𝑤)𝐺𝑡)) = ((𝑢𝑆(𝑇‘𝑤))𝐻(𝑇‘𝑡))) |
11 | | oveq1 6657 |
. . . . . 6
⊢ (𝑢 = 𝐴 → (𝑢𝑅𝑤) = (𝐴𝑅𝑤)) |
12 | 11 | oveq1d 6665 |
. . . . 5
⊢ (𝑢 = 𝐴 → ((𝑢𝑅𝑤)𝐺𝑡) = ((𝐴𝑅𝑤)𝐺𝑡)) |
13 | 12 | fveq2d 6195 |
. . . 4
⊢ (𝑢 = 𝐴 → (𝑇‘((𝑢𝑅𝑤)𝐺𝑡)) = (𝑇‘((𝐴𝑅𝑤)𝐺𝑡))) |
14 | | oveq1 6657 |
. . . . 5
⊢ (𝑢 = 𝐴 → (𝑢𝑆(𝑇‘𝑤)) = (𝐴𝑆(𝑇‘𝑤))) |
15 | 14 | oveq1d 6665 |
. . . 4
⊢ (𝑢 = 𝐴 → ((𝑢𝑆(𝑇‘𝑤))𝐻(𝑇‘𝑡)) = ((𝐴𝑆(𝑇‘𝑤))𝐻(𝑇‘𝑡))) |
16 | 13, 15 | eqeq12d 2637 |
. . 3
⊢ (𝑢 = 𝐴 → ((𝑇‘((𝑢𝑅𝑤)𝐺𝑡)) = ((𝑢𝑆(𝑇‘𝑤))𝐻(𝑇‘𝑡)) ↔ (𝑇‘((𝐴𝑅𝑤)𝐺𝑡)) = ((𝐴𝑆(𝑇‘𝑤))𝐻(𝑇‘𝑡)))) |
17 | | oveq2 6658 |
. . . . . 6
⊢ (𝑤 = 𝐵 → (𝐴𝑅𝑤) = (𝐴𝑅𝐵)) |
18 | 17 | oveq1d 6665 |
. . . . 5
⊢ (𝑤 = 𝐵 → ((𝐴𝑅𝑤)𝐺𝑡) = ((𝐴𝑅𝐵)𝐺𝑡)) |
19 | 18 | fveq2d 6195 |
. . . 4
⊢ (𝑤 = 𝐵 → (𝑇‘((𝐴𝑅𝑤)𝐺𝑡)) = (𝑇‘((𝐴𝑅𝐵)𝐺𝑡))) |
20 | | fveq2 6191 |
. . . . . 6
⊢ (𝑤 = 𝐵 → (𝑇‘𝑤) = (𝑇‘𝐵)) |
21 | 20 | oveq2d 6666 |
. . . . 5
⊢ (𝑤 = 𝐵 → (𝐴𝑆(𝑇‘𝑤)) = (𝐴𝑆(𝑇‘𝐵))) |
22 | 21 | oveq1d 6665 |
. . . 4
⊢ (𝑤 = 𝐵 → ((𝐴𝑆(𝑇‘𝑤))𝐻(𝑇‘𝑡)) = ((𝐴𝑆(𝑇‘𝐵))𝐻(𝑇‘𝑡))) |
23 | 19, 22 | eqeq12d 2637 |
. . 3
⊢ (𝑤 = 𝐵 → ((𝑇‘((𝐴𝑅𝑤)𝐺𝑡)) = ((𝐴𝑆(𝑇‘𝑤))𝐻(𝑇‘𝑡)) ↔ (𝑇‘((𝐴𝑅𝐵)𝐺𝑡)) = ((𝐴𝑆(𝑇‘𝐵))𝐻(𝑇‘𝑡)))) |
24 | | oveq2 6658 |
. . . . 5
⊢ (𝑡 = 𝐶 → ((𝐴𝑅𝐵)𝐺𝑡) = ((𝐴𝑅𝐵)𝐺𝐶)) |
25 | 24 | fveq2d 6195 |
. . . 4
⊢ (𝑡 = 𝐶 → (𝑇‘((𝐴𝑅𝐵)𝐺𝑡)) = (𝑇‘((𝐴𝑅𝐵)𝐺𝐶))) |
26 | | fveq2 6191 |
. . . . 5
⊢ (𝑡 = 𝐶 → (𝑇‘𝑡) = (𝑇‘𝐶)) |
27 | 26 | oveq2d 6666 |
. . . 4
⊢ (𝑡 = 𝐶 → ((𝐴𝑆(𝑇‘𝐵))𝐻(𝑇‘𝑡)) = ((𝐴𝑆(𝑇‘𝐵))𝐻(𝑇‘𝐶))) |
28 | 25, 27 | eqeq12d 2637 |
. . 3
⊢ (𝑡 = 𝐶 → ((𝑇‘((𝐴𝑅𝐵)𝐺𝑡)) = ((𝐴𝑆(𝑇‘𝐵))𝐻(𝑇‘𝑡)) ↔ (𝑇‘((𝐴𝑅𝐵)𝐺𝐶)) = ((𝐴𝑆(𝑇‘𝐵))𝐻(𝑇‘𝐶)))) |
29 | 16, 23, 28 | rspc3v 3325 |
. 2
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ 𝑋 ∧ 𝐶 ∈ 𝑋) → (∀𝑢 ∈ ℂ ∀𝑤 ∈ 𝑋 ∀𝑡 ∈ 𝑋 (𝑇‘((𝑢𝑅𝑤)𝐺𝑡)) = ((𝑢𝑆(𝑇‘𝑤))𝐻(𝑇‘𝑡)) → (𝑇‘((𝐴𝑅𝐵)𝐺𝐶)) = ((𝐴𝑆(𝑇‘𝐵))𝐻(𝑇‘𝐶)))) |
30 | 10, 29 | mpan9 486 |
1
⊢ (((𝑈 ∈ NrmCVec ∧ 𝑊 ∈ NrmCVec ∧ 𝑇 ∈ 𝐿) ∧ (𝐴 ∈ ℂ ∧ 𝐵 ∈ 𝑋 ∧ 𝐶 ∈ 𝑋)) → (𝑇‘((𝐴𝑅𝐵)𝐺𝐶)) = ((𝐴𝑆(𝑇‘𝐵))𝐻(𝑇‘𝐶))) |