Metamath Proof Explorer

Theorem golem1

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

Ref Expression
Hypotheses golem1.1 ⊢ 𝐴 ∈ Cℋ
golem1.2 ⊢ 𝐵 ∈ Cℋ
golem1.3 ⊢ 𝐶 ∈ Cℋ
golem1.4 ⊢ 𝐹 = ( ( ⊥ ‘ 𝐴 ) ∨ℋ ( 𝐴 ∩ 𝐵 ) )
golem1.5 ⊢ 𝐺 = ( ( ⊥ ‘ 𝐵 ) ∨ℋ ( 𝐵 ∩ 𝐶 ) )
golem1.6 ⊢ 𝐻 = ( ( ⊥ ‘ 𝐶 ) ∨ℋ ( 𝐶 ∩ 𝐴 ) )
golem1.7 ⊢ 𝐷 = ( ( ⊥ ‘ 𝐵 ) ∨ℋ ( 𝐵 ∩ 𝐴 ) )
golem1.8 ⊢ 𝑅 = ( ( ⊥ ‘ 𝐶 ) ∨ℋ ( 𝐶 ∩ 𝐵 ) )
golem1.9 ⊢ 𝑆 = ( ( ⊥ ‘ 𝐴 ) ∨ℋ ( 𝐴 ∩ 𝐶 ) )
Assertion golem1 ( 𝑓 ∈ States → ( ( ( 𝑓 ‘ 𝐹 ) + ( 𝑓 ‘ 𝐺 ) ) + ( 𝑓 ‘ 𝐻 ) ) = ( ( ( 𝑓 ‘ 𝐷 ) + ( 𝑓 ‘ 𝑅 ) ) + ( 𝑓 ‘ 𝑆 ) ) )

Proof

