Metamath Proof Explorer

Theorem sigarls

Description: Signed area is linear by the second argument. (Contributed by Saveliy Skresanov, 19-Sep-2017)

Ref Expression
Hypothesis sigar ⊢G=x∈ℂ,y∈ℂ⟼ℑ⁡x‾⁢y
Assertion sigarls ⊢A∈ℂ∧B∈ℂ∧C∈ℝ→AGB⁢C=AGB⁢C

Proof

Step Hyp Ref Expression
1 sigar ⊢G=x∈ℂ,y∈ℂ⟼ℑ⁡x‾⁢y
2 simp1 ⊢A∈ℂ∧B∈ℂ∧C∈ℝ→A∈ℂ
3 2 cjcld ⊢A∈ℂ∧B∈ℂ∧C∈ℝ→A‾∈ℂ
4 simp2 ⊢A∈ℂ∧B∈ℂ∧C∈ℝ→B∈ℂ
5 simpr ⊢B∈ℂ∧C∈ℝ→C∈ℝ
6 5 recnd ⊢B∈ℂ∧C∈ℝ→C∈ℂ
7 6 3adant1 ⊢A∈ℂ∧B∈ℂ∧C∈ℝ→C∈ℂ
8 3 4 7 mulassd ⊢A∈ℂ∧B∈ℂ∧C∈ℝ→A‾⁢B⁢C=A‾⁢B⁢C
9 8 fveq2d ⊢A∈ℂ∧B∈ℂ∧C∈ℝ→ℑ⁡A‾⁢B⁢C=ℑ⁡A‾⁢B⁢C
10 simp3 ⊢A∈ℂ∧B∈ℂ∧C∈ℝ→C∈ℝ
11 3 4 mulcld ⊢A∈ℂ∧B∈ℂ∧C∈ℝ→A‾⁢B∈ℂ
12 10 11 immul2d ⊢A∈ℂ∧B∈ℂ∧C∈ℝ→ℑ⁡C⁢A‾⁢B=C⁢ℑ⁡A‾⁢B
13 11 7 mulcomd ⊢A∈ℂ∧B∈ℂ∧C∈ℝ→A‾⁢B⁢C=C⁢A‾⁢B
14 13 fveq2d ⊢A∈ℂ∧B∈ℂ∧C∈ℝ→ℑ⁡A‾⁢B⁢C=ℑ⁡C⁢A‾⁢B
15 imcl ⊢A‾⁢B∈ℂ→ℑ⁡A‾⁢B∈ℝ
16 15 recnd ⊢A‾⁢B∈ℂ→ℑ⁡A‾⁢B∈ℂ
17 11 16 syl ⊢A∈ℂ∧B∈ℂ∧C∈ℝ→ℑ⁡A‾⁢B∈ℂ
18 17 7 mulcomd ⊢A∈ℂ∧B∈ℂ∧C∈ℝ→ℑ⁡A‾⁢B⁢C=C⁢ℑ⁡A‾⁢B
19 12 14 18 3eqtr4d ⊢A∈ℂ∧B∈ℂ∧C∈ℝ→ℑ⁡A‾⁢B⁢C=ℑ⁡A‾⁢B⁢C
20 9 19 eqtr3d ⊢A∈ℂ∧B∈ℂ∧C∈ℝ→ℑ⁡A‾⁢B⁢C=ℑ⁡A‾⁢B⁢C
21 simpl ⊢B∈ℂ∧C∈ℝ→B∈ℂ
22 21 6 mulcld ⊢B∈ℂ∧C∈ℝ→B⁢C∈ℂ
23 22 3adant1 ⊢A∈ℂ∧B∈ℂ∧C∈ℝ→B⁢C∈ℂ
24 1 sigarval ⊢A∈ℂ∧B⁢C∈ℂ→AGB⁢C=ℑ⁡A‾⁢B⁢C
25 2 23 24 syl2anc ⊢A∈ℂ∧B∈ℂ∧C∈ℝ→AGB⁢C=ℑ⁡A‾⁢B⁢C
26 1 sigarval ⊢A∈ℂ∧B∈ℂ→AGB=ℑ⁡A‾⁢B
27 26 3adant3 ⊢A∈ℂ∧B∈ℂ∧C∈ℝ→AGB=ℑ⁡A‾⁢B
28 27 oveq1d ⊢A∈ℂ∧B∈ℂ∧C∈ℝ→AGB⁢C=ℑ⁡A‾⁢B⁢C
29 20 25 28 3eqtr4d ⊢A∈ℂ∧B∈ℂ∧C∈ℝ→AGB⁢C=AGB⁢C