Theorem hosubeq0i

Description: If the difference between two operators is zero, they are equal. (Contributed by NM, 27-Jul-2006) (New usage is discouraged.)

	Ref	Expression
Hypotheses	hosd1.2	⊢ 𝑇 : ℋ ⟶ ℋ
	hosd1.3	⊢ 𝑈 : ℋ ⟶ ℋ
Assertion	hosubeq0i	⊢ ( ( 𝑇 −op 𝑈 ) = 0hop ↔ 𝑇 = 𝑈 )

Proof

Step	Hyp	Ref	Expression
1		hosd1.2	⊢ 𝑇 : ℋ ⟶ ℋ
2		hosd1.3	⊢ 𝑈 : ℋ ⟶ ℋ
3	1 2	honegsubi	⊢ ( 𝑇 +op ( - 1 ·op 𝑈 ) ) = ( 𝑇 −op 𝑈 )
4	3	eqeq1i	⊢ ( ( 𝑇 +op ( - 1 ·op 𝑈 ) ) = 0hop ↔ ( 𝑇 −op 𝑈 ) = 0hop )
5		oveq1	⊢ ( ( 𝑇 +op ( - 1 ·op 𝑈 ) ) = 0hop → ( ( 𝑇 +op ( - 1 ·op 𝑈 ) ) +op 𝑈 ) = ( 0hop +op 𝑈 ) )
6	4 5	sylbir	⊢ ( ( 𝑇 −op 𝑈 ) = 0hop → ( ( 𝑇 +op ( - 1 ·op 𝑈 ) ) +op 𝑈 ) = ( 0hop +op 𝑈 ) )
7		neg1cn	⊢ - 1 ∈ ℂ
8		homulcl	⊢ ( ( - 1 ∈ ℂ ∧ 𝑈 : ℋ ⟶ ℋ ) → ( - 1 ·op 𝑈 ) : ℋ ⟶ ℋ )
9	7 2 8	mp2an	⊢ ( - 1 ·op 𝑈 ) : ℋ ⟶ ℋ
10	1 9 2	hoadd32i	⊢ ( ( 𝑇 +op ( - 1 ·op 𝑈 ) ) +op 𝑈 ) = ( ( 𝑇 +op 𝑈 ) +op ( - 1 ·op 𝑈 ) )
11	1 2 9	hoaddassi	⊢ ( ( 𝑇 +op 𝑈 ) +op ( - 1 ·op 𝑈 ) ) = ( 𝑇 +op ( 𝑈 +op ( - 1 ·op 𝑈 ) ) )
12	2 2	honegsubi	⊢ ( 𝑈 +op ( - 1 ·op 𝑈 ) ) = ( 𝑈 −op 𝑈 )
13	2	hodidi	⊢ ( 𝑈 −op 𝑈 ) = 0hop
14	12 13	eqtri	⊢ ( 𝑈 +op ( - 1 ·op 𝑈 ) ) = 0hop
15	14	oveq2i	⊢ ( 𝑇 +op ( 𝑈 +op ( - 1 ·op 𝑈 ) ) ) = ( 𝑇 +op 0hop )
16	1	hoaddid1i	⊢ ( 𝑇 +op 0hop ) = 𝑇
17	15 16	eqtri	⊢ ( 𝑇 +op ( 𝑈 +op ( - 1 ·op 𝑈 ) ) ) = 𝑇
18	11 17	eqtri	⊢ ( ( 𝑇 +op 𝑈 ) +op ( - 1 ·op 𝑈 ) ) = 𝑇
19	10 18	eqtri	⊢ ( ( 𝑇 +op ( - 1 ·op 𝑈 ) ) +op 𝑈 ) = 𝑇
20		ho0f	⊢ 0hop : ℋ ⟶ ℋ
21	20 2	hoaddcomi	⊢ ( 0hop +op 𝑈 ) = ( 𝑈 +op 0hop )
22	2	hoaddid1i	⊢ ( 𝑈 +op 0hop ) = 𝑈
23	21 22	eqtri	⊢ ( 0hop +op 𝑈 ) = 𝑈
24	6 19 23	3eqtr3g	⊢ ( ( 𝑇 −op 𝑈 ) = 0hop → 𝑇 = 𝑈 )
25		oveq1	⊢ ( 𝑇 = 𝑈 → ( 𝑇 −op 𝑈 ) = ( 𝑈 −op 𝑈 ) )
26	25 13	eqtrdi	⊢ ( 𝑇 = 𝑈 → ( 𝑇 −op 𝑈 ) = 0hop )
27	24 26	impbii	⊢ ( ( 𝑇 −op 𝑈 ) = 0hop ↔ 𝑇 = 𝑈 )