Metamath Proof Explorer

Theorem golem2

Description: Lemma for Godowski's equation. (Contributed by NM, 13-Nov-1999) (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 golem2 ( 𝑓 ∈ States → ( ( 𝑓 ‘ ( ( 𝐹 ∩ 𝐺 ) ∩ 𝐻 ) ) = 1 → ( 𝑓 ‘ 𝐷 ) = 1 ) )

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 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 ) )