elcgrabasrd

Description: Helper theorem for the membership in the base set of the angle addition monoid. (Contributed by Thierry Arnoux, 23-Aug-2026)

	Ref	Expression
Hypotheses	elcgrabasrd.a	⊢ 𝐴 = { 𝑑 ∈ ( 𝑃 ↑_m ( 0 ..^ 3 ) ) ∣ ( ( 𝑑 ‘ 0 ) ≠ ( 𝑑 ‘ 1 ) ∧ ( 𝑑 ‘ 1 ) ≠ ( 𝑑 ‘ 2 ) ) }
	elcgrabasrd.p	⊢ ( 𝜑 → 𝑃 ∈ 𝑉 )
	elcgrabasrd.x	⊢ ( 𝜑 → 𝑋 ∈ 𝑃 )
	elcgrabasrd.y	⊢ ( 𝜑 → 𝑌 ∈ 𝑃 )
	elcgrabasrd.z	⊢ ( 𝜑 → 𝑍 ∈ 𝑃 )
	elcgrabasrd.1	⊢ ( 𝜑 → 𝑋 ≠ 𝑌 )
	elcgrabasrd.2	⊢ ( 𝜑 → 𝑌 ≠ 𝑍 )
Assertion	elcgrabasrd	⊢ ( 𝜑 → ⟨“ 𝑋 𝑌 𝑍 ”⟩ ∈ 𝐴 )

Proof

