| Step | Hyp | Ref | Expression | 
|---|
| 1 |  | ovex 7464 | . . . 4
⊢
(((bra‘𝐴)‘𝐵) · ((bra‘𝐶)‘𝑥)) ∈ V | 
| 2 |  | eqid 2737 | . . . 4
⊢ (𝑥 ∈ ℋ ↦
(((bra‘𝐴)‘𝐵) · ((bra‘𝐶)‘𝑥))) = (𝑥 ∈ ℋ ↦ (((bra‘𝐴)‘𝐵) · ((bra‘𝐶)‘𝑥))) | 
| 3 | 1, 2 | fnmpti 6711 | . . 3
⊢ (𝑥 ∈ ℋ ↦
(((bra‘𝐴)‘𝐵) · ((bra‘𝐶)‘𝑥))) Fn ℋ | 
| 4 |  | bracl 31968 | . . . . . 6
⊢ ((𝐴 ∈ ℋ ∧ 𝐵 ∈ ℋ) →
((bra‘𝐴)‘𝐵) ∈
ℂ) | 
| 5 |  | brafn 31966 | . . . . . 6
⊢ (𝐶 ∈ ℋ →
(bra‘𝐶):
ℋ⟶ℂ) | 
| 6 |  | hfmmval 31758 | . . . . . 6
⊢
((((bra‘𝐴)‘𝐵) ∈ ℂ ∧ (bra‘𝐶): ℋ⟶ℂ)
→ (((bra‘𝐴)‘𝐵) ·fn
(bra‘𝐶)) = (𝑥 ∈ ℋ ↦
(((bra‘𝐴)‘𝐵) · ((bra‘𝐶)‘𝑥)))) | 
| 7 | 4, 5, 6 | syl2an 596 | . . . . 5
⊢ (((𝐴 ∈ ℋ ∧ 𝐵 ∈ ℋ) ∧ 𝐶 ∈ ℋ) →
(((bra‘𝐴)‘𝐵) ·fn
(bra‘𝐶)) = (𝑥 ∈ ℋ ↦
(((bra‘𝐴)‘𝐵) · ((bra‘𝐶)‘𝑥)))) | 
| 8 | 7 | 3impa 1110 | . . . 4
⊢ ((𝐴 ∈ ℋ ∧ 𝐵 ∈ ℋ ∧ 𝐶 ∈ ℋ) →
(((bra‘𝐴)‘𝐵) ·fn
(bra‘𝐶)) = (𝑥 ∈ ℋ ↦
(((bra‘𝐴)‘𝐵) · ((bra‘𝐶)‘𝑥)))) | 
| 9 | 8 | fneq1d 6661 | . . 3
⊢ ((𝐴 ∈ ℋ ∧ 𝐵 ∈ ℋ ∧ 𝐶 ∈ ℋ) →
((((bra‘𝐴)‘𝐵) ·fn
(bra‘𝐶)) Fn ℋ
↔ (𝑥 ∈ ℋ
↦ (((bra‘𝐴)‘𝐵) · ((bra‘𝐶)‘𝑥))) Fn ℋ)) | 
| 10 | 3, 9 | mpbiri 258 | . 2
⊢ ((𝐴 ∈ ℋ ∧ 𝐵 ∈ ℋ ∧ 𝐶 ∈ ℋ) →
(((bra‘𝐴)‘𝐵) ·fn
(bra‘𝐶)) Fn
ℋ) | 
| 11 |  | brafn 31966 | . . . . 5
⊢ (𝐴 ∈ ℋ →
(bra‘𝐴):
ℋ⟶ℂ) | 
| 12 |  | kbop 31972 | . . . . 5
⊢ ((𝐵 ∈ ℋ ∧ 𝐶 ∈ ℋ) → (𝐵 ketbra 𝐶): ℋ⟶ ℋ) | 
| 13 |  | fco 6760 | . . . . 5
⊢
(((bra‘𝐴):
ℋ⟶ℂ ∧ (𝐵 ketbra 𝐶): ℋ⟶ ℋ) →
((bra‘𝐴) ∘
(𝐵 ketbra 𝐶)): ℋ⟶ℂ) | 
| 14 | 11, 12, 13 | syl2an 596 | . . . 4
⊢ ((𝐴 ∈ ℋ ∧ (𝐵 ∈ ℋ ∧ 𝐶 ∈ ℋ)) →
((bra‘𝐴) ∘
(𝐵 ketbra 𝐶)): ℋ⟶ℂ) | 
| 15 | 14 | 3impb 1115 | . . 3
⊢ ((𝐴 ∈ ℋ ∧ 𝐵 ∈ ℋ ∧ 𝐶 ∈ ℋ) →
((bra‘𝐴) ∘
(𝐵 ketbra 𝐶)): ℋ⟶ℂ) | 
| 16 | 15 | ffnd 6737 | . 2
⊢ ((𝐴 ∈ ℋ ∧ 𝐵 ∈ ℋ ∧ 𝐶 ∈ ℋ) →
((bra‘𝐴) ∘
(𝐵 ketbra 𝐶)) Fn ℋ) | 
| 17 |  | simpl1 1192 | . . . . 5
⊢ (((𝐴 ∈ ℋ ∧ 𝐵 ∈ ℋ ∧ 𝐶 ∈ ℋ) ∧ 𝑥 ∈ ℋ) → 𝐴 ∈
ℋ) | 
| 18 |  | simpl2 1193 | . . . . 5
⊢ (((𝐴 ∈ ℋ ∧ 𝐵 ∈ ℋ ∧ 𝐶 ∈ ℋ) ∧ 𝑥 ∈ ℋ) → 𝐵 ∈
ℋ) | 
| 19 |  | braval 31963 | . . . . 5
⊢ ((𝐴 ∈ ℋ ∧ 𝐵 ∈ ℋ) →
((bra‘𝐴)‘𝐵) = (𝐵 ·ih 𝐴)) | 
| 20 | 17, 18, 19 | syl2anc 584 | . . . 4
⊢ (((𝐴 ∈ ℋ ∧ 𝐵 ∈ ℋ ∧ 𝐶 ∈ ℋ) ∧ 𝑥 ∈ ℋ) →
((bra‘𝐴)‘𝐵) = (𝐵 ·ih 𝐴)) | 
| 21 |  | simpl3 1194 | . . . . 5
⊢ (((𝐴 ∈ ℋ ∧ 𝐵 ∈ ℋ ∧ 𝐶 ∈ ℋ) ∧ 𝑥 ∈ ℋ) → 𝐶 ∈
ℋ) | 
| 22 |  | simpr 484 | . . . . 5
⊢ (((𝐴 ∈ ℋ ∧ 𝐵 ∈ ℋ ∧ 𝐶 ∈ ℋ) ∧ 𝑥 ∈ ℋ) → 𝑥 ∈
ℋ) | 
| 23 |  | braval 31963 | . . . . 5
⊢ ((𝐶 ∈ ℋ ∧ 𝑥 ∈ ℋ) →
((bra‘𝐶)‘𝑥) = (𝑥 ·ih 𝐶)) | 
| 24 | 21, 22, 23 | syl2anc 584 | . . . 4
⊢ (((𝐴 ∈ ℋ ∧ 𝐵 ∈ ℋ ∧ 𝐶 ∈ ℋ) ∧ 𝑥 ∈ ℋ) →
((bra‘𝐶)‘𝑥) = (𝑥 ·ih 𝐶)) | 
| 25 | 20, 24 | oveq12d 7449 | . . 3
⊢ (((𝐴 ∈ ℋ ∧ 𝐵 ∈ ℋ ∧ 𝐶 ∈ ℋ) ∧ 𝑥 ∈ ℋ) →
(((bra‘𝐴)‘𝐵) · ((bra‘𝐶)‘𝑥)) = ((𝐵 ·ih 𝐴) · (𝑥 ·ih 𝐶))) | 
| 26 |  | hicl 31099 | . . . . . 6
⊢ ((𝐵 ∈ ℋ ∧ 𝐴 ∈ ℋ) → (𝐵
·ih 𝐴) ∈ ℂ) | 
| 27 | 18, 17, 26 | syl2anc 584 | . . . . 5
⊢ (((𝐴 ∈ ℋ ∧ 𝐵 ∈ ℋ ∧ 𝐶 ∈ ℋ) ∧ 𝑥 ∈ ℋ) → (𝐵
·ih 𝐴) ∈ ℂ) | 
| 28 | 20, 27 | eqeltrd 2841 | . . . 4
⊢ (((𝐴 ∈ ℋ ∧ 𝐵 ∈ ℋ ∧ 𝐶 ∈ ℋ) ∧ 𝑥 ∈ ℋ) →
((bra‘𝐴)‘𝐵) ∈
ℂ) | 
| 29 | 21, 5 | syl 17 | . . . 4
⊢ (((𝐴 ∈ ℋ ∧ 𝐵 ∈ ℋ ∧ 𝐶 ∈ ℋ) ∧ 𝑥 ∈ ℋ) →
(bra‘𝐶):
ℋ⟶ℂ) | 
| 30 |  | hfmval 31763 | . . . 4
⊢
((((bra‘𝐴)‘𝐵) ∈ ℂ ∧ (bra‘𝐶): ℋ⟶ℂ ∧
𝑥 ∈ ℋ) →
((((bra‘𝐴)‘𝐵) ·fn
(bra‘𝐶))‘𝑥) = (((bra‘𝐴)‘𝐵) · ((bra‘𝐶)‘𝑥))) | 
| 31 | 28, 29, 22, 30 | syl3anc 1373 | . . 3
⊢ (((𝐴 ∈ ℋ ∧ 𝐵 ∈ ℋ ∧ 𝐶 ∈ ℋ) ∧ 𝑥 ∈ ℋ) →
((((bra‘𝐴)‘𝐵) ·fn
(bra‘𝐶))‘𝑥) = (((bra‘𝐴)‘𝐵) · ((bra‘𝐶)‘𝑥))) | 
| 32 |  | hicl 31099 | . . . . . 6
⊢ ((𝑥 ∈ ℋ ∧ 𝐶 ∈ ℋ) → (𝑥
·ih 𝐶) ∈ ℂ) | 
| 33 | 22, 21, 32 | syl2anc 584 | . . . . 5
⊢ (((𝐴 ∈ ℋ ∧ 𝐵 ∈ ℋ ∧ 𝐶 ∈ ℋ) ∧ 𝑥 ∈ ℋ) → (𝑥
·ih 𝐶) ∈ ℂ) | 
| 34 |  | ax-his3 31103 | . . . . 5
⊢ (((𝑥
·ih 𝐶) ∈ ℂ ∧ 𝐵 ∈ ℋ ∧ 𝐴 ∈ ℋ) → (((𝑥
·ih 𝐶) ·ℎ 𝐵)
·ih 𝐴) = ((𝑥 ·ih 𝐶) · (𝐵 ·ih 𝐴))) | 
| 35 | 33, 18, 17, 34 | syl3anc 1373 | . . . 4
⊢ (((𝐴 ∈ ℋ ∧ 𝐵 ∈ ℋ ∧ 𝐶 ∈ ℋ) ∧ 𝑥 ∈ ℋ) → (((𝑥
·ih 𝐶) ·ℎ 𝐵)
·ih 𝐴) = ((𝑥 ·ih 𝐶) · (𝐵 ·ih 𝐴))) | 
| 36 | 12 | 3adant1 1131 | . . . . . 6
⊢ ((𝐴 ∈ ℋ ∧ 𝐵 ∈ ℋ ∧ 𝐶 ∈ ℋ) → (𝐵 ketbra 𝐶): ℋ⟶ ℋ) | 
| 37 |  | fvco3 7008 | . . . . . 6
⊢ (((𝐵 ketbra 𝐶): ℋ⟶ ℋ ∧ 𝑥 ∈ ℋ) →
(((bra‘𝐴) ∘
(𝐵 ketbra 𝐶))‘𝑥) = ((bra‘𝐴)‘((𝐵 ketbra 𝐶)‘𝑥))) | 
| 38 | 36, 37 | sylan 580 | . . . . 5
⊢ (((𝐴 ∈ ℋ ∧ 𝐵 ∈ ℋ ∧ 𝐶 ∈ ℋ) ∧ 𝑥 ∈ ℋ) →
(((bra‘𝐴) ∘
(𝐵 ketbra 𝐶))‘𝑥) = ((bra‘𝐴)‘((𝐵 ketbra 𝐶)‘𝑥))) | 
| 39 |  | kbval 31973 | . . . . . . 7
⊢ ((𝐵 ∈ ℋ ∧ 𝐶 ∈ ℋ ∧ 𝑥 ∈ ℋ) → ((𝐵 ketbra 𝐶)‘𝑥) = ((𝑥 ·ih 𝐶)
·ℎ 𝐵)) | 
| 40 | 18, 21, 22, 39 | syl3anc 1373 | . . . . . 6
⊢ (((𝐴 ∈ ℋ ∧ 𝐵 ∈ ℋ ∧ 𝐶 ∈ ℋ) ∧ 𝑥 ∈ ℋ) → ((𝐵 ketbra 𝐶)‘𝑥) = ((𝑥 ·ih 𝐶)
·ℎ 𝐵)) | 
| 41 | 40 | fveq2d 6910 | . . . . 5
⊢ (((𝐴 ∈ ℋ ∧ 𝐵 ∈ ℋ ∧ 𝐶 ∈ ℋ) ∧ 𝑥 ∈ ℋ) →
((bra‘𝐴)‘((𝐵 ketbra 𝐶)‘𝑥)) = ((bra‘𝐴)‘((𝑥 ·ih 𝐶)
·ℎ 𝐵))) | 
| 42 |  | hvmulcl 31032 | . . . . . . 7
⊢ (((𝑥
·ih 𝐶) ∈ ℂ ∧ 𝐵 ∈ ℋ) → ((𝑥 ·ih 𝐶)
·ℎ 𝐵) ∈ ℋ) | 
| 43 | 33, 18, 42 | syl2anc 584 | . . . . . 6
⊢ (((𝐴 ∈ ℋ ∧ 𝐵 ∈ ℋ ∧ 𝐶 ∈ ℋ) ∧ 𝑥 ∈ ℋ) → ((𝑥
·ih 𝐶) ·ℎ 𝐵) ∈
ℋ) | 
| 44 |  | braval 31963 | . . . . . 6
⊢ ((𝐴 ∈ ℋ ∧ ((𝑥
·ih 𝐶) ·ℎ 𝐵) ∈ ℋ) →
((bra‘𝐴)‘((𝑥 ·ih 𝐶)
·ℎ 𝐵)) = (((𝑥 ·ih 𝐶)
·ℎ 𝐵) ·ih 𝐴)) | 
| 45 | 17, 43, 44 | syl2anc 584 | . . . . 5
⊢ (((𝐴 ∈ ℋ ∧ 𝐵 ∈ ℋ ∧ 𝐶 ∈ ℋ) ∧ 𝑥 ∈ ℋ) →
((bra‘𝐴)‘((𝑥 ·ih 𝐶)
·ℎ 𝐵)) = (((𝑥 ·ih 𝐶)
·ℎ 𝐵) ·ih 𝐴)) | 
| 46 | 38, 41, 45 | 3eqtrd 2781 | . . . 4
⊢ (((𝐴 ∈ ℋ ∧ 𝐵 ∈ ℋ ∧ 𝐶 ∈ ℋ) ∧ 𝑥 ∈ ℋ) →
(((bra‘𝐴) ∘
(𝐵 ketbra 𝐶))‘𝑥) = (((𝑥 ·ih 𝐶)
·ℎ 𝐵) ·ih 𝐴)) | 
| 47 | 27, 33 | mulcomd 11282 | . . . 4
⊢ (((𝐴 ∈ ℋ ∧ 𝐵 ∈ ℋ ∧ 𝐶 ∈ ℋ) ∧ 𝑥 ∈ ℋ) → ((𝐵
·ih 𝐴) · (𝑥 ·ih 𝐶)) = ((𝑥 ·ih 𝐶) · (𝐵 ·ih 𝐴))) | 
| 48 | 35, 46, 47 | 3eqtr4d 2787 | . . 3
⊢ (((𝐴 ∈ ℋ ∧ 𝐵 ∈ ℋ ∧ 𝐶 ∈ ℋ) ∧ 𝑥 ∈ ℋ) →
(((bra‘𝐴) ∘
(𝐵 ketbra 𝐶))‘𝑥) = ((𝐵 ·ih 𝐴) · (𝑥 ·ih 𝐶))) | 
| 49 | 25, 31, 48 | 3eqtr4d 2787 | . 2
⊢ (((𝐴 ∈ ℋ ∧ 𝐵 ∈ ℋ ∧ 𝐶 ∈ ℋ) ∧ 𝑥 ∈ ℋ) →
((((bra‘𝐴)‘𝐵) ·fn
(bra‘𝐶))‘𝑥) = (((bra‘𝐴) ∘ (𝐵 ketbra 𝐶))‘𝑥)) | 
| 50 | 10, 16, 49 | eqfnfvd 7054 | 1
⊢ ((𝐴 ∈ ℋ ∧ 𝐵 ∈ ℋ ∧ 𝐶 ∈ ℋ) →
(((bra‘𝐴)‘𝐵) ·fn
(bra‘𝐶)) =
((bra‘𝐴) ∘
(𝐵 ketbra 𝐶))) |