Metamath Proof Explorer

Theorem eceqoveq

Description: Equality of equivalence relation in terms of an operation. (Contributed by NM, 15-Feb-1996) (Proof shortened by Mario Carneiro, 12-Aug-2015)

Ref Expression
Hypotheses eceqoveq.5 
|- .~ Er ( S X. S )
eceqoveq.7 
|- dom .+ = ( S X. S )
eceqoveq.8 
|- -. (/) e. S
eceqoveq.9 
|- ( ( x e. S /\ y e. S ) -> ( x .+ y ) e. S )
eceqoveq.10 
|- ( ( ( A e. S /\ B e. S ) /\ ( C e. S /\ D e. S ) ) -> ( <. A , B >. .~ <. C , D >. <-> ( A .+ D ) = ( B .+ C ) ) )
Assertion eceqoveq 
|- ( ( A e. S /\ C e. S ) -> ( [ <. A , B >. ] .~ = [ <. C , D >. ] .~ <-> ( A .+ D ) = ( B .+ C ) ) )

Proof

Step Hyp Ref Expression
1 eceqoveq.5 
 |-  .~ Er ( S X. S )
2 eceqoveq.7 
 |-  dom .+ = ( S X. S )
3 eceqoveq.8 
 |-  -. (/) e. S
4 eceqoveq.9 
 |-  ( ( x e. S /\ y e. S ) -> ( x .+ y ) e. S )
5 eceqoveq.10 
 |-  ( ( ( A e. S /\ B e. S ) /\ ( C e. S /\ D e. S ) ) -> ( <. A , B >. .~ <. C , D >. <-> ( A .+ D ) = ( B .+ C ) ) )
6 opelxpi 
 |-  ( ( A e. S /\ B e. S ) -> <. A , B >. e. ( S X. S ) )
7 6 ad2antrr 
 |-  ( ( ( ( A e. S /\ B e. S ) /\ C e. S ) /\ [ <. A , B >. ] .~ = [ <. C , D >. ] .~ ) -> <. A , B >. e. ( S X. S ) )
8 1 a1i 
 |-  ( ( ( ( A e. S /\ B e. S ) /\ C e. S ) /\ [ <. A , B >. ] .~ = [ <. C , D >. ] .~ ) -> .~ Er ( S X. S ) )
9 simpr 
 |-  ( ( ( ( A e. S /\ B e. S ) /\ C e. S ) /\ [ <. A , B >. ] .~ = [ <. C , D >. ] .~ ) -> [ <. A , B >. ] .~ = [ <. C , D >. ] .~ )
10 8 9 ereldm 
 |-  ( ( ( ( A e. S /\ B e. S ) /\ C e. S ) /\ [ <. A , B >. ] .~ = [ <. C , D >. ] .~ ) -> ( <. A , B >. e. ( S X. S ) <-> <. C , D >. e. ( S X. S ) ) )
11 7 10 mpbid 
 |-  ( ( ( ( A e. S /\ B e. S ) /\ C e. S ) /\ [ <. A , B >. ] .~ = [ <. C , D >. ] .~ ) -> <. C , D >. e. ( S X. S ) )
12 opelxp2 
 |-  ( <. C , D >. e. ( S X. S ) -> D e. S )
13 11 12 syl 
 |-  ( ( ( ( A e. S /\ B e. S ) /\ C e. S ) /\ [ <. A , B >. ] .~ = [ <. C , D >. ] .~ ) -> D e. S )
14 13 ex 
 |-  ( ( ( A e. S /\ B e. S ) /\ C e. S ) -> ( [ <. A , B >. ] .~ = [ <. C , D >. ] .~ -> D e. S ) )
15 4 caovcl 
 |-  ( ( B e. S /\ C e. S ) -> ( B .+ C ) e. S )
16 eleq1 
 |-  ( ( A .+ D ) = ( B .+ C ) -> ( ( A .+ D ) e. S <-> ( B .+ C ) e. S ) )
17 15 16 syl5ibr 
 |-  ( ( A .+ D ) = ( B .+ C ) -> ( ( B e. S /\ C e. S ) -> ( A .+ D ) e. S ) )
18 2 3 ndmovrcl 
 |-  ( ( A .+ D ) e. S -> ( A e. S /\ D e. S ) )
