Metamath Proof Explorer

Theorem ichexmpl2

Description: Example for interchangeable setvar variables in an arithmetic expression. (Contributed by AV, 31-Jul-2023)

Ref Expression
Assertion ichexmpl2 [ 𝑎 ⇄ 𝑏 ] ( ( 𝑎 ∈ ℂ ∧ 𝑏 ∈ ℂ ∧ 𝑐 ∈ ℂ ) → ( ( 𝑎 ↑ 2 ) + ( 𝑏 ↑ 2 ) ) = ( 𝑐 ↑ 2 ) )

Proof

Step Hyp Ref Expression
1 eleq1w ⊢ ( 𝑎 = 𝑡 → ( 𝑎 ∈ ℂ ↔ 𝑡 ∈ ℂ ) )
2 1 3anbi1d ⊢ ( 𝑎 = 𝑡 → ( ( 𝑎 ∈ ℂ ∧ 𝑏 ∈ ℂ ∧ 𝑐 ∈ ℂ ) ↔ ( 𝑡 ∈ ℂ ∧ 𝑏 ∈ ℂ ∧ 𝑐 ∈ ℂ ) ) )
3 oveq1 ⊢ ( 𝑎 = 𝑡 → ( 𝑎 ↑ 2 ) = ( 𝑡 ↑ 2 ) )
4 3 oveq1d ⊢ ( 𝑎 = 𝑡 → ( ( 𝑎 ↑ 2 ) + ( 𝑏 ↑ 2 ) ) = ( ( 𝑡 ↑ 2 ) + ( 𝑏 ↑ 2 ) ) )
5 4 eqeq1d ⊢ ( 𝑎 = 𝑡 → ( ( ( 𝑎 ↑ 2 ) + ( 𝑏 ↑ 2 ) ) = ( 𝑐 ↑ 2 ) ↔ ( ( 𝑡 ↑ 2 ) + ( 𝑏 ↑ 2 ) ) = ( 𝑐 ↑ 2 ) ) )
6 2 5 imbi12d ⊢ ( 𝑎 = 𝑡 → ( ( ( 𝑎 ∈ ℂ ∧ 𝑏 ∈ ℂ ∧ 𝑐 ∈ ℂ ) → ( ( 𝑎 ↑ 2 ) + ( 𝑏 ↑ 2 ) ) = ( 𝑐 ↑ 2 ) ) ↔ ( ( 𝑡 ∈ ℂ ∧ 𝑏 ∈ ℂ ∧ 𝑐 ∈ ℂ ) → ( ( 𝑡 ↑ 2 ) + ( 𝑏 ↑ 2 ) ) = ( 𝑐 ↑ 2 ) ) ) )
7 eleq1w ⊢ ( 𝑏 = 𝑎 → ( 𝑏 ∈ ℂ ↔ 𝑎 ∈ ℂ ) )
8 7 3anbi2d ⊢ ( 𝑏 = 𝑎 → ( ( 𝑡 ∈ ℂ ∧ 𝑏 ∈ ℂ ∧ 𝑐 ∈ ℂ ) ↔ ( 𝑡 ∈ ℂ ∧ 𝑎 ∈ ℂ ∧ 𝑐 ∈ ℂ ) ) )
9 oveq1 ⊢ ( 𝑏 = 𝑎 → ( 𝑏 ↑ 2 ) = ( 𝑎 ↑ 2 ) )
10 9 oveq2d ⊢ ( 𝑏 = 𝑎 → ( ( 𝑡 ↑ 2 ) + ( 𝑏 ↑ 2 ) ) = ( ( 𝑡 ↑ 2 ) + ( 𝑎 ↑ 2 ) ) )
11 10 eqeq1d ⊢ ( 𝑏 = 𝑎 → ( ( ( 𝑡 ↑ 2 ) + ( 𝑏 ↑ 2 ) ) = ( 𝑐 ↑ 2 ) ↔ ( ( 𝑡 ↑ 2 ) + ( 𝑎 ↑ 2 ) ) = ( 𝑐 ↑ 2 ) ) )
12 8 11 imbi12d ⊢ ( 𝑏 = 𝑎 → ( ( ( 𝑡 ∈ ℂ ∧ 𝑏 ∈ ℂ ∧ 𝑐 ∈ ℂ ) → ( ( 𝑡 ↑ 2 ) + ( 𝑏 ↑ 2 ) ) = ( 𝑐 ↑ 2 ) ) ↔ ( ( 𝑡 ∈ ℂ ∧ 𝑎 ∈ ℂ ∧ 𝑐 ∈ ℂ ) → ( ( 𝑡 ↑ 2 ) + ( 𝑎 ↑ 2 ) ) = ( 𝑐 ↑ 2 ) ) ) )
13 eleq1w ⊢ ( 𝑡 = 𝑏 → ( 𝑡 ∈ ℂ ↔ 𝑏 ∈ ℂ ) )
14 13 3anbi1d ⊢ ( 𝑡 = 𝑏 → ( ( 𝑡 ∈ ℂ ∧ 𝑎 ∈ ℂ ∧ 𝑐 ∈ ℂ ) ↔ ( 𝑏 ∈ ℂ ∧ 𝑎 ∈ ℂ ∧ 𝑐 ∈ ℂ ) ) )
15 oveq1 ⊢ ( 𝑡 = 𝑏 → ( 𝑡 ↑ 2 ) = ( 𝑏 ↑ 2 ) )
16 15 oveq1d ⊢ ( 𝑡 = 𝑏 → ( ( 𝑡 ↑ 2 ) + ( 𝑎 ↑ 2 ) ) = ( ( 𝑏 ↑ 2 ) + ( 𝑎 ↑ 2 ) ) )
17 16 eqeq1d ⊢ ( 𝑡 = 𝑏 → ( ( ( 𝑡 ↑ 2 ) + ( 𝑎 ↑ 2 ) ) = ( 𝑐 ↑ 2 ) ↔ ( ( 𝑏 ↑ 2 ) + ( 𝑎 ↑ 2 ) ) = ( 𝑐 ↑ 2 ) ) )
18 14 17 imbi12d ⊢ ( 𝑡 = 𝑏 → ( ( ( 𝑡 ∈ ℂ ∧ 𝑎 ∈ ℂ ∧ 𝑐 ∈ ℂ ) → ( ( 𝑡 ↑ 2 ) + ( 𝑎 ↑ 2 ) ) = ( 𝑐 ↑ 2 ) ) ↔ ( ( 𝑏 ∈ ℂ ∧ 𝑎 ∈ ℂ ∧ 𝑐 ∈ ℂ ) → ( ( 𝑏 ↑ 2 ) + ( 𝑎 ↑ 2 ) ) = ( 𝑐 ↑ 2 ) ) ) )
19 3ancoma ⊢ ( ( 𝑏 ∈ ℂ ∧ 𝑎 ∈ ℂ ∧ 𝑐 ∈ ℂ ) ↔ ( 𝑎 ∈ ℂ ∧ 𝑏 ∈ ℂ ∧ 𝑐 ∈ ℂ ) )
20 19 imbi1i ⊢ ( ( ( 𝑏 ∈ ℂ ∧ 𝑎 ∈ ℂ ∧ 𝑐 ∈ ℂ ) → ( ( 𝑏 ↑ 2 ) + ( 𝑎 ↑ 2 ) ) = ( 𝑐 ↑ 2 ) ) ↔ ( ( 𝑎 ∈ ℂ ∧ 𝑏 ∈ ℂ ∧ 𝑐 ∈ ℂ ) → ( ( 𝑏 ↑ 2 ) + ( 𝑎 ↑ 2 ) ) = ( 𝑐 ↑ 2 ) ) )
21 sqcl ⊢ ( 𝑏 ∈ ℂ → ( 𝑏 ↑ 2 ) ∈ ℂ )
22 21 3ad2ant2 ⊢ ( ( 𝑎 ∈ ℂ ∧ 𝑏 ∈ ℂ ∧ 𝑐 ∈ ℂ ) → ( 𝑏 ↑ 2 ) ∈ ℂ )
23 sqcl ⊢ ( 𝑎 ∈ ℂ → ( 𝑎 ↑ 2 ) ∈ ℂ )
24 23 3ad2ant1 ⊢ ( ( 𝑎 ∈ ℂ ∧ 𝑏 ∈ ℂ ∧ 𝑐 ∈ ℂ ) → ( 𝑎 ↑ 2 ) ∈ ℂ )
25 22 24 addcomd ⊢ ( ( 𝑎 ∈ ℂ ∧ 𝑏 ∈ ℂ ∧ 𝑐 ∈ ℂ ) → ( ( 𝑏 ↑ 2 ) + ( 𝑎 ↑ 2 ) ) = ( ( 𝑎 ↑ 2 ) + ( 𝑏 ↑ 2 ) ) )
26 25 eqeq1d ⊢ ( ( 𝑎 ∈ ℂ ∧ 𝑏 ∈ ℂ ∧ 𝑐 ∈ ℂ ) → ( ( ( 𝑏 ↑ 2 ) + ( 𝑎 ↑ 2 ) ) = ( 𝑐 ↑ 2 ) ↔ ( ( 𝑎 ↑ 2 ) + ( 𝑏 ↑ 2 ) ) = ( 𝑐 ↑ 2 ) ) )
27 26 pm5.74i ⊢ ( ( ( 𝑎 ∈ ℂ ∧ 𝑏 ∈ ℂ ∧ 𝑐 ∈ ℂ ) → ( ( 𝑏 ↑ 2 ) + ( 𝑎 ↑ 2 ) ) = ( 𝑐 ↑ 2 ) ) ↔ ( ( 𝑎 ∈ ℂ ∧ 𝑏 ∈ ℂ ∧ 𝑐 ∈ ℂ ) → ( ( 𝑎 ↑ 2 ) + ( 𝑏 ↑ 2 ) ) = ( 𝑐 ↑ 2 ) ) )
28 20 27 bitri ⊢ ( ( ( 𝑏 ∈ ℂ ∧ 𝑎 ∈ ℂ ∧ 𝑐 ∈ ℂ ) → ( ( 𝑏 ↑ 2 ) + ( 𝑎 ↑ 2 ) ) = ( 𝑐 ↑ 2 ) ) ↔ ( ( 𝑎 ∈ ℂ ∧ 𝑏 ∈ ℂ ∧ 𝑐 ∈ ℂ ) → ( ( 𝑎 ↑ 2 ) + ( 𝑏 ↑ 2 ) ) = ( 𝑐 ↑ 2 ) ) )
29 18 28 bitrdi ⊢ ( 𝑡 = 𝑏 → ( ( ( 𝑡 ∈ ℂ ∧ 𝑎 ∈ ℂ ∧ 𝑐 ∈ ℂ ) → ( ( 𝑡 ↑ 2 ) + ( 𝑎 ↑ 2 ) ) = ( 𝑐 ↑ 2 ) ) ↔ ( ( 𝑎 ∈ ℂ ∧ 𝑏 ∈ ℂ ∧ 𝑐 ∈ ℂ ) → ( ( 𝑎 ↑ 2 ) + ( 𝑏 ↑ 2 ) ) = ( 𝑐 ↑ 2 ) ) ) )
30 6 12 29 ichcircshi ⊢ [ 𝑎 ⇄ 𝑏 ] ( ( 𝑎 ∈ ℂ ∧ 𝑏 ∈ ℂ ∧ 𝑐 ∈ ℂ ) → ( ( 𝑎 ↑ 2 ) + ( 𝑏 ↑ 2 ) ) = ( 𝑐 ↑ 2 ) )