Theorem mat1dimbas

Description: A matrix with dimension 1 is an ordered pair with an ordered pair (of the one and only pair of indices) as first component. (Contributed by AV, 15-Aug-2019)

	Ref	Expression
Hypotheses	mat1dim.a	⊢ 𝐴 = ( { 𝐸 } Mat 𝑅 )
	mat1dim.b	⊢ 𝐵 = ( Base ‘ 𝑅 )
	mat1dim.o	⊢ 𝑂 = ⟨ 𝐸 , 𝐸 ⟩
Assertion	mat1dimbas	⊢ ( ( 𝑅 ∈ Ring ∧ 𝐸 ∈ 𝑉 ∧ 𝑋 ∈ 𝐵 ) → { ⟨ 𝑂 , 𝑋 ⟩ } ∈ ( Base ‘ 𝐴 ) )

Proof

Step	Hyp	Ref	Expression
1		mat1dim.a	⊢ 𝐴 = ( { 𝐸 } Mat 𝑅 )
2		mat1dim.b	⊢ 𝐵 = ( Base ‘ 𝑅 )
3		mat1dim.o	⊢ 𝑂 = ⟨ 𝐸 , 𝐸 ⟩
4		risset	⊢ ( 𝑋 ∈ 𝐵 ↔ ∃ 𝑟 ∈ 𝐵 𝑟 = 𝑋 )
5		eqcom	⊢ ( 𝑋 = 𝑟 ↔ 𝑟 = 𝑋 )
6	5	rexbii	⊢ ( ∃ 𝑟 ∈ 𝐵 𝑋 = 𝑟 ↔ ∃ 𝑟 ∈ 𝐵 𝑟 = 𝑋 )
7	4 6	sylbb2	⊢ ( 𝑋 ∈ 𝐵 → ∃ 𝑟 ∈ 𝐵 𝑋 = 𝑟 )
8	7	3ad2ant3	⊢ ( ( 𝑅 ∈ Ring ∧ 𝐸 ∈ 𝑉 ∧ 𝑋 ∈ 𝐵 ) → ∃ 𝑟 ∈ 𝐵 𝑋 = 𝑟 )
9		opex	⊢ ⟨ 𝐸 , 𝐸 ⟩ ∈ V
10	3 9	eqeltri	⊢ 𝑂 ∈ V
11		simp3	⊢ ( ( 𝑅 ∈ Ring ∧ 𝐸 ∈ 𝑉 ∧ 𝑋 ∈ 𝐵 ) → 𝑋 ∈ 𝐵 )
12		opthg	⊢ ( ( 𝑂 ∈ V ∧ 𝑋 ∈ 𝐵 ) → ( ⟨ 𝑂 , 𝑋 ⟩ = ⟨ 𝑂 , 𝑟 ⟩ ↔ ( 𝑂 = 𝑂 ∧ 𝑋 = 𝑟 ) ) )
13	10 11 12	sylancr	⊢ ( ( 𝑅 ∈ Ring ∧ 𝐸 ∈ 𝑉 ∧ 𝑋 ∈ 𝐵 ) → ( ⟨ 𝑂 , 𝑋 ⟩ = ⟨ 𝑂 , 𝑟 ⟩ ↔ ( 𝑂 = 𝑂 ∧ 𝑋 = 𝑟 ) ) )
14		opex	⊢ ⟨ 𝑂 , 𝑋 ⟩ ∈ V
15		sneqbg	⊢ ( ⟨ 𝑂 , 𝑋 ⟩ ∈ V → ( { ⟨ 𝑂 , 𝑋 ⟩ } = { ⟨ 𝑂 , 𝑟 ⟩ } ↔ ⟨ 𝑂 , 𝑋 ⟩ = ⟨ 𝑂 , 𝑟 ⟩ ) )
16	14 15	ax-mp	⊢ ( { ⟨ 𝑂 , 𝑋 ⟩ } = { ⟨ 𝑂 , 𝑟 ⟩ } ↔ ⟨ 𝑂 , 𝑋 ⟩ = ⟨ 𝑂 , 𝑟 ⟩ )
17		eqid	⊢ 𝑂 = 𝑂
18	17	biantrur	⊢ ( 𝑋 = 𝑟 ↔ ( 𝑂 = 𝑂 ∧ 𝑋 = 𝑟 ) )
19	13 16 18	3bitr4g	⊢ ( ( 𝑅 ∈ Ring ∧ 𝐸 ∈ 𝑉 ∧ 𝑋 ∈ 𝐵 ) → ( { ⟨ 𝑂 , 𝑋 ⟩ } = { ⟨ 𝑂 , 𝑟 ⟩ } ↔ 𝑋 = 𝑟 ) )
20	19	rexbidv	⊢ ( ( 𝑅 ∈ Ring ∧ 𝐸 ∈ 𝑉 ∧ 𝑋 ∈ 𝐵 ) → ( ∃ 𝑟 ∈ 𝐵 { ⟨ 𝑂 , 𝑋 ⟩ } = { ⟨ 𝑂 , 𝑟 ⟩ } ↔ ∃ 𝑟 ∈ 𝐵 𝑋 = 𝑟 ) )
21	8 20	mpbird	⊢ ( ( 𝑅 ∈ Ring ∧ 𝐸 ∈ 𝑉 ∧ 𝑋 ∈ 𝐵 ) → ∃ 𝑟 ∈ 𝐵 { ⟨ 𝑂 , 𝑋 ⟩ } = { ⟨ 𝑂 , 𝑟 ⟩ } )
22	1 2 3	mat1dimelbas	⊢ ( ( 𝑅 ∈ Ring ∧ 𝐸 ∈ 𝑉 ) → ( { ⟨ 𝑂 , 𝑋 ⟩ } ∈ ( Base ‘ 𝐴 ) ↔ ∃ 𝑟 ∈ 𝐵 { ⟨ 𝑂 , 𝑋 ⟩ } = { ⟨ 𝑂 , 𝑟 ⟩ } ) )
23	22	3adant3	⊢ ( ( 𝑅 ∈ Ring ∧ 𝐸 ∈ 𝑉 ∧ 𝑋 ∈ 𝐵 ) → ( { ⟨ 𝑂 , 𝑋 ⟩ } ∈ ( Base ‘ 𝐴 ) ↔ ∃ 𝑟 ∈ 𝐵 { ⟨ 𝑂 , 𝑋 ⟩ } = { ⟨ 𝑂 , 𝑟 ⟩ } ) )
24	21 23	mpbird	⊢ ( ( 𝑅 ∈ Ring ∧ 𝐸 ∈ 𝑉 ∧ 𝑋 ∈ 𝐵 ) → { ⟨ 𝑂 , 𝑋 ⟩ } ∈ ( Base ‘ 𝐴 ) )