Metamath Proof Explorer


Theorem csmdsymi

Description: Cross-symmetry implies M-symmetry. Theorem 1.9.1 of MaedaMaeda p. 3. (Contributed by NM, 24-Dec-2006) (New usage is discouraged.)

Ref Expression
Hypotheses csmdsym.1 A C
csmdsym.2 B C
Assertion csmdsymi c C c 𝑀 B B 𝑀 * c A 𝑀 B B 𝑀 A

Proof

Step Hyp Ref Expression
1 csmdsym.1 A C
2 csmdsym.2 B C
3 incom A B = B A
4 3 sseq1i A B x B A x
5 4 biimpri B A x A B x
6 chjcom x C B C x B = B x
7 2 6 mpan2 x C x B = B x
8 7 ineq1d x C x B A = B x A
9 incom B x A = A B x
10 8 9 syl6eq x C x B A = A B x
11 10 ad2antlr c C c 𝑀 B B 𝑀 * c A 𝑀 B x C A B x x A x B A = A B x
12 2 a1i x C B C
13 id x C x C
14 1 a1i x C A C
15 12 13 14 3jca x C B C x C A C
16 15 ad2antlr c C c 𝑀 B B 𝑀 * c A 𝑀 B x C A B x x A B C x C A C
17 inss2 A B B
18 ssid B B
19 17 18 pm3.2i A B B B B
20 sseq2 x = if x C x 0 A B x A B if x C x 0
21 sseq1 x = if x C x 0 x A if x C x 0 A
22 20 21 anbi12d x = if x C x 0 A B x x A A B if x C x 0 if x C x 0 A
23 22 3anbi2d x = if x C x 0 A 𝑀 B A B x x A A B B B B A 𝑀 B A B if x C x 0 if x C x 0 A A B B B B
24 breq1 x = if x C x 0 x 𝑀 B if x C x 0 𝑀 B
25 23 24 imbi12d x = if x C x 0 A 𝑀 B A B x x A A B B B B x 𝑀 B A 𝑀 B A B if x C x 0 if x C x 0 A A B B B B if x C x 0 𝑀 B
26 h0elch 0 C
27 26 elimel if x C x 0 C
28 1 2 27 2 mdslmd4i A 𝑀 B A B if x C x 0 if x C x 0 A A B B B B if x C x 0 𝑀 B
29 25 28 dedth x C A 𝑀 B A B x x A A B B B B x 𝑀 B
30 29 com12 A 𝑀 B A B x x A A B B B B x C x 𝑀 B
31 19 30 mp3an3 A 𝑀 B A B x x A x C x 𝑀 B
32 31 imp A 𝑀 B A B x x A x C x 𝑀 B
33 32 an32s A 𝑀 B x C A B x x A x 𝑀 B
34 33 adantlll c C c 𝑀 B B 𝑀 * c A 𝑀 B x C A B x x A x 𝑀 B
35 breq1 c = x c 𝑀 B x 𝑀 B
36 breq2 c = x B 𝑀 * c B 𝑀 * x
37 35 36 imbi12d c = x c 𝑀 B B 𝑀 * c x 𝑀 B B 𝑀 * x
38 37 rspccva c C c 𝑀 B B 𝑀 * c x C x 𝑀 B B 𝑀 * x
39 38 adantlr c C c 𝑀 B B 𝑀 * c A 𝑀 B x C x 𝑀 B B 𝑀 * x
40 39 adantr c C c 𝑀 B B 𝑀 * c A 𝑀 B x C A B x x A x 𝑀 B B 𝑀 * x
41 34 40 mpd c C c 𝑀 B B 𝑀 * c A 𝑀 B x C A B x x A B 𝑀 * x
42 simprr c C c 𝑀 B B 𝑀 * c A 𝑀 B x C A B x x A x A
43 dmdi B C x C A C B 𝑀 * x x A A B x = A B x
44 16 41 42 43 syl12anc c C c 𝑀 B B 𝑀 * c A 𝑀 B x C A B x x A A B x = A B x
45 1 2 chincli A B C
46 chjcom A B C x C A B x = x A B
47 45 46 mpan x C A B x = x A B
48 3 oveq2i x A B = x B A
49 47 48 syl6eq x C A B x = x B A
50 49 ad2antlr c C c 𝑀 B B 𝑀 * c A 𝑀 B x C A B x x A A B x = x B A
51 11 44 50 3eqtr2d c C c 𝑀 B B 𝑀 * c A 𝑀 B x C A B x x A x B A = x B A
52 51 ex c C c 𝑀 B B 𝑀 * c A 𝑀 B x C A B x x A x B A = x B A
53 5 52 sylani c C c 𝑀 B B 𝑀 * c A 𝑀 B x C B A x x A x B A = x B A
54 53 ralrimiva c C c 𝑀 B B 𝑀 * c A 𝑀 B x C B A x x A x B A = x B A
55 2 1 mdsl2bi B 𝑀 A x C B A x x A x B A = x B A
56 54 55 sylibr c C c 𝑀 B B 𝑀 * c A 𝑀 B B 𝑀 A