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\in {\mathbf{C}}_{\mathscr{H}}$$
	csmdsym.2	$$⊢B\in {\mathbf{C}}_{\mathscr{H}}$$
Assertion	csmdsymi	$$⊢\left(\forall c\in {\mathbf{C}}_{\mathscr{H}}\left(c{𝑀}_{\mathscr{H}}B\to B{𝑀}_{\mathscr{H}}^{*}c\right)\wedge A{𝑀}_{\mathscr{H}}B\right)\to B{𝑀}_{\mathscr{H}}A$$

Proof

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