Step	Hyp	Ref	Expression
1		elcgrabasrd.a	⊢ 𝐴 = { 𝑑 ∈ ( 𝑃 ↑_m ( 0 ..^ 3 ) ) ∣ ( ( 𝑑 ‘ 0 ) ≠ ( 𝑑 ‘ 1 ) ∧ ( 𝑑 ‘ 1 ) ≠ ( 𝑑 ‘ 2 ) ) }
2		elcgrabasrd.p	⊢ ( 𝜑 → 𝑃 ∈ 𝑉 )
3		elcgrabasrd.x	⊢ ( 𝜑 → 𝑋 ∈ 𝑃 )
4		elcgrabasrd.y	⊢ ( 𝜑 → 𝑌 ∈ 𝑃 )
5		elcgrabasrd.z	⊢ ( 𝜑 → 𝑍 ∈ 𝑃 )
6		elcgrabasrd.1	⊢ ( 𝜑 → 𝑋 ≠ 𝑌 )
7		elcgrabasrd.2	⊢ ( 𝜑 → 𝑌 ≠ 𝑍 )
8		fveq1	⊢ ( 𝑑 = ⟨“ 𝑋 𝑌 𝑍 ”⟩ → ( 𝑑 ‘ 0 ) = ( ⟨“ 𝑋 𝑌 𝑍 ”⟩ ‘ 0 ) )
9		fveq1	⊢ ( 𝑑 = ⟨“ 𝑋 𝑌 𝑍 ”⟩ → ( 𝑑 ‘ 1 ) = ( ⟨“ 𝑋 𝑌 𝑍 ”⟩ ‘ 1 ) )
10	8 9	neeq12d	⊢ ( 𝑑 = ⟨“ 𝑋 𝑌 𝑍 ”⟩ → ( ( 𝑑 ‘ 0 ) ≠ ( 𝑑 ‘ 1 ) ↔ ( ⟨“ 𝑋 𝑌 𝑍 ”⟩ ‘ 0 ) ≠ ( ⟨“ 𝑋 𝑌 𝑍 ”⟩ ‘ 1 ) ) )
11		fveq1	⊢ ( 𝑑 = ⟨“ 𝑋 𝑌 𝑍 ”⟩ → ( 𝑑 ‘ 2 ) = ( ⟨“ 𝑋 𝑌 𝑍 ”⟩ ‘ 2 ) )
12	9 11	neeq12d	⊢ ( 𝑑 = ⟨“ 𝑋 𝑌 𝑍 ”⟩ → ( ( 𝑑 ‘ 1 ) ≠ ( 𝑑 ‘ 2 ) ↔ ( ⟨“ 𝑋 𝑌 𝑍 ”⟩ ‘ 1 ) ≠ ( ⟨“ 𝑋 𝑌 𝑍 ”⟩ ‘ 2 ) ) )
13	10 12	anbi12d	⊢ ( 𝑑 = ⟨“ 𝑋 𝑌 𝑍 ”⟩ → ( ( ( 𝑑 ‘ 0 ) ≠ ( 𝑑 ‘ 1 ) ∧ ( 𝑑 ‘ 1 ) ≠ ( 𝑑 ‘ 2 ) ) ↔ ( ( ⟨“ 𝑋 𝑌 𝑍 ”⟩ ‘ 0 ) ≠ ( ⟨“ 𝑋 𝑌 𝑍 ”⟩ ‘ 1 ) ∧ ( ⟨“ 𝑋 𝑌 𝑍 ”⟩ ‘ 1 ) ≠ ( ⟨“ 𝑋 𝑌 𝑍 ”⟩ ‘ 2 ) ) ) )
14	2 3 4 5	s3rexrd	⊢ ( 𝜑 → ⟨“ 𝑋 𝑌 𝑍 ”⟩ ∈ ( 𝑃 ↑_m ( 0 ..^ 3 ) ) )
15		s3fv0	⊢ ( 𝑋 ∈ 𝑃 → ( ⟨“ 𝑋 𝑌 𝑍 ”⟩ ‘ 0 ) = 𝑋 )
16	3 15	syl	⊢ ( 𝜑 → ( ⟨“ 𝑋 𝑌 𝑍 ”⟩ ‘ 0 ) = 𝑋 )
17		s3fv1	⊢ ( 𝑌 ∈ 𝑃 → ( ⟨“ 𝑋 𝑌 𝑍 ”⟩ ‘ 1 ) = 𝑌 )
18	4 17	syl	⊢ ( 𝜑 → ( ⟨“ 𝑋 𝑌 𝑍 ”⟩ ‘ 1 ) = 𝑌 )
19	6 16 18	3netr4d	⊢ ( 𝜑 → ( ⟨“ 𝑋 𝑌 𝑍 ”⟩ ‘ 0 ) ≠ ( ⟨“ 𝑋 𝑌 𝑍 ”⟩ ‘ 1 ) )
20		s3fv2	⊢ ( 𝑍 ∈ 𝑃 → ( ⟨“ 𝑋 𝑌 𝑍 ”⟩ ‘ 2 ) = 𝑍 )
21	5 20	syl	⊢ ( 𝜑 → ( ⟨“ 𝑋 𝑌 𝑍 ”⟩ ‘ 2 ) = 𝑍 )
22	7 18 21	3netr4d	⊢ ( 𝜑 → ( ⟨“ 𝑋 𝑌 𝑍 ”⟩ ‘ 1 ) ≠ ( ⟨“ 𝑋 𝑌 𝑍 ”⟩ ‘ 2 ) )
23	19 22	jca	⊢ ( 𝜑 → ( ( ⟨“ 𝑋 𝑌 𝑍 ”⟩ ‘ 0 ) ≠ ( ⟨“ 𝑋 𝑌 𝑍 ”⟩ ‘ 1 ) ∧ ( ⟨“ 𝑋 𝑌 𝑍 ”⟩ ‘ 1 ) ≠ ( ⟨“ 𝑋 𝑌 𝑍 ”⟩ ‘ 2 ) ) )
24	13 14 23	elrabd	⊢ ( 𝜑 → ⟨“ 𝑋 𝑌 𝑍 ”⟩ ∈ { 𝑑 ∈ ( 𝑃 ↑_m ( 0 ..^ 3 ) ) ∣ ( ( 𝑑 ‘ 0 ) ≠ ( 𝑑 ‘ 1 ) ∧ ( 𝑑 ‘ 1 ) ≠ ( 𝑑 ‘ 2 ) ) } )
25	24 1	eleqtrrdi	⊢ ( 𝜑 → ⟨“ 𝑋 𝑌 𝑍 ”⟩ ∈ 𝐴 )

Metamath Proof Explorer

Theorem elcgrabasrd

Proof