Theorem goeqi

Description: Godowski's equation, shown here as a variant equivalent to Equation SF of Godowski p. 730. (Contributed by NM, 10-Nov-2002) (New usage is discouraged.)

	Ref	Expression
Hypotheses	goeq.1	$$⊢A\in {\mathbf{C}}_{\mathscr{H}}$$
	goeq.2	$$⊢B\in {\mathbf{C}}_{\mathscr{H}}$$
	goeq.3	$$⊢C\in {\mathbf{C}}_{\mathscr{H}}$$
	goeq.4	$$⊢F=\perp \left(A\right){\vee }_{\mathscr{H}}\left(A\cap B\right)$$
	goeq.5	$$⊢G=\perp \left(B\right){\vee }_{\mathscr{H}}\left(B\cap C\right)$$
	goeq.6	$$⊢H=\perp \left(C\right){\vee }_{\mathscr{H}}\left(C\cap A\right)$$
	goeq.7	$$⊢D=\perp \left(B\right){\vee }_{\mathscr{H}}\left(B\cap A\right)$$
Assertion	goeqi	$$⊢\left(F\cap G\right)\cap H\subseteq D$$

Proof

Step	Hyp	Ref	Expression
1		goeq.1	$$⊢A\in {\mathbf{C}}_{\mathscr{H}}$$
2		goeq.2	$$⊢B\in {\mathbf{C}}_{\mathscr{H}}$$
3		goeq.3	$$⊢C\in {\mathbf{C}}_{\mathscr{H}}$$
4		goeq.4	$$⊢F=\perp \left(A\right){\vee }_{\mathscr{H}}\left(A\cap B\right)$$
5		goeq.5	$$⊢G=\perp \left(B\right){\vee }_{\mathscr{H}}\left(B\cap C\right)$$
6		goeq.6	$$⊢H=\perp \left(C\right){\vee }_{\mathscr{H}}\left(C\cap A\right)$$
7		goeq.7	$$⊢D=\perp \left(B\right){\vee }_{\mathscr{H}}\left(B\cap A\right)$$
8	1	choccli	$$⊢\perp \left(A\right)\in {\mathbf{C}}_{\mathscr{H}}$$
9	1 2	chincli	$$⊢A\cap B\in {\mathbf{C}}_{\mathscr{H}}$$
10	8 9	chjcli	$$⊢\perp \left(A\right){\vee }_{\mathscr{H}}\left(A\cap B\right)\in {\mathbf{C}}_{\mathscr{H}}$$
11	4 10	eqeltri	$$⊢F\in {\mathbf{C}}_{\mathscr{H}}$$
12	2	choccli	$$⊢\perp \left(B\right)\in {\mathbf{C}}_{\mathscr{H}}$$
13	2 3	chincli	$$⊢B\cap C\in {\mathbf{C}}_{\mathscr{H}}$$
14	12 13	chjcli	$$⊢\perp \left(B\right){\vee }_{\mathscr{H}}\left(B\cap C\right)\in {\mathbf{C}}_{\mathscr{H}}$$
15	5 14	eqeltri	$$⊢G\in {\mathbf{C}}_{\mathscr{H}}$$
16	11 15	chincli	$$⊢F\cap G\in {\mathbf{C}}_{\mathscr{H}}$$
17	3	choccli	$$⊢\perp \left(C\right)\in {\mathbf{C}}_{\mathscr{H}}$$
18	3 1	chincli	$$⊢C\cap A\in {\mathbf{C}}_{\mathscr{H}}$$
19	17 18	chjcli	$$⊢\perp \left(C\right){\vee }_{\mathscr{H}}\left(C\cap A\right)\in {\mathbf{C}}_{\mathscr{H}}$$
20	6 19	eqeltri	$$⊢H\in {\mathbf{C}}_{\mathscr{H}}$$
21	16 20	chincli	$$⊢\left(F\cap G\right)\cap H\in {\mathbf{C}}_{\mathscr{H}}$$
22	2 1	chincli	$$⊢B\cap A\in {\mathbf{C}}_{\mathscr{H}}$$
23	12 22	chjcli	$$⊢\perp \left(B\right){\vee }_{\mathscr{H}}\left(B\cap A\right)\in {\mathbf{C}}_{\mathscr{H}}$$
24	7 23	eqeltri	$$⊢D\in {\mathbf{C}}_{\mathscr{H}}$$
25	21 24	stri	$$⊢\forall f\in \mathrm{States}\left(f\left(\left(F\cap G\right)\cap H\right)=1\to f\left(D\right)=1\right)\to \left(F\cap G\right)\cap H\subseteq D$$
26		eqid	$$⊢\perp \left(C\right){\vee }_{\mathscr{H}}\left(C\cap B\right)=\perp \left(C\right){\vee }_{\mathscr{H}}\left(C\cap B\right)$$
27		eqid	$$⊢\perp \left(A\right){\vee }_{\mathscr{H}}\left(A\cap C\right)=\perp \left(A\right){\vee }_{\mathscr{H}}\left(A\cap C\right)$$
28	1 2 3 4 5 6 7 26 27	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)$$
29	25 28	mprg	$$⊢\left(F\cap G\right)\cap H\subseteq D$$