Step | Hyp | Ref
| Expression |
1 | | ovex 6678 |
. . . 4
⊢
(((bra‘𝐴)‘𝐵) · ((bra‘𝐶)‘𝑥)) ∈ V |
2 | | eqid 2622 |
. . . 4
⊢ (𝑥 ∈ ℋ ↦
(((bra‘𝐴)‘𝐵) · ((bra‘𝐶)‘𝑥))) = (𝑥 ∈ ℋ ↦ (((bra‘𝐴)‘𝐵) · ((bra‘𝐶)‘𝑥))) |
3 | 1, 2 | fnmpti 6022 |
. . 3
⊢ (𝑥 ∈ ℋ ↦
(((bra‘𝐴)‘𝐵) · ((bra‘𝐶)‘𝑥))) Fn ℋ |
4 | | bracl 28808 |
. . . . . 6
⊢ ((𝐴 ∈ ℋ ∧ 𝐵 ∈ ℋ) →
((bra‘𝐴)‘𝐵) ∈
ℂ) |
5 | | brafn 28806 |
. . . . . 6
⊢ (𝐶 ∈ ℋ →
(bra‘𝐶):
ℋ⟶ℂ) |
6 | | hfmmval 28598 |
. . . . . 6
⊢
((((bra‘𝐴)‘𝐵) ∈ ℂ ∧ (bra‘𝐶): ℋ⟶ℂ)
→ (((bra‘𝐴)‘𝐵) ·fn
(bra‘𝐶)) = (𝑥 ∈ ℋ ↦
(((bra‘𝐴)‘𝐵) · ((bra‘𝐶)‘𝑥)))) |
7 | 4, 5, 6 | syl2an 494 |
. . . . 5
⊢ (((𝐴 ∈ ℋ ∧ 𝐵 ∈ ℋ) ∧ 𝐶 ∈ ℋ) →
(((bra‘𝐴)‘𝐵) ·fn
(bra‘𝐶)) = (𝑥 ∈ ℋ ↦
(((bra‘𝐴)‘𝐵) · ((bra‘𝐶)‘𝑥)))) |
8 | 7 | 3impa 1259 |
. . . 4
⊢ ((𝐴 ∈ ℋ ∧ 𝐵 ∈ ℋ ∧ 𝐶 ∈ ℋ) →
(((bra‘𝐴)‘𝐵) ·fn
(bra‘𝐶)) = (𝑥 ∈ ℋ ↦
(((bra‘𝐴)‘𝐵) · ((bra‘𝐶)‘𝑥)))) |
9 | 8 | fneq1d 5981 |
. . 3
⊢ ((𝐴 ∈ ℋ ∧ 𝐵 ∈ ℋ ∧ 𝐶 ∈ ℋ) →
((((bra‘𝐴)‘𝐵) ·fn
(bra‘𝐶)) Fn ℋ
↔ (𝑥 ∈ ℋ
↦ (((bra‘𝐴)‘𝐵) · ((bra‘𝐶)‘𝑥))) Fn ℋ)) |
10 | 3, 9 | mpbiri 248 |
. 2
⊢ ((𝐴 ∈ ℋ ∧ 𝐵 ∈ ℋ ∧ 𝐶 ∈ ℋ) →
(((bra‘𝐴)‘𝐵) ·fn
(bra‘𝐶)) Fn
ℋ) |
11 | | brafn 28806 |
. . . . 5
⊢ (𝐴 ∈ ℋ →
(bra‘𝐴):
ℋ⟶ℂ) |
12 | | kbop 28812 |
. . . . 5
⊢ ((𝐵 ∈ ℋ ∧ 𝐶 ∈ ℋ) → (𝐵 ketbra 𝐶): ℋ⟶ ℋ) |
13 | | fco 6058 |
. . . . 5
⊢
(((bra‘𝐴):
ℋ⟶ℂ ∧ (𝐵 ketbra 𝐶): ℋ⟶ ℋ) →
((bra‘𝐴) ∘
(𝐵 ketbra 𝐶)): ℋ⟶ℂ) |
14 | 11, 12, 13 | syl2an 494 |
. . . 4
⊢ ((𝐴 ∈ ℋ ∧ (𝐵 ∈ ℋ ∧ 𝐶 ∈ ℋ)) →
((bra‘𝐴) ∘
(𝐵 ketbra 𝐶)): ℋ⟶ℂ) |
15 | 14 | 3impb 1260 |
. . 3
⊢ ((𝐴 ∈ ℋ ∧ 𝐵 ∈ ℋ ∧ 𝐶 ∈ ℋ) →
((bra‘𝐴) ∘
(𝐵 ketbra 𝐶)): ℋ⟶ℂ) |
16 | | ffn 6045 |
. . 3
⊢
(((bra‘𝐴)
∘ (𝐵 ketbra 𝐶)): ℋ⟶ℂ
→ ((bra‘𝐴)
∘ (𝐵 ketbra 𝐶)) Fn ℋ) |
17 | 15, 16 | syl 17 |
. 2
⊢ ((𝐴 ∈ ℋ ∧ 𝐵 ∈ ℋ ∧ 𝐶 ∈ ℋ) →
((bra‘𝐴) ∘
(𝐵 ketbra 𝐶)) Fn ℋ) |
18 | | simpl1 1064 |
. . . . 5
⊢ (((𝐴 ∈ ℋ ∧ 𝐵 ∈ ℋ ∧ 𝐶 ∈ ℋ) ∧ 𝑥 ∈ ℋ) → 𝐴 ∈
ℋ) |
19 | | simpl2 1065 |
. . . . 5
⊢ (((𝐴 ∈ ℋ ∧ 𝐵 ∈ ℋ ∧ 𝐶 ∈ ℋ) ∧ 𝑥 ∈ ℋ) → 𝐵 ∈
ℋ) |
20 | | braval 28803 |
. . . . 5
⊢ ((𝐴 ∈ ℋ ∧ 𝐵 ∈ ℋ) →
((bra‘𝐴)‘𝐵) = (𝐵 ·ih 𝐴)) |
21 | 18, 19, 20 | syl2anc 693 |
. . . 4
⊢ (((𝐴 ∈ ℋ ∧ 𝐵 ∈ ℋ ∧ 𝐶 ∈ ℋ) ∧ 𝑥 ∈ ℋ) →
((bra‘𝐴)‘𝐵) = (𝐵 ·ih 𝐴)) |
22 | | simpl3 1066 |
. . . . 5
⊢ (((𝐴 ∈ ℋ ∧ 𝐵 ∈ ℋ ∧ 𝐶 ∈ ℋ) ∧ 𝑥 ∈ ℋ) → 𝐶 ∈
ℋ) |
23 | | simpr 477 |
. . . . 5
⊢ (((𝐴 ∈ ℋ ∧ 𝐵 ∈ ℋ ∧ 𝐶 ∈ ℋ) ∧ 𝑥 ∈ ℋ) → 𝑥 ∈
ℋ) |
24 | | braval 28803 |
. . . . 5
⊢ ((𝐶 ∈ ℋ ∧ 𝑥 ∈ ℋ) →
((bra‘𝐶)‘𝑥) = (𝑥 ·ih 𝐶)) |
25 | 22, 23, 24 | syl2anc 693 |
. . . 4
⊢ (((𝐴 ∈ ℋ ∧ 𝐵 ∈ ℋ ∧ 𝐶 ∈ ℋ) ∧ 𝑥 ∈ ℋ) →
((bra‘𝐶)‘𝑥) = (𝑥 ·ih 𝐶)) |
26 | 21, 25 | oveq12d 6668 |
. . 3
⊢ (((𝐴 ∈ ℋ ∧ 𝐵 ∈ ℋ ∧ 𝐶 ∈ ℋ) ∧ 𝑥 ∈ ℋ) →
(((bra‘𝐴)‘𝐵) · ((bra‘𝐶)‘𝑥)) = ((𝐵 ·ih 𝐴) · (𝑥 ·ih 𝐶))) |
27 | | hicl 27937 |
. . . . . 6
⊢ ((𝐵 ∈ ℋ ∧ 𝐴 ∈ ℋ) → (𝐵
·ih 𝐴) ∈ ℂ) |
28 | 19, 18, 27 | syl2anc 693 |
. . . . 5
⊢ (((𝐴 ∈ ℋ ∧ 𝐵 ∈ ℋ ∧ 𝐶 ∈ ℋ) ∧ 𝑥 ∈ ℋ) → (𝐵
·ih 𝐴) ∈ ℂ) |
29 | 21, 28 | eqeltrd 2701 |
. . . 4
⊢ (((𝐴 ∈ ℋ ∧ 𝐵 ∈ ℋ ∧ 𝐶 ∈ ℋ) ∧ 𝑥 ∈ ℋ) →
((bra‘𝐴)‘𝐵) ∈
ℂ) |
30 | 22, 5 | syl 17 |
. . . 4
⊢ (((𝐴 ∈ ℋ ∧ 𝐵 ∈ ℋ ∧ 𝐶 ∈ ℋ) ∧ 𝑥 ∈ ℋ) →
(bra‘𝐶):
ℋ⟶ℂ) |
31 | | hfmval 28603 |
. . . 4
⊢
((((bra‘𝐴)‘𝐵) ∈ ℂ ∧ (bra‘𝐶): ℋ⟶ℂ ∧
𝑥 ∈ ℋ) →
((((bra‘𝐴)‘𝐵) ·fn
(bra‘𝐶))‘𝑥) = (((bra‘𝐴)‘𝐵) · ((bra‘𝐶)‘𝑥))) |
32 | 29, 30, 23, 31 | syl3anc 1326 |
. . 3
⊢ (((𝐴 ∈ ℋ ∧ 𝐵 ∈ ℋ ∧ 𝐶 ∈ ℋ) ∧ 𝑥 ∈ ℋ) →
((((bra‘𝐴)‘𝐵) ·fn
(bra‘𝐶))‘𝑥) = (((bra‘𝐴)‘𝐵) · ((bra‘𝐶)‘𝑥))) |
33 | | hicl 27937 |
. . . . . 6
⊢ ((𝑥 ∈ ℋ ∧ 𝐶 ∈ ℋ) → (𝑥
·ih 𝐶) ∈ ℂ) |
34 | 23, 22, 33 | syl2anc 693 |
. . . . 5
⊢ (((𝐴 ∈ ℋ ∧ 𝐵 ∈ ℋ ∧ 𝐶 ∈ ℋ) ∧ 𝑥 ∈ ℋ) → (𝑥
·ih 𝐶) ∈ ℂ) |
35 | | ax-his3 27941 |
. . . . 5
⊢ (((𝑥
·ih 𝐶) ∈ ℂ ∧ 𝐵 ∈ ℋ ∧ 𝐴 ∈ ℋ) → (((𝑥
·ih 𝐶) ·ℎ 𝐵)
·ih 𝐴) = ((𝑥 ·ih 𝐶) · (𝐵 ·ih 𝐴))) |
36 | 34, 19, 18, 35 | syl3anc 1326 |
. . . 4
⊢ (((𝐴 ∈ ℋ ∧ 𝐵 ∈ ℋ ∧ 𝐶 ∈ ℋ) ∧ 𝑥 ∈ ℋ) → (((𝑥
·ih 𝐶) ·ℎ 𝐵)
·ih 𝐴) = ((𝑥 ·ih 𝐶) · (𝐵 ·ih 𝐴))) |
37 | 12 | 3adant1 1079 |
. . . . . 6
⊢ ((𝐴 ∈ ℋ ∧ 𝐵 ∈ ℋ ∧ 𝐶 ∈ ℋ) → (𝐵 ketbra 𝐶): ℋ⟶ ℋ) |
38 | | fvco3 6275 |
. . . . . 6
⊢ (((𝐵 ketbra 𝐶): ℋ⟶ ℋ ∧ 𝑥 ∈ ℋ) →
(((bra‘𝐴) ∘
(𝐵 ketbra 𝐶))‘𝑥) = ((bra‘𝐴)‘((𝐵 ketbra 𝐶)‘𝑥))) |
39 | 37, 38 | sylan 488 |
. . . . 5
⊢ (((𝐴 ∈ ℋ ∧ 𝐵 ∈ ℋ ∧ 𝐶 ∈ ℋ) ∧ 𝑥 ∈ ℋ) →
(((bra‘𝐴) ∘
(𝐵 ketbra 𝐶))‘𝑥) = ((bra‘𝐴)‘((𝐵 ketbra 𝐶)‘𝑥))) |
40 | | kbval 28813 |
. . . . . . 7
⊢ ((𝐵 ∈ ℋ ∧ 𝐶 ∈ ℋ ∧ 𝑥 ∈ ℋ) → ((𝐵 ketbra 𝐶)‘𝑥) = ((𝑥 ·ih 𝐶)
·ℎ 𝐵)) |
41 | 19, 22, 23, 40 | syl3anc 1326 |
. . . . . 6
⊢ (((𝐴 ∈ ℋ ∧ 𝐵 ∈ ℋ ∧ 𝐶 ∈ ℋ) ∧ 𝑥 ∈ ℋ) → ((𝐵 ketbra 𝐶)‘𝑥) = ((𝑥 ·ih 𝐶)
·ℎ 𝐵)) |
42 | 41 | fveq2d 6195 |
. . . . 5
⊢ (((𝐴 ∈ ℋ ∧ 𝐵 ∈ ℋ ∧ 𝐶 ∈ ℋ) ∧ 𝑥 ∈ ℋ) →
((bra‘𝐴)‘((𝐵 ketbra 𝐶)‘𝑥)) = ((bra‘𝐴)‘((𝑥 ·ih 𝐶)
·ℎ 𝐵))) |
43 | | hvmulcl 27870 |
. . . . . . 7
⊢ (((𝑥
·ih 𝐶) ∈ ℂ ∧ 𝐵 ∈ ℋ) → ((𝑥 ·ih 𝐶)
·ℎ 𝐵) ∈ ℋ) |
44 | 34, 19, 43 | syl2anc 693 |
. . . . . 6
⊢ (((𝐴 ∈ ℋ ∧ 𝐵 ∈ ℋ ∧ 𝐶 ∈ ℋ) ∧ 𝑥 ∈ ℋ) → ((𝑥
·ih 𝐶) ·ℎ 𝐵) ∈
ℋ) |
45 | | braval 28803 |
. . . . . 6
⊢ ((𝐴 ∈ ℋ ∧ ((𝑥
·ih 𝐶) ·ℎ 𝐵) ∈ ℋ) →
((bra‘𝐴)‘((𝑥 ·ih 𝐶)
·ℎ 𝐵)) = (((𝑥 ·ih 𝐶)
·ℎ 𝐵) ·ih 𝐴)) |
46 | 18, 44, 45 | syl2anc 693 |
. . . . 5
⊢ (((𝐴 ∈ ℋ ∧ 𝐵 ∈ ℋ ∧ 𝐶 ∈ ℋ) ∧ 𝑥 ∈ ℋ) →
((bra‘𝐴)‘((𝑥 ·ih 𝐶)
·ℎ 𝐵)) = (((𝑥 ·ih 𝐶)
·ℎ 𝐵) ·ih 𝐴)) |
47 | 39, 42, 46 | 3eqtrd 2660 |
. . . 4
⊢ (((𝐴 ∈ ℋ ∧ 𝐵 ∈ ℋ ∧ 𝐶 ∈ ℋ) ∧ 𝑥 ∈ ℋ) →
(((bra‘𝐴) ∘
(𝐵 ketbra 𝐶))‘𝑥) = (((𝑥 ·ih 𝐶)
·ℎ 𝐵) ·ih 𝐴)) |
48 | 28, 34 | mulcomd 10061 |
. . . 4
⊢ (((𝐴 ∈ ℋ ∧ 𝐵 ∈ ℋ ∧ 𝐶 ∈ ℋ) ∧ 𝑥 ∈ ℋ) → ((𝐵
·ih 𝐴) · (𝑥 ·ih 𝐶)) = ((𝑥 ·ih 𝐶) · (𝐵 ·ih 𝐴))) |
49 | 36, 47, 48 | 3eqtr4d 2666 |
. . 3
⊢ (((𝐴 ∈ ℋ ∧ 𝐵 ∈ ℋ ∧ 𝐶 ∈ ℋ) ∧ 𝑥 ∈ ℋ) →
(((bra‘𝐴) ∘
(𝐵 ketbra 𝐶))‘𝑥) = ((𝐵 ·ih 𝐴) · (𝑥 ·ih 𝐶))) |
50 | 26, 32, 49 | 3eqtr4d 2666 |
. 2
⊢ (((𝐴 ∈ ℋ ∧ 𝐵 ∈ ℋ ∧ 𝐶 ∈ ℋ) ∧ 𝑥 ∈ ℋ) →
((((bra‘𝐴)‘𝐵) ·fn
(bra‘𝐶))‘𝑥) = (((bra‘𝐴) ∘ (𝐵 ketbra 𝐶))‘𝑥)) |
51 | 10, 17, 50 | eqfnfvd 6314 |
1
⊢ ((𝐴 ∈ ℋ ∧ 𝐵 ∈ ℋ ∧ 𝐶 ∈ ℋ) →
(((bra‘𝐴)‘𝐵) ·fn
(bra‘𝐶)) =
((bra‘𝐴) ∘
(𝐵 ketbra 𝐶))) |