19 18 simprd 
 |-  ( ( A .+ D ) e. S -> D e. S )
20 17 19 syl6com 
 |-  ( ( B e. S /\ C e. S ) -> ( ( A .+ D ) = ( B .+ C ) -> D e. S ) )
21 20 adantll 
 |-  ( ( ( A e. S /\ B e. S ) /\ C e. S ) -> ( ( A .+ D ) = ( B .+ C ) -> D e. S ) )
22 1 a1i 
 |-  ( ( ( A e. S /\ B e. S ) /\ ( C e. S /\ D e. S ) ) -> .~ Er ( S X. S ) )
23 6 adantr 
 |-  ( ( ( A e. S /\ B e. S ) /\ ( C e. S /\ D e. S ) ) -> <. A , B >. e. ( S X. S ) )
24 22 23 erth 
 |-  ( ( ( A e. S /\ B e. S ) /\ ( C e. S /\ D e. S ) ) -> ( <. A , B >. .~ <. C , D >. <-> [ <. A , B >. ] .~ = [ <. C , D >. ] .~ ) )
25 24 5 bitr3d 
 |-  ( ( ( A e. S /\ B e. S ) /\ ( C e. S /\ D e. S ) ) -> ( [ <. A , B >. ] .~ = [ <. C , D >. ] .~ <-> ( A .+ D ) = ( B .+ C ) ) )
26 25 expr 
 |-  ( ( ( A e. S /\ B e. S ) /\ C e. S ) -> ( D e. S -> ( [ <. A , B >. ] .~ = [ <. C , D >. ] .~ <-> ( A .+ D ) = ( B .+ C ) ) ) )
27 14 21 26 pm5.21ndd 
 |-  ( ( ( A e. S /\ B e. S ) /\ C e. S ) -> ( [ <. A , B >. ] .~ = [ <. C , D >. ] .~ <-> ( A .+ D ) = ( B .+ C ) ) )
28 27 an32s 
 |-  ( ( ( A e. S /\ C e. S ) /\ B e. S ) -> ( [ <. A , B >. ] .~ = [ <. C , D >. ] .~ <-> ( A .+ D ) = ( B .+ C ) ) )
29 eqcom 
 |-  ( (/) = [ <. C , D >. ] .~ <-> [ <. C , D >. ] .~ = (/) )
30 erdm 
 |-  ( .~ Er ( S X. S ) -> dom .~ = ( S X. S ) )
31 1 30 ax-mp 
 |-  dom .~ = ( S X. S )
32 31 eleq2i 
 |-  ( <. C , D >. e. dom .~ <-> <. C , D >. e. ( S X. S ) )
33 ecdmn0 
 |-  ( <. C , D >. e. dom .~ <-> [ <. C , D >. ] .~ =/= (/) )
34 opelxp 
 |-  ( <. C , D >. e. ( S X. S ) <-> ( C e. S /\ D e. S ) )
35 32 33 34 3bitr3i 
 |-  ( [ <. C , D >. ] .~ =/= (/) <-> ( C e. S /\ D e. S ) )
36 35 simplbi2 
 |-  ( C e. S -> ( D e. S -> [ <. C , D >. ] .~ =/= (/) ) )
37 36 ad2antlr 
 |-  ( ( ( A e. S /\ C e. S ) /\ -. B e. S ) -> ( D e. S -> [ <. C , D >. ] .~ =/= (/) ) )
38 37 necon2bd 
 |-  ( ( ( A e. S /\ C e. S ) /\ -. B e. S ) -> ( [ <. C , D >. ] .~ = (/) -> -. D e. S ) )
39 simpr 
 |-  ( ( A e. S /\ D e. S ) -> D e. S )
40 2 ndmov 
 |-  ( -. ( A e. S /\ D e. S ) -> ( A .+ D ) = (/) )
41 39 40 nsyl5 
 |-  ( -. D e. S -> ( A .+ D ) = (/) )
42 38 41 syl6 
 |-  ( ( ( A e. S /\ C e. S ) /\ -. B e. S ) -> ( [ <. C , D >. ] .~ = (/) -> ( A .+ D ) = (/) ) )
