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