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	⊢ 𝐴 ∈ Cℋ
	goeq.2	⊢ 𝐵 ∈ Cℋ
	goeq.3	⊢ 𝐶 ∈ Cℋ
	goeq.4	⊢ 𝐹 = ( ( ⊥ ‘ 𝐴 ) ∨ℋ ( 𝐴 ∩ 𝐵 ) )
	goeq.5	⊢ 𝐺 = ( ( ⊥ ‘ 𝐵 ) ∨ℋ ( 𝐵 ∩ 𝐶 ) )
	goeq.6	⊢ 𝐻 = ( ( ⊥ ‘ 𝐶 ) ∨ℋ ( 𝐶 ∩ 𝐴 ) )
	goeq.7	⊢ 𝐷 = ( ( ⊥ ‘ 𝐵 ) ∨ℋ ( 𝐵 ∩ 𝐴 ) )
Assertion	goeqi	⊢ ( ( 𝐹 ∩ 𝐺 ) ∩ 𝐻 ) ⊆ 𝐷

Proof

Step	Hyp	Ref	Expression
1		goeq.1	⊢ 𝐴 ∈ Cℋ
2		goeq.2	⊢ 𝐵 ∈ Cℋ
3		goeq.3	⊢ 𝐶 ∈ Cℋ
4		goeq.4	⊢ 𝐹 = ( ( ⊥ ‘ 𝐴 ) ∨ℋ ( 𝐴 ∩ 𝐵 ) )
5		goeq.5	⊢ 𝐺 = ( ( ⊥ ‘ 𝐵 ) ∨ℋ ( 𝐵 ∩ 𝐶 ) )
6		goeq.6	⊢ 𝐻 = ( ( ⊥ ‘ 𝐶 ) ∨ℋ ( 𝐶 ∩ 𝐴 ) )
7		goeq.7	⊢ 𝐷 = ( ( ⊥ ‘ 𝐵 ) ∨ℋ ( 𝐵 ∩ 𝐴 ) )
8	1	choccli	⊢ ( ⊥ ‘ 𝐴 ) ∈ Cℋ
9	1 2	chincli	⊢ ( 𝐴 ∩ 𝐵 ) ∈ Cℋ
10	8 9	chjcli	⊢ ( ( ⊥ ‘ 𝐴 ) ∨ℋ ( 𝐴 ∩ 𝐵 ) ) ∈ Cℋ
11	4 10	eqeltri	⊢ 𝐹 ∈ Cℋ
12	2	choccli	⊢ ( ⊥ ‘ 𝐵 ) ∈ Cℋ
13	2 3	chincli	⊢ ( 𝐵 ∩ 𝐶 ) ∈ Cℋ
14	12 13	chjcli	⊢ ( ( ⊥ ‘ 𝐵 ) ∨ℋ ( 𝐵 ∩ 𝐶 ) ) ∈ Cℋ
15	5 14	eqeltri	⊢ 𝐺 ∈ Cℋ
16	11 15	chincli	⊢ ( 𝐹 ∩ 𝐺 ) ∈ Cℋ
17	3	choccli	⊢ ( ⊥ ‘ 𝐶 ) ∈ Cℋ
18	3 1	chincli	⊢ ( 𝐶 ∩ 𝐴 ) ∈ Cℋ
19	17 18	chjcli	⊢ ( ( ⊥ ‘ 𝐶 ) ∨ℋ ( 𝐶 ∩ 𝐴 ) ) ∈ Cℋ
20	6 19	eqeltri	⊢ 𝐻 ∈ Cℋ
21	16 20	chincli	⊢ ( ( 𝐹 ∩ 𝐺 ) ∩ 𝐻 ) ∈ Cℋ
22	2 1	chincli	⊢ ( 𝐵 ∩ 𝐴 ) ∈ Cℋ
23	12 22	chjcli	⊢ ( ( ⊥ ‘ 𝐵 ) ∨ℋ ( 𝐵 ∩ 𝐴 ) ) ∈ Cℋ
24	7 23	eqeltri	⊢ 𝐷 ∈ Cℋ
25	21 24	stri	⊢ ( ∀ 𝑓 ∈ States ( ( 𝑓 ‘ ( ( 𝐹 ∩ 𝐺 ) ∩ 𝐻 ) ) = 1 → ( 𝑓 ‘ 𝐷 ) = 1 ) → ( ( 𝐹 ∩ 𝐺 ) ∩ 𝐻 ) ⊆ 𝐷 )
26		eqid	⊢ ( ( ⊥ ‘ 𝐶 ) ∨ℋ ( 𝐶 ∩ 𝐵 ) ) = ( ( ⊥ ‘ 𝐶 ) ∨ℋ ( 𝐶 ∩ 𝐵 ) )
27		eqid	⊢ ( ( ⊥ ‘ 𝐴 ) ∨ℋ ( 𝐴 ∩ 𝐶 ) ) = ( ( ⊥ ‘ 𝐴 ) ∨ℋ ( 𝐴 ∩ 𝐶 ) )
28	1 2 3 4 5 6 7 26 27	golem2	⊢ ( 𝑓 ∈ States → ( ( 𝑓 ‘ ( ( 𝐹 ∩ 𝐺 ) ∩ 𝐻 ) ) = 1 → ( 𝑓 ‘ 𝐷 ) = 1 ) )
29	25 28	mprg	⊢ ( ( 𝐹 ∩ 𝐺 ) ∩ 𝐻 ) ⊆ 𝐷