43 eleq1 
 |-  ( ( A .+ D ) = (/) -> ( ( A .+ D ) e. S <-> (/) e. S ) )
44 3 43 mtbiri 
 |-  ( ( A .+ D ) = (/) -> -. ( A .+ D ) e. S )
45 35 simprbi 
 |-  ( [ <. C , D >. ] .~ =/= (/) -> D e. S )
46 4 caovcl 
 |-  ( ( A e. S /\ D e. S ) -> ( A .+ D ) e. S )
47 46 ex 
 |-  ( A e. S -> ( D e. S -> ( A .+ D ) e. S ) )
48 47 ad2antrr 
 |-  ( ( ( A e. S /\ C e. S ) /\ -. B e. S ) -> ( D e. S -> ( A .+ D ) e. S ) )
49 45 48 syl5 
 |-  ( ( ( A e. S /\ C e. S ) /\ -. B e. S ) -> ( [ <. C , D >. ] .~ =/= (/) -> ( A .+ D ) e. S ) )
50 49 necon1bd 
 |-  ( ( ( A e. S /\ C e. S ) /\ -. B e. S ) -> ( -. ( A .+ D ) e. S -> [ <. C , D >. ] .~ = (/) ) )
51 44 50 syl5 
 |-  ( ( ( A e. S /\ C e. S ) /\ -. B e. S ) -> ( ( A .+ D ) = (/) -> [ <. C , D >. ] .~ = (/) ) )
52 42 51 impbid 
 |-  ( ( ( A e. S /\ C e. S ) /\ -. B e. S ) -> ( [ <. C , D >. ] .~ = (/) <-> ( A .+ D ) = (/) ) )
53 29 52 bitrid 
 |-  ( ( ( A e. S /\ C e. S ) /\ -. B e. S ) -> ( (/) = [ <. C , D >. ] .~ <-> ( A .+ D ) = (/) ) )
54 31 eleq2i 
 |-  ( <. A , B >. e. dom .~ <-> <. A , B >. e. ( S X. S ) )
55 ecdmn0 
 |-  ( <. A , B >. e. dom .~ <-> [ <. A , B >. ] .~ =/= (/) )
56 opelxp 
 |-  ( <. A , B >. e. ( S X. S ) <-> ( A e. S /\ B e. S ) )
57 54 55 56 3bitr3i 
 |-  ( [ <. A , B >. ] .~ =/= (/) <-> ( A e. S /\ B e. S ) )
58 57 simprbi 
 |-  ( [ <. A , B >. ] .~ =/= (/) -> B e. S )
59 58 necon1bi 
 |-  ( -. B e. S -> [ <. A , B >. ] .~ = (/) )
60 59 adantl 
 |-  ( ( ( A e. S /\ C e. S ) /\ -. B e. S ) -> [ <. A , B >. ] .~ = (/) )
61 60 eqeq1d 
 |-  ( ( ( A e. S /\ C e. S ) /\ -. B e. S ) -> ( [ <. A , B >. ] .~ = [ <. C , D >. ] .~ <-> (/) = [ <. C , D >. ] .~ ) )
62 simpl 
 |-  ( ( B e. S /\ C e. S ) -> B e. S )
63 2 ndmov 
 |-  ( -. ( B e. S /\ C e. S ) -> ( B .+ C ) = (/) )
64 62 63 nsyl5 
 |-  ( -. B e. S -> ( B .+ C ) = (/) )
65 64 adantl 
 |-  ( ( ( A e. S /\ C e. S ) /\ -. B e. S ) -> ( B .+ C ) = (/) )
66 65 eqeq2d 
 |-  ( ( ( A e. S /\ C e. S ) /\ -. B e. S ) -> ( ( A .+ D ) = ( B .+ C ) <-> ( A .+ D ) = (/) ) )
67 53 61 66 3bitr4d 
 |-  ( ( ( A e. S /\ C e. S ) /\ -. B e. S ) -> ( [ <. A , B >. ] .~ = [ <. C , D >. ] .~ <-> ( A .+ D ) = ( B .+ C ) ) )
68 28 67 pm2.61dan 
 |-  ( ( A e. S /\ C e. S ) -> ( [ <. A , B >. ] .~ = [ <. C , D >. ] .~ <-> ( A .+ D ) = ( B .+ C ) ) )