Metamath Proof Explorer


Theorem mdexchi

Description: An exchange lemma for modular pairs. Lemma 1.6 of MaedaMaeda p. 2. (Contributed by NM, 22-Jun-2004) (New usage is discouraged.)

Ref Expression
Hypotheses mdexch.1 A C
mdexch.2 B C
mdexch.3 C C
Assertion mdexchi A 𝑀 B C 𝑀 A B C A B A C A 𝑀 B C A B = A B

Proof

Step Hyp Ref Expression
1 mdexch.1 A C
2 mdexch.2 B C
3 mdexch.3 C C
4 chjass C C A C x C C A x = C A x
5 3 1 4 mp3an12 x C C A x = C A x
6 3 1 chjcli C A C
7 chjcom x C C A C x C A = C A x
8 6 7 mpan2 x C x C A = C A x
9 chjcl A C x C A x C
10 1 9 mpan x C A x C
11 chjcom A x C C C A x C = C A x
12 10 3 11 sylancl x C A x C = C A x
13 5 8 12 3eqtr4d x C x C A = A x C
14 13 ineq1d x C x C A B = A x C B
15 inass A x C A B B = A x C A B B
16 incom A B B = B A B
17 1 2 chjcomi A B = B A
18 17 ineq2i B A B = B B A
19 2 1 chabs2i B B A = B
20 18 19 eqtri B A B = B
21 16 20 eqtri A B B = B
22 21 ineq2i A x C A B B = A x C B
23 15 22 eqtri A x C A B B = A x C B
24 14 23 eqtr4di x C x C A B = A x C A B B
25 24 ad2antrr x C x B C 𝑀 A B C A B A x C A B = A x C A B B
26 chlej2 x C B C A C x B A x A B
27 26 ex x C B C A C x B A x A B
28 2 1 27 mp3an23 x C x B A x A B
29 1 2 chjcli A B C
30 mdi C C A B C A x C C 𝑀 A B A x A B A x C A B = A x C A B
31 30 exp32 C C A B C A x C C 𝑀 A B A x A B A x C A B = A x C A B
32 3 29 31 mp3an12 A x C C 𝑀 A B A x A B A x C A B = A x C A B
33 10 32 syl x C C 𝑀 A B A x A B A x C A B = A x C A B
34 33 com23 x C A x A B C 𝑀 A B A x C A B = A x C A B
35 28 34 syld x C x B C 𝑀 A B A x C A B = A x C A B
36 35 imp31 x C x B C 𝑀 A B A x C A B = A x C A B
37 36 adantrr x C x B C 𝑀 A B C A B A A x C A B = A x C A B
38 3 29 chincli C A B C
39 chlej2 C A B C A C A x C C A B A A x C A B A x A
40 39 ex C A B C A C A x C C A B A A x C A B A x A
41 38 1 40 mp3an12 A x C C A B A A x C A B A x A
42 10 41 syl x C C A B A A x C A B A x A
43 42 imp x C C A B A A x C A B A x A
44 chjcom A x C A C A x A = A A x
45 10 1 44 sylancl x C A x A = A A x
46 1 chjidmi A A = A
47 46 oveq1i A A x = A x
48 chjass A C A C x C A A x = A A x
49 1 1 48 mp3an12 x C A A x = A A x
50 chjcom A C x C A x = x A
51 1 50 mpan x C A x = x A
52 47 49 51 3eqtr3a x C A A x = x A
53 45 52 eqtrd x C A x A = x A
54 53 adantr x C C A B A A x A = x A
55 43 54 sseqtrd x C C A B A A x C A B x A
56 55 ad2ant2rl x C x B C 𝑀 A B C A B A A x C A B x A
57 37 56 eqsstrd x C x B C 𝑀 A B C A B A A x C A B x A
58 57 ssrind x C x B C 𝑀 A B C A B A A x C A B B x A B
59 25 58 eqsstrd x C x B C 𝑀 A B C A B A x C A B x A B
60 59 adantrl x C x B A 𝑀 B C 𝑀 A B C A B A x C A B x A B
61 mdi A C B C x C A 𝑀 B x B x A B = x A B
62 61 exp32 A C B C x C A 𝑀 B x B x A B = x A B
63 1 2 62 mp3an12 x C A 𝑀 B x B x A B = x A B
64 63 com23 x C x B A 𝑀 B x A B = x A B
65 64 imp31 x C x B A 𝑀 B x A B = x A B
66 1 3 chub2i A C A
67 ssrin A C A A B C A B
68 66 67 ax-mp A B C A B
69 1 2 chincli A B C
70 6 2 chincli C A B C
71 chlej2 A B C C A B C x C A B C A B x A B x C A B
72 71 ex A B C C A B C x C A B C A B x A B x C A B
73 69 70 72 mp3an12 x C A B C A B x A B x C A B
74 68 73 mpi x C x A B x C A B
75 74 ad2antrr x C x B A 𝑀 B x A B x C A B
76 65 75 eqsstrd x C x B A 𝑀 B x A B x C A B
77 76 adantrr x C x B A 𝑀 B C 𝑀 A B C A B A x A B x C A B
78 60 77 sstrd x C x B A 𝑀 B C 𝑀 A B C A B A x C A B x C A B
79 78 exp31 x C x B A 𝑀 B C 𝑀 A B C A B A x C A B x C A B
80 79 com3r A 𝑀 B C 𝑀 A B C A B A x C x B x C A B x C A B
81 80 3impb A 𝑀 B C 𝑀 A B C A B A x C x B x C A B x C A B
82 81 ralrimiv A 𝑀 B C 𝑀 A B C A B A x C x B x C A B x C A B
83 mdbr2 C A C B C C A 𝑀 B x C x B x C A B x C A B
84 6 2 83 mp2an C A 𝑀 B x C x B x C A B x C A B
85 82 84 sylibr A 𝑀 B C 𝑀 A B C A B A C A 𝑀 B
86 3 1 chjcomi C A = A C
87 incom B A B = A B B
88 18 87 19 3eqtr3ri B = A B B
89 86 88 ineq12i C A B = A C A B B
90 inass A C A B B = A C A B B
91 1 2 chub1i A A B
92 mdi C C A B C A C C 𝑀 A B A A B A C A B = A C A B
93 92 exp32 C C A B C A C C 𝑀 A B A A B A C A B = A C A B
94 3 29 1 93 mp3an C 𝑀 A B A A B A C A B = A C A B
95 91 94 mpi C 𝑀 A B A C A B = A C A B
96 1 38 chjcomi A C A B = C A B A
97 38 1 chlejb1i C A B A C A B A = A
98 97 biimpi C A B A C A B A = A
99 96 98 syl5eq C A B A A C A B = A
100 95 99 sylan9eq C 𝑀 A B C A B A A C A B = A
101 100 ineq1d C 𝑀 A B C A B A A C A B B = A B
102 90 101 eqtr3id C 𝑀 A B C A B A A C A B B = A B
103 89 102 syl5eq C 𝑀 A B C A B A C A B = A B
104 103 3adant1 A 𝑀 B C 𝑀 A B C A B A C A B = A B
105 85 104 jca A 𝑀 B C 𝑀 A B C A B A C A 𝑀 B C A B = A B