Theorem golem1 10136

Description: Lemma for Godowski's equation.

Hypotheses

Ref	Expression
golem1.1	|- A e. CH
golem1.2	|- B e. CH
golem1.3	|- C e. CH
golem1.4	|- F = ((_|_` A) vH (A i^i B))
golem1.5	|- G = ((_|_` B) vH (B i^i C))
golem1.6	|- H = ((_|_` C) vH (C i^i A))
golem1.7	|- D = ((_|_` B) vH (B i^i A))
golem1.8	|- R = ((_|_` C) vH (C i^i B))
golem1.9	|- S = ((_|_` A) vH (A i^i C))

Assertion

Ref	Expression
golem1	|- (f e. States -> (((f` F) + (f` G)) + (f` H)) = (((f` D) + (f` R)) + (f` S)))

Proof of Theorem golem1

Step	Hyp	Ref	Expression
1		axaddass 5257	. . . . . . . 8 |- (((f` (_|_` A)) e. CC /\ (f` (_|_` B)) e. CC /\ (f` (_|_` C)) e. CC) -> (((f` (_|_` A)) + (f` (_|_` B))) + (f` (_|_` C))) = ((f` (_|_` A)) + ((f` (_|_` B)) + (f` (_|_` C)))))
2		golem1.1	. . . . . . . . . . 11 |- A e. CH
3	2	choccl 9124	. . . . . . . . . 10 |- (_|_` A) e. CH
4		stclt 10081	. . . . . . . . . 10 |- (f e. States -> ((_|_` A) e. CH -> (f` (_|_` A)) e. RR))
5	3, 4	mpi 44	. . . . . . . . 9 |- (f e. States -> (f` (_|_` A)) e. RR)
6	5	recnd 5295	. . . . . . . 8 |- (f e. States -> (f` (_|_` A)) e. CC)
7		golem1.2	. . . . . . . . . . 11 |- B e. CH
8	7	choccl 9124	. . . . . . . . . 10 |- (_|_` B) e. CH
9		stclt 10081	. . . . . . . . . 10 |- (f e. States -> ((_|_` B) e. CH -> (f` (_|_` B)) e. RR))
10	8, 9	mpi 44	. . . . . . . . 9 |- (f e. States -> (f` (_|_` B)) e. RR)
11	10	recnd 5295	. . . . . . . 8 |- (f e. States -> (f` (_|_` B)) e. CC)
12		golem1.3	. . . . . . . . . . 11 |- C e. CH
13	12	choccl 9124	. . . . . . . . . 10 |- (_|_` C) e. CH
14		stclt 10081	. . . . . . . . . 10 |- (f e. States -> ((_|_` C) e. CH -> (f` (_|_` C)) e. RR))
15	13, 14	mpi 44	. . . . . . . . 9 |- (f e. States -> (f` (_|_` C)) e. RR)
16	15	recnd 5295	. . . . . . . 8 |- (f e. States -> (f` (_|_` C)) e. CC)
17	1, 6, 11, 16	syl3anc 857	. . . . . . 7 |- (f e. States -> (((f` (_|_` A)) + (f` (_|_` B))) + (f` (_|_` C))) = ((f` (_|_` A)) + ((f` (_|_` B)) + (f` (_|_` C)))))
18		axaddcom 5255	. . . . . . . 8 |- (((f` (_|_` A)) e. CC /\ ((f` (_|_` B)) + (f` (_|_` C))) e. CC) -> ((f` (_|_` A)) + ((f` (_|_` B)) + (f` (_|_` C)))) = (((f` (_|_` B)) + (f` (_|_` C))) + (f` (_|_` A))))
19		axaddcl 5251	. . . . . . . . 9 |- (((f` (_|_` B)) e. CC /\ (f` (_|_` C)) e. CC) -> ((f` (_|_` B)) + (f` (_|_` C))) e. CC)
20	19, 11, 16	sylanc 471	. . . . . . . 8 |- (f e. States -> ((f` (_|_` B)) + (f` (_|_` C))) e. CC)
21	18, 6, 20	sylanc 471	. . . . . . 7 |- (f e. States -> ((f` (_|_` A)) + ((f` (_|_` B)) + (f` (_|_` C)))) = (((f` (_|_` B)) + (f` (_|_` C))) + (f` (_|_` A))))
22	17, 21	eqtrd 1504	. . . . . 6 |- (f e. States -> (((f` (_|_` A)) + (f` (_|_` B))) + (f` (_|_` C))) = (((f` (_|_` B)) + (f` (_|_` C))) + (f` (_|_` A))))
23	22	opreq1d 3966	. . . . 5 |- (f e. States -> ((((f` (_|_` A)) + (f` (_|_` B))) + (f` (_|_` C))) + (((f` (A i^i B)) + (f` (B i^i C))) + (f` (C i^i A)))) = ((((f` (_|_` B)) + (f` (_|_` C))) + (f` (_|_` A))) + (((f` (A i^i B)) + (f` (B i^i C))) + (f` (C i^i A)))))
24		add4t 5318	. . . . . 6 |- (((((f` (_|_` A)) + (f` (_|_` B))) e. CC /\ ((f` (A i^i B)) + (f` (B i^i C))) e. CC) /\ ((f` (_|_` C)) e. CC /\ (f` (C i^i A)) e. CC)) -> ((((f` (_|_` A)) + (f` (_|_` B))) + ((f` (A i^i B)) + (f` (B i^i C)))) + ((f` (_|_` C)) + (f` (C i^i A)))) = ((((f` (_|_` A)) + (f` (_|_` B))) + (f` (_|_` C))) + (((f` (A i^i B)) + (f` (B i^i C))) + (f` (C i^i A)))))
25		axaddcl 5251	. . . . . . 7 |- (((f` (_|_` A)) e. CC /\ (f` (_|_` B)) e. CC) -> ((f` (_|_` A)) + (f` (_|_` B))) e. CC)
26	25, 6, 11	sylanc 471	. . . . . 6 |- (f e. States -> ((f` (_|_` A)) + (f` (_|_` B))) e. CC)
27		axaddcl 5251	. . . . . . 7 |- (((f` (A i^i B)) e. CC /\ (f` (B i^i C)) e. CC) -> ((f` (A i^i B)) + (f` (B i^i C))) e. CC)
28	2, 7	chincl 9321	. . . . . . . . 9 |- (A i^i B) e. CH
29		stclt 10081	. . . . . . . . 9 |- (f e. States -> ((A i^i B) e. CH -> (f` (A i^i B)) e. RR))
30	28, 29	mpi 44	. . . . . . . 8 |- (f e. States -> (f` (A i^i B)) e. RR)
31	30	recnd 5295	. . . . . . 7 |- (f e. States -> (f` (A i^i B)) e. CC)
32	7, 12	chincl 9321	. . . . . . . . 9 |- (B i^i C) e. CH
33		stclt 10081	. . . . . . . . 9 |- (f e. States -> ((B i^i C) e. CH -> (f` (B i^i C)) e. RR))
34	32, 33	mpi 44	. . . . . . . 8 |- (f e. States -> (f` (B i^i C)) e. RR)
35	34	recnd 5295	. . . . . . 7 |- (f e. States -> (f` (B i^i C)) e. CC)
36	27, 31, 35	sylanc 471	. . . . . 6 |- (f e. States -> ((f` (A i^i B)) + (f` (B i^i C))) e. CC)
37	12, 2	chincl 9321	. . . . . . . 8 |- (C i^i A) e. CH
38		stclt 10081	. . . . . . . 8 |- (f e. States -> ((C i^i A) e. CH -> (f` (C i^i A)) e. RR))
39	37, 38	mpi 44	. . . . . . 7 |- (f e. States -> (f` (C i^i A)) e. RR)
40	39	recnd 5295	. . . . . 6 |- (f e. States -> (f` (C i^i A)) e. CC)
41	24, 26, 36, 16, 40	syl2anc 472	. . . . 5 |- (f e. States -> ((((f` (_|_` A)) + (f` (_|_` B))) + ((f` (A i^i B)) + (f` (B i^i C)))) + ((f` (_|_` C)) + (f` (C i^i A)))) = ((((f` (_|_` A)) + (f` (_|_` B))) + (f` (_|_` C))) + (((f` (A i^i B)) + (f` (B i^i C))) + (f` (C i^i A)))))
42		add4t 5318	. . . . . 6 |- (((((f` (_|_` B)) + (f` (_|_` C))) e. CC /\ ((f` (A i^i B)) + (f` (B i^i C))) e. CC) /\ ((f` (_|_` A)) e. CC /\ (f` (C i^i A)) e. CC)) -> ((((f` (_|_` B)) + (f` (_|_` C))) + ((f` (A i^i B)) + (f` (B i^i C)))) + ((f` (_|_` A)) + (f` (C i^i A)))) = ((((f` (_|_` B)) + (f` (_|_` C))) + (f` (_|_` A))) + (((f` (A i^i B)) + (f` (B i^i C))) + (f` (C i^i A)))))
43	42, 20, 36, 6, 40	syl2anc 472	. . . . 5 |- (f e. States -> ((((f` (_|_` B)) + (f` (_|_` C))) + ((f` (A i^i B)) + (f` (B i^i C)))) + ((f` (_|_` A)) + (f` (C