Theorem stji1i

Description: Join of components of Sasaki arrow ->1. (Contributed by NM, 24-Oct-1999) (New usage is discouraged.)

	Ref	Expression
Hypotheses	stle.1	⊢ 𝐴 ∈ Cℋ
	stle.2	⊢ 𝐵 ∈ Cℋ
Assertion	stji1i	⊢ ( 𝑆 ∈ States → ( 𝑆 ‘ ( ( ⊥ ‘ 𝐴 ) ∨ℋ ( 𝐴 ∩ 𝐵 ) ) ) = ( ( 𝑆 ‘ ( ⊥ ‘ 𝐴 ) ) + ( 𝑆 ‘ ( 𝐴 ∩ 𝐵 ) ) ) )

Proof

Step	Hyp	Ref	Expression
1		stle.1	⊢ 𝐴 ∈ Cℋ
2		stle.2	⊢ 𝐵 ∈ Cℋ
3	1	choccli	⊢ ( ⊥ ‘ 𝐴 ) ∈ Cℋ
4	1 2	chincli	⊢ ( 𝐴 ∩ 𝐵 ) ∈ Cℋ
5	3 4	pm3.2i	⊢ ( ( ⊥ ‘ 𝐴 ) ∈ Cℋ ∧ ( 𝐴 ∩ 𝐵 ) ∈ Cℋ )
6		inss1	⊢ ( 𝐴 ∩ 𝐵 ) ⊆ 𝐴
7	4 1	chsscon3i	⊢ ( ( 𝐴 ∩ 𝐵 ) ⊆ 𝐴 ↔ ( ⊥ ‘ 𝐴 ) ⊆ ( ⊥ ‘ ( 𝐴 ∩ 𝐵 ) ) )
8	6 7	mpbi	⊢ ( ⊥ ‘ 𝐴 ) ⊆ ( ⊥ ‘ ( 𝐴 ∩ 𝐵 ) )
9		stj	⊢ ( 𝑆 ∈ States → ( ( ( ( ⊥ ‘ 𝐴 ) ∈ Cℋ ∧ ( 𝐴 ∩ 𝐵 ) ∈ Cℋ ) ∧ ( ⊥ ‘ 𝐴 ) ⊆ ( ⊥ ‘ ( 𝐴 ∩ 𝐵 ) ) ) → ( 𝑆 ‘ ( ( ⊥ ‘ 𝐴 ) ∨ℋ ( 𝐴 ∩ 𝐵 ) ) ) = ( ( 𝑆 ‘ ( ⊥ ‘ 𝐴 ) ) + ( 𝑆 ‘ ( 𝐴 ∩ 𝐵 ) ) ) ) )
10	5 8 9	mp2ani	⊢ ( 𝑆 ∈ States → ( 𝑆 ‘ ( ( ⊥ ‘ 𝐴 ) ∨ℋ ( 𝐴 ∩ 𝐵 ) ) ) = ( ( 𝑆 ‘ ( ⊥ ‘ 𝐴 ) ) + ( 𝑆 ‘ ( 𝐴 ∩ 𝐵 ) ) ) )