| Step | Hyp | Ref
| Expression |
| 1 | | dmadjop 31907 |
. . 3
⊢ (𝑆 ∈ dom
adjℎ → 𝑆: ℋ⟶ ℋ) |
| 2 | | dmadjop 31907 |
. . 3
⊢ (𝑇 ∈ dom
adjℎ → 𝑇: ℋ⟶ ℋ) |
| 3 | | hoaddcl 31777 |
. . 3
⊢ ((𝑆: ℋ⟶ ℋ ∧
𝑇: ℋ⟶ ℋ)
→ (𝑆 +op
𝑇): ℋ⟶
ℋ) |
| 4 | 1, 2, 3 | syl2an 596 |
. 2
⊢ ((𝑆 ∈ dom
adjℎ ∧ 𝑇 ∈ dom adjℎ) →
(𝑆 +op 𝑇): ℋ⟶
ℋ) |
| 5 | | dmadjrn 31914 |
. . . 4
⊢ (𝑆 ∈ dom
adjℎ → (adjℎ‘𝑆) ∈ dom
adjℎ) |
| 6 | | dmadjop 31907 |
. . . 4
⊢
((adjℎ‘𝑆) ∈ dom adjℎ →
(adjℎ‘𝑆): ℋ⟶ ℋ) |
| 7 | 5, 6 | syl 17 |
. . 3
⊢ (𝑆 ∈ dom
adjℎ → (adjℎ‘𝑆): ℋ⟶ ℋ) |
| 8 | | dmadjrn 31914 |
. . . 4
⊢ (𝑇 ∈ dom
adjℎ → (adjℎ‘𝑇) ∈ dom
adjℎ) |
| 9 | | dmadjop 31907 |
. . . 4
⊢
((adjℎ‘𝑇) ∈ dom adjℎ →
(adjℎ‘𝑇): ℋ⟶ ℋ) |
| 10 | 8, 9 | syl 17 |
. . 3
⊢ (𝑇 ∈ dom
adjℎ → (adjℎ‘𝑇): ℋ⟶ ℋ) |
| 11 | | hoaddcl 31777 |
. . 3
⊢
(((adjℎ‘𝑆): ℋ⟶ ℋ ∧
(adjℎ‘𝑇): ℋ⟶ ℋ) →
((adjℎ‘𝑆) +op
(adjℎ‘𝑇)): ℋ⟶
ℋ) |
| 12 | 7, 10, 11 | syl2an 596 |
. 2
⊢ ((𝑆 ∈ dom
adjℎ ∧ 𝑇 ∈ dom adjℎ) →
((adjℎ‘𝑆) +op
(adjℎ‘𝑇)): ℋ⟶
ℋ) |
| 13 | | adj2 31953 |
. . . . . . . 8
⊢ ((𝑆 ∈ dom
adjℎ ∧ 𝑥 ∈ ℋ ∧ 𝑦 ∈ ℋ) → ((𝑆‘𝑥) ·ih 𝑦) = (𝑥 ·ih
((adjℎ‘𝑆)‘𝑦))) |
| 14 | 13 | 3expb 1121 |
. . . . . . 7
⊢ ((𝑆 ∈ dom
adjℎ ∧ (𝑥 ∈ ℋ ∧ 𝑦 ∈ ℋ)) → ((𝑆‘𝑥) ·ih 𝑦) = (𝑥 ·ih
((adjℎ‘𝑆)‘𝑦))) |
| 15 | 14 | adantlr 715 |
. . . . . 6
⊢ (((𝑆 ∈ dom
adjℎ ∧ 𝑇 ∈ dom adjℎ) ∧
(𝑥 ∈ ℋ ∧
𝑦 ∈ ℋ)) →
((𝑆‘𝑥)
·ih 𝑦) = (𝑥 ·ih
((adjℎ‘𝑆)‘𝑦))) |
| 16 | | adj2 31953 |
. . . . . . . 8
⊢ ((𝑇 ∈ dom
adjℎ ∧ 𝑥 ∈ ℋ ∧ 𝑦 ∈ ℋ) → ((𝑇‘𝑥) ·ih 𝑦) = (𝑥 ·ih
((adjℎ‘𝑇)‘𝑦))) |
| 17 | 16 | 3expb 1121 |
. . . . . . 7
⊢ ((𝑇 ∈ dom
adjℎ ∧ (𝑥 ∈ ℋ ∧ 𝑦 ∈ ℋ)) → ((𝑇‘𝑥) ·ih 𝑦) = (𝑥 ·ih
((adjℎ‘𝑇)‘𝑦))) |
| 18 | 17 | adantll 714 |
. . . . . 6
⊢ (((𝑆 ∈ dom
adjℎ ∧ 𝑇 ∈ dom adjℎ) ∧
(𝑥 ∈ ℋ ∧
𝑦 ∈ ℋ)) →
((𝑇‘𝑥)
·ih 𝑦) = (𝑥 ·ih
((adjℎ‘𝑇)‘𝑦))) |
| 19 | 15, 18 | oveq12d 7449 |
. . . . 5
⊢ (((𝑆 ∈ dom
adjℎ ∧ 𝑇 ∈ dom adjℎ) ∧
(𝑥 ∈ ℋ ∧
𝑦 ∈ ℋ)) →
(((𝑆‘𝑥)
·ih 𝑦) + ((𝑇‘𝑥) ·ih 𝑦)) = ((𝑥 ·ih
((adjℎ‘𝑆)‘𝑦)) + (𝑥 ·ih
((adjℎ‘𝑇)‘𝑦)))) |
| 20 | 1 | ffvelcdmda 7104 |
. . . . . . 7
⊢ ((𝑆 ∈ dom
adjℎ ∧ 𝑥 ∈ ℋ) → (𝑆‘𝑥) ∈ ℋ) |
| 21 | 20 | ad2ant2r 747 |
. . . . . 6
⊢ (((𝑆 ∈ dom
adjℎ ∧ 𝑇 ∈ dom adjℎ) ∧
(𝑥 ∈ ℋ ∧
𝑦 ∈ ℋ)) →
(𝑆‘𝑥) ∈ ℋ) |
| 22 | 2 | ffvelcdmda 7104 |
. . . . . . 7
⊢ ((𝑇 ∈ dom
adjℎ ∧ 𝑥 ∈ ℋ) → (𝑇‘𝑥) ∈ ℋ) |
| 23 | 22 | ad2ant2lr 748 |
. . . . . 6
⊢ (((𝑆 ∈ dom
adjℎ ∧ 𝑇 ∈ dom adjℎ) ∧
(𝑥 ∈ ℋ ∧
𝑦 ∈ ℋ)) →
(𝑇‘𝑥) ∈ ℋ) |
| 24 | | simprr 773 |
. . . . . 6
⊢ (((𝑆 ∈ dom
adjℎ ∧ 𝑇 ∈ dom adjℎ) ∧
(𝑥 ∈ ℋ ∧
𝑦 ∈ ℋ)) →
𝑦 ∈
ℋ) |
| 25 | | ax-his2 31102 |
. . . . . 6
⊢ (((𝑆‘𝑥) ∈ ℋ ∧ (𝑇‘𝑥) ∈ ℋ ∧ 𝑦 ∈ ℋ) → (((𝑆‘𝑥) +ℎ (𝑇‘𝑥)) ·ih 𝑦) = (((𝑆‘𝑥) ·ih 𝑦) + ((𝑇‘𝑥) ·ih 𝑦))) |
| 26 | 21, 23, 24, 25 | syl3anc 1373 |
. . . . 5
⊢ (((𝑆 ∈ dom
adjℎ ∧ 𝑇 ∈ dom adjℎ) ∧
(𝑥 ∈ ℋ ∧
𝑦 ∈ ℋ)) →
(((𝑆‘𝑥) +ℎ (𝑇‘𝑥)) ·ih 𝑦) = (((𝑆‘𝑥) ·ih 𝑦) + ((𝑇‘𝑥) ·ih 𝑦))) |
| 27 | | simprl 771 |
. . . . . 6
⊢ (((𝑆 ∈ dom
adjℎ ∧ 𝑇 ∈ dom adjℎ) ∧
(𝑥 ∈ ℋ ∧
𝑦 ∈ ℋ)) →
𝑥 ∈
ℋ) |
| 28 | | adjcl 31951 |
. . . . . . 7
⊢ ((𝑆 ∈ dom
adjℎ ∧ 𝑦 ∈ ℋ) →
((adjℎ‘𝑆)‘𝑦) ∈ ℋ) |
| 29 | 28 | ad2ant2rl 749 |
. . . . . 6
⊢ (((𝑆 ∈ dom
adjℎ ∧ 𝑇 ∈ dom adjℎ) ∧
(𝑥 ∈ ℋ ∧
𝑦 ∈ ℋ)) →
((adjℎ‘𝑆)‘𝑦) ∈ ℋ) |
| 30 | | adjcl 31951 |
. . . . . . 7
⊢ ((𝑇 ∈ dom
adjℎ ∧ 𝑦 ∈ ℋ) →
((adjℎ‘𝑇)‘𝑦) ∈ ℋ) |
| 31 | 30 | ad2ant2l 746 |
. . . . . 6
⊢ (((𝑆 ∈ dom
adjℎ ∧ 𝑇 ∈ dom adjℎ) ∧
(𝑥 ∈ ℋ ∧
𝑦 ∈ ℋ)) →
((adjℎ‘𝑇)‘𝑦) ∈ ℋ) |
| 32 | | his7 31109 |
. . . . . 6
⊢ ((𝑥 ∈ ℋ ∧
((adjℎ‘𝑆)‘𝑦) ∈ ℋ ∧
((adjℎ‘𝑇)‘𝑦) ∈ ℋ) → (𝑥 ·ih
(((adjℎ‘𝑆)‘𝑦) +ℎ
((adjℎ‘𝑇)‘𝑦))) = ((𝑥 ·ih
((adjℎ‘𝑆)‘𝑦)) + (𝑥 ·ih
((adjℎ‘𝑇)‘𝑦)))) |
| 33 | 27, 29, 31, 32 | syl3anc 1373 |
. . . . 5
⊢ (((𝑆 ∈ dom
adjℎ ∧ 𝑇 ∈ dom adjℎ) ∧
(𝑥 ∈ ℋ ∧
𝑦 ∈ ℋ)) →
(𝑥
·ih (((adjℎ‘𝑆)‘𝑦) +ℎ
((adjℎ‘𝑇)‘𝑦))) = ((𝑥 ·ih
((adjℎ‘𝑆)‘𝑦)) + (𝑥 ·ih
((adjℎ‘𝑇)‘𝑦)))) |
| 34 | 19, 26, 33 | 3eqtr4rd 2788 |
. . . 4
⊢ (((𝑆 ∈ dom
adjℎ ∧ 𝑇 ∈ dom adjℎ) ∧
(𝑥 ∈ ℋ ∧
𝑦 ∈ ℋ)) →
(𝑥
·ih (((adjℎ‘𝑆)‘𝑦) +ℎ
((adjℎ‘𝑇)‘𝑦))) = (((𝑆‘𝑥) +ℎ (𝑇‘𝑥)) ·ih 𝑦)) |
| 35 | 7, 10 | anim12i 613 |
. . . . . . 7
⊢ ((𝑆 ∈ dom
adjℎ ∧ 𝑇 ∈ dom adjℎ) →
((adjℎ‘𝑆): ℋ⟶ ℋ ∧
(adjℎ‘𝑇): ℋ⟶
ℋ)) |
| 36 | | hosval 31759 |
. . . . . . . 8
⊢
(((adjℎ‘𝑆): ℋ⟶ ℋ ∧
(adjℎ‘𝑇): ℋ⟶ ℋ ∧ 𝑦 ∈ ℋ) →
(((adjℎ‘𝑆) +op
(adjℎ‘𝑇))‘𝑦) = (((adjℎ‘𝑆)‘𝑦) +ℎ
((adjℎ‘𝑇)‘𝑦))) |
| 37 | 36 | 3expa 1119 |
. . . . . . 7
⊢
((((adjℎ‘𝑆): ℋ⟶ ℋ ∧
(adjℎ‘𝑇): ℋ⟶ ℋ) ∧ 𝑦 ∈ ℋ) →
(((adjℎ‘𝑆) +op
(adjℎ‘𝑇))‘𝑦) = (((adjℎ‘𝑆)‘𝑦) +ℎ
((adjℎ‘𝑇)‘𝑦))) |
| 38 | 35, 37 | sylan 580 |
. . . . . 6
⊢ (((𝑆 ∈ dom
adjℎ ∧ 𝑇 ∈ dom adjℎ) ∧
𝑦 ∈ ℋ) →
(((adjℎ‘𝑆) +op
(adjℎ‘𝑇))‘𝑦) = (((adjℎ‘𝑆)‘𝑦) +ℎ
((adjℎ‘𝑇)‘𝑦))) |
| 39 | 38 | adantrl 716 |
. . . . 5
⊢ (((𝑆 ∈ dom
adjℎ ∧ 𝑇 ∈ dom adjℎ) ∧
(𝑥 ∈ ℋ ∧
𝑦 ∈ ℋ)) →
(((adjℎ‘𝑆) +op
(adjℎ‘𝑇))‘𝑦) = (((adjℎ‘𝑆)‘𝑦) +ℎ
((adjℎ‘𝑇)‘𝑦))) |
| 40 | 39 | oveq2d 7447 |
. . . 4
⊢ (((𝑆 ∈ dom
adjℎ ∧ 𝑇 ∈ dom adjℎ) ∧
(𝑥 ∈ ℋ ∧
𝑦 ∈ ℋ)) →
(𝑥
·ih (((adjℎ‘𝑆) +op
(adjℎ‘𝑇))‘𝑦)) = (𝑥 ·ih
(((adjℎ‘𝑆)‘𝑦) +ℎ
((adjℎ‘𝑇)‘𝑦)))) |
| 41 | 1, 2 | anim12i 613 |
. . . . . . 7
⊢ ((𝑆 ∈ dom
adjℎ ∧ 𝑇 ∈ dom adjℎ) →
(𝑆: ℋ⟶ ℋ
∧ 𝑇: ℋ⟶
ℋ)) |
| 42 | | hosval 31759 |
. . . . . . . 8
⊢ ((𝑆: ℋ⟶ ℋ ∧
𝑇: ℋ⟶ ℋ
∧ 𝑥 ∈ ℋ)
→ ((𝑆 +op
𝑇)‘𝑥) = ((𝑆‘𝑥) +ℎ (𝑇‘𝑥))) |
| 43 | 42 | 3expa 1119 |
. . . . . . 7
⊢ (((𝑆: ℋ⟶ ℋ ∧
𝑇: ℋ⟶ ℋ)
∧ 𝑥 ∈ ℋ)
→ ((𝑆 +op
𝑇)‘𝑥) = ((𝑆‘𝑥) +ℎ (𝑇‘𝑥))) |
| 44 | 41, 43 | sylan 580 |
. . . . . 6
⊢ (((𝑆 ∈ dom
adjℎ ∧ 𝑇 ∈ dom adjℎ) ∧
𝑥 ∈ ℋ) →
((𝑆 +op 𝑇)‘𝑥) = ((𝑆‘𝑥) +ℎ (𝑇‘𝑥))) |
| 45 | 44 | adantrr 717 |
. . . . 5
⊢ (((𝑆 ∈ dom
adjℎ ∧ 𝑇 ∈ dom adjℎ) ∧
(𝑥 ∈ ℋ ∧
𝑦 ∈ ℋ)) →
((𝑆 +op 𝑇)‘𝑥) = ((𝑆‘𝑥) +ℎ (𝑇‘𝑥))) |
| 46 | 45 | oveq1d 7446 |
. . . 4
⊢ (((𝑆 ∈ dom
adjℎ ∧ 𝑇 ∈ dom adjℎ) ∧
(𝑥 ∈ ℋ ∧
𝑦 ∈ ℋ)) →
(((𝑆 +op 𝑇)‘𝑥) ·ih 𝑦) = (((𝑆‘𝑥) +ℎ (𝑇‘𝑥)) ·ih 𝑦)) |
| 47 | 34, 40, 46 | 3eqtr4rd 2788 |
. . 3
⊢ (((𝑆 ∈ dom
adjℎ ∧ 𝑇 ∈ dom adjℎ) ∧
(𝑥 ∈ ℋ ∧
𝑦 ∈ ℋ)) →
(((𝑆 +op 𝑇)‘𝑥) ·ih 𝑦) = (𝑥 ·ih
(((adjℎ‘𝑆) +op
(adjℎ‘𝑇))‘𝑦))) |
| 48 | 47 | ralrimivva 3202 |
. 2
⊢ ((𝑆 ∈ dom
adjℎ ∧ 𝑇 ∈ dom adjℎ) →
∀𝑥 ∈ ℋ
∀𝑦 ∈ ℋ
(((𝑆 +op 𝑇)‘𝑥) ·ih 𝑦) = (𝑥 ·ih
(((adjℎ‘𝑆) +op
(adjℎ‘𝑇))‘𝑦))) |
| 49 | | adjeq 31954 |
. 2
⊢ (((𝑆 +op 𝑇): ℋ⟶ ℋ ∧
((adjℎ‘𝑆) +op
(adjℎ‘𝑇)): ℋ⟶ ℋ ∧
∀𝑥 ∈ ℋ
∀𝑦 ∈ ℋ
(((𝑆 +op 𝑇)‘𝑥) ·ih 𝑦) = (𝑥 ·ih
(((adjℎ‘𝑆) +op
(adjℎ‘𝑇))‘𝑦))) →
(adjℎ‘(𝑆 +op 𝑇)) = ((adjℎ‘𝑆) +op
(adjℎ‘𝑇))) |
| 50 | 4, 12, 48, 49 | syl3anc 1373 |
1
⊢ ((𝑆 ∈ dom
adjℎ ∧ 𝑇 ∈ dom adjℎ) →
(adjℎ‘(𝑆 +op 𝑇)) = ((adjℎ‘𝑆) +op
(adjℎ‘𝑇))) |