Si A y B son matrices cuadradas, ¿cómo se demuestra que det | A . B | = det | A | . det | B |? Algunos libros lo 'demuestran' con ejemplos...

Una de las primeras cosas que hice fue consultar ProofWiki y vi que ahí hay varias demostraciones diferentes.

https://proofwiki.org/wiki/Determinant_of_Matrix_Product

No recuerdo si alguna vez me contaron alguna demostración de esa propiedad, pero la número 4 me resultó ligeramente familiar. La más difícil me pareció la 3… que se basa en una fórmula más general, que es válida para matrices m n y n m respectivamente, es decir, una fórmula donde A y B no tienen por qué ser cuadradas.
Las demostraciones 1 y 2 me parecen bastante "asequibles", es decir, ni son demostraciones muy largas, ni se apoyan en unas bases que sean descomunalmente complicadas ni alejadas del conocimiento o nociones habituales sobre matrices.

Lo anterior serían demostraciones que me parecen rigurosas, que es lo que pedía la pregunta.

Luego, podría dar alguna "visión" intuitiva.
La idea de determinante equivale a un "volumen con signo" en matrices 3x3, como expliqué en otra respuesta [1]. Me mantendré, de momento, en 3D, en matrices 3x3.
Y recordemos que una matriz equivale a transformación lineal, es decir, si tenemos un vector columna c, entonces B·c sería la imagen de c después de una transformación lineal B. Si la columna c es [1 0 0]^T el vector B·c será la primera columna de B, si c=[0 1 0]^T devolverá la 2ª columna y si es [0 0 1]^T la tercera columna.
Entonces, esa idea de "volumen con signo" también es una idea de "cómo de amplia" es la deformación del espacio que produce la transformación lineal. Entendiendo por "amplitud" o "tamaño" el "volumen" sobre unos vectores de referencia. Si los vectores columna de B (b1, b2, b3) son grandes (módulo grande) pero están muy juntos, casi en el mismo plano, el volumen puede ser pequeño.
Del mismo modo A producirá otra transformación cuyo determinante será también el "grado de amplitud".
Y la matriz A·B es la que caracteriza la composición de ambas, primero transformar con B y luego con A. Si B deforma primero en un grado |B| y luego A lo hace en un grado |A| el grado de deformación después de hacer las dos será la multiplicación: |A| · |B|
Toda esta noción que se visualiza mejor en 3D se ampliaría para cualquier dimensión n, cuando las matrices sean nxn.

Ejemplo:
La transformación A=2·I tiene un 2 en cada elemento de la diagonal, y su determinante es 2·2·…·2 = 2^n. Otra transformación B solo amplía por 3 el primer vector canónico pero deja igual al resto. La matriz B sería una matriz diagonal cuyo primer autovalor es 3 y el resto son 1. Esto significa que el determinante es 3, solo amplía el "hipervolumen" en un factor 3. La matriz A·B sería también diagonal, con un 6 como primer autovalor y un 2 en el resto. El determinante |AB| es 3·2^n que es la multiplicación de los factores de "engordamiento del espacio" que producen cada una de las transformaciones.

Bueno, esto de ejemplos es justo lo que trata de evitar la pregunta pero puede servir como complemento a las ideas intuitivas.

Según Terence Tao, uno de los matemáticos más famosos e importantes de la actualidad, es conveniente unir el rigor de las demostraciones con las ideas intuitivas.
Sin ideas intuitivas, todo se vuelve más abstracto, más pesado y es difícil de evaluar si un teorema puede tener mayor o menor utilidad para la física o situaciones del mundo real. Y sin rigor solamente se pueden hacer conjeturas, hipótesis, sin llegar a nada completamente seguro.

Volviendo a las demostraciones rigurosas, ahora pondré otro extremo, una demostración muy rigurosa y documentada aunque incomprensible para un humano normal, por ser demasiado larga y usar un lenguaje apartado del lenguaje coloquial.

Por curiosidad, busqué en Metamath
determinant product site:us.metamath.org - Google Search
Y encontré esta demostración
mdetmul - Metamath Proof Explorer
que resulta tener nada menos que 269 pasos!!

Esto último es una mera anécdota…
Metamath, aparte de una web, es también el nombre de un lenguaje para expresar teoremas en matemáticas abstractas (más o menos al estilo que describió Gödel: toda proposición sería una secuencia de símbolos, de un conjunto finito de símbolos).
Una demostración sería una secuencia de pasos lógicos, normalmente implicaciones, que conectan unas premisas y axiomas o definiciones con una proposición final. Lo que hace Metamath es recopilar demostraciones expresadas en su lenguaje propio y las verifica automáticamente con un programa informático… Una vez comprobadas (validadas) genera una página web con esa demostración, en la cual se puede ver cada uno de los pasos individuales, en qué se basa cada paso, las hipótesis o premisas originales y la conclusión… así como la persona que contribuyó ese teorema, en qué fecha y una descripción. En este caso, fue añadido por Stefan O'Rear en 2018.

Notas al pie