Theorem basendxnmulrndx

Description: The slot for the base set is not the slot for the ring (multiplication) operation in an extensible structure. (Contributed by AV, 16-Feb-2020)

	Ref	Expression
Assertion	basendxnmulrndx	⊢ ( Base ‘ ndx ) ≠ ( .r ‘ ndx )

Proof

Step	Hyp	Ref	Expression
1		df-base	⊢ Base = Slot 1
2		1nn	⊢ 1 ∈ ℕ
3	1 2	ndxarg	⊢ ( Base ‘ ndx ) = 1
4		1re	⊢ 1 ∈ ℝ
5		1lt3	⊢ 1 < 3
6	4 5	ltneii	⊢ 1 ≠ 3
7		mulrndx	⊢ ( .r ‘ ndx ) = 3
8	6 7	neeqtrri	⊢ 1 ≠ ( .r ‘ ndx )
9	3 8	eqnetri	⊢ ( Base ‘ ndx ) ≠ ( .r ‘ ndx )