Step Hyp Ref Expression
1 golem1.1 ⊢ 𝐴 ∈ Cℋ
2 golem1.2 ⊢ 𝐵 ∈ Cℋ
3 golem1.3 ⊢ 𝐶 ∈ Cℋ
4 golem1.4 ⊢ 𝐹 = ( ( ⊥ ‘ 𝐴 ) ∨ℋ ( 𝐴 ∩ 𝐵 ) )
5 golem1.5 ⊢ 𝐺 = ( ( ⊥ ‘ 𝐵 ) ∨ℋ ( 𝐵 ∩ 𝐶 ) )
6 golem1.6 ⊢ 𝐻 = ( ( ⊥ ‘ 𝐶 ) ∨ℋ ( 𝐶 ∩ 𝐴 ) )
7 golem1.7 ⊢ 𝐷 = ( ( ⊥ ‘ 𝐵 ) ∨ℋ ( 𝐵 ∩ 𝐴 ) )
8 golem1.8 ⊢ 𝑅 = ( ( ⊥ ‘ 𝐶 ) ∨ℋ ( 𝐶 ∩ 𝐵 ) )
9 golem1.9 ⊢ 𝑆 = ( ( ⊥ ‘ 𝐴 ) ∨ℋ ( 𝐴 ∩ 𝐶 ) )
10 1 choccli ⊢ ( ⊥ ‘ 𝐴 ) ∈ Cℋ
11 stcl ⊢ ( 𝑓 ∈ States → ( ( ⊥ ‘ 𝐴 ) ∈ Cℋ → ( 𝑓 ‘ ( ⊥ ‘ 𝐴 ) ) ∈ ℝ ) )
12 10 11 mpi ⊢ ( 𝑓 ∈ States → ( 𝑓 ‘ ( ⊥ ‘ 𝐴 ) ) ∈ ℝ )
13 12 recnd ⊢ ( 𝑓 ∈ States → ( 𝑓 ‘ ( ⊥ ‘ 𝐴 ) ) ∈ ℂ )
14 2 choccli ⊢ ( ⊥ ‘ 𝐵 ) ∈ Cℋ
15 stcl ⊢ ( 𝑓 ∈ States → ( ( ⊥ ‘ 𝐵 ) ∈ Cℋ → ( 𝑓 ‘ ( ⊥ ‘ 𝐵 ) ) ∈ ℝ ) )
16 14 15 mpi ⊢ ( 𝑓 ∈ States → ( 𝑓 ‘ ( ⊥ ‘ 𝐵 ) ) ∈ ℝ )
17 16 recnd ⊢ ( 𝑓 ∈ States → ( 𝑓 ‘ ( ⊥ ‘ 𝐵 ) ) ∈ ℂ )
18 3 choccli ⊢ ( ⊥ ‘ 𝐶 ) ∈ Cℋ
19 stcl ⊢ ( 𝑓 ∈ States → ( ( ⊥ ‘ 𝐶 ) ∈ Cℋ → ( 𝑓 ‘ ( ⊥ ‘ 𝐶 ) ) ∈ ℝ ) )
20 18 19 mpi ⊢ ( 𝑓 ∈ States → ( 𝑓 ‘ ( ⊥ ‘ 𝐶 ) ) ∈ ℝ )
21 20 recnd ⊢ ( 𝑓 ∈ States → ( 𝑓 ‘ ( ⊥ ‘ 𝐶 ) ) ∈ ℂ )
22 13 17 21 addassd ⊢ ( 𝑓 ∈ States → ( ( ( 𝑓 ‘ ( ⊥ ‘ 𝐴 ) ) + ( 𝑓 ‘ ( ⊥ ‘ 𝐵 ) ) ) + ( 𝑓 ‘ ( ⊥ ‘ 𝐶 ) ) ) = ( ( 𝑓 ‘ ( ⊥ ‘ 𝐴 ) ) + ( ( 𝑓 ‘ ( ⊥ ‘ 𝐵 ) ) + ( 𝑓 ‘ ( ⊥ ‘ 𝐶 ) ) ) ) )
23 17 21 addcld ⊢ ( 𝑓 ∈ States → ( ( 𝑓 ‘ ( ⊥ ‘ 𝐵 ) ) + ( 𝑓 ‘ ( ⊥ ‘ 𝐶 ) ) ) ∈ ℂ )
24 13 23 addcomd ⊢ ( 𝑓 ∈ States → ( ( 𝑓 ‘ ( ⊥ ‘ 𝐴 ) ) + ( ( 𝑓 ‘ ( ⊥ ‘ 𝐵 ) ) + ( 𝑓 ‘ ( ⊥ ‘ 𝐶 ) ) ) ) = ( ( ( 𝑓 ‘ ( ⊥ ‘ 𝐵 ) ) + ( 𝑓 ‘ ( ⊥ ‘ 𝐶 ) ) ) + ( 𝑓 ‘ ( ⊥ ‘ 𝐴 ) ) ) )
25 22 24 eqtrd ⊢ ( 𝑓 ∈ States → ( ( ( 𝑓 ‘ ( ⊥ ‘ 𝐴 ) ) + ( 𝑓 ‘ ( ⊥ ‘ 𝐵 ) ) ) + ( 𝑓 ‘ ( ⊥ ‘ 𝐶 ) ) ) = ( ( ( 𝑓 ‘ ( ⊥ ‘ 𝐵 ) ) + ( 𝑓 ‘ ( ⊥ ‘ 𝐶 ) ) ) + ( 𝑓 ‘ ( ⊥ ‘ 𝐴 ) ) ) )
26 25 oveq1d ⊢ ( 𝑓 ∈ States → ( ( ( ( 𝑓 ‘ ( ⊥ ‘ 𝐴 ) ) + ( 𝑓 ‘ ( ⊥ ‘ 𝐵 ) ) ) + ( 𝑓 ‘ ( ⊥ ‘ 𝐶 ) ) ) + ( ( ( 𝑓 ‘ ( 𝐴 ∩ 𝐵 ) ) + ( 𝑓 ‘ ( 𝐵 ∩ 𝐶 ) ) ) + ( 𝑓 ‘ ( 𝐶 ∩ 𝐴 ) ) ) ) = ( ( ( ( 𝑓 ‘ ( ⊥ ‘ 𝐵 ) ) + ( 𝑓 ‘ ( ⊥ ‘ 𝐶 ) ) ) + ( 𝑓 ‘ ( ⊥ ‘ 𝐴 ) ) ) + ( ( ( 𝑓 ‘ ( 𝐴 ∩ 𝐵 ) ) + ( 𝑓 ‘ ( 𝐵 ∩ 𝐶 ) ) ) + ( 𝑓 ‘ ( 𝐶 ∩ 𝐴 ) ) ) ) )
27 13 17 addcld ⊢ ( 𝑓 ∈ States → ( ( 𝑓 ‘ ( ⊥ ‘ 𝐴 ) ) + ( 𝑓 ‘ ( ⊥ ‘ 𝐵 ) ) ) ∈ ℂ )
28 1 2 chincli ⊢ ( 𝐴 ∩ 𝐵 ) ∈ Cℋ
29 stcl ⊢ ( 𝑓 ∈ States → ( ( 𝐴 ∩ 𝐵 ) ∈ Cℋ → ( 𝑓 ‘ ( 𝐴 ∩ 𝐵 ) ) ∈ ℝ ) )
30 28 29 mpi ⊢ ( 𝑓 ∈ States → ( 𝑓 ‘ ( 𝐴 ∩ 𝐵 ) ) ∈ ℝ )
31 30 recnd ⊢ ( 𝑓 ∈ States → ( 𝑓 ‘ ( 𝐴 ∩ 𝐵 ) ) ∈ ℂ )
32 2 3 chincli ⊢ ( 𝐵 ∩ 𝐶 ) ∈ Cℋ
33 stcl ⊢ ( 𝑓 ∈ States → ( ( 𝐵 ∩ 𝐶 ) ∈ Cℋ → ( 𝑓 ‘ ( 𝐵 ∩ 𝐶 ) ) ∈ ℝ ) )
34 32 33 mpi ⊢ ( 𝑓 ∈ States → ( 𝑓 ‘ ( 𝐵 ∩ 𝐶 ) ) ∈ ℝ )
35 34 recnd ⊢ ( 𝑓 ∈ States → ( 𝑓 ‘ ( 𝐵 ∩ 𝐶 ) ) ∈ ℂ )
36 31 35 addcld ⊢ ( 𝑓 ∈ States → ( ( 𝑓 ‘ ( 𝐴 ∩ 𝐵 ) ) + ( 𝑓 ‘ ( 𝐵 ∩ 𝐶 ) ) ) ∈ ℂ )
37 3 1 chincli ⊢ ( 𝐶 ∩ 𝐴 ) ∈ Cℋ
38 stcl ⊢ ( 𝑓 ∈ States → ( ( 𝐶 ∩ 𝐴 ) ∈ Cℋ → ( 𝑓 ‘ ( 𝐶 ∩ 𝐴 ) ) ∈ ℝ ) )
39 37 38 mpi ⊢ ( 𝑓 ∈ States → ( 𝑓 ‘ ( 𝐶 ∩ 𝐴 ) ) ∈ ℝ )
40 39 recnd ⊢ ( 𝑓 ∈ States → ( 𝑓 ‘ ( 𝐶 ∩ 𝐴 ) ) ∈ ℂ )
41 27 36 21 40 add4d ⊢ ( 𝑓 ∈ States → ( ( ( ( 𝑓 ‘ ( ⊥ ‘ 𝐴 ) ) + ( 𝑓 ‘ ( ⊥ ‘ 𝐵 ) ) ) + ( ( 𝑓 ‘ ( 𝐴 ∩ 𝐵 ) ) + ( 𝑓 ‘ ( 𝐵 ∩ 𝐶 ) ) ) ) + ( ( 𝑓 ‘ ( ⊥ ‘ 𝐶 ) ) + ( 𝑓 ‘ ( 𝐶 ∩ 𝐴 ) ) ) ) = ( ( ( ( 𝑓 ‘ ( ⊥ ‘ 𝐴 ) ) + ( 𝑓 ‘ ( ⊥ ‘ 𝐵 ) ) ) + ( 𝑓 ‘ ( ⊥ ‘ 𝐶 ) ) ) + ( ( ( 𝑓 ‘ ( 𝐴 ∩ 𝐵 ) ) + ( 𝑓 ‘ ( 𝐵 ∩ 𝐶 ) ) ) + ( 𝑓 ‘ ( 𝐶 ∩ 𝐴 ) ) ) ) )
42 23 36 13 40 add4d ⊢ ( 𝑓 ∈ States → ( ( ( ( 𝑓 ‘ ( ⊥ ‘ 𝐵 ) ) + ( 𝑓 ‘ ( ⊥ ‘ 𝐶 ) ) ) + ( ( 𝑓 ‘ ( 𝐴 ∩ 𝐵 ) ) + ( 𝑓 ‘ ( 𝐵 ∩ 𝐶 ) ) ) ) + ( ( 𝑓 ‘ ( ⊥ ‘ 𝐴 ) ) + ( 𝑓 ‘ ( 𝐶 ∩ 𝐴 ) ) ) ) = ( ( ( ( 𝑓 ‘ ( ⊥ ‘ 𝐵 ) ) + ( 𝑓 ‘ ( ⊥ ‘ 𝐶 ) ) ) + ( 𝑓 ‘ ( ⊥ ‘ 𝐴 ) ) ) + ( ( ( 𝑓 ‘ ( 𝐴 ∩ 𝐵 ) ) + ( 𝑓 ‘ ( 𝐵 ∩ 𝐶 ) ) ) + ( 𝑓 ‘ ( 𝐶 ∩ 𝐴 ) ) ) ) )
43 26 41 42 3eqtr4d ⊢ ( 𝑓 ∈ States → ( ( ( ( 𝑓 ‘ ( ⊥ ‘ 𝐴 ) ) + ( 𝑓 ‘ ( ⊥ ‘ 𝐵 ) ) ) + ( ( 𝑓 ‘ ( 𝐴 ∩ 𝐵 ) ) + ( 𝑓 ‘ ( 𝐵 ∩ 𝐶 ) ) ) ) + ( ( 𝑓 ‘ ( ⊥ ‘ 𝐶 ) ) + ( 𝑓 ‘ ( 𝐶 ∩ 𝐴 ) ) ) ) = ( ( ( ( 𝑓 ‘ ( ⊥ ‘ 𝐵 ) ) + ( 𝑓 ‘ ( ⊥ ‘ 𝐶 ) ) ) + ( ( 𝑓 ‘ ( 𝐴 ∩ 𝐵 ) ) + ( 𝑓 ‘ ( 𝐵 ∩ 𝐶 ) ) ) ) + ( ( 𝑓 ‘ ( ⊥ ‘ 𝐴 ) ) + ( 𝑓 ‘ ( 𝐶 ∩ 𝐴 ) ) ) ) )
44 13 31 17 35 add4d ⊢ ( 𝑓 ∈ States → ( ( ( 𝑓 ‘ ( ⊥ ‘ 𝐴 ) ) + ( 𝑓 ‘ ( 𝐴 ∩ 𝐵 ) ) ) + ( ( 𝑓 ‘ ( ⊥ ‘ 𝐵 ) ) + ( 𝑓 ‘ ( 𝐵 ∩ 𝐶 ) ) ) ) = ( ( ( 𝑓 ‘ ( ⊥ ‘ 𝐴 ) ) + ( 𝑓 ‘ ( ⊥ ‘ 𝐵 ) ) ) + ( ( 𝑓 ‘ ( 𝐴 ∩ 𝐵 ) ) + ( 𝑓 ‘ ( 𝐵 ∩ 𝐶 ) ) ) ) )
45 44 oveq1d ⊢ ( 𝑓 ∈ States → ( ( ( ( 𝑓 ‘ ( ⊥ ‘ 𝐴 ) ) + ( 𝑓 ‘ ( 𝐴 ∩ 𝐵 ) ) ) + ( ( 𝑓 ‘ ( ⊥ ‘ 𝐵 ) ) + ( 𝑓 ‘ ( 𝐵 ∩ 𝐶 ) ) ) ) + ( ( 𝑓 ‘ ( ⊥ ‘ 𝐶 ) ) + ( 𝑓 ‘ ( 𝐶 ∩ 𝐴 ) ) ) ) = ( ( ( ( 𝑓 ‘ ( ⊥ ‘ 𝐴 ) ) + ( 𝑓 ‘ ( ⊥ ‘ 𝐵 ) ) ) + ( ( 𝑓 ‘ ( 𝐴 ∩ 𝐵 ) ) + ( 𝑓 ‘ ( 𝐵 ∩ 𝐶 ) ) ) ) + ( ( 𝑓 ‘ ( ⊥ ‘ 𝐶 ) ) + ( 𝑓 ‘ ( 𝐶 ∩ 𝐴 ) ) ) ) )
46 17 31 21 35 add4d ⊢ ( 𝑓 ∈ States → ( ( ( 𝑓 ‘ ( ⊥ ‘ 𝐵 ) ) + ( 𝑓 ‘ ( 𝐴 ∩ 𝐵 ) ) ) + ( ( 𝑓 ‘ ( ⊥ ‘ 𝐶 ) ) + ( 𝑓 ‘ ( 𝐵 ∩ 𝐶 ) ) ) ) = ( ( ( 𝑓 ‘ ( ⊥ ‘ 𝐵 ) ) + ( 𝑓 ‘ ( ⊥ ‘ 𝐶 ) ) ) + ( ( 𝑓 ‘ ( 𝐴 ∩ 𝐵 ) ) + ( 𝑓 ‘ ( 𝐵 ∩ 𝐶 ) ) ) ) )
47 46 oveq1d ⊢ ( 𝑓 ∈ States → ( ( ( ( 𝑓 ‘ ( ⊥ ‘ 𝐵 ) ) + ( 𝑓 ‘ ( 𝐴 ∩ 𝐵 ) ) ) + ( ( 𝑓 ‘ ( ⊥ ‘ 𝐶 ) ) + ( 𝑓 ‘ ( 𝐵 ∩ 𝐶 ) ) ) ) + ( ( 𝑓 ‘ ( ⊥ ‘ 𝐴 ) ) + ( 𝑓 ‘ ( 𝐶 ∩ 𝐴 ) ) ) ) = ( ( ( ( 𝑓 ‘ ( ⊥ ‘ 𝐵 ) ) + ( 𝑓 ‘ ( ⊥ ‘ 𝐶 ) ) ) + ( ( 𝑓 ‘ ( 𝐴 ∩ 𝐵 ) ) + ( 𝑓 ‘ ( 𝐵 ∩ 𝐶 ) ) ) ) + ( ( 𝑓 ‘ ( ⊥ ‘ 𝐴 ) ) + ( 𝑓 ‘ ( 𝐶 ∩ 𝐴 ) ) ) ) )
48 43 45 47 3eqtr4d ⊢ ( 𝑓 ∈ States → ( ( ( ( 𝑓 ‘ ( ⊥ ‘ 𝐴 ) ) + ( 𝑓 ‘ ( 𝐴 ∩ 𝐵 ) ) ) + ( ( 𝑓 ‘ ( ⊥ ‘ 𝐵 ) ) + ( 𝑓 ‘ ( 𝐵 ∩ 𝐶 ) ) ) ) + ( ( 𝑓 ‘ ( ⊥ ‘ 𝐶 ) ) + ( 𝑓 ‘ ( 𝐶 ∩ 𝐴 ) ) ) ) = ( ( ( ( 𝑓 ‘ ( ⊥ ‘ 𝐵 ) ) + ( 𝑓 ‘ ( 𝐴 ∩ 𝐵 ) ) ) + ( ( 𝑓 ‘ ( ⊥ ‘ 𝐶 ) ) + ( 𝑓 ‘ ( 𝐵 ∩ 𝐶 ) ) ) ) + ( ( 𝑓 ‘ ( ⊥ ‘ 𝐴 ) ) + ( 𝑓 ‘ ( 𝐶 ∩ 𝐴 ) ) ) ) )
49 1 2 stji1i ⊢ ( 𝑓 ∈ States → ( 𝑓 ‘ ( ( ⊥ ‘ 𝐴 ) ∨ℋ ( 𝐴 ∩ 𝐵 ) ) ) = ( ( 𝑓 ‘ ( ⊥ ‘ 𝐴 ) ) + ( 𝑓 ‘ ( 𝐴 ∩ 𝐵 ) ) ) )
50 2 3 stji1i ⊢ ( 𝑓 ∈ States → ( 𝑓 ‘ ( ( ⊥ ‘ 𝐵 ) ∨ℋ ( 𝐵 ∩ 𝐶 ) ) ) = ( ( 𝑓 ‘ ( ⊥ ‘ 𝐵 ) ) + ( 𝑓 ‘ ( 𝐵 ∩ 𝐶 ) ) ) )
51 49 50 oveq12d ⊢ ( 𝑓 ∈ States → ( ( 𝑓 ‘ ( ( ⊥ ‘ 𝐴 ) ∨ℋ ( 𝐴 ∩ 𝐵 ) ) ) + ( 𝑓 ‘ ( ( ⊥ ‘ 𝐵 ) ∨ℋ ( 𝐵 ∩ 𝐶 ) ) ) ) = ( ( ( 𝑓 ‘ ( ⊥ ‘ 𝐴 ) ) + ( 𝑓 ‘ ( 𝐴 ∩ 𝐵 ) ) ) + ( ( 𝑓 ‘ ( ⊥ ‘ 𝐵 ) ) + ( 𝑓 ‘ ( 𝐵 ∩ 𝐶 ) ) ) ) )
52 3 1 stji1i ⊢ ( 𝑓 ∈ States → ( 𝑓 ‘ ( ( ⊥ ‘ 𝐶 ) ∨ℋ ( 𝐶 ∩ 𝐴 ) ) ) = ( ( 𝑓 ‘ ( ⊥ ‘ 𝐶 ) ) + ( 𝑓 ‘ ( 𝐶 ∩ 𝐴 ) ) ) )
53 51 52 oveq12d ⊢ ( 𝑓 ∈ States → ( ( ( 𝑓 ‘ ( ( ⊥ ‘ 𝐴 ) ∨ℋ ( 𝐴 ∩ 𝐵 ) ) ) + ( 𝑓 ‘ ( ( ⊥ ‘ 𝐵 ) ∨ℋ ( 𝐵 ∩ 𝐶 ) ) ) ) + ( 𝑓 ‘ ( ( ⊥ ‘ 𝐶 ) ∨ℋ ( 𝐶 ∩ 𝐴 ) ) ) ) = ( ( ( ( 𝑓 ‘ ( ⊥ ‘ 𝐴 ) ) + ( 𝑓 ‘ ( 𝐴 ∩ 𝐵 ) ) ) + ( ( 𝑓 ‘ ( ⊥ ‘ 𝐵 ) ) + ( 𝑓 ‘ ( 𝐵 ∩ 𝐶 ) ) ) ) + ( ( 𝑓 ‘ ( ⊥ ‘ 𝐶 ) ) + ( 𝑓 ‘ ( 𝐶 ∩ 𝐴 ) ) ) ) )
54 2 1 stji1i ⊢ ( 𝑓 ∈ States → ( 𝑓 ‘ ( ( ⊥ ‘ 𝐵 ) ∨ℋ ( 𝐵 ∩ 𝐴 ) ) ) = ( ( 𝑓 ‘ ( ⊥ ‘ 𝐵 ) ) + ( 𝑓 ‘ ( 𝐵 ∩ 𝐴 ) ) ) )
55 incom ⊢ ( 𝐵 ∩ 𝐴 ) = ( 𝐴 ∩ 𝐵 )
56 55 fveq2i ⊢ ( 𝑓 ‘ ( 𝐵 ∩ 𝐴 ) ) = ( 𝑓 ‘ ( 𝐴 ∩ 𝐵 ) )
57 56 oveq2i ⊢ ( ( 𝑓 ‘ ( ⊥ ‘ 𝐵 ) ) + ( 𝑓 ‘ ( 𝐵 ∩ 𝐴 ) ) ) = ( ( 𝑓 ‘ ( ⊥ ‘ 𝐵 ) ) + ( 𝑓 ‘ ( 𝐴 ∩ 𝐵 ) ) )
58 54 57 eqtrdi ⊢ ( 𝑓 ∈ States → ( 𝑓 ‘ ( ( ⊥ ‘ 𝐵 ) ∨ℋ ( 𝐵 ∩ 𝐴 ) ) ) = ( ( 𝑓 ‘ ( ⊥ ‘ 𝐵 ) ) + ( 𝑓 ‘ ( 𝐴 ∩ 𝐵 ) ) ) )
59 3 2 stji1i ⊢ ( 𝑓 ∈ States → ( 𝑓 ‘ ( ( ⊥ ‘ 𝐶 ) ∨ℋ ( 𝐶 ∩ 𝐵 ) ) ) = ( ( 𝑓 ‘ ( ⊥ ‘ 𝐶 ) ) + ( 𝑓 ‘ ( 𝐶 ∩ 𝐵 ) ) ) )
60 incom ⊢ ( 𝐶 ∩ 𝐵 ) = ( 𝐵 ∩ 𝐶 )
61 60 fveq2i ⊢ ( 𝑓 ‘ ( 𝐶 ∩ 𝐵 ) ) = ( 𝑓 ‘ ( 𝐵 ∩ 𝐶 ) )
62 61 oveq2i ⊢ ( ( 𝑓 ‘ ( ⊥ ‘ 𝐶 ) ) + ( 𝑓 ‘ ( 𝐶 ∩ 𝐵 ) ) ) = ( ( 𝑓 ‘ ( ⊥ ‘ 𝐶 ) ) + ( 𝑓 ‘ ( 𝐵 ∩ 𝐶 ) ) )
63 59 62 eqtrdi ⊢ ( 𝑓 ∈ States → ( 𝑓 ‘ ( ( ⊥ ‘ 𝐶 ) ∨ℋ ( 𝐶 ∩ 𝐵 ) ) ) = ( ( 𝑓 ‘ ( ⊥ ‘ 𝐶 ) ) + ( 𝑓 ‘ ( 𝐵 ∩ 𝐶 ) ) ) )
64 58 63 oveq12d ⊢ ( 𝑓 ∈ States → ( ( 𝑓 ‘ ( ( ⊥ ‘ 𝐵 ) ∨ℋ ( 𝐵 ∩ 𝐴 ) ) ) + ( 𝑓 ‘ ( ( ⊥ ‘ 𝐶 ) ∨ℋ ( 𝐶 ∩ 𝐵 ) ) ) ) = ( ( ( 𝑓 ‘ ( ⊥ ‘ 𝐵 ) ) + ( 𝑓 ‘ ( 𝐴 ∩ 𝐵 ) ) ) + ( ( 𝑓 ‘ ( ⊥ ‘ 𝐶 ) ) + ( 𝑓 ‘ ( 𝐵 ∩ 𝐶 ) ) ) ) )
65 1 3 stji1i ⊢ ( 𝑓 ∈ States → ( 𝑓 ‘ ( ( ⊥ ‘ 𝐴 ) ∨ℋ ( 𝐴 ∩ 𝐶 ) ) ) = ( ( 𝑓 ‘ ( ⊥ ‘ 𝐴 ) ) + ( 𝑓 ‘ ( 𝐴 ∩ 𝐶 ) ) ) )
66 incom ⊢ ( 𝐴 ∩ 𝐶 ) = ( 𝐶 ∩ 𝐴 )
67 66 fveq2i ⊢ ( 𝑓 ‘ ( 𝐴 ∩ 𝐶 ) ) = ( 𝑓 ‘ ( 𝐶 ∩ 𝐴 ) )
68 67 oveq2i ⊢ ( ( 𝑓 ‘ ( ⊥ ‘ 𝐴 ) ) + ( 𝑓 ‘ ( 𝐴 ∩ 𝐶 ) ) ) = ( ( 𝑓 ‘ ( ⊥ ‘ 𝐴 ) ) + ( 𝑓 ‘ ( 𝐶 ∩ 𝐴 ) ) )
69 65 68 eqtrdi ⊢ ( 𝑓 ∈ States → ( 𝑓 ‘ ( ( ⊥ ‘ 𝐴 ) ∨ℋ ( 𝐴 ∩ 𝐶 ) ) ) = ( ( 𝑓 ‘ ( ⊥ ‘ 𝐴 ) ) + ( 𝑓 ‘ ( 𝐶 ∩ 𝐴 ) ) ) )
70 64 69 oveq12d ⊢ ( 𝑓 ∈ States → ( ( ( 𝑓 ‘ ( ( ⊥ ‘ 𝐵 ) ∨ℋ ( 𝐵 ∩ 𝐴 ) ) ) + ( 𝑓 ‘ ( ( ⊥ ‘ 𝐶 ) ∨ℋ ( 𝐶 ∩ 𝐵 ) ) ) ) + ( 𝑓 ‘ ( ( ⊥ ‘ 𝐴 ) ∨ℋ ( 𝐴 ∩ 𝐶 ) ) ) ) = ( ( ( ( 𝑓 ‘ ( ⊥ ‘ 𝐵 ) ) + ( 𝑓 ‘ ( 𝐴 ∩ 𝐵 ) ) ) + ( ( 𝑓 ‘ ( ⊥ ‘ 𝐶 ) ) + ( 𝑓 ‘ ( 𝐵 ∩ 𝐶 ) ) ) ) + ( ( 𝑓 ‘ ( ⊥ ‘ 𝐴 ) ) + ( 𝑓 ‘ ( 𝐶 ∩ 𝐴 ) ) ) ) )
71 48 53 70 3eqtr4d ⊢ ( 𝑓 ∈ States → ( ( ( 𝑓 ‘ ( ( ⊥ ‘ 𝐴 ) ∨ℋ ( 𝐴 ∩ 𝐵 ) ) ) + ( 𝑓 ‘ ( ( ⊥ ‘ 𝐵 ) ∨ℋ ( 𝐵 ∩ 𝐶 ) ) ) ) + ( 𝑓 ‘ ( ( ⊥ ‘ 𝐶 ) ∨ℋ ( 𝐶 ∩ 𝐴 ) ) ) ) = ( ( ( 𝑓 ‘ ( ( ⊥ ‘ 𝐵 ) ∨ℋ ( 𝐵 ∩ 𝐴 ) ) ) + ( 𝑓 ‘ ( ( ⊥ ‘ 𝐶 ) ∨ℋ ( 𝐶 ∩ 𝐵 ) ) ) ) + ( 𝑓 ‘ ( ( ⊥ ‘ 𝐴 ) ∨ℋ ( 𝐴 ∩ 𝐶 ) ) ) ) )
72 4 fveq2i ⊢ ( 𝑓 ‘ 𝐹 ) = ( 𝑓 ‘ ( ( ⊥ ‘ 𝐴 ) ∨ℋ ( 𝐴 ∩ 𝐵 ) ) )
73 5 fveq2i ⊢ ( 𝑓 ‘ 𝐺 ) = ( 𝑓 ‘ ( ( ⊥ ‘ 𝐵 ) ∨ℋ ( 𝐵 ∩ 𝐶 ) ) )
74 72 73 oveq12i ⊢ ( ( 𝑓 ‘ 𝐹 ) + ( 𝑓 ‘ 𝐺 ) ) = ( ( 𝑓 ‘ ( ( ⊥ ‘ 𝐴 ) ∨ℋ ( 𝐴 ∩ 𝐵 ) ) ) + ( 𝑓 ‘ ( ( ⊥ ‘ 𝐵 ) ∨ℋ ( 𝐵 ∩ 𝐶 ) ) ) )
75 6 fveq2i ⊢ ( 𝑓 ‘ 𝐻 ) = ( 𝑓 ‘ ( ( ⊥ ‘ 𝐶 ) ∨ℋ ( 𝐶 ∩ 𝐴 ) ) )
76 74 75 oveq12i ⊢ ( ( ( 𝑓 ‘ 𝐹 ) + ( 𝑓 ‘ 𝐺 ) ) + ( 𝑓 ‘ 𝐻 ) ) = ( ( ( 𝑓 ‘ ( ( ⊥ ‘ 𝐴 ) ∨ℋ ( 𝐴 ∩ 𝐵 ) ) ) + ( 𝑓 ‘ ( ( ⊥ ‘ 𝐵 ) ∨ℋ ( 𝐵 ∩ 𝐶 ) ) ) ) + ( 𝑓 ‘ ( ( ⊥ ‘ 𝐶 ) ∨ℋ ( 𝐶 ∩ 𝐴 ) ) ) )
77 7 fveq2i ⊢ ( 𝑓 ‘ 𝐷 ) = ( 𝑓 ‘ ( ( ⊥ ‘ 𝐵 ) ∨ℋ ( 𝐵 ∩ 𝐴 ) ) )
78 8 fveq2i ⊢ ( 𝑓 ‘ 𝑅 ) = ( 𝑓 ‘ ( ( ⊥ ‘ 𝐶 ) ∨ℋ ( 𝐶 ∩ 𝐵 ) ) )
79 77 78 oveq12i ⊢ ( ( 𝑓 ‘ 𝐷 ) + ( 𝑓 ‘ 𝑅 ) ) = ( ( 𝑓 ‘ ( ( ⊥ ‘ 𝐵 ) ∨ℋ ( 𝐵 ∩ 𝐴 ) ) ) + ( 𝑓 ‘ ( ( ⊥ ‘ 𝐶 ) ∨ℋ ( 𝐶 ∩ 𝐵 ) ) ) )
80 9 fveq2i ⊢ ( 𝑓 ‘ 𝑆 ) = ( 𝑓 ‘ ( ( ⊥ ‘ 𝐴 ) ∨ℋ ( 𝐴 ∩ 𝐶 ) ) )
81 79 80 oveq12i ⊢ ( ( ( 𝑓 ‘ 𝐷 ) + ( 𝑓 ‘ 𝑅 ) ) + ( 𝑓 ‘ 𝑆 ) ) = ( ( ( 𝑓 ‘ ( ( ⊥ ‘ 𝐵 ) ∨ℋ ( 𝐵 ∩ 𝐴 ) ) ) + ( 𝑓 ‘ ( ( ⊥ ‘ 𝐶 ) ∨ℋ ( 𝐶 ∩ 𝐵 ) ) ) ) + ( 𝑓 ‘ ( ( ⊥ ‘ 𝐴 ) ∨ℋ ( 𝐴 ∩ 𝐶 ) ) ) )
82 71 76 81 3eqtr4g ⊢ ( 𝑓 ∈ States → ( ( ( 𝑓 ‘ 𝐹 ) + ( 𝑓 ‘ 𝐺 ) ) + ( 𝑓 ‘ 𝐻 ) ) = ( ( ( 𝑓 ‘ 𝐷 ) + ( 𝑓 ‘ 𝑅 ) ) + ( 𝑓 ‘ 𝑆 ) ) )