Metamath Proof Explorer

Theorem lnopeq0lem2

Description: Lemma for lnopeq0i . (Contributed by NM, 26-Jul-2006) (New usage is discouraged.)

Ref Expression
Hypothesis lnopeq0.1 ⊢T∈LinOp
Assertion lnopeq0lem2 ⊢A∈ℋ∧B∈ℋ→T⁡A⋅ihB=T⁡A+ℎB⋅ihA+ℎB-T⁡A-ℎB⋅ihA-ℎB+i⁢T⁡A+ℎi⋅ℎB⋅ihA+ℎi⋅ℎB−T⁡A-ℎi⋅ℎB⋅ihA-ℎi⋅ℎB4

Proof

Step Hyp Ref Expression
1 lnopeq0.1 ⊢T∈LinOp
2 fveq2 ⊢A=ifA∈ℋA0ℎ→T⁡A=T⁡ifA∈ℋA0ℎ
3 2 oveq1d ⊢A=ifA∈ℋA0ℎ→T⁡A⋅ihB=T⁡ifA∈ℋA0ℎ⋅ihB
4 fvoveq1 ⊢A=ifA∈ℋA0ℎ→T⁡A+ℎB=T⁡ifA∈ℋA0ℎ+ℎB
5 oveq1 ⊢A=ifA∈ℋA0ℎ→A+ℎB=ifA∈ℋA0ℎ+ℎB
6 4 5 oveq12d ⊢A=ifA∈ℋA0ℎ→T⁡A+ℎB⋅ihA+ℎB=T⁡ifA∈ℋA0ℎ+ℎB⋅ihifA∈ℋA0ℎ+ℎB
7 fvoveq1 ⊢A=ifA∈ℋA0ℎ→T⁡A-ℎB=T⁡ifA∈ℋA0ℎ-ℎB
8 oveq1 ⊢A=ifA∈ℋA0ℎ→A-ℎB=ifA∈ℋA0ℎ-ℎB
9 7 8 oveq12d ⊢A=ifA∈ℋA0ℎ→T⁡A-ℎB⋅ihA-ℎB=T⁡ifA∈ℋA0ℎ-ℎB⋅ihifA∈ℋA0ℎ-ℎB
10 6 9 oveq12d ⊢A=ifA∈ℋA0ℎ→T⁡A+ℎB⋅ihA+ℎB−T⁡A-ℎB⋅ihA-ℎB=T⁡ifA∈ℋA0ℎ+ℎB⋅ihifA∈ℋA0ℎ+ℎB−T⁡ifA∈ℋA0ℎ-ℎB⋅ihifA∈ℋA0ℎ-ℎB
11 fvoveq1 ⊢A=ifA∈ℋA0ℎ→T⁡A+ℎi⋅ℎB=T⁡ifA∈ℋA0ℎ+ℎi⋅ℎB
12 oveq1 ⊢A=ifA∈ℋA0ℎ→A+ℎi⋅ℎB=ifA∈ℋA0ℎ+ℎi⋅ℎB
13 11 12 oveq12d ⊢A=ifA∈ℋA0ℎ→T⁡A+ℎi⋅ℎB⋅ihA+ℎi⋅ℎB=T⁡ifA∈ℋA0ℎ+ℎi⋅ℎB⋅ihifA∈ℋA0ℎ+ℎi⋅ℎB
14 fvoveq1 ⊢A=ifA∈ℋA0ℎ→T⁡A-ℎi⋅ℎB=T⁡ifA∈ℋA0ℎ-ℎi⋅ℎB
15 oveq1 ⊢A=ifA∈ℋA0ℎ→A-ℎi⋅ℎB=ifA∈ℋA0ℎ-ℎi⋅ℎB
16 14 15 oveq12d ⊢A=ifA∈ℋA0ℎ→T⁡A-ℎi⋅ℎB⋅ihA-ℎi⋅ℎB=T⁡ifA∈ℋA0ℎ-ℎi⋅ℎB⋅ihifA∈ℋA0ℎ-ℎi⋅ℎB
17 13 16 oveq12d ⊢A=ifA∈ℋA0ℎ→T⁡A+ℎi⋅ℎB⋅ihA+ℎi⋅ℎB−T⁡A-ℎi⋅ℎB⋅ihA-ℎi⋅ℎB=T⁡ifA∈ℋA0ℎ+ℎi⋅ℎB⋅ihifA∈ℋA0ℎ+ℎi⋅ℎB−T⁡ifA∈ℋA0ℎ-ℎi⋅ℎB⋅ihifA∈ℋA0ℎ-ℎi⋅ℎB
18 17 oveq2d ⊢A=ifA∈ℋA0ℎ→i⁢T⁡A+ℎi⋅ℎB⋅ihA+ℎi⋅ℎB−T⁡A-ℎi⋅ℎB⋅ihA-ℎi⋅ℎB=i⁢T⁡ifA∈ℋA0ℎ+ℎi⋅ℎB⋅ihifA∈ℋA0ℎ+ℎi⋅ℎB−T⁡ifA∈ℋA0ℎ-ℎi⋅ℎB⋅ihifA∈ℋA0ℎ-ℎi⋅ℎB
19 10 18 oveq12d ⊢A=ifA∈ℋA0ℎ→T⁡A+ℎB⋅ihA+ℎB-T⁡A-ℎB⋅ihA-ℎB+i⁢T⁡A+ℎi⋅ℎB⋅ihA+ℎi⋅ℎB−T⁡A-ℎi⋅ℎB⋅ihA-ℎi⋅ℎB=T⁡ifA∈ℋA0ℎ+ℎB⋅ihifA∈ℋA0ℎ+ℎB-T⁡ifA∈ℋA0ℎ-ℎB⋅ihifA∈ℋA0ℎ-ℎB+i⁢T⁡ifA∈ℋA0ℎ+ℎi⋅ℎB⋅ihifA∈ℋA0ℎ+ℎi⋅ℎB−T⁡ifA∈ℋA0ℎ-ℎi⋅ℎB⋅ihifA∈ℋA0ℎ-ℎi⋅ℎB
20 19 oveq1d ⊢A=ifA∈ℋA0ℎ→T⁡A+ℎB⋅ihA+ℎB-T⁡A-ℎB⋅ihA-ℎB+i⁢T⁡A+ℎi⋅ℎB⋅ihA+ℎi⋅ℎB−T⁡A-ℎi⋅ℎB⋅ihA-ℎi⋅ℎB4=T⁡ifA∈ℋA0ℎ+ℎB⋅ihifA∈ℋA0ℎ+ℎB-T⁡ifA∈ℋA0ℎ-ℎB⋅ihifA∈ℋA0ℎ-ℎB+i⁢T⁡ifA∈ℋA0ℎ+ℎi⋅ℎB⋅ihifA∈ℋA0ℎ+ℎi⋅ℎB−T⁡ifA∈ℋA0ℎ-ℎi⋅ℎB⋅ihifA∈ℋA0ℎ-ℎi⋅ℎB4
21 3 20 eqeq12d ⊢A=ifA∈ℋA0ℎ→T⁡A⋅ihB=T⁡A+ℎB⋅ihA+ℎB-T⁡A-ℎB⋅ihA-ℎB+i⁢T⁡A+ℎi⋅ℎB⋅ihA+ℎi⋅ℎB−T⁡A-ℎi⋅ℎB⋅ihA-ℎi⋅ℎB4↔T⁡ifA∈ℋA0ℎ⋅ihB=T⁡ifA∈ℋA0ℎ+ℎB⋅ihifA∈ℋA0ℎ+ℎB-T⁡ifA∈ℋA0ℎ-ℎB⋅ihifA∈ℋA0ℎ-ℎB+i⁢T⁡ifA∈ℋA0ℎ+ℎi⋅ℎB⋅ihifA∈ℋA0ℎ+ℎi⋅ℎB−T⁡ifA∈ℋA0ℎ-ℎi⋅ℎB⋅ihifA∈ℋA0ℎ-ℎi⋅ℎB4
22 oveq2 ⊢B=ifB∈ℋB0ℎ→T⁡ifA∈ℋA0ℎ⋅ihB=T⁡ifA∈ℋA0ℎ⋅ihifB∈ℋB0ℎ
23 oveq2 ⊢B=ifB∈ℋB0ℎ→ifA∈ℋA0ℎ+ℎB=ifA∈ℋA0ℎ+ℎifB∈ℋB0ℎ
24 23 fveq2d ⊢B=ifB∈ℋB0ℎ→T⁡ifA∈ℋA0ℎ+ℎB=T⁡ifA∈ℋA0ℎ+ℎifB∈ℋB0ℎ
25 24 23 oveq12d ⊢B=ifB∈ℋB0ℎ→T⁡ifA∈ℋA0ℎ+ℎB⋅ihifA∈ℋA0ℎ+ℎB=T⁡ifA∈ℋA0ℎ+ℎifB∈ℋB0ℎ⋅ihifA∈ℋA0ℎ+ℎifB∈ℋB0ℎ
26 oveq2 ⊢B=ifB∈ℋB0ℎ→ifA∈ℋA0ℎ-ℎB=ifA∈ℋA0ℎ-ℎifB∈ℋB0ℎ
27 26 fveq2d ⊢B=ifB∈ℋB0ℎ→T⁡ifA∈ℋA0ℎ-ℎB=T⁡ifA∈ℋA0ℎ-ℎifB∈ℋB0ℎ
28 27 26 oveq12d ⊢B=ifB∈ℋB0ℎ→T⁡ifA∈ℋA0ℎ-ℎB⋅ihifA∈ℋA0ℎ-ℎB=T⁡ifA∈ℋA0ℎ-ℎifB∈ℋB0ℎ⋅ihifA∈ℋA0ℎ-ℎifB∈ℋB0ℎ
29 25 28 oveq12d ⊢B=ifB∈ℋB0ℎ→T⁡ifA∈ℋA0ℎ+ℎB⋅ihifA∈ℋA0ℎ+ℎB−T⁡ifA∈ℋA0ℎ-ℎB⋅ihifA∈ℋA0ℎ-ℎB=T⁡ifA∈ℋA0ℎ+ℎifB∈ℋB0ℎ⋅ihifA∈ℋA0ℎ+ℎifB∈ℋB0ℎ−T⁡ifA∈ℋA0ℎ-ℎifB∈ℋB0ℎ⋅ihifA∈ℋA0ℎ-ℎifB∈ℋB0ℎ
30 oveq2 ⊢B=ifB∈ℋB0ℎ→i⋅ℎB=i⋅ℎifB∈ℋB0ℎ
31 30 oveq2d ⊢B=ifB∈ℋB0ℎ→ifA∈ℋA0ℎ+ℎi⋅ℎB=ifA∈ℋA0ℎ+ℎi⋅ℎifB∈ℋB0ℎ
32 31 fveq2d ⊢B=ifB∈ℋB0ℎ→T⁡ifA∈ℋA0ℎ+ℎi⋅ℎB=T⁡ifA∈ℋA0ℎ+ℎi⋅ℎifB∈ℋB0ℎ
33 32 31 oveq12d ⊢B=ifB∈ℋB0ℎ→T⁡ifA∈ℋA0ℎ+ℎi⋅ℎB⋅ihifA∈ℋA0ℎ+ℎi⋅ℎB=T⁡ifA∈ℋA0ℎ+ℎi⋅ℎifB∈ℋB0ℎ⋅ihifA∈ℋA0ℎ+ℎi⋅ℎifB∈ℋB0ℎ
34 30 oveq2d ⊢B=ifB∈ℋB0ℎ→ifA∈ℋA0ℎ-ℎi⋅ℎB=ifA∈ℋA0ℎ-ℎi⋅ℎifB∈ℋB0ℎ
35 34 fveq2d ⊢B=ifB∈ℋB0ℎ→T⁡ifA∈ℋA0ℎ-ℎi⋅ℎB=T⁡ifA∈ℋA0ℎ-ℎi⋅ℎifB∈ℋB0ℎ
36 35 34 oveq12d ⊢B=ifB∈ℋB0ℎ→T⁡ifA∈ℋA0ℎ-ℎi⋅ℎB⋅ihifA∈ℋA0ℎ-ℎi⋅ℎB=T⁡ifA∈ℋA0ℎ-ℎi⋅ℎifB∈ℋB0ℎ⋅ihifA∈ℋA0ℎ-ℎi⋅ℎifB∈ℋB0ℎ
37 33 36 oveq12d ⊢B=ifB∈ℋB0ℎ→T⁡ifA∈ℋA0ℎ+ℎi⋅ℎB⋅ihifA∈ℋA0ℎ+ℎi⋅ℎB−T⁡ifA∈ℋA0ℎ-ℎi⋅ℎB⋅ihifA∈ℋA0ℎ-ℎi⋅ℎB=T⁡ifA∈ℋA0ℎ+ℎi⋅ℎifB∈ℋB0ℎ⋅ihifA∈ℋA0ℎ+ℎi⋅ℎifB∈ℋB0ℎ−T⁡ifA∈ℋA0ℎ-ℎi⋅ℎifB∈ℋB0ℎ⋅ihifA∈ℋA0ℎ-ℎi⋅ℎifB∈ℋB0ℎ
38 37 oveq2d ⊢B=ifB∈ℋB0ℎ→i⁢T⁡ifA∈ℋA0ℎ+ℎi⋅ℎB⋅ihifA∈ℋA0ℎ+ℎi⋅ℎB−T⁡ifA∈ℋA0ℎ-ℎi⋅ℎB⋅ihifA∈ℋA0ℎ-ℎi⋅ℎB=i⁢T⁡ifA∈ℋA0ℎ+ℎi⋅ℎifB∈ℋB0ℎ⋅ihifA∈ℋA0ℎ+ℎi⋅ℎifB∈ℋB0ℎ−T⁡ifA∈ℋA0ℎ-ℎi⋅ℎifB∈ℋB0ℎ⋅ihifA∈ℋA0ℎ-ℎi⋅ℎifB∈ℋB0ℎ
39 29 38 oveq12d ⊢B=ifB∈ℋB0ℎ→T⁡ifA∈ℋA0ℎ+ℎB⋅ihifA∈ℋA0ℎ+ℎB-T⁡ifA∈ℋA0ℎ-ℎB⋅ihifA∈ℋA0ℎ-ℎB+i⁢T⁡ifA∈ℋA0ℎ+ℎi⋅ℎB⋅ihifA∈ℋA0ℎ+ℎi⋅ℎB−T⁡ifA∈ℋA0ℎ-ℎi⋅ℎB⋅ihifA∈ℋA0ℎ-ℎi⋅ℎB=T⁡ifA∈ℋA0ℎ+ℎifB∈ℋB0ℎ⋅ihifA∈ℋA0ℎ+ℎifB∈ℋB0ℎ-T⁡ifA∈ℋA0ℎ-ℎifB∈ℋB0ℎ⋅ihifA∈ℋA0ℎ-ℎifB∈ℋB0ℎ+i⁢T⁡ifA∈ℋA0ℎ+ℎi⋅ℎifB∈ℋB0ℎ⋅ihifA∈ℋA0ℎ+ℎi⋅ℎifB∈ℋB0ℎ−T⁡ifA∈ℋA0ℎ-ℎi⋅ℎifB∈ℋB0ℎ⋅ihifA∈ℋA0ℎ-ℎi⋅ℎifB∈ℋB0ℎ
40 39 oveq1d ⊢B=ifB∈ℋB0ℎ→T⁡ifA∈ℋA0ℎ+ℎB⋅ihifA∈ℋA0ℎ+ℎB-T⁡ifA∈ℋA0ℎ-ℎB⋅ihifA∈ℋA0ℎ-ℎB+i⁢T⁡ifA∈ℋA0ℎ+ℎi⋅ℎB⋅ihifA∈ℋA0ℎ+ℎi⋅ℎB−T⁡ifA∈ℋA0ℎ-ℎi⋅ℎB⋅ihifA∈ℋA0ℎ-ℎi⋅ℎB4=T⁡ifA∈ℋA0ℎ+ℎifB∈ℋB0ℎ⋅ihifA∈ℋA0ℎ+ℎifB∈ℋB0ℎ-T⁡ifA∈ℋA0ℎ-ℎifB∈ℋB0ℎ⋅ihifA∈ℋA0ℎ-ℎifB∈ℋB0ℎ+i⁢T⁡ifA∈ℋA0ℎ+ℎi⋅ℎifB∈ℋB0ℎ⋅ihifA∈ℋA0ℎ+ℎi⋅ℎifB∈ℋB0ℎ−T⁡ifA∈ℋA0ℎ-ℎi⋅ℎifB∈ℋB0ℎ⋅ihifA∈ℋA0ℎ-ℎi⋅ℎifB∈ℋB0ℎ4
41 22 40 eqeq12d ⊢B=ifB∈ℋB0ℎ→T⁡ifA∈ℋA0ℎ⋅ihB=T⁡ifA∈ℋA0ℎ+ℎB⋅ihifA∈ℋA0ℎ+ℎB-T⁡ifA∈ℋA0ℎ-ℎB⋅ihifA∈ℋA0ℎ-ℎB+i⁢T⁡ifA∈ℋA0ℎ+ℎi⋅ℎB⋅ihifA∈ℋA0ℎ+ℎi⋅ℎB−T⁡ifA∈ℋA0ℎ-ℎi⋅ℎB⋅ihifA∈ℋA0ℎ-ℎi⋅ℎB4↔T⁡ifA∈ℋA0ℎ⋅ihifB∈ℋB0ℎ=T⁡ifA∈ℋA0ℎ+ℎifB∈ℋB0ℎ⋅ihifA∈ℋA0ℎ+ℎifB∈ℋB0ℎ-T⁡ifA∈ℋA0ℎ-ℎifB∈ℋB0ℎ⋅ihifA∈ℋA0ℎ-ℎifB∈ℋB0ℎ+i⁢T⁡ifA∈ℋA0ℎ+ℎi⋅ℎifB∈ℋB0ℎ⋅ihifA∈ℋA0ℎ+ℎi⋅ℎifB∈ℋB0ℎ−T⁡ifA∈ℋA0ℎ-ℎi⋅ℎifB∈ℋB0ℎ⋅ihifA∈ℋA0ℎ-ℎi⋅ℎifB∈ℋB0ℎ4
42 ifhvhv0 ⊢ifA∈ℋA0ℎ∈ℋ
43 ifhvhv0 ⊢ifB∈ℋB0ℎ∈ℋ
44 1 42 43 lnopeq0lem1 ⊢T⁡ifA∈ℋA0ℎ⋅ihifB∈ℋB0ℎ=T⁡ifA∈ℋA0ℎ+ℎifB∈ℋB0ℎ⋅ihifA∈ℋA0ℎ+ℎifB∈ℋB0ℎ-T⁡ifA∈ℋA0ℎ-ℎifB∈ℋB0ℎ⋅ihifA∈ℋA0ℎ-ℎifB∈ℋB0ℎ+i⁢T⁡ifA∈ℋA0ℎ+ℎi⋅ℎifB∈ℋB0ℎ⋅ihifA∈ℋA0ℎ+ℎi⋅ℎifB∈ℋB0ℎ−T⁡ifA∈ℋA0ℎ-ℎi⋅ℎifB∈ℋB0ℎ⋅ihifA∈ℋA0ℎ-ℎi⋅ℎifB∈ℋB0ℎ4
45 21 41 44 dedth2h ⊢A∈ℋ∧B∈ℋ→T⁡A⋅ihB=T⁡A+ℎB⋅ihA+ℎB-T⁡A-ℎB⋅ihA-ℎB+i⁢T⁡A+ℎi⋅ℎB⋅ihA+ℎi⋅ℎB−T⁡A-ℎi⋅ℎB⋅ihA-ℎi⋅ℎB4