Theorem csmdsym 10256

Description: Cross-symmetry implies M-symmetry. Theorem 1.9.1 of [MaedaMaeda] p. 3.

Hypotheses

Ref	Expression
csmdsym.1	|- A e. CH
csmdsym.2	|- B e. CH

Assertion

Ref	Expression
csmdsym	|- ((A.c e. CH (c MH B -> B MH* c) /\ A MH B) -> B MH A)

Distinct variable group:   B,c

Proof of Theorem csmdsym

Step	Hyp	Ref	Expression
1		csmdsym.2	. . . . . . . . . 10 |- B e. CH
2		chjcomt 9424	. . . . . . . . . 10 |- ((x e. CH /\ B e. CH) -> (x vH B) = (B vH x))
3	1, 2	mpan2 698	. . . . . . . . 9 |- (x e. CH -> (x vH B) = (B vH x))
4	3	ineq1d 2219	. . . . . . . 8 |- (x e. CH -> ((x vH B) i^i A) = ((B vH x) i^i A))
5		incom 2211	. . . . . . . 8 |- ((B vH x) i^i A) = (A i^i (B vH x))
6	4, 5	syl6eq 1526	. . . . . . 7 |- (x e. CH -> ((x vH B) i^i A) = (A i^i (B vH x)))
7	6	ad2antlr 407	. . . . . 6 |- ((((A.c e. CH (c MH B -> B MH* c) /\ A MH B) /\ x e. CH) /\ ((A i^i B) (_ x /\ x (_ A)) -> ((x vH B) i^i A) = (A i^i (B vH x)))
8		dmdit 10224	. . . . . . 7 |- (((B e. CH /\ x e. CH /\ A e. CH) /\ (B MH* x /\ x (_ A)) -> ((A i^i B) vH x) = (A i^i (B vH x)))
9	1	a1i 8	. . . . . . . . 9 |- (x e. CH -> B e. CH)
10		id 59	. . . . . . . . 9 |- (x e. CH -> x e. CH)
11		csmdsym.1	. . . . . . . . . 10 |- A e. CH
12	11	a1i 8	. . . . . . . . 9 |- (x e. CH -> A e. CH)
13	9, 10, 12	3jca 821	. . . . . . . 8 |- (x e. CH -> (B e. CH /\ x e. CH /\ A e. CH))
14	13	ad2antlr 407	. . . . . . 7 |- ((((A.c e. CH (c MH B -> B MH* c) /\ A MH B) /\ x e. CH) /\ ((A i^i B) (_ x /\ x (_ A)) -> (B e. CH /\ x e. CH /\ A e. CH))
15		inss2 2234	. . . . . . . . . . . . . 14 |- (A i^i B) (_ B
16		ssid 2083	. . . . . . . . . . . . . 14 |- B (_ B
17	15, 16	pm3.2i 285	. . . . . . . . . . . . 13 |- ((A i^i B) (_ B /\ B (_ B)
18		sseq2 2086	. . . . . . . . . . . . . . . . . 18 |- (x = if(x e. CH, x, 0H) -> ((A i^i B) (_ x <-> (A i^i B) (_ if(x e. CH, x, 0H)))
19		sseq1 2085	. . . . . . . . . . . . . . . . . 18 |- (x = if(x e. CH, x, 0H) -> (x (_ A <-> if(x e. CH, x, 0H) (_ A))
20	18, 19	anbi12d 630	. . . . . . . . . . . . . . . . 17 |- (x = if(x e. CH, x, 0H) -> (((A i^i B) (_ x /\ x (_ A) <-> ((A i^i B) (_ if(x e. CH, x, 0H) /\ if(x e. CH, x, 0H) (_ A)))
21	20	3anbi2d 900	. . . . . . . . . . . . . . . 16 |- (x = if(x e. CH, x, 0H) -> ((A MH B /\ ((A i^i B) (_ x /\ x (_ A) /\ ((A i^i B) (_ B /\ B (_ B)) <-> (A MH B /\ ((A i^i B) (_ if(x e. CH, x, 0H) /\ if(x e. CH, x, 0H) (_ A) /\ ((A i^i B) (_ B /\ B (_ B))))
22		breq1 2627	. . . . . . . . . . . . . . . 16 |- (x = if(x e. CH, x, 0H) -> (x MH B <-> if(x e. CH, x, 0H) MH B))
23	21, 22	imbi12d 628	. . . . . . . . . . . . . . 15 |- (x = if(x e. CH, x, 0H) -> (((A MH B /\ ((A i^i B) (_ x /\ x (_ A) /\ ((A i^i B) (_ B /\ B (_ B)) -> x MH B) <-> ((A MH B /\ ((A i^i B) (_ if(x e. CH, x, 0H) /\ if(x e. CH, x, 0H) (_ A) /\ ((A i^i B) (_ B /\ B (_ B)) -> if(x e. CH, x, 0H) MH B)))
24		h0elch 9122	. . . . . . . . . . . . . . . . 17 |- 0H e. CH
25	24	elimel 2398	. . . . . . . . . . . . . . . 16 |- if(x e. CH, x, 0H) e. CH
26	11, 1, 25, 1	mdslmd4 10255	. . . . . . . . . . . . . . 15 |- ((A MH B /\ ((A i^i B) (_ if(x e. CH, x, 0H) /\ if(x e. CH, x, 0H) (_ A) /\ ((A i^i B) (_ B /\ B (_ B)) -> if(x e. CH, x, 0H) MH B)
27	23, 26	dedth 2387	. . . . . . . . . . . . . 14 |- (x e. CH -> ((A MH B /\ ((A i^i B) (_ x /\ x (_ A) /\ ((A i^i B) (_ B /\ B (_ B)) -> x MH B))
28	27	com12 11	. . . . . . . . . . . . 13 |- ((A MH B /\ ((A i^i B) (_ x /\ x (_ A) /\ ((A i^i B) (_ B /\ B (_ B)) -> (x e. CH -> x MH B))
29	17, 28	mp3an3 907	. . . . . . . . . . . 12 |- ((A MH B /\ ((A i^i B) (_ x /\ x (_ A)) -> (x e. CH -> x MH B))
30	29	imp 350	. . . . . . . . . . 11 |- (((A MH B /\ ((A i^i B) (_ x /\ x (_ A)) /\ x e. CH) -> x MH B)
31	30	an1rs 491	. . . . . . . . . 10 |- (((A MH B /\ x e. CH) /\ ((A i^i B) (_ x /\ x (_ A)) -> x MH B)
32	31	adantlll 398	. . . . . . . . 9 |- ((((A.c e. CH (c MH B -> B MH* c) /\ A MH B) /\ x e. CH) /\ ((A i^i B) (_ x /\ x (_ A)) -> x MH B)
33		breq1 2627	. . . . . . . . . . . . 13 |- (c = x -> (c MH B <-> x MH B))
34		breq2 2628	. . . . . . . . . . . . 13 |- (c = x -> (B MH* c <-> B MH* x))
35	33, 34	imbi12d 628	. . . . . . . . . . . 12 |- (c = x -> ((c MH B -> B MH* c) <-> (x MH B -> B MH* x)))
36	35	rcla4cva 1879	. . . . . . . . . . 11 |- ((A.c e. CH (c MH B -> B MH* c) /\ x e. CH) -> (x MH B -> B MH* x))
37	36	adantlr 395	. . . . . . . . . 10 |- (((A.c e. CH (c MH B -> B MH* c) /\ A MH B) /\ x e. CH) -> (x MH B -> B MH* x))
38	37	adantr 391	. . . . . . . . 9 |- ((((A.c e. CH (c MH B -> B MH* c) /\ A MH B) /\ x e. CH) /\ ((A i^i B) (_ x /\ x (_ A)) -> (x MH B -> B MH* x))
39	32, 38	mpd 26	. . . . . . . 8 |- ((((A.c e. CH (c MH B -> B MH* c) /\ A MH B) /\ x e. CH) /\ ((A i^i B) (_ x /\ x (_ A)) -> B MH* x)
40		simprr 417	. . . . . . . 8 |- ((((A.c e. CH (c MH B -> B MH* c) /\ A MH B) /\ x e. CH) /\ ((A i^i B) (_ x /\ x (_ A)) -> x (_ A)
41	39, 40	jca 288	. . . . . . 7 |- ((((A.c e. CH (c MH B -> B MH* c) /\ A MH B) /\ x e. CH) /\ ((A i^i B) (_ x /\ x (_ A)) -> (B MH* x /\ x (_ A))
42	8, 14, 41	sylanc 473	. . . . . 6 |- ((((A.c e. CH (c MH B -> B MH* c) /\ A MH B) /\ x e. CH) /\ ((A i^i B) (_ x /\ x (_ A)) -> ((A i^i B) vH x) = (A i^i (B vH x)))
43	11, 1	chincl 9378	. . . . . . . . 9 |- (A i^i B) e. CH
44		chjcomt 9424	. . . . . . . . 9 |- (((A i^i B) e. CH /\ x e. CH) -> ((A i^i B) vH x) = (x vH (A i^i B)))
45	43, 44	mpan 697	. . . . . . . 8 |- (x e. CH -> ((A i^i B) vH x) = (x vH (A i^i B)))
46		incom 2211	. . . . . . . . 9 |- (A i^i B) = (B i^i A)
47	46	opreq2i 3978	. . . . . . . 8 |- (x vH (A i^i B)) = (x vH (B i^i A))
48	45, 47	syl6eq 1526	. . . . . . 7 |- (x e. CH -> ((A i^i B) vH x) = (x vH (B i^i A)))
49	48	ad2antlr 407	. . . . . 6 |- ((((A.c e. CH (c MH B -> B MH* c) /\ A MH B) /\ x e. CH) /\ ((A i^i B) (_ x /\ x (_ A)) -> ((A i^i B) vH x) = (x vH (B i^i A)))
50	7, 42, 49	3eqtr2d 1516	. . . . 5 |- ((((A.c e. CH (c MH B -> B MH* c) /\ A MH B) /\ x e. CH) /\ ((A i^i B) (_ x /\ x (_ A)) -> ((x vH B) i^i A) = (x vH (B i^i A)))
51	50	ex 373	. . . 4 |- (((A.c e. CH (c MH B -> B MH* c) /\ A MH B) /\ x e. CH) -> (((A i^i B) (_ x /\ x (_ A) -> ((x vH B) i^i A) = (x vH (B i^i A))))
52	46	sseq1i 2088	. . . . 5 |- ((A i^i B) (_ x <-> (B i^i A) (_ x)
53	52	biimpr 152	. . . 4 |- ((B i^i A) (_ x -> (A i^i B) (_ x)
54	51, 53	sylani 466	. . 3 |- (((A.c e. CH (c MH B -> B MH* c) /\ A MH B) /\ x e. CH) -> (((B i^i A) (_ x /\ x (_ A) -> ((x vH B) i^i A) = (x vH (B i^i A))))
55	54	r19.21aiva 1717	. 2 |- ((A.c e. CH (c MH B -> B MH* c) /\ A MH B) -> A.x e. CH (((B i^i A) (_ x /\ x (_ A) -> ((x vH B) i^i A) = (x vH (B i^i A))))
56	1, 11	mdsl2b 10245	. 2