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 |
1 2
|
chincli |
⊢ ( 𝐴 ∩ 𝐵 ) ∈ Cℋ |
12 |
10 11
|
chjcli |
⊢ ( ( ⊥ ‘ 𝐴 ) ∨ℋ ( 𝐴 ∩ 𝐵 ) ) ∈ Cℋ |
13 |
4 12
|
eqeltri |
⊢ 𝐹 ∈ Cℋ |
14 |
2
|
choccli |
⊢ ( ⊥ ‘ 𝐵 ) ∈ Cℋ |
15 |
2 3
|
chincli |
⊢ ( 𝐵 ∩ 𝐶 ) ∈ Cℋ |
16 |
14 15
|
chjcli |
⊢ ( ( ⊥ ‘ 𝐵 ) ∨ℋ ( 𝐵 ∩ 𝐶 ) ) ∈ Cℋ |
17 |
5 16
|
eqeltri |
⊢ 𝐺 ∈ Cℋ |
18 |
3
|
choccli |
⊢ ( ⊥ ‘ 𝐶 ) ∈ Cℋ |
19 |
3 1
|
chincli |
⊢ ( 𝐶 ∩ 𝐴 ) ∈ Cℋ |
20 |
18 19
|
chjcli |
⊢ ( ( ⊥ ‘ 𝐶 ) ∨ℋ ( 𝐶 ∩ 𝐴 ) ) ∈ Cℋ |
21 |
6 20
|
eqeltri |
⊢ 𝐻 ∈ Cℋ |
22 |
13 17 21
|
stm1add3i |
⊢ ( 𝑓 ∈ States → ( ( 𝑓 ‘ ( ( 𝐹 ∩ 𝐺 ) ∩ 𝐻 ) ) = 1 → ( ( ( 𝑓 ‘ 𝐹 ) + ( 𝑓 ‘ 𝐺 ) ) + ( 𝑓 ‘ 𝐻 ) ) = 3 ) ) |
23 |
1 2 3 4 5 6 7 8 9
|
golem1 |
⊢ ( 𝑓 ∈ States → ( ( ( 𝑓 ‘ 𝐹 ) + ( 𝑓 ‘ 𝐺 ) ) + ( 𝑓 ‘ 𝐻 ) ) = ( ( ( 𝑓 ‘ 𝐷 ) + ( 𝑓 ‘ 𝑅 ) ) + ( 𝑓 ‘ 𝑆 ) ) ) |
24 |
23
|
eqeq1d |
⊢ ( 𝑓 ∈ States → ( ( ( ( 𝑓 ‘ 𝐹 ) + ( 𝑓 ‘ 𝐺 ) ) + ( 𝑓 ‘ 𝐻 ) ) = 3 ↔ ( ( ( 𝑓 ‘ 𝐷 ) + ( 𝑓 ‘ 𝑅 ) ) + ( 𝑓 ‘ 𝑆 ) ) = 3 ) ) |
25 |
22 24
|
sylibd |
⊢ ( 𝑓 ∈ States → ( ( 𝑓 ‘ ( ( 𝐹 ∩ 𝐺 ) ∩ 𝐻 ) ) = 1 → ( ( ( 𝑓 ‘ 𝐷 ) + ( 𝑓 ‘ 𝑅 ) ) + ( 𝑓 ‘ 𝑆 ) ) = 3 ) ) |
26 |
2 1
|
chincli |
⊢ ( 𝐵 ∩ 𝐴 ) ∈ Cℋ |
27 |
14 26
|
chjcli |
⊢ ( ( ⊥ ‘ 𝐵 ) ∨ℋ ( 𝐵 ∩ 𝐴 ) ) ∈ Cℋ |
28 |
7 27
|
eqeltri |
⊢ 𝐷 ∈ Cℋ |
29 |
3 2
|
chincli |
⊢ ( 𝐶 ∩ 𝐵 ) ∈ Cℋ |
30 |
18 29
|
chjcli |
⊢ ( ( ⊥ ‘ 𝐶 ) ∨ℋ ( 𝐶 ∩ 𝐵 ) ) ∈ Cℋ |
31 |
8 30
|
eqeltri |
⊢ 𝑅 ∈ Cℋ |
32 |
1 3
|
chincli |
⊢ ( 𝐴 ∩ 𝐶 ) ∈ Cℋ |
33 |
10 32
|
chjcli |
⊢ ( ( ⊥ ‘ 𝐴 ) ∨ℋ ( 𝐴 ∩ 𝐶 ) ) ∈ Cℋ |
34 |
9 33
|
eqeltri |
⊢ 𝑆 ∈ Cℋ |
35 |
28 31 34
|
stadd3i |
⊢ ( 𝑓 ∈ States → ( ( ( ( 𝑓 ‘ 𝐷 ) + ( 𝑓 ‘ 𝑅 ) ) + ( 𝑓 ‘ 𝑆 ) ) = 3 → ( 𝑓 ‘ 𝐷 ) = 1 ) ) |
36 |
25 35
|
syld |
⊢ ( 𝑓 ∈ States → ( ( 𝑓 ‘ ( ( 𝐹 ∩ 𝐺 ) ∩ 𝐻 ) ) = 1 → ( 𝑓 ‘ 𝐷 ) = 1 ) ) |