golem1

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

	Ref	Expression
Hypotheses	golem1.1	$⊢ A \in C_{ℋ}$
	golem1.2	$⊢ B \in C_{ℋ}$
	golem1.3	$⊢ C \in C_{ℋ}$
	golem1.4	$⊢ F = ⊥ (A) \lor_{ℋ} (A \cap B)$
	golem1.5	$⊢ G = ⊥ (B) \lor_{ℋ} (B \cap C)$
	golem1.6	$⊢ H = ⊥ (C) \lor_{ℋ} (C \cap A)$
	golem1.7	$⊢ D = ⊥ (B) \lor_{ℋ} (B \cap A)$
	golem1.8	$⊢ R = ⊥ (C) \lor_{ℋ} (C \cap B)$
	golem1.9	$⊢ S = ⊥ (A) \lor_{ℋ} (A \cap C)$
Assertion	golem1	$⊢ f \in States \to f (F) + f (G) + f (H) = f (D) + f (R) + f (S)$

Proof

Step	Hyp	Ref	Expression
1		golem1.1	$⊢ A \in C_{ℋ}$
2		golem1.2	$⊢ B \in C_{ℋ}$
3		golem1.3	$⊢ C \in C_{ℋ}$
4		golem1.4	$⊢ F = ⊥ (A) \lor_{ℋ} (A \cap B)$
5		golem1.5	$⊢ G = ⊥ (B) \lor_{ℋ} (B \cap C)$
6		golem1.6	$⊢ H = ⊥ (C) \lor_{ℋ} (C \cap A)$
7		golem1.7	$⊢ D = ⊥ (B) \lor_{ℋ} (B \cap A)$
8		golem1.8	$⊢ R = ⊥ (C) \lor_{ℋ} (C \cap B)$
9		golem1.9	$⊢ S = ⊥ (A) \lor_{ℋ} (A \cap C)$
10	1	choccli	$⊢ ⊥ (A) \in C_{ℋ}$
11		stcl	$⊢ f \in States \to (⊥ (A) \in C_{ℋ} \to f (⊥ (A)) \in ℝ)$
12	10 11	mpi	$⊢ f \in States \to f (⊥ (A)) \in ℝ$
13	12	recnd	$⊢ f \in States \to f (⊥ (A)) \in ℂ$
14	2	choccli	$⊢ ⊥ (B) \in C_{ℋ}$
15		stcl	$⊢ f \in States \to (⊥ (B) \in C_{ℋ} \to f (⊥ (B)) \in ℝ)$
16	14 15	mpi	$⊢ f \in States \to f (⊥ (B)) \in ℝ$
17	16	recnd	$⊢ f \in States \to f (⊥ (B)) \in ℂ$
18	3	choccli	$⊢ ⊥ (C) \in C_{ℋ}$
19		stcl	$⊢ f \in States \to (⊥ (C) \in C_{ℋ} \to f (⊥ (C)) \in ℝ)$
20	18 19	mpi	$⊢ f \in States \to f (⊥ (C)) \in ℝ$
21	20	recnd	$⊢ f \in States \to f (⊥ (C)) \in ℂ$
22	13 17 21	addassd	$⊢ f \in States \to f (⊥ (A)) + f (⊥ (B)) + f (⊥ (C)) = f (⊥ (A)) + f (⊥ (B)) + f (⊥ (C))$
23	17 21	addcld	$⊢ f \in States \to f (⊥ (B)) + f (⊥ (C)) \in ℂ$
24	13 23	addcomd	$⊢ f \in States \to f (⊥ (A)) + f (⊥ (B)) + f (⊥ (C)) = f (⊥ (B)) + f (⊥ (C)) + f (⊥ (A))$
25	22 24	eqtrd	$⊢ f \in States \to f (⊥ (A)) + f (⊥ (B)) + f (⊥ (C)) = f (⊥ (B)) + f (⊥ (C)) + f (⊥ (A))$
26	25	oveq1d	$⊢ f \in States \to (f (⊥ (A)) + f (⊥ (B))) + f (⊥ (C)) + (f (A \cap B) + f (B \cap C)) + f (C \cap A) = (f (⊥ (B)) + f (⊥ (C))) + f (⊥ (A)) + (f (A \cap B) + f (B \cap C)) + f (C \cap A)$
27	13 17	addcld	$⊢ f \in States \to f (⊥ (A)) + f (⊥ (B)) \in ℂ$
28	1 2	chincli	$⊢ A \cap B \in C_{ℋ}$
29		stcl	$⊢ f \in States \to (A \cap B \in C_{ℋ} \to f (A \cap B) \in ℝ)$
30	28 29	mpi	$⊢ f \in States \to f (A \cap B) \in ℝ$
31	30	recnd	$⊢ f \in States \to f (A \cap B) \in ℂ$
32	2 3	chincli	$⊢ B \cap C \in C_{ℋ}$
33		stcl	$⊢ f \in States \to (B \cap C \in C_{ℋ} \to f (B \cap C) \in ℝ)$
34	32 33	mpi	$⊢ f \in States \to f (B \cap C) \in ℝ$
35	34	recnd	$⊢ f \in States \to f (B \cap C) \in ℂ$
36	31 35	addcld	$⊢ f \in States \to f (A \cap B) + f (B \cap C) \in ℂ$
37	3 1	chincli	$⊢ C \cap A \in C_{ℋ}$
38		stcl	$⊢ f \in States \to (C \cap A \in C_{ℋ} \to f (C \cap A) \in ℝ)$
39	37 38	mpi	$⊢ f \in States \to f (C \cap A) \in ℝ$
40	39	recnd	$⊢ f \in States \to f (C \cap A) \in ℂ$
41	27 36 21 40	add4d	$⊢ f \in States \to (f (⊥ (A)) + f (⊥ (B))) + (f (A \cap B) + f (B \cap C)) + f (⊥ (C)) + f (C \cap A) = (f (⊥ (A)) + f (⊥ (B))) + f (⊥ (C)) + (f (A \cap B) + f (B \cap C)) + f (C \cap A)$
42	23 36 13 40	add4d	$⊢ f \in States \to (f (⊥ (B)) + f (⊥ (C))) + (f (A \cap B) + f (B \cap C)) + f (⊥ (A)) + f (C \cap A) = (f (⊥ (B)) + f (⊥ (C))) + f (⊥ (A)) + (f (A \cap B) + f (B \cap C)) + f (C \cap A)$
43	26 41 42	3eqtr4d	$⊢ f \in States \to (f (⊥ (A)) + f (⊥ (B))) + (f (A \cap B) + f (B \cap C)) + f (⊥ (C)) + f (C \cap A) = (f (⊥ (B)) + f (⊥ (C))) + (f (A \cap B) + f (B \cap C)) + f (⊥ (A)) + f (C \cap A)$
44	13 31 17 35	add4d	$⊢ f \in States \to f (⊥ (A)) + f (A \cap B) + f (⊥ (B)) + f (B \cap C) = f (⊥ (A)) + f (⊥ (B)) + f (A \cap B) + f (B \cap C)$
45	44	oveq1d	$⊢ f \in States \to (f (⊥ (A)) + f (A \cap B)) + (f (⊥ (B)) + f (B \cap C)) + f (⊥ (C)) + f (C \cap A) = (f (⊥ (A)) + f (⊥ (B))) + (f (A \cap B) + f (B \cap C)) + f (⊥ (C)) + f (C \cap A)$
46	17 31 21 35	add4d	$⊢ f \in States \to f (⊥ (B)) + f (A \cap B) + f (⊥ (C)) + f (B \cap C) = f (⊥ (B)) + f (⊥ (C)) + f (A \cap B) + f (B \cap C)$
47	46	oveq1d	$⊢ f \in States \to (f (⊥ (B)) + f (A \cap B)) + (f (⊥ (C)) + f (B \cap C)) + f (⊥ (A)) + f (C \cap A) = (f (⊥ (B)) + f (⊥ (C))) + (f (A \cap B) + f (B \cap C)) + f (⊥ (A)) + f (C \cap A)$
48	43 45 47	3eqtr4d	$⊢ f \in States \to (f (⊥ (A)) + f (A \cap B)) + (f (⊥ (B)) + f (B \cap C)) + f (⊥ (C)) + f (C \cap A) = (f (⊥ (B)) + f (A \cap B)) + (f (⊥ (C)) + f (B \cap C)) + f (⊥ (A)) + f (C \cap A)$
49	1 2	stji1i	$⊢ f \in States \to f (⊥ (A) \lor_{ℋ} (A \cap B)) = f (⊥ (A)) + f (A \cap B)$
50	2 3	stji1i	$⊢ f \in States \to f (⊥ (B) \lor_{ℋ} (B \cap C)) = f (⊥ (B)) + f (B \cap C)$
51	49 50	oveq12d	$⊢ f \in States \to f (⊥ (A) \lor_{ℋ} (A \cap B)) + f (⊥ (B) \lor_{ℋ} (B \cap C)) = f (⊥ (A)) + f (A \cap B) + f (⊥ (B)) + f (B \cap C)$
52	3 1	stji1i	$⊢ f \in States \to f (⊥ (C) \lor_{ℋ} (C \cap A)) = f (⊥ (C)) + f (C \cap A)$
53	51 52	oveq12d	$⊢ f \in States \to f (⊥ (A) \lor_{ℋ} (A \cap B)) + f (⊥ (B) \lor_{ℋ} (B \cap C)) + f (⊥ (C) \lor_{ℋ} (C \cap A)) = (f (⊥ (A)) + f (A \cap B)) + (f (⊥ (B)) + f (B \cap C)) + f (⊥ (C)) + f (C \cap A)$
54	2 1	stji1i	$⊢ f \in States \to f (⊥ (B) \lor_{ℋ} (B \cap A)) = f (⊥ (B)) + f (B \cap A)$
55		incom	$⊢ B \cap A = A \cap B$
56	55	fveq2i	$⊢ f (B \cap A) = f (A \cap B)$
57	56	oveq2i	$⊢ f (⊥ (B)) + f (B \cap A) = f (⊥ (B)) + f (A \cap B)$
58	54 57	syl6eq	$⊢ f \in States \to f (⊥ (B) \lor_{ℋ} (B \cap A)) = f (⊥ (B)) + f (A \cap B)$
59	3 2	stji1i	$⊢ f \in States \to f (⊥ (C) \lor_{ℋ} (C \cap B)) = f (⊥ (C)) + f (C \cap B)$
60		incom	$⊢ C \cap B = B \cap C$
61	60	fveq2i	$⊢ f (C \cap B) = f (B \cap C)$
62	61	oveq2i	$⊢ f (⊥ (C)) + f (C \cap B) = f (⊥ (C)) + f (B \cap C)$
63	59 62	syl6eq	$⊢ f \in States \to f (⊥ (C) \lor_{ℋ} (C \cap B)) = f (⊥ (C)) + f (B \cap C)$
64	58 63	oveq12d	$⊢ f \in States \to f (⊥ (B) \lor_{ℋ} (B \cap A)) + f (⊥ (C) \lor_{ℋ} (C \cap B)) = f (⊥ (B)) + f (A \cap B) + f (⊥ (C)) + f (B \cap C)$
65	1 3	stji1i	$⊢ f \in States \to f (⊥ (A) \lor_{ℋ} (A \cap C)) = f (⊥ (A)) + f (A \cap C)$
66		incom	$⊢ A \cap C = C \cap A$
67	66	fveq2i	$⊢ f (A \cap C) = f (C \cap A)$
68	67	oveq2i	$⊢ f (⊥ (A)) + f (A \cap C) = f (⊥ (A)) + f (C \cap A)$
69	65 68	syl6eq	$⊢ f \in States \to f (⊥ (A) \lor_{ℋ} (A \cap C)) = f (⊥ (A)) + f (C \cap A)$
70	64 69	oveq12d	$⊢ f \in States \to f (⊥ (B) \lor_{ℋ} (B \cap A)) + f (⊥ (C) \lor_{ℋ} (C \cap B)) + f (⊥ (A) \lor_{ℋ} (A \cap C)) = (f (⊥ (B)) + f (A \cap B)) + (f (⊥ (C)) + f (B \cap C)) + f (⊥ (A)) + f (C \cap A)$
71	48 53 70	3eqtr4d	$⊢ f \in States \to f (⊥ (A) \lor_{ℋ} (A \cap B)) + f (⊥ (B) \lor_{ℋ} (B \cap C)) + f (⊥ (C) \lor_{ℋ} (C \cap A)) = f (⊥ (B) \lor_{ℋ} (B \cap A)) + f (⊥ (C) \lor_{ℋ} (C \cap B)) + f (⊥ (A) \lor_{ℋ} (A \cap C))$
72	4	fveq2i	$⊢ f (F) = f (⊥ (A) \lor_{ℋ} (A \cap B))$
73	5	fveq2i	$⊢ f (G) = f (⊥ (B) \lor_{ℋ} (B \cap C))$
74	72 73	oveq12i	$⊢ f (F) + f (G) = f (⊥ (A) \lor_{ℋ} (A \cap B)) + f (⊥ (B) \lor_{ℋ} (B \cap C))$
75	6	fveq2i	$⊢ f (H) = f (⊥ (C) \lor_{ℋ} (C \cap A))$
76	74 75	oveq12i	$⊢ f (F) + f (G) + f (H) = f (⊥ (A) \lor_{ℋ} (A \cap B)) + f (⊥ (B) \lor_{ℋ} (B \cap C)) + f (⊥ (C) \lor_{ℋ} (C \cap A))$
77	7	fveq2i	$⊢ f (D) = f (⊥ (B) \lor_{ℋ} (B \cap A))$
78	8	fveq2i	$⊢ f (R) = f (⊥ (C) \lor_{ℋ} (C \cap B))$
79	77 78	oveq12i	$⊢ f (D) + f (R) = f (⊥ (B) \lor_{ℋ} (B \cap A)) + f (⊥ (C) \lor_{ℋ} (C \cap B))$
80	9	fveq2i	$⊢ f (S) = f (⊥ (A) \lor_{ℋ} (A \cap C))$
81	79 80	oveq12i	$⊢ f (D) + f (R) + f (S) = f (⊥ (B) \lor_{ℋ} (B \cap A)) + f (⊥ (C) \lor_{ℋ} (C \cap B)) + f (⊥ (A) \lor_{ℋ} (A \cap C))$
82	71 76 81	3eqtr4g	$⊢ f \in States \to f (F) + f (G) + f (H) = f (D) + f (R) + f (S)$

Metamath Proof Explorer

Theorem golem1

Proof