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 
|- [ a <> b ] ( ( a e. CC /\ b e. CC /\ c e. CC ) -> ( ( a ^ 2 ) + ( b ^ 2 ) ) = ( c ^ 2 ) )

Proof

Step Hyp Ref Expression
1 eleq1w 
 |-  ( a = t -> ( a e. CC <-> t e. CC ) )
2 1 3anbi1d 
 |-  ( a = t -> ( ( a e. CC /\ b e. CC /\ c e. CC ) <-> ( t e. CC /\ b e. CC /\ c e. CC ) ) )
3 oveq1 
 |-  ( a = t -> ( a ^ 2 ) = ( t ^ 2 ) )
4 3 oveq1d 
 |-  ( a = t -> ( ( a ^ 2 ) + ( b ^ 2 ) ) = ( ( t ^ 2 ) + ( b ^ 2 ) ) )
5 4 eqeq1d 
 |-  ( a = t -> ( ( ( a ^ 2 ) + ( b ^ 2 ) ) = ( c ^ 2 ) <-> ( ( t ^ 2 ) + ( b ^ 2 ) ) = ( c ^ 2 ) ) )
6 2 5 imbi12d 
 |-  ( a = t -> ( ( ( a e. CC /\ b e. CC /\ c e. CC ) -> ( ( a ^ 2 ) + ( b ^ 2 ) ) = ( c ^ 2 ) ) <-> ( ( t e. CC /\ b e. CC /\ c e. CC ) -> ( ( t ^ 2 ) + ( b ^ 2 ) ) = ( c ^ 2 ) ) ) )
7 eleq1w 
 |-  ( b = a -> ( b e. CC <-> a e. CC ) )
8 7 3anbi2d 
 |-  ( b = a -> ( ( t e. CC /\ b e. CC /\ c e. CC ) <-> ( t e. CC /\ a e. CC /\ c e. CC ) ) )
9 oveq1 
 |-  ( b = a -> ( b ^ 2 ) = ( a ^ 2 ) )
10 9 oveq2d 
 |-  ( b = a -> ( ( t ^ 2 ) + ( b ^ 2 ) ) = ( ( t ^ 2 ) + ( a ^ 2 ) ) )
11 10 eqeq1d 
 |-  ( b = a -> ( ( ( t ^ 2 ) + ( b ^ 2 ) ) = ( c ^ 2 ) <-> ( ( t ^ 2 ) + ( a ^ 2 ) ) = ( c ^ 2 ) ) )
12 8 11 imbi12d 
 |-  ( b = a -> ( ( ( t e. CC /\ b e. CC /\ c e. CC ) -> ( ( t ^ 2 ) + ( b ^ 2 ) ) = ( c ^ 2 ) ) <-> ( ( t e. CC /\ a e. CC /\ c e. CC ) -> ( ( t ^ 2 ) + ( a ^ 2 ) ) = ( c ^ 2 ) ) ) )
13 eleq1w 
 |-  ( t = b -> ( t e. CC <-> b e. CC ) )
14 13 3anbi1d 
 |-  ( t = b -> ( ( t e. CC /\ a e. CC /\ c e. CC ) <-> ( b e. CC /\ a e. CC /\ c e. CC ) ) )
15 oveq1 
 |-  ( t = b -> ( t ^ 2 ) = ( b ^ 2 ) )
16 15 oveq1d 
 |-  ( t = b -> ( ( t ^ 2 ) + ( a ^ 2 ) ) = ( ( b ^ 2 ) + ( a ^ 2 ) ) )
17 16 eqeq1d 
 |-  ( t = b -> ( ( ( t ^ 2 ) + ( a ^ 2 ) ) = ( c ^ 2 ) <-> ( ( b ^ 2 ) + ( a ^ 2 ) ) = ( c ^ 2 ) ) )
18 14 17 imbi12d 
 |-  ( t = b -> ( ( ( t e. CC /\ a e. CC /\ c e. CC ) -> ( ( t ^ 2 ) + ( a ^ 2 ) ) = ( c ^ 2 ) ) <-> ( ( b e. CC /\ a e. CC /\ c e. CC ) -> ( ( b ^ 2 ) + ( a ^ 2 ) ) = ( c ^ 2 ) ) ) )
19 3ancoma 
 |-  ( ( b e. CC /\ a e. CC /\ c e. CC ) <-> ( a e. CC /\ b e. CC /\ c e. CC ) )
20 19 imbi1i 
 |-  ( ( ( b e. CC /\ a e. CC /\ c e. CC ) -> ( ( b ^ 2 ) + ( a ^ 2 ) ) = ( c ^ 2 ) ) <-> ( ( a e. CC /\ b e. CC /\ c e. CC ) -> ( ( b ^ 2 ) + ( a ^ 2 ) ) = ( c ^ 2 ) ) )
21 sqcl 
 |-  ( b e. CC -> ( b ^ 2 ) e. CC )
22 21 3ad2ant2 
 |-  ( ( a e. CC /\ b e. CC /\ c e. CC ) -> ( b ^ 2 ) e. CC )
23 sqcl 
 |-  ( a e. CC -> ( a ^ 2 ) e. CC )
24 23 3ad2ant1 
 |-  ( ( a e. CC /\ b e. CC /\ c e. CC ) -> ( a ^ 2 ) e. CC )
25 22 24 addcomd 
 |-  ( ( a e. CC /\ b e. CC /\ c e. CC ) -> ( ( b ^ 2 ) + ( a ^ 2 ) ) = ( ( a ^ 2 ) + ( b ^ 2 ) ) )
26 25 eqeq1d 
 |-  ( ( a e. CC /\ b e. CC /\ c e. CC ) -> ( ( ( b ^ 2 ) + ( a ^ 2 ) ) = ( c ^ 2 ) <-> ( ( a ^ 2 ) + ( b ^ 2 ) ) = ( c ^ 2 ) ) )
27 26 pm5.74i 
 |-  ( ( ( a e. CC /\ b e. CC /\ c e. CC ) -> ( ( b ^ 2 ) + ( a ^ 2 ) ) = ( c ^ 2 ) ) <-> ( ( a e. CC /\ b e. CC /\ c e. CC ) -> ( ( a ^ 2 ) + ( b ^ 2 ) ) = ( c ^ 2 ) ) )
28 20 27 bitri 
 |-  ( ( ( b e. CC /\ a e. CC /\ c e. CC ) -> ( ( b ^ 2 ) + ( a ^ 2 ) ) = ( c ^ 2 ) ) <-> ( ( a e. CC /\ b e. CC /\ c e. CC ) -> ( ( a ^ 2 ) + ( b ^ 2 ) ) = ( c ^ 2 ) ) )
29 18 28 bitrdi 
 |-  ( t = b -> ( ( ( t e. CC /\ a e. CC /\ c e. CC ) -> ( ( t ^ 2 ) + ( a ^ 2 ) ) = ( c ^ 2 ) ) <-> ( ( a e. CC /\ b e. CC /\ c e. CC ) -> ( ( a ^ 2 ) + ( b ^ 2 ) ) = ( c ^ 2 ) ) ) )
30 6 12 29 ichcircshi 
 |-  [ a <> b ] ( ( a e. CC /\ b e. CC /\ c e. CC ) -> ( ( a ^ 2 ) + ( b ^ 2 ) ) = ( c ^ 2 ) )