Theorem golem2

Description: Lemma for Godowski's equation. (Contributed by NM, 13-Nov-1999) (New usage is discouraged.)

	Ref	Expression
Hypotheses	golem1.1	$$⊢A\in {\mathbf{C}}_{\mathscr{H}}$$
	golem1.2	$$⊢B\in {\mathbf{C}}_{\mathscr{H}}$$
	golem1.3	$$⊢C\in {\mathbf{C}}_{\mathscr{H}}$$
	golem1.4	$$⊢F=\perp \left(A\right){\vee }_{\mathscr{H}}\left(A\cap B\right)$$
	golem1.5	$$⊢G=\perp \left(B\right){\vee }_{\mathscr{H}}\left(B\cap C\right)$$
	golem1.6	$$⊢H=\perp \left(C\right){\vee }_{\mathscr{H}}\left(C\cap A\right)$$
	golem1.7	$$⊢D=\perp \left(B\right){\vee }_{\mathscr{H}}\left(B\cap A\right)$$
	golem1.8	$$⊢R=\perp \left(C\right){\vee }_{\mathscr{H}}\left(C\cap B\right)$$
	golem1.9	$$⊢S=\perp \left(A\right){\vee }_{\mathscr{H}}\left(A\cap C\right)$$
Assertion	golem2	$$⊢f\in \mathrm{States}\to \left(f\left(\left(F\cap G\right)\cap H\right)=1\to f\left(D\right)=1\right)$$

Proof

Step	Hyp	Ref	Expression
1		golem1.1	$$⊢A\in {\mathbf{C}}_{\mathscr{H}}$$
2		golem1.2	$$⊢B\in {\mathbf{C}}_{\mathscr{H}}$$
3		golem1.3	$$⊢C\in {\mathbf{C}}_{\mathscr{H}}$$
4		golem1.4	$$⊢F=\perp \left(A\right){\vee }_{\mathscr{H}}\left(A\cap B\right)$$
5		golem1.5	$$⊢G=\perp \left(B\right){\vee }_{\mathscr{H}}\left(B\cap C\right)$$
6		golem1.6	$$⊢H=\perp \left(C\right){\vee }_{\mathscr{H}}\left(C\cap A\right)$$
7		golem1.7	$$⊢D=\perp \left(B\right){\vee }_{\mathscr{H}}\left(B\cap A\right)$$
8		golem1.8	$$⊢R=\perp \left(C\right){\vee }_{\mathscr{H}}\left(C\cap B\right)$$
9		golem1.9	$$⊢S=\perp \left(A\right){\vee }_{\mathscr{H}}\left(A\cap C\right)$$
10	1	choccli	$$⊢\perp \left(A\right)\in {\mathbf{C}}_{\mathscr{H}}$$
11	1 2	chincli	$$⊢A\cap B\in {\mathbf{C}}_{\mathscr{H}}$$
12	10 11	chjcli	$$⊢\perp \left(A\right){\vee }_{\mathscr{H}}\left(A\cap B\right)\in {\mathbf{C}}_{\mathscr{H}}$$
13	4 12	eqeltri	$$⊢F\in {\mathbf{C}}_{\mathscr{H}}$$
14	2	choccli	$$⊢\perp \left(B\right)\in {\mathbf{C}}_{\mathscr{H}}$$
15	2 3	chincli	$$⊢B\cap C\in {\mathbf{C}}_{\mathscr{H}}$$
16	14 15	chjcli	$$⊢\perp \left(B\right){\vee }_{\mathscr{H}}\left(B\cap C\right)\in {\mathbf{C}}_{\mathscr{H}}$$
17	5 16	eqeltri	$$⊢G\in {\mathbf{C}}_{\mathscr{H}}$$
18	3	choccli	$$⊢\perp \left(C\right)\in {\mathbf{C}}_{\mathscr{H}}$$
19	3 1	chincli	$$⊢C\cap A\in {\mathbf{C}}_{\mathscr{H}}$$
20	18 19	chjcli	$$⊢\perp \left(C\right){\vee }_{\mathscr{H}}\left(C\cap A\right)\in {\mathbf{C}}_{\mathscr{H}}$$
21	6 20	eqeltri	$$⊢H\in {\mathbf{C}}_{\mathscr{H}}$$
22	13 17 21	stm1add3i	$$⊢f\in \mathrm{States}\to \left(f\left(\left(F\cap G\right)\cap H\right)=1\to f\left(F\right)+f\left(G\right)+f\left(H\right)=3\right)$$
23	1 2 3 4 5 6 7 8 9	golem1	$$⊢f\in \mathrm{States}\to f\left(F\right)+f\left(G\right)+f\left(H\right)=f\left(D\right)+f\left(R\right)+f\left(S\right)$$
24	23	eqeq1d	$$⊢f\in \mathrm{States}\to \left(f\left(F\right)+f\left(G\right)+f\left(H\right)=3\leftrightarrow f\left(D\right)+f\left(R\right)+f\left(S\right)=3\right)$$
25	22 24	sylibd	$$⊢f\in \mathrm{States}\to \left(f\left(\left(F\cap G\right)\cap H\right)=1\to f\left(D\right)+f\left(R\right)+f\left(S\right)=3\right)$$
26	2 1	chincli	$$⊢B\cap A\in {\mathbf{C}}_{\mathscr{H}}$$
27	14 26	chjcli	$$⊢\perp \left(B\right){\vee }_{\mathscr{H}}\left(B\cap A\right)\in {\mathbf{C}}_{\mathscr{H}}$$
28	7 27	eqeltri	$$⊢D\in {\mathbf{C}}_{\mathscr{H}}$$
29	3 2	chincli	$$⊢C\cap B\in {\mathbf{C}}_{\mathscr{H}}$$
30	18 29	chjcli	$$⊢\perp \left(C\right){\vee }_{\mathscr{H}}\left(C\cap B\right)\in {\mathbf{C}}_{\mathscr{H}}$$
31	8 30	eqeltri	$$⊢R\in {\mathbf{C}}_{\mathscr{H}}$$
32	1 3	chincli	$$⊢A\cap C\in {\mathbf{C}}_{\mathscr{H}}$$
33	10 32	chjcli	$$⊢\perp \left(A\right){\vee }_{\mathscr{H}}\left(A\cap C\right)\in {\mathbf{C}}_{\mathscr{H}}$$
34	9 33	eqeltri	$$⊢S\in {\mathbf{C}}_{\mathscr{H}}$$
35	28 31 34	stadd3i	$$⊢f\in \mathrm{States}\to \left(f\left(D\right)+f\left(R\right)+f\left(S\right)=3\to f\left(D\right)=1\right)$$
36	25 35	syld	$$⊢f\in \mathrm{States}\to \left(f\left(\left(F\cap G\right)\cap H\right)=1\to f\left(D\right)=1\right)$$